internlm/Lean-Github huggingface dataset:
Theorem: subst_preservation
Proof 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 *)
Proof 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₂✝
Theorem: subst_preservation
Proof 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
Proof state after:
no goals
Theorem: subst_preservation
Proof 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)
Proof state after:
no goals
Theorem: subst_preservation
Proof 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
Proof 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₂✝
Theorem: subst_preservation
Proof 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]
Proof 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✝
Theorem: subst_preservation
Proof 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
Proof 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✝
Theorem: subst_preservation
Proof 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
Proof state after:
no goals
Theorem: subst_preservation
Proof 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
Proof state after:
no goals
Theorem: subst_preservation
Proof 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
Proof state after:
no goals
Theorem: subst_preservation
Proof 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
Proof state after:
no goals
Theorem: subst_preservation
Proof 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
Proof state after:
no goals
Theorem: subst_preservation
Proof 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 ?_ ?_
Proof 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₁]
Theorem: subst_preservation
Proof 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
Proof state after:
no goals
Theorem: subst_preservation
Proof 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)]
Proof state after:
no goals
Theorem: subst_preservation
Proof 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)
Proof state after:
no goals
Theorem: preservation
Proof 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
Proof 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₂✝
Theorem: 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₂✝
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
Proof state after:
no goals
Theorem: preservation
Proof 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)
Proof state after:
no goals
Theorem: preservation
Proof 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₂)
Proof state after:
no goals
Theorem: 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₂✝
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
Proof state after:
no goals
Theorem: preservation
Proof 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)
Proof state after:
no goals
Theorem: preservation
Proof 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 *
Proof 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₂✝
Theorem: preservation
Proof 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₁
Proof 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₂✝
Theorem: preservation
Proof 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₂
Proof 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₂✝
Theorem: preservation
Proof 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₂
Proof 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₂✝
Theorem: preservation
Proof 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₂)
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ctx : Ctx
t : Term
ty : Ty
h : type ctx t = some ty
⊢ ctx ⊢ t ⋮ ty
Tactic:
induction t generalizing ty ctx <;> simp [type, bind, Option.bind] at h
Proof state after:
case var
fvar✝ : Nat
ctx : Ctx
ty : Ty
h : ctx fvar✝ = some ty
⊢ ctx ⊢ Term.var fvar✝ ⋮ ty

case abs
ty✝ : Ty
body✝ : Term
body_ih✝ : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type (↥ctx)[0 ↦ ty✝] body✝, fun __do_lift => pure (Ty.arrow ty✝ __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty

case app
t₁✝ t₂✝ : Term
t₁_ih✝ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁✝ = some ty → ctx ⊢ t₁✝ ⋮ ty
t₂_ih✝ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂✝ = some ty → ctx ⊢ t₂✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type ctx t₁✝ with
    | some (Ty.arrow ty₁ ty₂) =>
      match type ctx t₂✝, fun __do_lift => if ty₁ = __do_lift then some ty₂ else none with
      | none, x => none
      | some a, b => b a
    | x => none) =
    some ty
⊢ ctx ⊢ Term.app t₁✝ t₂✝ ⋮ ty
Theorem: type_correct
Proof state before:
fvar✝ : Nat
ctx : Ctx
ty : Ty
h : ctx fvar✝ = some ty
⊢ ctx ⊢ Term.var fvar✝ ⋮ ty
Tactic:
case var => exact .var h
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type (↥ctx)[0 ↦ ty✝] body✝, fun __do_lift => pure (Ty.arrow ty✝ __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
case abs hi => 
  split at h <;> try contradiction
  case _ ht =>
    simp [pure] at h
    subst h
    exact .abs (hi ht)
Proof state after:
no goals
Theorem: type_correct
Proof state before:
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type ctx t₁ with
    | some (Ty.arrow ty₁ ty₂) =>
      match type ctx t₂, fun __do_lift => if ty₁ = __do_lift then some ty₂ else none with
      | none, x => none
      | some a, b => b a
    | x => none) =
    some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
Tactic:
case app t₁ t₂ hi₁ hi₂ =>
  cases h₁ : type ctx t₁ <;> cases h₂ : type ctx t₂ <;> simp_all [h₁, h₂]
  all_goals split at h <;> try contradiction
  case _ ty₁ ty₂ _ ty₁₁ _ ha =>
    specialize hi₁ h₁
    split at h <;> simp_all
    exact .app hi₁ (hi₂ h₂)
Proof state after:
no goals
Theorem: type_correct
Proof state before:
fvar✝ : Nat
ctx : Ctx
ty : Ty
h : ctx fvar✝ = some ty
⊢ ctx ⊢ Term.var fvar✝ ⋮ ty
Tactic:
exact .var h
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type (↥ctx)[0 ↦ ty✝] body✝, fun __do_lift => pure (Ty.arrow ty✝ __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
split at h <;> try contradiction
Proof state after:
case h_2
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
heq✝ : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : (fun __do_lift => pure (Ty.arrow ty✝ __do_lift)) a✝ = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Theorem: type_correct
Proof state before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : (fun __do_lift => pure (Ty.arrow ty✝ __do_lift)) a✝ = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
case _ ht =>
  simp [pure] at h
  subst h
  exact .abs (hi ht)
Proof state after:
no goals
Theorem: type_correct
Proof state before:
case h_1
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
heq✝ : type (↥ctx)[0 ↦ ty✝] body✝ = none
h : none = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
contradiction
Proof state after:
no goals
Theorem: type_correct
Proof state before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : (fun __do_lift => pure (Ty.arrow ty✝ __do_lift)) a✝ = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
simp [pure] at h
Proof state after:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : Ty.arrow ty✝ a✝ = ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Theorem: type_correct
Proof state before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : Ty.arrow ty✝ a✝ = ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
Tactic:
subst h
Proof state after:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ Ty.arrow ty✝ a✝
Theorem: type_correct
Proof state before:
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ Ty.arrow ty✝ a✝
Tactic:
exact .abs (hi ht)
Proof state after:
no goals