Theorem: Lean4Lean.TrExpr.inScope (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' : VExpr
H : TrExpr env Us Δ e e'
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ) e (VLCtx.bvars Δ)
Tactic:
induction H with
| @bvar e A Δ i h1 =>
  simp [InScope]
  induction Δ generalizing i e A with
  | nil => cases h1
  | cons d Δ ih =>
    match d, i with
    | (none, _), 0 => exact Nat.succ_pos _
    | (none, _), _ + 1 =>
      simp [VLCtx.find?, VLCtx.next, bind] at h1
      obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
      exact Nat.succ_lt_succ (ih h1)
    | (some _, _), _ =>
      simp [VLCtx.find?, VLCtx.next, bind] at h1
      obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
      exact ih h1
| fvar h1 => exact VLCtx.find?_eq_some.1 ⟨_, h1⟩
| sort | const | lit | mdata => trivial
| app _ _ _ _ ih1 ih2
| lam _ _ _ ih1 ih2
| forallE _ _ _ _ ih1 ih2 => exact ⟨ih1, ih2⟩
| letE _ _ _ _ ih1 ih2 ih3 => exact ⟨ih1, ih2, ih3⟩
| proj _ _ ih => exact ih
State after:
no goals

State before:
case bvar
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' e A : VExpr
Δ : VLCtx
i : Nat
h1 : VLCtx.find? Δ (Sum.inl i) = some (e, A)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.bvar i) (VLCtx.bvars Δ)
Tactic:
simp [InScope]
State after:
case bvar
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' e A : VExpr
Δ : VLCtx
i : Nat
h1 : VLCtx.find? Δ (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars Δ

State before:
case bvar
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' e A : VExpr
Δ : VLCtx
i : Nat
h1 : VLCtx.find? Δ (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars Δ
Tactic:
induction Δ generalizing i e A with
| nil => cases h1
| cons d Δ ih =>
  match d, i with
  | (none, _), 0 => exact Nat.succ_pos _
  | (none, _), _ + 1 =>
    simp [VLCtx.find?, VLCtx.next, bind] at h1
    obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
    exact Nat.succ_lt_succ (ih h1)
  | (some _, _), _ =>
    simp [VLCtx.find?, VLCtx.next, bind] at h1
    obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
    exact ih h1
State after:
no goals

State before:
case bvar.nil
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e✝ : Expr
e' e A : VExpr
i : Nat
h1 : VLCtx.find? [] (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars []
Tactic:
cases h1
State after:
no goals

State before:
case bvar.cons
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
h1 : VLCtx.find? (d :: Δ) (Sum.inl i) = some (e, A)
⊢ i < VLCtx.bvars (d :: Δ)
Tactic:
match d, i with
| (none, _), 0 => exact Nat.succ_pos _
| (none, _), _ + 1 =>
  simp [VLCtx.find?, VLCtx.next, bind] at h1
  obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
  exact Nat.succ_lt_succ (ih h1)
| (some _, _), _ =>
  simp [VLCtx.find?, VLCtx.next, bind] at h1
  obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
  exact ih h1
State after:
no goals

State before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
h1 : VLCtx.find? ((none, snd✝) :: Δ) (Sum.inl 0) = some (e, A)
⊢ 0 < VLCtx.bvars ((none, snd✝) :: Δ)
Tactic:
exact Nat.succ_pos _
State after:
no goals

State before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
n✝ : Nat
h1 : VLCtx.find? ((none, snd✝) :: Δ) (Sum.inl (n✝ + 1)) = some (e, A)
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝) :: Δ)
Tactic:
simp [VLCtx.find?, VLCtx.next, bind] at h1
State after:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
n✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl n✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝) :: Δ)

State before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
snd✝ : VLocalDecl
n✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl n✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝) :: Δ)
Tactic:
obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
State after:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
snd✝¹ : VLocalDecl
n✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl n✝) = some (fst✝, snd✝)
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝¹) :: Δ)

State before:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
snd✝¹ : VLocalDecl
n✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl n✝) = some (fst✝, snd✝)
⊢ n✝ + 1 < VLCtx.bvars ((none, snd✝¹) :: Δ)
Tactic:
exact Nat.succ_lt_succ (ih h1)
State after:
no goals

State before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
val✝ : FVarId
snd✝ : VLocalDecl
x✝ : Nat
h1 : VLCtx.find? ((some val✝, snd✝) :: Δ) (Sum.inl x✝) = some (e, A)
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝) :: Δ)
Tactic:
simp [VLCtx.find?, VLCtx.next, bind] at h1
State after:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
val✝ : FVarId
snd✝ : VLocalDecl
x✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl x✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝) :: Δ)

State before:
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e✝ : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
e A : VExpr
i : Nat
val✝ : FVarId
snd✝ : VLocalDecl
x✝ : Nat
h1 :
  ∃ a,
    VLCtx.find? Δ (Sum.inl x✝) = some a ∧
      VExpr.liftN (VLocalDecl.depth snd✝) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth snd✝) a.snd = A
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝) :: Δ)
Tactic:
obtain ⟨⟨_, _⟩, h1, rfl, rfl⟩ := h1
State after:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
val✝ : FVarId
snd✝¹ : VLocalDecl
x✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl x✝) = some (fst✝, snd✝)
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝¹) :: Δ)

State before:
case intro.mk.intro.intro
env : VEnv
henv : Ordered env
Us : List Name
Δ✝ : VLCtx
e : Expr
e' : VExpr
d : Option FVarId × VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ih : ∀ {e A : VExpr} {i : Nat}, VLCtx.find? Δ (Sum.inl i) = some (e, A) → i < VLCtx.bvars Δ
i : Nat
val✝ : FVarId
snd✝¹ : VLocalDecl
x✝ : Nat
fst✝ snd✝ : VExpr
h1 : VLCtx.find? Δ (Sum.inl x✝) = some (fst✝, snd✝)
⊢ x✝ < VLCtx.bvars ((some val✝, snd✝¹) :: Δ)
Tactic:
exact ih h1
State after:
no goals

State before:
case fvar
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' e✝ A✝ : VExpr
Δ✝ : VLCtx
fv✝ : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv✝) = some (e✝, A✝)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.fvar fv✝) (VLCtx.bvars Δ✝)
Tactic:
exact VLCtx.find?_eq_some.1 ⟨_, h1⟩
State after:
no goals

State before:
case mdata
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
a_ih✝ : InScope (fun x => x ∈ VLCtx.fvars Δ✝) e✝ (VLCtx.bvars Δ✝)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.mdata d✝ e✝) (VLCtx.bvars Δ✝)
Tactic:
trivial
State after:
no goals

State before:
case forallE
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
a✝³ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
a✝² : 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 : InScope (fun x => x ∈ VLCtx.fvars Δ✝) ty✝ (VLCtx.bvars Δ✝)
ih2 :
  InScope (fun x => x ∈ VLCtx.fvars ((none, VLocalDecl.vlam ty'✝) :: Δ✝)) body✝
    (VLCtx.bvars ((none, VLocalDecl.vlam ty'✝) :: Δ✝))
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.forallE name✝ ty✝ body✝ bi✝) (VLCtx.bvars Δ✝)
Tactic:
exact ⟨ih1, ih2⟩
State after:
no goals

State before:
case letE
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
a✝³ : 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 : InScope (fun x => x ∈ VLCtx.fvars Δ✝) ty✝ (VLCtx.bvars Δ✝)
ih2 : InScope (fun x => x ∈ VLCtx.fvars Δ✝) val✝ (VLCtx.bvars Δ✝)
ih3 :
  InScope (fun x => x ∈ VLCtx.fvars ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝)) body✝
    (VLCtx.bvars ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝))
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.letE name✝ ty✝ val✝ body✝ bi✝) (VLCtx.bvars Δ✝)
Tactic:
exact ⟨ih1, ih2, ih3⟩
State after:
no goals

State before:
case proj
env : VEnv
henv : Ordered env
Us : List Name
Δ : VLCtx
e : Expr
e' : VExpr
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
a✝¹ : TrExpr env Us Δ✝ e✝ e'✝
a✝ : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih : InScope (fun x => x ∈ VLCtx.fvars Δ✝) e✝ (VLCtx.bvars Δ✝)
⊢ InScope (fun x => x ∈ VLCtx.fvars Δ✝) (Expr.proj s✝ i✝ e✝) (VLCtx.bvars Δ✝)
Tactic:
exact ih
State after:
no goals