internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar.inl.succ.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
i : Nat
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inl i) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Tactic:
refine ⟨_, ih (v := .inl i) hΔ'.1 H, ?_⟩
Proof state after:
case cons_bvar.inl.succ.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
i : Nat
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inl i) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).fst =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
    VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).snd =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar.inr
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
H :
  ∃ a,
    VLCtx.find? Δ✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth d) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) a.snd = A
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst = VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd = VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d)
Tactic:
obtain ⟨⟨e, A⟩, H, rfl, rfl⟩ := H
Proof state after:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.fst =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) a.snd =
          VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Tactic:
refine ⟨_, ih (v := .inr fv) hΔ'.1 H, ?_⟩
Proof state after:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).fst =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
    VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).snd =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar.inr.intro.mk.intro.intro
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ'✝ → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ'✝ v = some (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝)
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
fv : FVarId
e A : VExpr
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).fst =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).fst) (k✝ + VLocalDecl.depth d) ∧
    VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) (VExpr.liftN n✝ e k✝, VExpr.liftN n✝ A k✝).snd =
      VExpr.liftN n✝ (VExpr.liftN (VLocalDecl.depth d) (e, A).snd) (k✝ + VLocalDecl.depth d)
Tactic:
cases d <;> simp [VExpr.lift_liftN', liftN, value, type, depth, VExpr.liftN]
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Us : List Name
e : Expr
e' : VExpr
W : VLCtx.LiftN Δ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
H : TrExpr env Us Δ e e'
⊢ TrExpr env Us Δ' e (VExpr.liftN n e' k)
Tactic:
induction H generalizing Δ' dk k with
| bvar h1 => exact .bvar (W.find? hΔ' h1)
| fvar h1 => exact .fvar (W.find? hΔ' h1)
| sort h1 => exact .sort h1
| const h1 h2 h3 => exact .const h1 h2 h3
| app h1 h2 _ _ ih1 ih2 =>
  exact .app (h1.weakN henv W.toCtx) (h2.weakN henv W.toCtx) (ih1 W hΔ') (ih2 W hΔ')
| lam h1 _ _ ih1 ih2 =>
  have h1 := h1.weakN henv W.toCtx
  exact .lam h1 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
| forallE h1 h2 _ _ ih1 ih2 =>
  have h1 := h1.weakN henv W.toCtx
  have h2 := h2.weakN henv W.toCtx.succ
  exact .forallE h1 h2 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
| letE h1 _ _ _ ih1 ih2 ih3 =>
  have h1 := h1.weakN henv W.toCtx
  exact .letE h1 (ih1 W hΔ') (ih2 W hΔ') (ih3 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
| lit _ ih => exact .lit (ih W hΔ')
| mdata _ ih => exact .mdata (ih W hΔ')
| proj _ h2 ih => exact .proj (ih W hΔ') (h2.weakN W.toCtx)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case bvar
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
i✝ : Nat
h1 : VLCtx.find? Δ✝ (Sum.inl i✝) = some (e✝, A✝)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.bvar i✝) (VExpr.liftN n e✝ k)
Tactic:
exact .bvar (W.find? hΔ' h1)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case fvar
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.fvar fv✝) (VExpr.liftN n e✝ k)
Tactic:
exact .fvar (W.find? hΔ' h1)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case sort
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
h1 : VLevel.ofLevel Us u✝ = some u'✝
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.sort u✝) (VExpr.liftN n (VExpr.sort u'✝) k)
Tactic:
exact .sort h1
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case const
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
h3 : List.length us✝ = ci✝.uvars
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.const c✝ us✝) (VExpr.liftN n (VExpr.const c✝ us'✝) k)
Tactic:
exact .const h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case app
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝² : Expr
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
a✝¹ : TrExpr env Us Δ✝ f✝ f'✝
a✝ : TrExpr env Us Δ✝ a✝² a'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' f✝ (VExpr.liftN n f'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' a✝² (VExpr.liftN n a'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.app f✝ a✝²) (VExpr.liftN n (VExpr.app f'✝ a'✝) k)
Tactic:
exact .app (h1.weakN henv W.toCtx) (h2.weakN henv W.toCtx) (ih1 W hΔ') (ih2 W hΔ')
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case lam
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.lam name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.lam ty'✝ body'✝) k)
Tactic:
have h1 := h1.weakN henv W.toCtx
Proof state after:
case lam
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.lam name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.lam ty'✝ body'✝) k)
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case lam
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.lam name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.lam ty'✝ body'✝) k)
Tactic:
exact .lam h1 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Tactic:
have h1 := h1.weakN henv W.toCtx
Proof state after:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2 : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Tactic:
have h2 := h2.weakN henv W.toCtx.succ
Proof state after:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
h2 : IsType env (List.length Us) (VExpr.liftN n ty'✝ k :: VLCtx.toCtx Δ') (VExpr.liftN n body'✝ (k + 1))
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case forallE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
a✝¹ : TrExpr env Us Δ✝ ty✝ ty'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n ty'✝ k)
h2 : IsType env (List.length Us) (VExpr.liftN n ty'✝ k :: VLCtx.toCtx Δ') (VExpr.liftN n body'✝ (k + 1))
⊢ TrExpr env Us Δ' (Expr.forallE name✝ ty✝ body✝ bi✝) (VExpr.liftN n (VExpr.forallE ty'✝ body'✝) k)
Tactic:
exact .forallE h1 h2 (ih1 W hΔ') (ih2 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case letE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝
a✝¹ : TrExpr env Us Δ✝ val✝ val'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' val✝ (VExpr.liftN n val'✝ k)
ih3 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VExpr.liftN n body'✝ k)
Tactic:
have h1 := h1.weakN henv W.toCtx
Proof state after:
case letE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝
a✝¹ : TrExpr env Us Δ✝ val✝ val'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' val✝ (VExpr.liftN n val'✝ k)
ih3 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n val'✝ k) (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VExpr.liftN n body'✝ k)
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case letE
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
a✝² : TrExpr env Us Δ✝ ty✝ ty'✝
a✝¹ : TrExpr env Us Δ✝ val✝ val'✝
a✝ : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' ty✝ (VExpr.liftN n ty'✝ k)
ih2 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' val✝ (VExpr.liftN n val'✝ k)
ih3 :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' body✝ (VExpr.liftN n body'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ') (VExpr.liftN n val'✝ k) (VExpr.liftN n ty'✝ k)
⊢ TrExpr env Us Δ' (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VExpr.liftN n body'✝ k)
Tactic:
exact .letE h1 (ih1 W hΔ') (ih2 W hΔ') (ih3 (W.cons_bvar _) ⟨hΔ', nofun, h1⟩)
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case lit
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k →
      VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' (Literal.toConstructor l✝) (VExpr.liftN n e✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.lit l✝) (VExpr.liftN n e✝ k)
Tactic:
exact .lit (ih W hΔ')
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case mdata
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
ih :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' e✝ (VExpr.liftN n e'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.mdata d✝ e✝) (VExpr.liftN n e'✝ k)
Tactic:
exact .mdata (ih W hΔ')
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN
Proof state before:
case proj
env : VEnv
henv : Ordered env
Δ : VLCtx
n : Nat
Us : List Name
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
a✝ : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih :
  ∀ {Δ' : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ✝ Δ' dk n k → VLCtx.WF env (List.length Us) Δ' → TrExpr env Us Δ' e✝ (VExpr.liftN n e'✝ k)
Δ' : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ✝ Δ' dk n k
hΔ' : VLCtx.WF env (List.length Us) Δ'
⊢ TrExpr env Us Δ' (Expr.proj s✝ i✝ e✝) (VExpr.liftN n e''✝ k)
Tactic:
exact .proj (ih W hΔ') (h2.weakN W.toCtx)
Proof state after:
no goals