Theorem: Lean4Lean.VEnv.HasTypeU1.induction (Lean4Lean/Theory/Typing/StratifiedUntyped.lean)

State before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
H : HasTypeU1 env U defEq Γ e A
⊢ HasType env U Γ e A
Tactic:
induction H with
| bvar h => exact .bvar h
| const h1 h2 h3 => exact .const h1 h2 h3
| sort h => exact .sort h
| app _ _ ih1 ih2 => exact .app (ih1 hΓ) (ih2 hΓ)
| lam _ _ ih1 ih2 => exact .lam (ih1 hΓ) (ih2 ⟨hΓ, _, ih1 hΓ⟩)
| forallE _ _ ih1 ih2 => exact .forallE (ih1 hΓ) (ih2 ⟨hΓ, _, ih1 hΓ⟩)
| defeq h1 _ ih =>
  let ⟨_, h⟩ := (ih hΓ).isType henv hΓ
  exact (IH h h1).defeq (ih hΓ)
State after:
no goals

State before:
case bvar
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.bvar i✝) A✝
Tactic:
exact .bvar h
State after:
no goals

State before:
case const
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = ci✝.uvars
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.const c✝ ls✝) (instL ls✝ ci✝.type)
Tactic:
exact .const h1 h2 h3
State after:
no goals

State before:
case sort
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
l✝ : VLevel
h : VLevel.WF U l✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.sort l✝) (VExpr.sort (VLevel.succ l✝))
Tactic:
exact .sort h
State after:
no goals

State before:
case app
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
f✝ A✝ B✝ a✝² : VExpr
a✝¹ : HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
a✝ : HasTypeU1 env U defEq Γ✝ a✝² A✝
ih1 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ f✝ (VExpr.forallE A✝ B✝)
ih2 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ a✝² A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.app f✝ a✝²) (inst B✝ a✝²)
Tactic:
exact .app (ih1 hΓ) (ih2 hΓ)
State after:
no goals

State before:
case lam
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
body✝ B✝ : VExpr
a✝¹ : HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝)
a✝ : HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ B✝
ih1 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ A✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → HasType env U (A✝ :: Γ✝) body✝ B✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.lam A✝ body✝) (VExpr.forallE A✝ B✝)
Tactic:
exact .lam (ih1 hΓ) (ih2 ⟨hΓ, _, ih1 hΓ⟩)
State after:
no goals

State before:
case forallE
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
body✝ : VExpr
v✝ : VLevel
a✝¹ : HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝)
a✝ : HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ (VExpr.sort v✝)
ih1 : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ A✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → HasType env U (A✝ :: Γ✝) body✝ (VExpr.sort v✝)
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact .forallE (ih1 hΓ) (ih2 ⟨hΓ, _, ih1 hΓ⟩)
State after:
no goals

State before:
case defeq
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ B✝ e✝ : VExpr
h1 : defEq Γ✝ A✝ B✝
a✝ : HasTypeU1 env U defEq Γ✝ e✝ A✝
ih : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ e✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ HasType env U Γ✝ e✝ B✝
Tactic:
let ⟨_, h⟩ := (ih hΓ).isType henv hΓ
State after:
case defeq
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ B✝ e✝ : VExpr
h1 : defEq Γ✝ A✝ B✝
a✝ : HasTypeU1 env U defEq Γ✝ e✝ A✝
ih : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ e✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U Γ✝ A✝ (VExpr.sort w✝)
⊢ HasType env U Γ✝ e✝ B✝

State before:
case defeq
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, HasType env U Γ e1 A → defEq Γ e1 e2 → IsDefEq env U Γ e1 e2 A
e A : VExpr
Γ✝ : List VExpr
A✝ B✝ e✝ : VExpr
h1 : defEq Γ✝ A✝ B✝
a✝ : HasTypeU1 env U defEq Γ✝ e✝ A✝
ih : OnCtx Γ✝ (IsType env U) → HasType env U Γ✝ e✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U Γ✝ A✝ (VExpr.sort w✝)
⊢ HasType env U Γ✝ e✝ B✝
Tactic:
exact (IH h h1).defeq (ih hΓ)
State after:
no goals