internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case constDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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' (List.map (VExpr.instL ls) Γ✝) (VExpr.const c✝ (List.map (VLevel.inst ls) ls₁))
    (VExpr.const c✝ (List.map (VLevel.inst ls) ls₂)) (VExpr.instL (List.map (VLevel.inst ls) ls₁) ci✝.type)
Tactic:
exact .constDF h1 (by simp [h2, VLevel.WF.inst hls]) (by simp [h3, VLevel.WF.inst hls])
  (by simp [h4]) (by simpa using h5.imp fun _ _ => VLevel.inst_congr_l)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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₂
⊢ ∀ (l : VLevel), l ∈ List.map (VLevel.inst ls) ls₁ → VLevel.WF U' l
Tactic:
simp [h2, VLevel.WF.inst hls]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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₂
⊢ ∀ (l : VLevel), l ∈ List.map (VLevel.inst ls) ls₂ → VLevel.WF U' l
Tactic:
simp [h3, VLevel.WF.inst hls]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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₂
⊢ List.length (List.map (VLevel.inst ls) ls₁) = ci✝.uvars
Tactic:
simp [h4]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : 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₂
⊢ List.Forall₂ (fun x x_1 => x ≈ x_1) (List.map (VLevel.inst ls) ls₁) (List.map (VLevel.inst ls) ls₂)
Tactic:
simpa using h5.imp fun _ _ => VLevel.inst_congr_l
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case appDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 :
  IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls f✝) (VExpr.instL ls f'✝)
    (VExpr.instL ls (VExpr.forallE A✝ B✝))
ih2 : IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls a✝²) (VExpr.instL ls a'✝) (VExpr.instL ls A✝)
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (app f✝ a✝²)) (VExpr.instL ls (app f'✝ a'✝))
    (VExpr.instL ls (inst B✝ a✝²))
Tactic:
exact VExpr.instL_instN ▸ .appDF ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case lamDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 :
  IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A'✝)
    (VExpr.instL ls (VExpr.sort u✝))
ih2 :
  IsDefEq env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls body✝) (VExpr.instL ls body'✝)
    (VExpr.instL ls B✝)
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (lam A✝ body✝)) (VExpr.instL ls (lam A'✝ body'✝))
    (VExpr.instL ls (VExpr.forallE A✝ B✝))
Tactic:
exact .lamDF ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case forallEDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 :
  IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A'✝)
    (VExpr.instL ls (VExpr.sort u✝))
ih2 :
  IsDefEq env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls body✝) (VExpr.instL ls body'✝)
    (VExpr.instL ls (VExpr.sort v✝))
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.forallE A✝ body✝))
    (VExpr.instL ls (VExpr.forallE A'✝ body'✝)) (VExpr.instL ls (VExpr.sort (VLevel.imax u✝ v✝)))
Tactic:
exact .forallEDF ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case defeqDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 :
  IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls B✝) (VExpr.instL ls (VExpr.sort u✝))
ih2 : IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e1✝) (VExpr.instL ls e2✝) (VExpr.instL ls A✝)
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e1✝) (VExpr.instL ls e2✝) (VExpr.instL ls B✝)
Tactic:
exact .defeqDF ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case beta
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : IsDefEq env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls e✝) (VExpr.instL ls e✝) (VExpr.instL ls B✝)
ih2 : IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e'✝) (VExpr.instL ls e'✝) (VExpr.instL ls A✝)
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (app (lam A✝ e✝) e'✝)) (VExpr.instL ls (inst e✝ e'✝))
    (VExpr.instL ls (inst B✝ e'✝))
Tactic:
simpa using .beta ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case eta
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls (VExpr.forallE A✝ B✝))
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (lam A✝ (app (lift e✝) (VExpr.bvar 0))))
    (VExpr.instL ls e✝) (VExpr.instL ls (VExpr.forallE A✝ B✝))
Tactic:
simpa [VExpr.instL] using .eta ih
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case proofIrrel
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
ih1 :
  IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls p✝) (VExpr.instL ls p✝)
    (VExpr.instL ls (VExpr.sort VLevel.zero))
ih2 : IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h✝) (VExpr.instL ls h✝) (VExpr.instL ls p✝)
ih3 : IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h'✝) (VExpr.instL ls h'✝) (VExpr.instL ls p✝)
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h✝) (VExpr.instL ls h'✝) (VExpr.instL ls p✝)
Tactic:
exact .proofIrrel ih1 ih2 ih3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
Tactic:
simp [VExpr.instL, VExpr.instL_instL]
Proof state after:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
Tactic:
exact .extra h1 (by simp [h2, VLevel.WF.inst hls]) (by simp [h3])
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
⊢ ∀ (l : VLevel), l ∈ List.map (VLevel.inst ls) ls✝ → VLevel.WF U' l
Tactic:
simp [h2, VLevel.WF.inst hls]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
⊢ List.length (List.map (VLevel.inst ls) ls✝) = df✝.uvars
Tactic:
simp [h3]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
k : Nat
Γ₁ Γ : List VExpr
e1 e2 A : VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ₁ Γ
H : IsDefEq env U Γ₁ e1 e2 A
⊢ IsDefEq env U Γ (inst e1 e₀ k) (inst e2 e₀ k) (inst A e₀ k)
Tactic:
induction H generalizing Γ k with
| @bvar _ i ty h =>
  dsimp [inst]
  induction W generalizing i ty with
  | zero =>
    cases h with simp [inst_lift]
    | zero => exact h₀
    | succ h => exact .bvar h
  | succ _ ih =>
    cases h with (simp; rw [Nat.add_comm, ← VExpr.liftN_instN_lo (hj := Nat.zero_le _)])
    | zero => exact .bvar .zero
    | succ h => exact (ih h).weak henv
| symm _ ih => exact .symm (ih W)
| trans _ _ ih1 ih2 => exact .trans (ih1 W) (ih2 W)
| sortDF h1 h2 h3 => exact .sortDF h1 h2 h3
| constDF h1 h2 h3 h4 h5 =>
  rw [(henv.closedC h1).instL.instN_eq (Nat.zero_le _)]
  exact .constDF h1 h2 h3 h4 h5
| appDF _ _ ih1 ih2 => exact VExpr.inst_inst_hi .. ▸ .appDF (ih1 W) (ih2 W)
| lamDF _ _ ih1 ih2 => exact .lamDF (ih1 W) (ih2 W.succ)
| forallEDF _ _ ih1 ih2 => exact .forallEDF (ih1 W) (ih2 W.succ)
| defeqDF _ _ ih1 ih2 => exact .defeqDF (ih1 W) (ih2 W)
| beta _ _ ih1 ih2 =>
  exact VExpr.inst_inst_hi .. ▸ VExpr.inst_inst_hi .. ▸ .beta (ih1 W.succ) (ih2 W)
| eta _ ih =>
  have := IsDefEq.eta (ih W)
  rw [lift, VExpr.liftN_instN_lo (hj := Nat.zero_le _), Nat.add_comm] at this
  simpa [inst]
| proofIrrel _ _ _ ih1 ih2 ih3 => exact .proofIrrel (ih1 W) (ih2 W) (ih3 W)
| extra h1 h2 h3 =>
  have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
  rw [
    hA1.instL.instN_eq (Nat.zero_le _),
    hA2.instL.instN_eq (Nat.zero_le _),
    hA3.instL.instN_eq (Nat.zero_le _)]
  exact .extra h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
h : Lookup Γ✝ i ty
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (VExpr.bvar i) e₀ k) (inst (VExpr.bvar i) e₀ k) (inst ty e₀ k)
Tactic:
dsimp [inst]
Proof state after:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
h : Lookup Γ✝ i ty
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
h : Lookup Γ✝ i ty
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Tactic:
induction W generalizing i ty with
| zero =>
  cases h with simp [inst_lift]
  | zero => exact h₀
  | succ h => exact .bvar h
| succ _ ih =>
  cases h with (simp; rw [Nat.add_comm, ← VExpr.liftN_instN_lo (hj := Nat.zero_le _)])
  | zero => exact .bvar .zero
  | succ h => exact (ih h).weak henv
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
i : Nat
ty : VExpr
h : Lookup (A₀ :: Γ₀) i ty
⊢ IsDefEq env U Γ₀ (instVar i e₀) (instVar i e₀) (inst ty e₀)
Tactic:
cases h with simp [inst_lift]
| zero => exact h₀
| succ h => exact .bvar h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.zero.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
⊢ IsDefEq env U Γ₀ e₀ e₀ A₀
Tactic:
exact h₀
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.zero.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ₀ n✝ ty✝
⊢ IsDefEq env U Γ₀ (VExpr.bvar n✝) (VExpr.bvar n✝) ty✝
Tactic:
exact .bvar h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat} {ty : VExpr}, Lookup Γ✝ i ty → IsDefEq env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
i : Nat
ty : VExpr
h : Lookup (A✝ :: Γ✝) i ty
⊢ IsDefEq env U (inst A✝ e₀ k✝ :: Γ'✝) (instVar i e₀ (k✝ + 1)) (instVar i e₀ (k✝ + 1)) (inst ty e₀ (k✝ + 1))
Tactic:
cases h with (simp; rw [Nat.add_comm, ← VExpr.liftN_instN_lo (hj := Nat.zero_le _)])
| zero => exact .bvar .zero
| succ h => exact (ih h).weak henv
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat} {ty : VExpr}, Lookup Γ✝ i ty → IsDefEq env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEq env U (inst A✝ e₀ k✝ :: Γ'✝) (instVar (n✝ + 1) e₀ (k✝ + 1)) (instVar (n✝ + 1) e₀ (k✝ + 1))
    (inst (lift ty✝) e₀ (k✝ + 1))
Tactic:
simp
Proof state after:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat} {ty : VExpr}, Lookup Γ✝ i ty → IsDefEq env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEq env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝)) (inst (lift ty✝) e₀ (k✝ + 1))
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat} {ty : VExpr}, Lookup Γ✝ i ty → IsDefEq env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEq env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝)) (inst (lift ty✝) e₀ (k✝ + 1))
Tactic:
rw [Nat.add_comm, ← VExpr.liftN_instN_lo (hj := Nat.zero_le _)]
Proof state after:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat} {ty : VExpr}, Lookup Γ✝ i ty → IsDefEq env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEq env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝)) (liftN 1 (inst ty✝ e₀ k✝))
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.succ.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat} {ty : VExpr}, Lookup Γ✝ i ty → IsDefEq env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
⊢ IsDefEq env U (inst A✝ e₀ k✝ :: Γ'✝) (VExpr.bvar 0) (VExpr.bvar 0) (liftN 1 (inst A✝ e₀ k✝))
Tactic:
exact .bvar .zero
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat} {ty : VExpr}, Lookup Γ✝ i ty → IsDefEq env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEq env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝)) (liftN 1 (inst ty✝ e₀ k✝))
Tactic:
exact (ih h).weak henv
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case symm
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst e'✝ e₀ k) (inst e✝ e₀ k) (inst A✝ e₀ k)
Tactic:
exact .symm (ih W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case trans
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEq env U Γ✝ e₂✝ e₃✝ A✝
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e₁✝ e₀ k) (inst e₂✝ e₀ k) (inst A✝ e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e₂✝ e₀ k) (inst e₃✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst e₁✝ e₀ k) (inst e₃✝ e₀ k) (inst A✝ e₀ k)
Tactic:
exact .trans (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case sortDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ 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'✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (VExpr.sort l✝) e₀ k) (inst (VExpr.sort l'✝) e₀ k) (inst (VExpr.sort (VLevel.succ l✝)) e₀ k)
Tactic:
exact .sortDF h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case constDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ 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'✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (VExpr.const c✝ ls✝) e₀ k) (inst (VExpr.const c✝ ls'✝) e₀ k)
    (inst (VExpr.instL ls✝ ci✝.type) e₀ k)
Tactic:
rw [(henv.closedC h1).instL.instN_eq (Nat.zero_le _)]
Proof state after:
case constDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ 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'✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (VExpr.const c✝ ls✝) e₀ k) (inst (VExpr.const c✝ ls'✝) e₀ k) (VExpr.instL ls✝ ci✝.type)
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case constDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ 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'✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (VExpr.const c✝ ls✝) e₀ k) (inst (VExpr.const c✝ ls'✝) e₀ k) (VExpr.instL ls✝ ci✝.type)
Tactic:
exact .constDF h1 h2 h3 h4 h5
Proof state after:
no goals