Theorem: preservation (STLC.lean)

State before:
ctx : Ctx
t : Term
ty : Ty
t' : Term
ht : ctx ⊢ t ⋮ ty
he : t ⇒ t'
⊢ ctx ⊢ t' ⋮ ty
Tactic:
induction ht generalizing t' <;> cases he
State after:
case app.app₁
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝² : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝¹ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : ∀ {t' : Term}, t₁✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {t' : Term}, t₂✝ ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
t₁'✝ : Term
a✝ : t₁✝ ⇒ t₁'✝
⊢ ctx✝ ⊢ Term.app t₁'✝ t₂✝ ⋮ ty₂✝

case app.app₂
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝² : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : ∀ {t' : Term}, t₂✝ ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
t₂'✝ : Term
v₁✝ : Value
a✝¹ :
  ctx✝ ⊢
    match v₁✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁✝ ty₂✝
a_ih✝ :
  ∀ {t' : Term},
    (match v₁✝ with
        | Value.abs ty body => Term.abs ty body) ⇒
        t' →
      ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : t₂✝ ⇒ t₂'✝
⊢ ctx✝ ⊢
    Term.app
      (match v₁✝ with
      | Value.abs ty body => Term.abs ty body)
      t₂'✝ ⋮
    ty₂✝

case app.beta
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
a✝¹ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ :
  ctx✝ ⊢
    match v✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    ty₁✝
a_ih✝ :
  ∀ {t' : Term},
    (match v✝ with
        | Value.abs ty body => Term.abs ty body) ⇒
        t' →
      ctx✝ ⊢ t' ⋮ ty₁✝
⊢ ctx✝ ⊢
    Term.shift Dir.down 0
      t✝[0 ↦
        Term.shift Dir.up 0
          (match v✝ with
          | Value.abs ty body => Term.abs ty body)] ⋮
    ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
ht : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi : ∀ {t' : Term}, t₁✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {t' : Term}, t₂✝ ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
t₁'✝ : Term
he : t₁✝ ⇒ t₁'✝
⊢ ctx✝ ⊢ Term.app t₁'✝ t₂✝ ⋮ ty₂✝
Tactic:
case app.app₁ _ ht hi _ _ he => exact .app (hi he) ht
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi : ∀ {t' : Term}, t₂✝ ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
t₂'✝ : Term
v₁✝ : Value
ht :
  ctx✝ ⊢
    match v₁✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁✝ ty₂✝
a_ih✝ :
  ∀ {t' : Term},
    (match v₁✝ with
        | Value.abs ty body => Term.abs ty body) ⇒
        t' →
      ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
he : t₂✝ ⇒ t₂'✝
⊢ ctx✝ ⊢
    Term.app
      (match v₁✝ with
      | Value.abs ty body => Term.abs ty body)
      t₂'✝ ⋮
    ty₂✝
Tactic:
case app.app₂ hi _ _ ht _ he => exact .app ht (hi he)
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ :
  ctx✝ ⊢
    match v✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    ty₁✝
a_ih✝ :
  ∀ {t' : Term},
    (match v✝ with
        | Value.abs ty body => Term.abs ty body) ⇒
        t' →
      ctx✝ ⊢ t' ⋮ ty₁✝
⊢ ctx✝ ⊢
    Term.shift Dir.down 0
      t✝[0 ↦
        Term.shift Dir.up 0
          (match v✝ with
          | Value.abs ty body => Term.abs ty body)] ⋮
    ty₂✝
Tactic:
case app.beta ht₁ _ ht₂ _ => 
  simp at * 
  have ⟨_, h, hc⟩ := inversion_abs ht₁
  injection h with h₁ h₂
  subst h₁ h₂
  exact shift_down_preservation <| subst_preservation hc (shift_up_preservation ht₂)
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
ht : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi : ∀ {t' : Term}, t₁✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {t' : Term}, t₂✝ ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
t₁'✝ : Term
he : t₁✝ ⇒ t₁'✝
⊢ ctx✝ ⊢ Term.app t₁'✝ t₂✝ ⋮ ty₂✝
Tactic:
exact .app (hi he) ht
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi : ∀ {t' : Term}, t₂✝ ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
t₂'✝ : Term
v₁✝ : Value
ht :
  ctx✝ ⊢
    match v₁✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁✝ ty₂✝
a_ih✝ :
  ∀ {t' : Term},
    (match v₁✝ with
        | Value.abs ty body => Term.abs ty body) ⇒
        t' →
      ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
he : t₂✝ ⇒ t₂'✝
⊢ ctx✝ ⊢
    Term.app
      (match v₁✝ with
      | Value.abs ty body => Term.abs ty body)
      t₂'✝ ⋮
    ty₂✝
Tactic:
exact .app ht (hi he)
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ :
  ctx✝ ⊢
    match v✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    ty₁✝
a_ih✝ :
  ∀ {t' : Term},
    (match v✝ with
        | Value.abs ty body => Term.abs ty body) ⇒
        t' →
      ctx✝ ⊢ t' ⋮ ty₁✝
⊢ ctx✝ ⊢
    Term.shift Dir.down 0
      t✝[0 ↦
        Term.shift Dir.up 0
          (match v✝ with
          | Value.abs ty body => Term.abs ty body)] ⋮
    ty₂✝
Tactic:
simp at *
State after:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝
Tactic:
have ⟨_, h, hc⟩ := inversion_abs ht₁
State after:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
w✝ : Ty
h : Ty.arrow ty₁✝ ty₂✝ = Ty.arrow ty✝ w✝
hc : (↥ctx✝)[0 ↦ ty✝] ⊢ t✝ ⋮ w✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
w✝ : Ty
h : Ty.arrow ty₁✝ ty₂✝ = Ty.arrow ty✝ w✝
hc : (↥ctx✝)[0 ↦ ty✝] ⊢ t✝ ⋮ w✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝
Tactic:
injection h with h₁ h₂
State after:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
w✝ : Ty
hc : (↥ctx✝)[0 ↦ ty✝] ⊢ t✝ ⋮ w✝
h₁ : ty₁✝ = ty✝
h₂ : ty₂✝ = w✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
w✝ : Ty
hc : (↥ctx✝)[0 ↦ ty✝] ⊢ t✝ ⋮ w✝
h₁ : ty₁✝ = ty✝
h₂ : ty₂✝ = w✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝
Tactic:
subst h₁ h₂
State after:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ : Ty
t✝ : Term
v✝ : Value
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
ht₁ : ctx✝ ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {t' : Term}, Term.abs ty₁✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
hc : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ : Ty
t✝ : Term
v✝ : Value
ht₂ : ctx✝ ⊢ Term.abs v✝.1 v✝.2 ⋮ ty₁✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs v✝.1 v✝.2 ⇒ t' → ctx✝ ⊢ t' ⋮ ty₁✝
ht₁ : ctx✝ ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {t' : Term}, Term.abs ty₁✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
hc : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ ctx✝ ⊢ Term.shift Dir.down 0 t✝[0 ↦ Term.shift Dir.up 0 (Term.abs v✝.1 v✝.2)] ⋮ ty₂✝
Tactic:
exact shift_down_preservation <| subst_preservation hc (shift_up_preservation ht₂)
State after:
no goals