Theorem: weakening (STLC.lean)

State before:
ctx : Ctx
t : Term
ty : Ty
x : Nat
ty' : Ty
ht : ctx ⊢ t ⋮ ty
hx : ctx x = none
⊢ ctx[x ↦ ty'] ⊢ t ⋮ ty
Tactic:
induction ht generalizing x
State after:
case var
ctx : Ctx
t : Term
ty ty' : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.var x✝ ⋮ ty✝

case abs
ctx : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ∀ {x : Nat}, (↥ctx✝)[0 ↦ ty₁✝] x = none → (↥ctx✝)[0 ↦ ty₁✝][x ↦ ty'] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝

case app
ctx : Ctx
t : Term
ty ty' : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.app t₁✝ t₂✝ ⋮ ty₂✝

State before:
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
⊢ ctx[x ↦ ty'] ⊢ Term.var y ⋮ ty✝
Tactic:
case var ctx _ y hy => 
  refine .var (hy ▸ ctx.set_get_ne _ _ ?_)
  intro h
  injection (h ▸ hx) ▸ hy
State after:
no goals

State before:
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : ∀ {x : Nat}, (↥ctx)[0 ↦ ty₁✝] x = none → (↥ctx)[0 ↦ ty₁✝][x ↦ ty'] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
Tactic:
case abs ctx _ _ _ hi =>
  specialize hi <| (hx ▸ ctx.shift_succ x) ▸ (↥ctx).set_get_ne 0 (x + 1)
  rw [(↥ctx).set_ne_comm 0 (x + 1), ctx.shift_set_comm x] at hi
  exact .abs hi
State after:
no goals

State before:
ctx : Ctx
t : Term
ty ty' : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
hi₂ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.app t₁✝ t₂✝ ⋮ ty₂✝
Tactic:
case app hi₁ hi₂ => exact .app (hi₁ hx) (hi₂ hx)
State after:
no goals

State before:
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
⊢ ctx[x ↦ ty'] ⊢ Term.var y ⋮ ty✝
Tactic:
refine .var (hy ▸ ctx.set_get_ne _ _ ?_)
State after:
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
⊢ x ≠ y

State before:
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
⊢ x ≠ y
Tactic:
intro h
State after:
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
h : x = y
⊢ False

State before:
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
h : x = y
⊢ False
Tactic:
injection (h ▸ hx) ▸ hy
State after:
no goals

State before:
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : ∀ {x : Nat}, (↥ctx)[0 ↦ ty₁✝] x = none → (↥ctx)[0 ↦ ty₁✝][x ↦ ty'] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
Tactic:
specialize hi <| (hx ▸ ctx.shift_succ x) ▸ (↥ctx).set_get_ne 0 (x + 1)
State after:
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
hi : (↥ctx)[0 ↦ ty₁✝][x + 1 ↦ ty'] ⊢ t✝ ⋮ ty₂✝
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝

State before:
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
hi : (↥ctx)[0 ↦ ty₁✝][x + 1 ↦ ty'] ⊢ t✝ ⋮ ty₂✝
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
Tactic:
rw [(↥ctx).set_ne_comm 0 (x + 1), ctx.shift_set_comm x] at hi
State after:
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
hi : (↥ctx[x ↦ ty'])[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝

State before:
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
hi : (↥ctx[x ↦ ty'])[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
Tactic:
exact .abs hi
State after:
no goals

State before:
ctx : Ctx
t : Term
ty ty' : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
hi₂ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.app t₁✝ t₂✝ ⋮ ty₂✝
Tactic:
exact .app (hi₁ hx) (hi₂ hx)
State after:
no goals