Theorem: Lean4Lean.VLCtx.LiftN.toCtx (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
Δ Δ' : VLCtx
dk n k : Nat
W : LiftN Δ Δ' dk n k
⊢ Ctx.LiftN n k (VLCtx.toCtx Δ) (VLCtx.toCtx Δ')
Tactic:
induction W with
| refl => exact .zero []
| @skip_fvar _ Δ' _ _ d _ ih =>
  match d with
  | .vlet .. => exact ih
  | .vlam A =>
    generalize hΓ' : VLCtx.toCtx Δ' = Γ' at ih
    let .zero As eq := ih
    simp [VLCtx.toCtx, hΓ']
    exact .zero (A :: As) (eq ▸ rfl)
| cons_bvar d _ ih =>
  match d with
  | .vlet .. => exact ih
  | .vlam A => exact .succ ih
State after:
no goals

State before:
case refl
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ : VLCtx
⊢ Ctx.LiftN 0 0 (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ✝)
Tactic:
exact .zero []
State after:
no goals

State before:
case skip_fvar
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ')
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth d) 0 (VLCtx.toCtx Δ✝) (VLCtx.toCtx ((some fv✝, d) :: Δ'))
Tactic:
match d with
| .vlet .. => exact ih
| .vlam A =>
  generalize hΓ' : VLCtx.toCtx Δ' = Γ' at ih
  let .zero As eq := ih
  simp [VLCtx.toCtx, hΓ']
  exact .zero (A :: As) (eq ▸ rfl)
State after:
no goals

State before:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ')
type✝ value✝ : VExpr
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlet type✝ value✝)) 0 (VLCtx.toCtx Δ✝)
    (VLCtx.toCtx ((some fv✝, VLocalDecl.vlet type✝ value✝) :: Δ'))
Tactic:
exact ih
State after:
no goals

State before:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ')
A : VExpr
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlam A)) 0 (VLCtx.toCtx Δ✝)
    (VLCtx.toCtx ((some fv✝, VLocalDecl.vlam A) :: Δ'))
Tactic:
generalize hΓ' : VLCtx.toCtx Δ' = Γ' at ih
State after:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
A : VExpr
Γ' : List VExpr
hΓ' : VLCtx.toCtx Δ' = Γ'
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) Γ'
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlam A)) 0 (VLCtx.toCtx Δ✝)
    (VLCtx.toCtx ((some fv✝, VLocalDecl.vlam A) :: Δ'))

State before:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
A : VExpr
Γ' : List VExpr
hΓ' : VLCtx.toCtx Δ' = Γ'
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) Γ'
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlam A)) 0 (VLCtx.toCtx Δ✝)
    (VLCtx.toCtx ((some fv✝, VLocalDecl.vlam A) :: Δ'))
Tactic:
let .zero As eq := ih
State after:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
A : VExpr
Γ' : List VExpr
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) Γ'
As : List VExpr
eq : List.length As = n✝
hΓ' : VLCtx.toCtx Δ' = As ++ VLCtx.toCtx Δ✝
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlam A)) 0 (VLCtx.toCtx Δ✝)
    (VLCtx.toCtx ((some fv✝, VLocalDecl.vlam A) :: Δ'))

State before:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
A : VExpr
Γ' : List VExpr
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) Γ'
As : List VExpr
eq : List.length As = n✝
hΓ' : VLCtx.toCtx Δ' = As ++ VLCtx.toCtx Δ✝
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlam A)) 0 (VLCtx.toCtx Δ✝)
    (VLCtx.toCtx ((some fv✝, VLocalDecl.vlam A) :: Δ'))
Tactic:
simp [VLCtx.toCtx, hΓ']
State after:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
A : VExpr
Γ' : List VExpr
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) Γ'
As : List VExpr
eq : List.length As = n✝
hΓ' : VLCtx.toCtx Δ' = As ++ VLCtx.toCtx Δ✝
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlam A)) 0 (VLCtx.toCtx Δ✝) (A :: (As ++ VLCtx.toCtx Δ✝))

State before:
Δ Δ'✝ : VLCtx
dk n k : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv✝ : FVarId
d : VLocalDecl
a✝ : LiftN Δ✝ Δ' 0 n✝ 0
A : VExpr
Γ' : List VExpr
ih : Ctx.LiftN n✝ 0 (VLCtx.toCtx Δ✝) Γ'
As : List VExpr
eq : List.length As = n✝
hΓ' : VLCtx.toCtx Δ' = As ++ VLCtx.toCtx Δ✝
⊢ Ctx.LiftN (n✝ + VLocalDecl.depth (VLocalDecl.vlam A)) 0 (VLCtx.toCtx Δ✝) (A :: (As ++ VLCtx.toCtx Δ✝))
Tactic:
exact .zero (A :: As) (eq ▸ rfl)
State after:
no goals

State before:
case cons_bvar
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : Ctx.LiftN n✝ k✝ (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ'✝)
⊢ Ctx.LiftN n✝ (k✝ + VLocalDecl.depth d) (VLCtx.toCtx ((none, d) :: Δ✝))
    (VLCtx.toCtx ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝))
Tactic:
match d with
| .vlet .. => exact ih
| .vlam A => exact .succ ih
State after:
no goals

State before:
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : Ctx.LiftN n✝ k✝ (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ'✝)
type✝ value✝ : VExpr
⊢ Ctx.LiftN n✝ (k✝ + VLocalDecl.depth (VLocalDecl.vlet type✝ value✝))
    (VLCtx.toCtx ((none, VLocalDecl.vlet type✝ value✝) :: Δ✝))
    (VLCtx.toCtx ((none, VLocalDecl.liftN (VLocalDecl.vlet type✝ value✝) n✝ k✝) :: Δ'✝))
Tactic:
exact ih
State after:
no goals

State before:
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : Ctx.LiftN n✝ k✝ (VLCtx.toCtx Δ✝) (VLCtx.toCtx Δ'✝)
A : VExpr
⊢ Ctx.LiftN n✝ (k✝ + VLocalDecl.depth (VLocalDecl.vlam A)) (VLCtx.toCtx ((none, VLocalDecl.vlam A) :: Δ✝))
    (VLCtx.toCtx ((none, VLocalDecl.liftN (VLocalDecl.vlam A) n✝ k✝) :: Δ'✝))
Tactic:
exact .succ ih
State after:
no goals