internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case lamDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ihA :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A'✝ (VExpr.sort u✝)
ihB :
  HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝ :
  HasType1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEq1 env U hasType defEq (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
ihb :
  HasType1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasType1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) body✝ body'✝ B✝
ihb' :
  HasType1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasType1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEq1 env U hasType defEq (A'✝ :: Γ✝) body✝ body'✝ B✝
⊢ HasType1 env U defEq Γ✝ (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
exact .defeq (hdf <| .symm <| .forallEDF ihA.2.2 ihB.2.2) <| .lam ihA.2.1 ihb'.2.1
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case forallEDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 :
  HasType1 env U defEq (A✝ :: Γ✝) body✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A✝ :: Γ✝) body'✝ (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih3 :
  HasType1 env U defEq (A'✝ :: Γ✝) body✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A'✝ :: Γ✝) body'✝ (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq (A'✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
⊢ HasType1 env U defEq Γ✝ (VExpr.forallE A✝ body✝) (VExpr.sort (VLevel.imax u✝ v✝)) ∧
    HasType1 env U defEq Γ✝ (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝)) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝)
        (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact ⟨.forallE ih1.1 ih2.1, .forallE ih1.2.1 ih3.2.1, .forallEDF ih1.2.2 ih2.2.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case defeqDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
ih1 :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ B✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ B✝ (VExpr.sort u✝)
ih2 : HasType1 env U defEq Γ✝ e1✝ A✝ ∧ HasType1 env U defEq Γ✝ e2✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e1✝ e2✝ A✝
⊢ HasType1 env U defEq Γ✝ e1✝ B✝ ∧ HasType1 env U defEq Γ✝ e2✝ B✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e1✝ e2✝ B✝
Tactic:
exact ⟨.defeq (hdf ih1.2.2) ih2.1, .defeq (hdf ih1.2.2) ih2.2.1, .defeqDF (hdf ih1.2.2) ih2.2.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case beta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ihA :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A✝ (VExpr.sort u✝)
a_ih✝¹ :
  HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
ihe :
  HasType1 env U defEq (A✝ :: Γ✝) e✝ B✝ ∧
    HasType1 env U defEq (A✝ :: Γ✝) e✝ B✝ ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) e✝ e✝ B✝
ihe' : HasType1 env U defEq Γ✝ e'✝ A✝ ∧ HasType1 env U defEq Γ✝ e'✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e'✝ e'✝ A✝
a_ih✝ :
  HasType1 env U defEq Γ✝ (inst B✝ e'✝) (VExpr.sort v✝) ∧
    HasType1 env U defEq Γ✝ (inst B✝ e'✝) (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
ihee :
  HasType1 env U defEq Γ✝ (inst e✝ e'✝) (inst B✝ e'✝) ∧
    HasType1 env U defEq Γ✝ (inst e✝ e'✝) (inst B✝ e'✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
⊢ HasType1 env U defEq Γ✝ (app (lam A✝ e✝) e'✝) (inst B✝ e'✝) ∧
    HasType1 env U defEq Γ✝ (inst e✝ e'✝) (inst B✝ e'✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
exact ⟨.app (.lam ihA.1 ihe.1) ihe'.1, ihee.1, .beta (hty ihe.1) (hty ihe'.1)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case eta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
ihA :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A✝ (VExpr.sort u✝)
a_ih✝¹ :
  HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝ :
  HasType1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasType1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
ihe :
  HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEq1 env U hasType defEq Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ihe' :
  HasType1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasType1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEq1 env U hasType defEq (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
this : HasType1 env U defEq (A✝ :: Γ✝) (app (lift e✝) (VExpr.bvar 0)) B✝
⊢ HasType1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
exact ⟨.lam ihA.1 this, ihe.1, .eta (hty ihe.1)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case proofIrrel
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEqStrong env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
ih1 :
  HasType1 env U defEq Γ✝ p✝ (VExpr.sort VLevel.zero) ∧
    HasType1 env U defEq Γ✝ p✝ (VExpr.sort VLevel.zero) ∧ IsDefEq1 env U hasType defEq Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
ih2 : HasType1 env U defEq Γ✝ h✝ p✝ ∧ HasType1 env U defEq Γ✝ h✝ p✝ ∧ IsDefEq1 env U hasType defEq Γ✝ h✝ h✝ p✝
ih3 : HasType1 env U defEq Γ✝ h'✝ p✝ ∧ HasType1 env U defEq Γ✝ h'✝ p✝ ∧ IsDefEq1 env U hasType defEq Γ✝ h'✝ h'✝ p✝
⊢ HasType1 env U defEq Γ✝ h✝ p✝ ∧ HasType1 env U defEq Γ✝ h'✝ p✝ ∧ IsDefEq1 env U hasType defEq Γ✝ h✝ h'✝ p✝
Tactic:
exact ⟨ih2.1, ih3.1, .proofIrrel (hty ih1.1) (hty ih2.1) (hty ih3.1)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case extra
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  HasType1 env U defEq [] (VExpr.instL ls✝ df✝.type) (VExpr.sort u✝) ∧
    HasType1 env U defEq [] (VExpr.instL ls✝ df✝.type) (VExpr.sort u✝) ∧
      IsDefEq1 env U hasType defEq [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (VExpr.sort u✝)
a_ih✝¹ :
  HasType1 env U defEq [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
    HasType1 env U defEq [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEq1 env U hasType defEq [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a_ih✝ :
  HasType1 env U defEq [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
    HasType1 env U defEq [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEq1 env U hasType defEq [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
ihl' :
  HasType1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
    HasType1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
ihr' :
  HasType1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
    HasType1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
⊢ HasType1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type) ∧
    HasType1 env U defEq Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
exact ⟨ihl'.1, ihr'.1, .extra h1 h2 h3⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e A : VExpr
H : HasType1 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 ih2
| lam _ _ ih1 ih2 => exact .lam ih1 ih2
| forallE _ _ ih1 ih2 => exact .forallE ih1 ih2
| defeq h1 _ ih => exact (IH h1).defeq ih
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
case bvar
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
⊢ HasType env U Γ✝ (VExpr.bvar i✝) A✝
Tactic:
exact .bvar h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
case const
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
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
⊢ HasType env U Γ✝ (VExpr.const c✝ ls✝) (instL ls✝ ci✝.type)
Tactic:
exact .const h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
case sort
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e A : VExpr
Γ✝ : List VExpr
l✝ : VLevel
h : VLevel.WF U l✝
⊢ HasType env U Γ✝ (VExpr.sort l✝) (VExpr.sort (VLevel.succ l✝))
Tactic:
exact .sort h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
case app
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e A : VExpr
Γ✝ : List VExpr
f✝ A✝ B✝ a✝² : VExpr
a✝¹ : HasType1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
a✝ : HasType1 env U defEq Γ✝ a✝² A✝
ih1 : HasType env U Γ✝ f✝ (VExpr.forallE A✝ B✝)
ih2 : HasType env U Γ✝ a✝² A✝
⊢ HasType env U Γ✝ (VExpr.app f✝ a✝²) (inst B✝ a✝²)
Tactic:
exact .app ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
case lam
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
body✝ B✝ : VExpr
a✝¹ : HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝)
a✝ : HasType1 env U defEq (A✝ :: Γ✝) body✝ B✝
ih1 : HasType env U Γ✝ A✝ (VExpr.sort u✝)
ih2 : HasType env U (A✝ :: Γ✝) body✝ B✝
⊢ HasType env U Γ✝ (VExpr.lam A✝ body✝) (VExpr.forallE A✝ B✝)
Tactic:
exact .lam ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
case forallE
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
body✝ : VExpr
v✝ : VLevel
a✝¹ : HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝)
a✝ : HasType1 env U defEq (A✝ :: Γ✝) body✝ (VExpr.sort v✝)
ih1 : HasType env U Γ✝ A✝ (VExpr.sort u✝)
ih2 : HasType env U (A✝ :: Γ✝) body✝ (VExpr.sort v✝)
⊢ HasType env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact .forallE ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType1.induction
Proof state before:
case defeq
env : VEnv
U : Nat
henv : Ordered env
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
IH : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e✝ : VExpr
h1 : defEq Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : HasType1 env U defEq Γ✝ e✝ A✝
ih : HasType env U Γ✝ e✝ A✝
⊢ HasType env U Γ✝ e✝ B✝
Tactic:
exact (IH h1).defeq ih
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
H : IsDefEq1 env U hasType defEq Γ e1 e2 A
⊢ IsDefEq env U Γ e1 e2 A
Tactic:
induction H with
| refl h => exact hty h
| symm _ ih => exact ih.symm
| trans _ _ ih1 ih2 => exact ih1.trans ih2
| constDF h1 h2 h3 h4 h5 => exact .constDF h1 h2 h3 h4 h5
| sortDF h1 h2 h3 => exact .sortDF h1 h2 h3
| appDF _ _ ih1 ih2 => exact .appDF ih1 ih2
| lamDF _ _ ih1 ih2 => exact .lamDF ih1 ih2
| forallEDF _ _ ih1 ih2 => exact .forallEDF ih1 ih2
| defeqDF h1 _ ih => exact .defeqDF (hdf h1) ih
| beta h1 h2 => exact .beta (hty h1) (hty h2)
| eta h => exact .eta (hty h)
| proofIrrel h1 h2 h3 => exact .proofIrrel (hty h1) (hty h2) (hty h3)
| extra h1 h2 h3 => exact .extra h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case refl
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ : VExpr
h : hasType Γ✝ e✝ A✝
⊢ IsDefEq env U Γ✝ e✝ e✝ A✝
Tactic:
exact hty h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case symm
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq1 env U hasType defEq Γ✝ e✝ e'✝ A✝
ih : IsDefEq env U Γ✝ e✝ e'✝ A✝
⊢ IsDefEq env U Γ✝ e'✝ e✝ A✝
Tactic:
exact ih.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case trans
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEq1 env U hasType defEq Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEq1 env U hasType defEq Γ✝ e₂✝ e₃✝ A✝
ih1 : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
ih2 : IsDefEq env U Γ✝ e₂✝ e₃✝ A✝
⊢ IsDefEq env U Γ✝ e₁✝ e₃✝ A✝
Tactic:
exact ih1.trans ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case constDF
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
⊢ IsDefEq env U Γ✝ (const c✝ ls✝) (const c✝ ls'✝) (instL ls✝ ci✝.type)
Tactic:
exact .constDF h1 h2 h3 h4 h5
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case sortDF
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
h2 : VLevel.WF U l'✝
h3 : l✝ ≈ l'✝
⊢ IsDefEq env U Γ✝ (sort l✝) (sort l'✝) (sort (VLevel.succ l✝))
Tactic:
exact .sortDF h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case appDF
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq1 env U hasType defEq Γ✝ f✝ f'✝ (forallE A✝ B✝)
a✝ : IsDefEq1 env U hasType defEq Γ✝ a✝² a'✝ A✝
ih1 : IsDefEq env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
ih2 : IsDefEq env U Γ✝ a✝² a'✝ A✝
⊢ IsDefEq env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
exact .appDF ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case lamDF
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
b✝ b'✝ B✝ : VExpr
a✝¹ : IsDefEq1 env U hasType defEq Γ✝ A✝ A'✝ (sort u✝)
a✝ : IsDefEq1 env U hasType defEq (A✝ :: Γ✝) b✝ b'✝ B✝
ih1 : IsDefEq env U Γ✝ A✝ A'✝ (sort u✝)
ih2 : IsDefEq env U (A✝ :: Γ✝) b✝ b'✝ B✝
⊢ IsDefEq env U Γ✝ (lam A✝ b✝) (lam A'✝ b'✝) (forallE A✝ B✝)
Tactic:
exact .lamDF ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq1.induction
Proof state before:
case forallEDF
env : VEnv
U : Nat
henv : Ordered env
hasType : List VExpr → VExpr → VExpr → Prop
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, hasType Γ e A → HasType env U Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, defEq Γ e1 e2 A → IsDefEq env U Γ e1 e2 A
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ B'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq1 env U hasType defEq Γ✝ A✝ A'✝ (sort u✝)
a✝ : IsDefEq1 env U hasType defEq (A✝ :: Γ✝) B✝ B'✝ (sort v✝)
ih1 : IsDefEq env U Γ✝ A✝ A'✝ (sort u✝)
ih2 : IsDefEq env U (A✝ :: Γ✝) B✝ B'✝ (sort v✝)
⊢ IsDefEq env U Γ✝ (forallE A✝ B✝) (forallE A'✝ B'✝) (sort (VLevel.imax u✝ v✝))
Tactic:
exact .forallEDF ih1 ih2
Proof state after:
no goals