Theorem: subst_preservation (STLC.lean)

State before:
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
ht : ctx[x ↦ ty'] ⊢ t ⋮ ty
hs : ctx ⊢ s ⋮ ty'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty
Tactic:
generalize hc : ctx[x ↦ ty'] = ctx'
State after:
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
ht : ctx[x ↦ ty'] ⊢ t ⋮ ty
hs : ctx ⊢ s ⋮ ty'
ctx' : Ctx
hc : ctx[x ↦ ty'] = ctx'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty

State before:
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
ht : ctx[x ↦ ty'] ⊢ t ⋮ ty
hs : ctx ⊢ s ⋮ ty'
ctx' : Ctx
hc : ctx[x ↦ ty'] = ctx'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty
Tactic:
rw [hc] at ht
State after:
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
hs : ctx ⊢ s ⋮ ty'
ctx' : Ctx
ht : ctx' ⊢ t ⋮ ty
hc : ctx[x ↦ ty'] = ctx'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty

State before:
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
hs : ctx ⊢ s ⋮ ty'
ctx' : Ctx
ht : ctx' ⊢ t ⋮ ty
hc : ctx[x ↦ ty'] = ctx'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty
Tactic:
induction ht generalizing ctx x s <;> (subst hc; try simp at *)
State after:
case var
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : ctx[x ↦ ty'] x✝ = some ty✝
⊢ ctx ⊢ (Term.var x✝)[x ↦ s] ⋮ ty✝

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

case app
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝¹ : ctx[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = ctx[x ↦ ty'] → ctx_1 ⊢ t₁✝[x_1 ↦ s] ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = ctx[x ↦ ty'] → ctx_1 ⊢ t₂✝[x_1 ↦ s] ⋮ ty₁✝
⊢ ctx ⊢ (Term.app t₁✝ t₂✝)[x ↦ s] ⋮ ty₂✝

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : ctx[x ↦ ty'] x✝ = some ty✝
⊢ ctx ⊢ (Term.var x✝)[x ↦ s] ⋮ ty✝
Tactic:
case var hc =>
  simp [Term.subst]
  split <;> simp [Ctx.set] at hc
  case inl h => simp_all
  case inr h => exact .var <| by simp_all
State after:
no goals

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

State before:
case app
ty' : Ty
t : Term
ty : Ty
ctx' 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 : Ctx} {s : Term}, (ctx ⊢ s ⋮ ty') → ctx[x ↦ ty'] = ctx✝ → ctx ⊢ t₁✝[x ↦ s] ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {x : Nat} {ctx : Ctx} {s : Term}, (ctx ⊢ s ⋮ ty') → ctx[x ↦ ty'] = ctx✝ → ctx ⊢ t₂✝[x ↦ s] ⋮ ty₁✝
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : ctx[x ↦ ty'] = ctx✝
⊢ ctx ⊢ (Term.app t₁✝ t₂✝)[x ↦ s] ⋮ ty₂✝
Tactic:
subst hc
State after:
case app
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝¹ : ctx[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = ctx[x ↦ ty'] → ctx_1 ⊢ t₁✝[x_1 ↦ s] ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = ctx[x ↦ ty'] → ctx_1 ⊢ t₂✝[x_1 ↦ s] ⋮ ty₁✝
⊢ ctx ⊢ (Term.app t₁✝ t₂✝)[x ↦ s] ⋮ ty₂✝

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : ctx[x ↦ ty'] x✝ = some ty✝
⊢ ctx ⊢ (Term.var x✝)[x ↦ s] ⋮ ty✝
Tactic:
simp [Term.subst]
State after:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : ctx[x ↦ ty'] x✝ = some ty✝
⊢ ctx ⊢ if x✝ = x then s else Term.var x✝ ⋮ ty✝

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : ctx[x ↦ ty'] x✝ = some ty✝
⊢ ctx ⊢ if x✝ = x then s else Term.var x✝ ⋮ ty✝
Tactic:
split <;> simp [Ctx.set] at hc
State after:
case inl
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h✝ : x✝ = x
⊢ ctx ⊢ s ⋮ ty✝

case inr
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h✝ : ¬x✝ = x
⊢ ctx ⊢ Term.var x✝ ⋮ ty✝

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h : x✝ = x
⊢ ctx ⊢ s ⋮ ty✝
Tactic:
case inl h => simp_all
State after:
no goals

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h : ¬x✝ = x
⊢ ctx ⊢ Term.var x✝ ⋮ ty✝
Tactic:
case inr h => exact .var <| by simp_all
State after:
no goals

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h : x✝ = x
⊢ ctx ⊢ s ⋮ ty✝
Tactic:
simp_all
State after:
no goals

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h : ¬x✝ = x
⊢ ctx ⊢ Term.var x✝ ⋮ ty✝
Tactic:
exact .var <| by simp_all
State after:
no goals

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h : ¬x✝ = x
⊢ ctx x✝ = some ty✝
Tactic:
simp_all
State after:
no goals

State before:
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty₁ : Ty
t✝ : Term
ty₂✝ : Ty
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : (↥ctx[x ↦ ty'])[0 ↦ ty₁] ⊢ t✝ ⋮ ty₂✝
hi :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁] → ctx_1 ⊢ t✝[x_1 ↦ s] ⋮ ty₂✝
⊢ ctx ⊢ (Term.abs ty₁ t✝)[x ↦ s] ⋮ Ty.arrow ty₁ ty₂✝
Tactic:
refine Types.abs <| hi ?_ ?_
State after:
case refine_1
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty₁ : Ty
t✝ : Term
ty₂✝ : Ty
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : (↥ctx[x ↦ ty'])[0 ↦ ty₁] ⊢ t✝ ⋮ ty₂✝
hi :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁] → ctx_1 ⊢ t✝[x_1 ↦ s] ⋮ ty₂✝
⊢ (↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 0 s ⋮ ty'

case refine_2
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty₁ : Ty
t✝ : Term
ty₂✝ : Ty
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : (↥ctx[x ↦ ty'])[0 ↦ ty₁] ⊢ t✝ ⋮ ty₂✝
hi :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁] → ctx_1 ⊢ t✝[x_1 ↦ s] ⋮ ty₂✝
⊢ (↥ctx)[0 ↦ ty₁][x + 1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁]

State before:
case refine_1
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty₁ : Ty
t✝ : Term
ty₂✝ : Ty
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : (↥ctx[x ↦ ty'])[0 ↦ ty₁] ⊢ t✝ ⋮ ty₂✝
hi :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁] → ctx_1 ⊢ t✝[x_1 ↦ s] ⋮ ty₂✝
⊢ (↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 0 s ⋮ ty'
Tactic:
exact weakening (shift_up_preservation hs) Ctx.shift_zero
State after:
no goals

State before:
case refine_2
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty₁ : Ty
t✝ : Term
ty₂✝ : Ty
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : (↥ctx[x ↦ ty'])[0 ↦ ty₁] ⊢ t✝ ⋮ ty₂✝
hi :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁] → ctx_1 ⊢ t✝[x_1 ↦ s] ⋮ ty₂✝
⊢ (↥ctx)[0 ↦ ty₁][x + 1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁]
Tactic:
rw [←ctx.shift_set_comm, (↥ctx).set_ne_comm 0 (x + 1)]
State after:
no goals

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