internlm/Lean-Github huggingface dataset:
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨_, h₁⟩ := h₁
Proof state after:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
w✝ : Value
h₁ : t₁✝ = Term.abs w✝.1 w✝.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
w✝ : Value
h₁ : t₁✝ = Term.abs w✝.1 w✝.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨_, h₂⟩ := h₂
Proof state after:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
h₁ : t₁✝ = Term.abs w✝¹.1 w✝¹.2
w✝ : Term
h₂ : t₂✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
h₁ : t₁✝ = Term.abs w✝¹.1 w✝¹.2
w✝ : Term
h₂ : t₂✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
subst h₁
Proof state after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
t₂✝ : Term
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
w✝ : Term
h₂ : t₂✝ ⇒ w✝
ht₁ : ∅ ⊢ Term.abs w✝¹.1 w✝¹.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs w✝¹.1 w✝¹.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs w✝¹.1 w✝¹.2) t₂✝ ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
t₂✝ : Term
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
w✝ : Term
h₂ : t₂✝ ⇒ w✝
ht₁ : ∅ ⊢ Term.abs w✝¹.1 w✝¹.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs w✝¹.1 w✝¹.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs w✝¹.1 w✝¹.2) t₂✝ ⇒ t'
Tactic:
exact ⟨_, .app₂ _ h₂⟩
Proof state after:
no goals
Theorem: Ctx.set_get_ne
Proof state before:
ty : Ty
ctx : Ctx
x y : Nat
h : autoParam (x ≠ y) _auto✝
⊢ ctx[x ↦ ty] y = ctx y
Tactic:
simp [set, h.symm]
Proof state after:
no goals
Theorem: Ctx.set_ne_comm
Proof state before:
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
⊢ ctx[x₁ ↦ ty₁][x₂ ↦ ty₂] = ctx[x₂ ↦ ty₂][x₁ ↦ ty₁]
Tactic:
funext
Proof state after:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ ctx[x₁ ↦ ty₁][x₂ ↦ ty₂] x✝ = ctx[x₂ ↦ ty₂][x₁ ↦ ty₁] x✝
Theorem: Ctx.set_ne_comm
Proof state before:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ ctx[x₁ ↦ ty₁][x₂ ↦ ty₂] x✝ = ctx[x₂ ↦ ty₂][x₁ ↦ ty₁] x✝
Tactic:
simp [set]
Proof state after:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ (if x✝ = x₂ then some ty₂ else if x✝ = x₁ then some ty₁ else ctx x✝) =
    if x✝ = x₁ then some ty₁ else if x✝ = x₂ then some ty₂ else ctx x✝
Theorem: Ctx.set_ne_comm
Proof state before:
case h
ty₂ ty₁ : Ty
ctx : Ctx
x₁ x₂ : Nat
h : autoParam (x₁ ≠ x₂) _auto✝
x✝ : Nat
⊢ (if x✝ = x₂ then some ty₂ else if x✝ = x₁ then some ty₁ else ctx x✝) =
    if x✝ = x₁ then some ty₁ else if x✝ = x₂ then some ty₂ else ctx x✝
Tactic:
split <;> split <;> simp_all
Proof state after:
no goals
Theorem: Ctx.shift_set_comm
Proof state before:
ty : Ty
ctx : Ctx
x : Nat
⊢ (↥ctx)[x + 1 ↦ ty] = ↥ctx[x ↦ ty]
Tactic:
funext
Proof state after:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (↥ctx)[x + 1 ↦ ty] x✝ = ↥ctx[x ↦ ty] x✝
Theorem: Ctx.shift_set_comm
Proof state before:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (↥ctx)[x + 1 ↦ ty] x✝ = ↥ctx[x ↦ ty] x✝
Tactic:
simp [shift, set]
Proof state after:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (if x✝ = x + 1 then some ty
    else
      match x✝ with
      | 0 => none
      | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Theorem: Ctx.shift_set_comm
Proof state before:
case h
ty : Ty
ctx : Ctx
x x✝ : Nat
⊢ (if x✝ = x + 1 then some ty
    else
      match x✝ with
      | 0 => none
      | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Tactic:
split
Proof state after:
case h.inl
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : x✝ = x + 1
⊢ some ty =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1

case h.inr
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : ¬x✝ = x + 1
⊢ (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Theorem: Ctx.shift_set_comm
Proof state before:
case h.inl
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : x✝ = x + 1
⊢ some ty =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Tactic:
simp [*]
Proof state after:
no goals
Theorem: Ctx.shift_set_comm
Proof state before:
case h.inr
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : ¬x✝ = x + 1
⊢ (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: weakening
Proof 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
Proof 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₂✝
Theorem: weakening
Proof 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
Proof state after:
no goals
Theorem: weakening
Proof 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
Proof state after:
no goals
Theorem: weakening
Proof 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)
Proof state after:
no goals
Theorem: weakening
Proof 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 _ _ ?_)
Proof 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
Theorem: weakening
Proof 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
Proof 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
Theorem: weakening
Proof 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
Proof state after:
no goals
Theorem: weakening
Proof 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)
Proof 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₂✝
Theorem: weakening
Proof 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
Proof 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₂✝
Theorem: weakening
Proof 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
Proof state after:
no goals
Theorem: weakening
Proof 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)
Proof state after:
no goals
Theorem: shift_up_preservation
Proof state before:
ctx : Ctx
t : Term
ty : Ty
h : ctx ⊢ t ⋮ ty
⊢ ↥ctx ⊢ Term.shift Dir.up 0 t ⋮ ty
Tactic:
induction h
Proof 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₂✝
Theorem: shift_up_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_up_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_up_preservation
Proof 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₂
Proof state after:
no goals
Theorem: shift_up_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_up_preservation
Proof 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 ?_
Proof 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₂
Theorem: shift_up_preservation
Proof 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
Proof 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₂
Theorem: shift_up_preservation
Proof 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 *
Proof 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₂
Theorem: shift_up_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_up_preservation
Proof 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₂
Proof state after:
no goals
Theorem: shift_down_preservation
Proof 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'
Proof 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
Theorem: shift_down_preservation
Proof 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
Proof 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
Theorem: shift_down_preservation
Proof 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 *)
Proof 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₂✝
Theorem: shift_down_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_down_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_down_preservation
Proof 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₂
Proof state after:
no goals
Theorem: shift_down_preservation
Proof 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
Proof 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₂✝
Theorem: shift_down_preservation
Proof 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 *
Proof 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₂✝
Theorem: shift_down_preservation
Proof 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 *
Proof 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₂✝
Theorem: shift_down_preservation
Proof 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]
Proof 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✝
Theorem: shift_down_preservation
Proof 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
Proof 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✝
Theorem: shift_down_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_down_preservation
Proof 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
Proof 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✝
Theorem: shift_down_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_down_preservation
Proof 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
Proof state after:
no goals
Theorem: shift_down_preservation
Proof 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₂
Proof state after:
no goals
Theorem: subst_preservation
Proof 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'
Proof 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
Theorem: subst_preservation
Proof 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
Proof 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