internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (VExpr.const c✝ ls✝) k) (liftN n (VExpr.const c✝ ls'✝) k) (instL ls✝ ci✝.type)
Tactic:
exact .constDF h1 h2 h3 h4 h5
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case appDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n f✝ k) (liftN n f'✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n a✝² k) (liftN n a'✝ k) (liftN n A✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (app f✝ a✝²) k) (liftN n (app f'✝ a'✝) k) (liftN n (inst B✝ a✝²) k)
Tactic:
exact liftN_inst_hi .. ▸ .appDF (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case lamDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n A✝ k) (liftN n A'✝ k) (liftN n (VExpr.sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEq env U Γ' (liftN n body✝ k) (liftN n body'✝ k) (liftN n B✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (lam A✝ body✝) k) (liftN n (lam A'✝ body'✝) k) (liftN n (VExpr.forallE A✝ B✝) k)
Tactic:
exact .lamDF (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case forallEDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n A✝ k) (liftN n A'✝ k) (liftN n (VExpr.sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEq env U Γ' (liftN n body✝ k) (liftN n body'✝ k) (liftN n (VExpr.sort v✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (VExpr.forallE A✝ body✝) k) (liftN n (VExpr.forallE A'✝ body'✝) k)
    (liftN n (VExpr.sort (VLevel.imax u✝ v✝)) k)
Tactic:
exact .forallEDF (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case defeqDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n A✝ k) (liftN n B✝ k) (liftN n (VExpr.sort u✝) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e1✝ k) (liftN n e2✝ k) (liftN n A✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n e1✝ k) (liftN n e2✝ k) (liftN n B✝ k)
Tactic:
exact .defeqDF (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case beta
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (A✝ :: Γ✝) Γ' → IsDefEq env U Γ' (liftN n e✝ k) (liftN n e✝ k) (liftN n B✝ k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e'✝ k) (liftN n e'✝ k) (liftN n A✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (app (lam A✝ e✝) e'✝) k) (liftN n (inst e✝ e'✝) k) (liftN n (inst B✝ e'✝) k)
Tactic:
exact VExpr.liftN_inst_hi .. ▸ VExpr.liftN_instN_hi .. ▸ .beta (ih1 W.succ) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case eta
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e✝ k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (lam A✝ (app (lift e✝) (VExpr.bvar 0))) k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
Tactic:
have := IsDefEq.eta (ih W)
Proof state after:
case eta
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e✝ k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
this :
  IsDefEq env U Γ' (lam (liftN n A✝ k) (app (lift (liftN n e✝ k)) (VExpr.bvar 0))) (liftN n e✝ k)
    (VExpr.forallE (liftN n A✝ k) (liftN n B✝ (k + 1)))
⊢ IsDefEq env U Γ' (liftN n (lam A✝ (app (lift e✝) (VExpr.bvar 0))) k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case eta
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e✝ k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
this :
  IsDefEq env U Γ' (lam (liftN n A✝ k) (app (lift (liftN n e✝ k)) (VExpr.bvar 0))) (liftN n e✝ k)
    (VExpr.forallE (liftN n A✝ k) (liftN n B✝ (k + 1)))
⊢ IsDefEq env U Γ' (liftN n (lam A✝ (app (lift e✝) (VExpr.bvar 0))) k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
Tactic:
simp [liftN]
Proof state after:
case eta
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e✝ k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
this :
  IsDefEq env U Γ' (lam (liftN n A✝ k) (app (lift (liftN n e✝ k)) (VExpr.bvar 0))) (liftN n e✝ k)
    (VExpr.forallE (liftN n A✝ k) (liftN n B✝ (k + 1)))
⊢ IsDefEq env U Γ' (lam (liftN n A✝ k) (app (liftN n (lift e✝) (k + 1)) (VExpr.bvar 0))) (liftN n e✝ k)
    (VExpr.forallE (liftN n A✝ k) (liftN n B✝ (k + 1)))
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case eta
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e✝ k) (liftN n e✝ k) (liftN n (VExpr.forallE A✝ B✝) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
this :
  IsDefEq env U Γ' (lam (liftN n A✝ k) (app (lift (liftN n e✝ k)) (VExpr.bvar 0))) (liftN n e✝ k)
    (VExpr.forallE (liftN n A✝ k) (liftN n B✝ (k + 1)))
⊢ IsDefEq env U Γ' (lam (liftN n A✝ k) (app (liftN n (lift e✝) (k + 1)) (VExpr.bvar 0))) (liftN n e✝ k)
    (VExpr.forallE (liftN n A✝ k) (liftN n B✝ (k + 1)))
Tactic:
rwa [← lift_liftN']
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case proofIrrel
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n p✝ k) (liftN n p✝ k) (liftN n (VExpr.sort VLevel.zero) k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n h✝ k) (liftN n h✝ k) (liftN n p✝ k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n h'✝ k) (liftN n h'✝ k) (liftN n p✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n h✝ k) (liftN n h'✝ k) (liftN n p✝ k)
Tactic:
exact .proofIrrel (ih1 W) (ih2 W) (ih3 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.type) k)
Tactic:
have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
Proof state after:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.type) k)
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ' (liftN n (instL ls✝ df✝.lhs) k) (liftN n (instL ls✝ df✝.rhs) k) (liftN n (instL ls✝ df✝.type) k)
Tactic:
rw [
  hA1.instL.liftN_eq (Nat.zero_le _),
  hA2.instL.liftN_eq (Nat.zero_le _),
  hA3.instL.liftN_eq (Nat.zero_le _)]
Proof state after:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case extra
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
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
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ' (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
Tactic:
exact .extra h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakR
Proof state before:
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
hΓ : CtxClosed Γ
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
⊢ IsDefEq env U (Γ ++ Γ') e1 e2 A
Tactic:
have ⟨h1, h2, h3⟩ := H.closedN' henv.closed hΓ
Proof state after:
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
hΓ : CtxClosed Γ
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
h1 : ClosedN e1 (List.length Γ)
h2 : ClosedN e2 (List.length Γ)
h3 : ClosedN A (List.length Γ)
⊢ IsDefEq env U (Γ ++ Γ') e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.weakR
Proof state before:
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
hΓ : CtxClosed Γ
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
h1 : ClosedN e1 (List.length Γ)
h2 : ClosedN e2 (List.length Γ)
h3 : ClosedN A (List.length Γ)
⊢ IsDefEq env U (Γ ++ Γ') e1 e2 A
Tactic:
simpa [h1.liftN_eq, h2.liftN_eq, h3.liftN_eq] using H.weakN henv (.right hΓ Γ')
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weak'
Proof state before:
env : VEnv
henv : Ordered env
l : Lift
Γ Γ' : List VExpr
U : Nat
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
H : IsDefEq env U Γ e1 e2 A
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Tactic:
generalize e : l.depth = n
Proof state after:
env : VEnv
henv : Ordered env
l : Lift
Γ Γ' : List VExpr
U : Nat
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
H : IsDefEq env U Γ e1 e2 A
n : Nat
e : Lift.depth l = n
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Theorem: Lean4Lean.VEnv.IsDefEq.weak'
Proof state before:
env : VEnv
henv : Ordered env
l : Lift
Γ Γ' : List VExpr
U : Nat
e1 e2 A : VExpr
W : Ctx.Lift' l Γ Γ'
H : IsDefEq env U Γ e1 e2 A
n : Nat
e : Lift.depth l = n
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Tactic:
induction n generalizing l Γ' with
| zero => simpa [lift'_depth_zero e, W.depth_zero e] using H
| succ n ih =>
  obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
  have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
  simp only [Lift.consN_skip_eq, lift'_comp, lift'_consN_skipN]
  exact (ih W1 Lift.depth_consN).weakN henv W2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weak'
Proof state before:
case zero
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
l : Lift
Γ' : List VExpr
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.zero
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Tactic:
simpa [lift'_depth_zero e, W.depth_zero e] using H
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weak'
Proof state before:
case succ
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
n : Nat
ih :
  ∀ {l : Lift} {Γ' : List VExpr},
    Ctx.Lift' l Γ Γ' → Lift.depth l = n → IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
l : Lift
Γ' : List VExpr
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.succ n
⊢ IsDefEq env U Γ' (lift' e1 l) (lift' e2 l) (lift' A l)
Tactic:
obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
Proof state after:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEq env U Γ' (lift' e1 (Lift.consN (Lift.skip l) k)) (lift' e2 (Lift.consN (Lift.skip l) k))
    (lift' A (Lift.consN (Lift.skip l) k))
Theorem: Lean4Lean.VEnv.IsDefEq.weak'
Proof state before:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ IsDefEq env U Γ' (lift' e1 (Lift.consN (Lift.skip l) k)) (lift' e2 (Lift.consN (Lift.skip l) k))
    (lift' A (Lift.consN (Lift.skip l) k))
Tactic:
have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
Proof state after:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEq env U Γ' (lift' e1 (Lift.consN (Lift.skip l) k)) (lift' e2 (Lift.consN (Lift.skip l) k))
    (lift' A (Lift.consN (Lift.skip l) k))
Theorem: Lean4Lean.VEnv.IsDefEq.weak'
Proof state before:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEq env U Γ' (lift' e1 (Lift.consN (Lift.skip l) k)) (lift' e2 (Lift.consN (Lift.skip l) k))
    (lift' A (Lift.consN (Lift.skip l) k))
Tactic:
simp only [Lift.consN_skip_eq, lift'_comp, lift'_consN_skipN]
Proof state after:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEq env U Γ' (liftN 1 (lift' e1 (Lift.consN l k)) k) (liftN 1 (lift' e2 (Lift.consN l k)) k)
    (liftN 1 (lift' A (Lift.consN l k)) k)
Theorem: Lean4Lean.VEnv.IsDefEq.weak'
Proof state before:
case succ.intro.intro.intro
env : VEnv
henv : Ordered env
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → IsDefEq env U Γ' (lift' e1 l_1) (lift' e2 l_1) (lift' A l_1)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ IsDefEq env U Γ' (liftN 1 (lift' e1 (Lift.consN l k)) k) (liftN 1 (lift' e2 (Lift.consN l k)) k)
    (liftN 1 (lift' A (Lift.consN l k)) k)
Tactic:
exact (ih W1 Lift.depth_consN).weakN henv W2
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
H : IsDefEq env U Γ e1 e2 A
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ) (VExpr.instL ls e1) (VExpr.instL ls e2) (VExpr.instL ls A)
Tactic:
induction H with
| bvar h => refine .bvar h.instL
| symm _ ih => exact .symm ih
| trans _ _ ih1 ih2 => exact .trans ih1 ih2
| sortDF _ _ h3 =>
  exact .sortDF (VLevel.WF.inst hls) (VLevel.WF.inst hls) (VLevel.inst_congr_l h3)
| @constDF _ _ ls₁ ls₂ _ h1 h2 h3 h4 h5 =>
  simp [VExpr.instL, VExpr.instL_instL]
  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)
| appDF _ _ ih1 ih2 => exact VExpr.instL_instN ▸ .appDF ih1 ih2
| lamDF _ _ ih1 ih2 => exact .lamDF ih1 ih2
| forallEDF _ _ ih1 ih2 => exact .forallEDF ih1 ih2
| defeqDF _ _ ih1 ih2 => exact .defeqDF ih1 ih2
| beta _ _ ih1 ih2 => simpa using .beta ih1 ih2
| eta _ ih => simpa [VExpr.instL] using .eta ih
| proofIrrel _ _ _ ih1 ih2 ih3 => exact .proofIrrel ih1 ih2 ih3
| extra h1 h2 h3 =>
  simp [VExpr.instL, VExpr.instL_instL]
  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:
case bvar
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
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.bvar i✝)) (VExpr.instL ls (VExpr.bvar i✝))
    (VExpr.instL ls A✝)
Tactic:
refine .bvar h.instL
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case symm
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✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : 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 e'✝) (VExpr.instL ls e✝) (VExpr.instL ls A✝)
Tactic:
exact .symm ih
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case trans
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₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEq env U Γ✝ e₂✝ e₃✝ A✝
ih1 : IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e₁✝) (VExpr.instL ls e₂✝) (VExpr.instL ls A✝)
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 e₁✝) (VExpr.instL ls e₃✝) (VExpr.instL ls A✝)
Tactic:
exact .trans ih1 ih2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instL
Proof state before:
case sortDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
a✝¹ : VLevel.WF U l✝
a✝ : VLevel.WF U l'✝
h3 : l✝ ≈ l'✝
⊢ IsDefEq env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.sort l✝)) (VExpr.instL ls (VExpr.sort l'✝))
    (VExpr.instL ls (VExpr.sort (VLevel.succ l✝)))
Tactic:
exact .sortDF (VLevel.WF.inst hls) (VLevel.WF.inst hls) (VLevel.inst_congr_l h3)
Proof state after:
no goals
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.instL ls (VExpr.const c✝ ls₁))
    (VExpr.instL ls (VExpr.const c✝ ls₂)) (VExpr.instL ls (VExpr.instL ls₁ ci✝.type))
Tactic:
simp [VExpr.instL, VExpr.instL_instL]
Proof state after:
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)