Theorem: shift_up_preservation (STLC.lean)

State before:
ctx : Ctx
t : Term
ty : Ty
h : ctx ⊢ t ⋮ ty
⊢ ↥ctx ⊢ Term.shift Dir.up 0 t ⋮ ty
Tactic:
induction h
State after:
case var
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.var x✝) ⋮ ty✝

case abs
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ↥(↥ctx✝)[0 ↦ ty₁✝] ⊢ Term.shift Dir.up 0 t✝ ⋮ ty₂✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.abs ty₁✝ t✝) ⋮ Ty.arrow ty₁✝ ty₂✝

case 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✝¹ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₂✝ ⋮ ty₁✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
h : ctx✝ x✝ = some ty✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.var x✝) ⋮ ty✝
Tactic:
case var h => exact .var h
State after:
no goals

State before:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : ↥(↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ ↥ctx ⊢ Term.shift Dir.up 0 (Term.abs ty₁ t) ⋮ Ty.arrow ty₁ ty₂
Tactic:
case abs ty₁ ctx t ty₂ ht hi =>
  refine .abs ?_
  rw [←Ctx.shift_set_comm] at hi
  simp at *
  sorry
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₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
hi₂ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₂✝ ⋮ ty₁✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝
Tactic:
case app hi₁ hi₂ => exact .app hi₁ hi₂
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
h : ctx✝ x✝ = some ty✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.var x✝) ⋮ ty✝
Tactic:
exact .var h
State after:
no goals

State before:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : ↥(↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ ↥ctx ⊢ Term.shift Dir.up 0 (Term.abs ty₁ t) ⋮ Ty.arrow ty₁ ty₂
Tactic:
refine .abs ?_
State after:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : ↥(↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up (0 + 1) t ⋮ ty₂

State before:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : ↥(↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up (0 + 1) t ⋮ ty₂
Tactic:
rw [←Ctx.shift_set_comm] at hi
State after:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : (↥↥ctx)[0 + 1 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up (0 + 1) t ⋮ ty₂

State before:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : (↥↥ctx)[0 + 1 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up (0 + 1) t ⋮ ty₂
Tactic:
simp at *
State after:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : (↥↥ctx)[1 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 1 t ⋮ ty₂

State before:
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : (↥↥ctx)[1 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 1 t ⋮ ty₂
Tactic:
sorry
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₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
hi₂ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₂✝ ⋮ ty₁✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝
Tactic:
exact .app hi₁ hi₂
State after:
no goals