internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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)
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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
Proof 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) :: Δ'))
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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
Proof 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) :: Δ'))
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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Γ']
Proof 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 Δ✝))
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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)
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.toCtx
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.wf
Proof state before:
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
W : LiftN Δ Δ' dk n k
hΔ' : WF env U Δ'
⊢ WF env U Δ
Tactic:
induction W with
| refl => exact hΔ'
| skip_fvar _ _ _ ih => exact ih hΔ'.1
| cons_bvar _ W ih =>
  let ⟨hΔ', _, h2⟩ := hΔ'
  exact ⟨ih hΔ', nofun, (VLocalDecl.weakN_iff henv hΔ'.toCtx W.toCtx).1 h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.wf
Proof state before:
case refl
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ : VLCtx
hΔ' : WF env U Δ✝
⊢ WF env U Δ✝
Tactic:
exact hΔ'
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.wf
Proof state before:
case skip_fvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
n✝ : Nat
fv✝ : FVarId
d✝ : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ 0 n✝ 0
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ' : WF env U ((some fv✝, d✝) :: Δ'✝)
⊢ WF env U Δ✝
Tactic:
exact ih hΔ'.1
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.wf
Proof state before:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ' : WF env U ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
⊢ WF env U ((none, d✝) :: Δ✝)
Tactic:
let ⟨hΔ', _, h2⟩ := hΔ'
Proof state after:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ'✝ : WF env U ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
hΔ' : WF env U Δ'✝
left✝ : ∀ (fv : FVarId), none = some fv → ¬fv ∈ fvars Δ'✝
h2 : VLocalDecl.WF env U (VLCtx.toCtx Δ'✝) (VLocalDecl.liftN d✝ n✝ k✝)
⊢ WF env U ((none, d✝) :: Δ✝)
Theorem: Lean4Lean.VLCtx.LiftN.wf
Proof state before:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k U : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : WF env U Δ'✝ → WF env U Δ✝
hΔ'✝ : WF env U ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
hΔ' : WF env U Δ'✝
left✝ : ∀ (fv : FVarId), none = some fv → ¬fv ∈ fvars Δ'✝
h2 : VLocalDecl.WF env U (VLCtx.toCtx Δ'✝) (VLocalDecl.liftN d✝ n✝ k✝)
⊢ WF env U ((none, d✝) :: Δ✝)
Tactic:
exact ⟨ih hΔ', nofun, (VLocalDecl.weakN_iff henv hΔ'.toCtx W.toCtx).1 h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.fvars_suffix
Proof state before:
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
W : LiftN Δ Δ' dk n k
⊢ fvars Δ <:+ fvars Δ'
Tactic:
induction W with
| refl => exact List.suffix_refl _
| skip_fvar _ _ _ ih => exact ih.trans (List.suffix_cons ..)
| cons_bvar _ _ ih => exact ih
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.fvars_suffix
Proof state before:
case refl
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ : VLCtx
⊢ fvars Δ✝ <:+ fvars Δ✝
Tactic:
exact List.suffix_refl _
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.fvars_suffix
Proof state before:
case skip_fvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ Δ'✝ : VLCtx
n✝ : Nat
fv✝ : FVarId
d✝ : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ 0 n✝ 0
ih : fvars Δ✝ <:+ fvars Δ'✝
⊢ fvars Δ✝ <:+ fvars ((some fv✝, d✝) :: Δ'✝)
Tactic:
exact ih.trans (List.suffix_cons ..)
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.fvars_suffix
Proof state before:
case cons_bvar
env : VEnv
henv : Ordered env
Δ Δ' : VLCtx
dk n k : Nat
Δ✝ Δ'✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
a✝ : LiftN Δ✝ Δ'✝ dk✝ n✝ k✝
ih : fvars Δ✝ <:+ fvars Δ'✝
⊢ fvars ((none, d✝) :: Δ✝) <:+ fvars ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ'✝)
Tactic:
exact ih
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case refl
Δ Δ' : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ : VLCtx
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U Δ✝
H : VLCtx.find? Δ✝ v = some (e, A)
⊢ VLCtx.find? Δ✝ v = some (VExpr.liftN 0 e, VExpr.liftN 0 A)
Tactic:
simp [H]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case skip_fvar
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
H : VLCtx.find? Δ✝ v = some (e, A)
⊢ VLCtx.find? ((some fv', d✝) :: Δ') v =
    some (VExpr.liftN (n✝ + VLocalDecl.depth d✝) e, VExpr.liftN (n✝ + VLocalDecl.depth d✝) A)
Tactic:
simp [VLCtx.find?]
Proof state after:
case skip_fvar
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
H : VLCtx.find? Δ✝ v = some (e, A)
⊢ (match next (some fv') v with
    | none => some (VLocalDecl.value d✝, VLocalDecl.type d✝)
    | some v =>
      Option.bind (VLCtx.find? Δ' v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d✝) __discr.fst, VExpr.liftN (VLocalDecl.depth d✝) __discr.snd)) =
    some (VExpr.liftN (n✝ + VLocalDecl.depth d✝) e, VExpr.liftN (n✝ + VLocalDecl.depth d✝) A)
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case skip_fvar.inl
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
val✝ : Nat
H : VLCtx.find? Δ✝ (Sum.inl val✝) = some (e, A)
⊢ ∃ a,
    VLCtx.find? Δ' (Sum.inl val✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth d✝) a.fst = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
        VExpr.liftN (VLocalDecl.depth d✝) a.snd = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
exact ⟨_, ih hΔ'.1 H, by simp [VExpr.liftN_liftN]⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
val✝ : Nat
H : VLCtx.find? Δ✝ (Sum.inl val✝) = some (e, A)
⊢ VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).fst =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).snd =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
simp [VExpr.liftN_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case skip_fvar.inr
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
⊢ (match if (fv' == fv) = true then none else some (Sum.inr fv) with
    | none => some (VLocalDecl.value d✝, VLocalDecl.type d✝)
    | some v =>
      Option.bind (VLCtx.find? Δ' v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d✝) __discr.fst, VExpr.liftN (VLocalDecl.depth d✝) __discr.snd)) =
    some (VExpr.liftN (n✝ + VLocalDecl.depth d✝) e, VExpr.liftN (n✝ + VLocalDecl.depth d✝) A)
Tactic:
cases eq : fv' == fv <;> simp
Proof state after:
case skip_fvar.inr.false
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = false
⊢ ∃ a,
    VLCtx.find? Δ' (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth d✝) a.fst = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
        VExpr.liftN (VLocalDecl.depth d✝) a.snd = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A

case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ VLocalDecl.value d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VLocalDecl.type d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case skip_fvar.inr.false
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = false
⊢ ∃ a,
    VLCtx.find? Δ' (Sum.inr fv) = some a ∧
      VExpr.liftN (VLocalDecl.depth d✝) a.fst = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
        VExpr.liftN (VLocalDecl.depth d✝) a.snd = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
exact ⟨_, ih hΔ'.1 H, by simp [VExpr.liftN_liftN]⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = false
⊢ VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).fst =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VExpr.liftN (VLocalDecl.depth d✝) (VExpr.liftN n✝ e, VExpr.liftN n✝ A).snd =
      VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
simp [VExpr.liftN_liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ VLocalDecl.value d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) e ∧
    VLocalDecl.type d✝ = VExpr.liftN (n✝ + VLocalDecl.depth d✝) A
Tactic:
refine ((List.pairwise_cons.1 hΔ'.fvars_nodup).1 fv' ?_ rfl).elim
Proof state after:
case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ fv' ∈ List.filterMap (fun x => x.fst) Δ'
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case skip_fvar.inr.true
Δ Δ'✝ : VLCtx
dk n k : Nat
env : VEnv
U : Nat
Δ✝ Δ' : VLCtx
n✝ : Nat
fv' : FVarId
d✝ : VLocalDecl
W : LiftN Δ✝ Δ' 0 n✝ 0
ih :
  ∀ {v : Nat ⊕ FVarId} {e A : VExpr},
    WF env U Δ' → VLCtx.find? Δ✝ v = some (e, A) → VLCtx.find? Δ' v = some (VExpr.liftN n✝ e, VExpr.liftN n✝ A)
e A : VExpr
hΔ' : WF env U ((some fv', d✝) :: Δ')
fv : FVarId
H : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
eq : (fv' == fv) = true
⊢ fv' ∈ List.filterMap (fun x => x.fst) Δ'
Tactic:
exact W.fvars_suffix.subset ((beq_iff_eq ..).1 eq ▸ find?_eq_some.1 ⟨_, H⟩)
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar
Δ Δ' : 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✝)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
H : VLCtx.find? ((none, d) :: Δ✝) v = some (e, A)
⊢ VLCtx.find? ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝) v =
    some (VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d), VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d))
Tactic:
simp [VLCtx.find?] at H ⊢
Proof state after:
case cons_bvar
Δ Δ' : 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✝)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
H :
  (match next none v with
    | none => some (VLocalDecl.value d, VLocalDecl.type d)
    | some v =>
      Option.bind (VLCtx.find? Δ✝ v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd)) =
    some (e, A)
⊢ (match next none v with
    | none => some (VLocalDecl.value (VLocalDecl.liftN d n✝ k✝), VLocalDecl.type (VLocalDecl.liftN d n✝ k✝))
    | some v =>
      Option.bind (VLCtx.find? Δ'✝ v) fun __discr =>
        some
          (VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.fst,
            VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.snd)) =
    some (VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d), VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d))
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar
Δ Δ' : 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✝)
v : Nat ⊕ FVarId
e A : VExpr
hΔ' : WF env U ((none, VLocalDecl.liftN d n✝ k✝) :: Δ'✝)
H :
  (match next none v with
    | none => some (VLocalDecl.value d, VLocalDecl.type d)
    | some v =>
      Option.bind (VLCtx.find? Δ✝ v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd)) =
    some (e, A)
⊢ (match next none v with
    | none => some (VLocalDecl.value (VLocalDecl.liftN d n✝ k✝), VLocalDecl.type (VLocalDecl.liftN d n✝ k✝))
    | some v =>
      Option.bind (VLCtx.find? Δ'✝ v) fun __discr =>
        some
          (VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.fst,
            VExpr.liftN (VLocalDecl.depth (VLocalDecl.liftN d n✝ k✝)) __discr.snd)) =
    some (VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d), VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d))
Tactic:
obtain ⟨_|i⟩ | fv := v <;> simp [VLCtx.next, bind] at H ⊢ <;>
  [(obtain ⟨rfl, rfl⟩ := H);
   (obtain ⟨⟨e, A⟩, H, rfl, rfl⟩ := H
    refine ⟨_, ih (v := .inl i) hΔ'.1 H, ?_⟩);
   (obtain ⟨⟨e, A⟩, H, rfl, rfl⟩ := H
    refine ⟨_, ih (v := .inr fv) hΔ'.1 H, ?_⟩)] <;>
  open VLocalDecl in
  cases d <;> simp [VExpr.lift_liftN', liftN, value, type, depth, VExpr.liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar.inl.zero
Δ Δ' : 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✝) :: Δ'✝)
H : VLocalDecl.value d = e ∧ VLocalDecl.type d = A
⊢ VLocalDecl.value (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ e (k✝ + VLocalDecl.depth d) ∧
    VLocalDecl.type (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ A (k✝ + VLocalDecl.depth d)
Tactic:
obtain ⟨rfl, rfl⟩ := H
Proof state after:
case cons_bvar.inl.zero.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✝) :: Δ'✝)
⊢ VLocalDecl.value (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ (VLocalDecl.value d) (k✝ + VLocalDecl.depth d) ∧
    VLocalDecl.type (VLocalDecl.liftN d n✝ k✝) = VExpr.liftN n✝ (VLocalDecl.type d) (k✝ + VLocalDecl.depth d)
Theorem: Lean4Lean.VLCtx.LiftN.find?
Proof state before:
case cons_bvar.inl.succ
Δ Δ' : 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✝) :: Δ'✝)
i : Nat
H :
  ∃ a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth d) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) a.snd = A
⊢ ∃ a,
    VLCtx.find? Δ'✝ (Sum.inl i) = 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.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)