Theorem: shift_down_preservation (STLC.lean)

State before:
ctx : Ctx
t : Term
ty : Ty
h : ↥ctx ⊢ t ⋮ ty
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty
Tactic:
generalize hc : ↥ctx = ctx'
State after:
ctx : Ctx
t : Term
ty : Ty
h : ↥ctx ⊢ t ⋮ ty
ctx' : Ctx
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty

State before:
ctx : Ctx
t : Term
ty : Ty
h : ↥ctx ⊢ t ⋮ ty
ctx' : Ctx
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty
Tactic:
rw [hc] at h
State after:
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
h : ctx' ⊢ t ⋮ ty
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty

State before:
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
h : ctx' ⊢ t ⋮ ty
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty
Tactic:
induction h <;> (subst hc; try simp at *)
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.down 0 (Term.var x✝) ⋮ ty✝

case abs
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty₁✝ : Ty
t✝ : Term
ty₂✝ : Ty
a✝ : (↥↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ↥ctx = (↥↥ctx)[0 ↦ ty₁✝] → ctx ⊢ Term.shift Dir.down 0 t✝ ⋮ ty₂✝
⊢ ctx ⊢ Term.shift Dir.down 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.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 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.down 0 (Term.var x✝) ⋮ ty✝
Tactic:
case var h =>
  simp_all [Term.shift, Ctx.shift, Dir.move]
  split <;> try split at h <;> try contradiction
  exact .var h
State after:
no goals

State before:
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty₁✝ : Ty
t✝ : Term
ty₂✝ : Ty
a✝ : (↥↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ↥ctx = (↥↥ctx)[0 ↦ ty₁✝] → ctx ⊢ Term.shift Dir.down 0 t✝ ⋮ ty₂✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.abs ty₁✝ t✝) ⋮ Ty.arrow ty₁✝ ty₂✝
Tactic:
case abs => 
  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.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
hi₂ : ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝
Tactic:
case app hi₁ hi₂ => exact .app hi₁ hi₂
State after:
no goals

State before:
case app
ctx : Ctx
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✝¹ : ↥ctx = ctx✝ → ctx ⊢ Term.shift Dir.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ↥ctx = ctx✝ → ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
hc : ↥ctx = ctx✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝
Tactic:
subst hc
State after:
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 = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ↥ctx = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝

State before:
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 = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ↥ctx = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝
Tactic:
try simp at *
State after:
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.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝

State before:
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 = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ↥ctx = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝
Tactic:
simp at *
State after:
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.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 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.down 0 (Term.var x✝) ⋮ ty✝
Tactic:
simp_all [Term.shift, Ctx.shift, Dir.move]
State after:
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
h :
  (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    some ty✝
⊢ ctx ⊢ if x✝ < 0 then Term.var x✝ else Term.var (x✝ - 1) ⋮ ty✝

State before:
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
h :
  (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    some ty✝
⊢ ctx ⊢ if x✝ < 0 then Term.var x✝ else Term.var (x✝ - 1) ⋮ ty✝
Tactic:
split <;> try split at h <;> try contradiction
State after:
case inr.h_2
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝¹ x✝ : Nat
h✝ : ¬Nat.succ x✝ < 0
h : ctx x✝ = some ty✝
⊢ ctx ⊢ Term.var (Nat.succ x✝ - 1) ⋮ ty✝

State before:
case inr.h_2
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝¹ x✝ : Nat
h✝ : ¬Nat.succ x✝ < 0
h : ctx x✝ = some ty✝
⊢ ctx ⊢ Term.var (Nat.succ x✝ - 1) ⋮ ty✝
Tactic:
exact .var h
State after:
no goals

State before:
case inr
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
h :
  (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    some ty✝
h✝ : ¬x✝ < 0
⊢ ctx ⊢ Term.var (x✝ - 1) ⋮ ty✝
Tactic:
split at h <;> try contradiction
State after:
case inr.h_2
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝¹ x✝ : Nat
h✝ : ¬Nat.succ x✝ < 0
h : ctx x✝ = some ty✝
⊢ ctx ⊢ Term.var (Nat.succ x✝ - 1) ⋮ ty✝

State before:
case inr.h_1
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
h✝ : ¬0 < 0
h : none = some ty✝
⊢ ctx ⊢ Term.var (0 - 1) ⋮ ty✝
Tactic:
contradiction
State after:
no goals

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