internlm/Lean-Github huggingface dataset:
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof state before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
this :
  evalFin t₁ (fun i => if hj : ↑i < arity (Term.xor t₁ t₂) then seq { val := ↑i, isLt := hj } else fun x => false) n =
    evalFin t₂ (fun i => if hj : ↑i < arity (Term.xor t₁ t₂) then seq { val := ↑i, isLt := hj } else fun x => false) n
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n
Tactic:
simp at this
Proof state after:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
this :
  evalFin t₁ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n =
    evalFin t₂ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof state before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
this :
  evalFin t₁ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n =
    evalFin t₂ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n
Tactic:
convert this
Proof state after:
no goals
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof state before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
Tactic:
intro h seq m
Proof state after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h :
  ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
    evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
      evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i
seq : ℕ → ℕ → Bool
m : ℕ
⊢ evalFin t₁ (fun i => seq ↑i) m = evalFin t₂ (fun i => seq ↑i) m
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof state before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h :
  ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
    evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
      evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i
seq : ℕ → ℕ → Bool
m : ℕ
⊢ evalFin t₁ (fun i => seq ↑i) m = evalFin t₂ (fun i => seq ↑i) m
Tactic:
exact h (λ j => seq j) _
Proof state after:
no goals
Theorem: uniqueness
Proof state before:
ctx : Ctx
t : Term
ty₁ ty₂ : Ty
h₁ : ctx ⊢ t ⋮ ty₁
h₂ : ctx ⊢ t ⋮ ty₂
⊢ ty₁ = ty₂
Tactic:
induction h₁ generalizing ty₂ <;> cases h₂
Proof state after:
case var.var
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝¹ : ctx✝ x✝ = some ty✝
ty₂ : Ty
a✝ : ctx✝ x✝ = some ty₂
⊢ ty✝ = ty₂

case abs.abs
ctx : Ctx
t : Term
ty₁ ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝¹ : Ty
a✝¹ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝¹
a_ih✝ : ∀ {ty₂ : Ty}, ((↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂) → ty₂✝¹ = ty₂
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ Ty.arrow ty₁✝ ty₂✝¹ = Ty.arrow ty₁✝ ty₂✝

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✝¹ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₁✝ ⋮ ty₂) → Ty.arrow ty₁✝¹ ty₂✝ = ty₂
a_ih✝ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₂✝ ⋮ ty₂) → ty₁✝¹ = ty₂
ty₂ ty₁✝ : Ty
a✝¹ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a✝ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂
⊢ ty₂✝ = ty₂
Theorem: uniqueness
Proof state before:
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
h₁ : ctx✝ x✝ = some ty✝
ty₂ : Ty
h₂ : ctx✝ x✝ = some ty₂
⊢ ty✝ = ty₂
Tactic:
case var.var h₁ h₂      => injection h₁ ▸ h₂
Proof state after:
no goals
Theorem: uniqueness
Proof state before:
ctx : Ctx
t : Term
ty₁ ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝¹ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝¹
hi : ∀ {ty₂ : Ty}, ((↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂) → ty₂✝¹ = ty₂
ty₂✝ : Ty
h : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ Ty.arrow ty₁✝ ty₂✝¹ = Ty.arrow ty₁✝ ty₂✝
Tactic:
case abs.abs hi _ h     => rw [hi h]
Proof state after:
no goals
Theorem: uniqueness
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 : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₁✝ ⋮ ty₂) → Ty.arrow ty₁✝¹ ty₂✝ = ty₂
a_ih✝ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₂✝ ⋮ ty₂) → ty₁✝¹ = ty₂
ty₂ ty₁✝ : Ty
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
h : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂
⊢ ty₂✝ = ty₂
Tactic:
case app.app hi _ _ _ h => injection hi h
Proof state after:
no goals
Theorem: uniqueness
Proof state before:
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
h₁ : ctx✝ x✝ = some ty✝
ty₂ : Ty
h₂ : ctx✝ x✝ = some ty₂
⊢ ty✝ = ty₂
Tactic:
injection h₁ ▸ h₂
Proof state after:
no goals
Theorem: uniqueness
Proof state before:
ctx : Ctx
t : Term
ty₁ ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝¹ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝¹
hi : ∀ {ty₂ : Ty}, ((↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂) → ty₂✝¹ = ty₂
ty₂✝ : Ty
h : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ Ty.arrow ty₁✝ ty₂✝¹ = Ty.arrow ty₁✝ ty₂✝
Tactic:
rw [hi h]
Proof state after:
no goals
Theorem: uniqueness
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 : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₁✝ ⋮ ty₂) → Ty.arrow ty₁✝¹ ty₂✝ = ty₂
a_ih✝ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₂✝ ⋮ ty₂) → ty₁✝¹ = ty₂
ty₂ ty₁✝ : Ty
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
h : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂
⊢ ty₂✝ = ty₂
Tactic:
injection hi h
Proof state after:
no goals
Theorem: canonical_forms
Proof state before:
ty₁ ty₂ : Ty
v : Value
h :
  ∅ ⊢
    match v with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, v = Value.abs ty₁ t
Tactic:
cases v
Proof state after:
case abs
ty₁ ty₂ ty✝ : Ty
body✝ : Term
h :
  ∅ ⊢
    match Value.abs ty✝ body✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body✝ = Value.abs ty₁ t
Theorem: canonical_forms
Proof state before:
ty₁ ty₂ ty✝ : Ty
body : Term
h :
  ∅ ⊢
    match Value.abs ty✝ body with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
Tactic:
case abs body =>
  simp at h
  exists body
  have ⟨_, h, _⟩ := inversion_abs h
  injection h with h
  rw [h]
Proof state after:
no goals
Theorem: canonical_forms
Proof state before:
ty₁ ty₂ ty✝ : Ty
body : Term
h :
  ∅ ⊢
    match Value.abs ty✝ body with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
Tactic:
simp at h
Proof state after:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
Theorem: canonical_forms
Proof state before:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
Tactic:
exists body
Proof state after:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Theorem: canonical_forms
Proof state before:
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Tactic:
have ⟨_, h, _⟩ := inversion_abs h
Proof state after:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
h : Ty.arrow ty₁ ty₂ = Ty.arrow ty✝ w✝
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Theorem: canonical_forms
Proof state before:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
h : Ty.arrow ty₁ ty₂ = Ty.arrow ty✝ w✝
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Tactic:
injection h with h
Proof state after:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
h : ty₁ = ty✝
ty₂_eq✝ : ty₂ = w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Theorem: canonical_forms
Proof state before:
ty₁ ty₂ ty✝ : Ty
body : Term
h✝ : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
w✝ : Ty
right✝ : (↥∅)[0 ↦ ty✝] ⊢ body ⋮ w✝
h : ty₁ = ty✝
ty₂_eq✝ : ty₂ = w✝
⊢ Value.abs ty✝ body = Value.abs ty₁ body
Tactic:
rw [h]
Proof state after:
no goals
Theorem: progress
Proof state before:
t : Term
ty : Ty
h : ∅ ⊢ t ⋮ ty
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Tactic:
generalize hc : (∅ : Ctx) = ctx
Proof state after:
t : Term
ty : Ty
h : ∅ ⊢ t ⋮ ty
ctx : Ctx
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
h : ∅ ⊢ t ⋮ ty
ctx : Ctx
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Tactic:
rw [hc] at h
Proof state after:
t : Term
ty : Ty
ctx : Ctx
h : ctx ⊢ t ⋮ ty
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
h : ctx ⊢ t ⋮ ty
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
Tactic:
induction h <;> (subst hc; simp at *)
Proof state after:
case var
t : Term
ty : Ty
ctx : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ∅ x✝ = some ty✝
⊢ (∃ v, False) ∨ ∃ t', Term.var x✝ ⇒ t'

case abs
t : Term
ty : Ty
ctx : Ctx
ty₁✝ : Ty
t✝ : Term
ty₂✝ : Ty
a✝ : (↥∅)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ∅ = (↥∅)[0 ↦ ty₁✝] → (∃ v, t✝ = Term.abs v.1 v.2) ∨ ∃ t', t✝ ⇒ t'
⊢ (∃ v, ty₁✝ = v.1 ∧ t✝ = v.2) ∨ ∃ t', Term.abs ty₁✝ t✝ ⇒ t'

case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
a_ih✝ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty✝ : Ty
x✝ : Nat
h : ∅ x✝ = some ty✝
⊢ (∃ v, False) ∨ ∃ t', Term.var x✝ ⇒ t'
Tactic:
case var h => injection h
Proof state after:
no goals
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty₁ : Ty
t₁ : Term
ty₂✝ : Ty
a✝ : (↥∅)[0 ↦ ty₁] ⊢ t₁ ⋮ ty₂✝
a_ih✝ : ∅ = (↥∅)[0 ↦ ty₁] → (∃ v, t₁ = Term.abs v.1 v.2) ∨ ∃ t', t₁ ⇒ t'
⊢ (∃ v, ty₁ = v.1 ∧ t₁ = v.2) ∨ ∃ t', Term.abs ty₁ t₁ ⇒ t'
Tactic:
case abs ty₁ t₁ _ _ _ => exact .inl ⟨⟨_, _⟩, rfl, rfl⟩
Proof state after:
no goals
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case app hi₁ hi₂ =>
  cases hi₁ <;> apply Or.inr
  case inr h =>
    have ⟨_, h⟩ := h
    exact ⟨_, .app₁ _ h⟩
  case inl ty₁ _ _ ht₁ _ h₁ =>
    cases hi₂ 
    case inl h₂ =>
      have ⟨v₁, hv₁⟩ := h₁ 
      have ⟨v₂, hv₂⟩ := h₂
      subst hv₁ hv₂
      have ⟨body₁, hv₁⟩ := canonical_forms ht₁
      subst hv₁
      exact ⟨_, .beta ..⟩ 
    case inr h₂ =>
      have ⟨_, h₁⟩ := h₁
      have ⟨_, h₂⟩ := h₂
      subst h₁
      exact ⟨_, .app₂ _ h₂⟩
Proof state after:
no goals
Theorem: progress
Proof state before:
case app
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✝ →
    (∃ v,
        t₁✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₁✝ ⇒ t'
a_ih✝ :
  ∅ = ctx✝ →
    (∃ v,
        t₂✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₂✝ ⇒ t'
hc : ∅ = ctx✝
⊢ (∃ v,
      Term.app t₁✝ t₂✝ =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
subst hc
Proof state after:
case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∅ = ∅ →
    (∃ v,
        t₁✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₁✝ ⇒ t'
a_ih✝ :
  ∅ = ∅ →
    (∃ v,
        t₂✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₂✝ ⇒ t'
⊢ (∃ v,
      Term.app t₁✝ t₂✝ =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Theorem: progress
Proof state before:
case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∅ = ∅ →
    (∃ v,
        t₁✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₁✝ ⇒ t'
a_ih✝ :
  ∅ = ∅ →
    (∃ v,
        t₂✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₂✝ ⇒ t'
⊢ (∃ v,
      Term.app t₁✝ t₂✝ =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
simp at *
Proof state after:
case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
a_ih✝ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty✝ : Ty
x✝ : Nat
h : ∅ x✝ = some ty✝
⊢ (∃ v, False) ∨ ∃ t', Term.var x✝ ⇒ t'
Tactic:
injection h
Proof state after:
no goals
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty₁ : Ty
t₁ : Term
ty₂✝ : Ty
a✝ : (↥∅)[0 ↦ ty₁] ⊢ t₁ ⋮ ty₂✝
a_ih✝ : ∅ = (↥∅)[0 ↦ ty₁] → (∃ v, t₁ = Term.abs v.1 v.2) ∨ ∃ t', t₁ ⇒ t'
⊢ (∃ v, ty₁ = v.1 ∧ t₁ = v.2) ∨ ∃ t', Term.abs ty₁ t₁ ⇒ t'
Tactic:
exact .inl ⟨⟨_, _⟩, rfl, rfl⟩
Proof state after:
no goals
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
cases hi₁ <;> apply Or.inr
Proof state after:
case inl.h
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

case inr.h
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ t', t₁✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h : ∃ t', t₁✝ ⇒ t'
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case inr h =>
  have ⟨_, h⟩ := h
  exact ⟨_, .app₁ _ h⟩
Proof state after:
no goals
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₁
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case inl ty₁ _ _ ht₁ _ h₁ =>
  cases hi₂ 
  case inl h₂ =>
    have ⟨v₁, hv₁⟩ := h₁ 
    have ⟨v₂, hv₂⟩ := h₂
    subst hv₁ hv₂
    have ⟨body₁, hv₁⟩ := canonical_forms ht₁
    subst hv₁
    exact ⟨_, .beta ..⟩ 
  case inr h₂ =>
    have ⟨_, h₁⟩ := h₁
    have ⟨_, h₂⟩ := h₂
    subst h₁
    exact ⟨_, .app₂ _ h₂⟩
Proof state after:
no goals
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
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
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ t', t₁✝ ⇒ t'
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
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ t', t₁✝ ⇒ t'
w✝ : Term
h : t₁✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
exact ⟨_, .app₁ _ h⟩
Proof state after:
no goals
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₁
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h₁ : ∃ v, t₁✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
cases hi₂
Proof state after:
case inl
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✝ : ∃ v, t₂✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

case inr
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'
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₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
case inl h₂ =>
  have ⟨v₁, hv₁⟩ := h₁ 
  have ⟨v₂, hv₂⟩ := h₂
  subst hv₁ hv₂
  have ⟨body₁, hv₁⟩ := canonical_forms ht₁
  subst hv₁
  exact ⟨_, .beta ..⟩
Proof state after:
no goals
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:
case inr h₂ =>
  have ⟨_, h₁⟩ := h₁
  have ⟨_, h₂⟩ := h₂
  subst h₁
  exact ⟨_, .app₂ _ h₂⟩
Proof state after:
no goals
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₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨v₁, hv₁⟩ := 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₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.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₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
have ⟨v₂, hv₂⟩ := 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₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.2
v₂ : Value
hv₂ : t₂✝ = Term.abs v₂.1 v₂.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₂ : ∃ v, t₂✝ = Term.abs v.1 v.2
v₁ : Value
hv₁ : t₁✝ = Term.abs v₁.1 v₁.2
v₂ : Value
hv₂ : t₂✝ = Term.abs v₂.1 v₂.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
Tactic:
subst hv₁ hv₂
Proof state after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'
Tactic:
have ⟨body₁, hv₁⟩ := canonical_forms ht₁
Proof state after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
hv₁ : v₁ = Value.abs ty₁ body₁
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₁ v₂ : Value
ht₁ : ∅ ⊢ Term.abs v₁.1 v₁.2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs v₁.1 v₁.2 = Term.abs v.1 v.2
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
hv₁ : v₁ = Value.abs ty₁ body₁
⊢ ∃ t', Term.app (Term.abs v₁.1 v₁.2) (Term.abs v₂.1 v₂.2) ⇒ t'
Tactic:
subst hv₁
Proof state after:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₂ : Value
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
ht₁ : ∅ ⊢ Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2) (Term.abs v₂.1 v₂.2) ⇒ t'
Theorem: progress
Proof state before:
t : Term
ty : Ty
ctx : Ctx
ty₁ ty₂✝ : Ty
v₂ : Value
a✝ : ∅ ⊢ Term.abs v₂.1 v₂.2 ⋮ ty₁
h₂ : ∃ v, Term.abs v₂.1 v₂.2 = Term.abs v.1 v.2
body₁ : Term
ht₁ : ∅ ⊢ Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 ⋮ Ty.arrow ty₁ ty₂✝
h₁ : ∃ v, Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2 = Term.abs v.1 v.2
⊢ ∃ t', Term.app (Term.abs (Value.abs ty₁ body₁).1 (Value.abs ty₁ body₁).2) (Term.abs v₂.1 v₂.2) ⇒ t'
Tactic:
exact ⟨_, .beta ..⟩
Proof state after:
no goals