Theorem: LoVe.FnExp.progress (LoVe/Labs/Lab6Solution.lean)

State before:
e : FnExp
τ : FnType
⊢ e ∶ τ → Value e ∨ ∃ e', e ⇒ e'
Tactic:
intro htp
State after:
e : FnExp
τ : FnType
htp : e ∶ τ
⊢ Value e ∨ ∃ e', e ⇒ e'

State before:
e : FnExp
τ : FnType
htp : e ∶ τ
⊢ Value e ∨ ∃ e', e ⇒ e'
Tactic:
induction htp with
| fn => exact Or.inl Value.fn
| arg => exact Or.inl Value.arg
| @appZero f x hf hx ihf ihx =>
  apply Or.inr
  cases ihf with
  | inl hval =>
    cases hval with
    | @fn n =>
      cases hf
      apply Exists.intro x
      apply Step.appZero
    | arg => cases hf
  | inr hstep =>
    cases hstep with | intro f' hf' =>
    apply Exists.intro (app f' x)
    exact Step.appArg hf'      
| @appSucc f x n hf hx ihf ihx =>
  apply Or.inr
  cases ihf with
  | inl hval =>
    cases hf with
    | fn =>
      apply Exists.intro (fn n)
      exact Step.appSucc
    | appSucc => cases hval
  | inr hstep =>
    cases hstep with | intro f' hf' =>
    apply Exists.intro (app f' x)
    exact Step.appArg hf'
State after:
no goals

State before:
case fn
e : FnExp
τ : FnType
n✝ : ℕ
⊢ Value (fn n✝) ∨ ∃ e', fn n✝ ⇒ e'
Tactic:
exact Or.inl Value.fn
State after:
no goals

State before:
case arg
e : FnExp
τ : FnType
⊢ Value arg ∨ ∃ e', arg ⇒ e'
Tactic:
exact Or.inl Value.arg
State after:
no goals

State before:
case appZero
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ Value (app f x) ∨ ∃ e', app f x ⇒ e'
Tactic:
apply Or.inr
State after:
case appZero.h
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'

State before:
case appZero.h
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases ihf with
| inl hval =>
  cases hval with
  | @fn n =>
    cases hf
    apply Exists.intro x
    apply Step.appZero
  | arg => cases hf
| inr hstep =>
  cases hstep with | intro f' hf' =>
  apply Exists.intro (app f' x)
  exact Step.appArg hf'
State after:
no goals

State before:
case appZero.h.inl
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value f
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hval with
| @fn n =>
  cases hf
  apply Exists.intro x
  apply Step.appZero
| arg => cases hf
State after:
no goals

State before:
case appZero.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
n : ℕ
hf : fn n ∶ function 0
⊢ ∃ e', app (fn n) x ⇒ e'
Tactic:
cases hf
State after:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app (fn 0) x ⇒ e'

State before:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app (fn 0) x ⇒ e'
Tactic:
apply Exists.intro x
State after:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ app (fn 0) x ⇒ x

State before:
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ app (fn 0) x ⇒ x
Tactic:
apply Step.appZero
State after:
no goals

State before:
case appZero.h.inl.arg
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hf : arg ∶ function 0
⊢ ∃ e', app arg x ⇒ e'
Tactic:
cases hf
State after:
no goals

State before:
case appZero.h.inr
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hstep : ∃ e', f ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hstep with | intro f' hf' =>
apply Exists.intro (app f' x)
exact Step.appArg hf'
State after:
no goals

State before:
case appZero.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ ∃ e', app f x ⇒ e'
Tactic:
apply Exists.intro (app f' x)
State after:
case appZero.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x

State before:
case appZero.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x
Tactic:
exact Step.appArg hf'
State after:
no goals

State before:
case appSucc
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ Value (app f x) ∨ ∃ e', app f x ⇒ e'
Tactic:
apply Or.inr
State after:
case appSucc.h
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'

State before:
case appSucc.h
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihf : Value f ∨ ∃ e', f ⇒ e'
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases ihf with
| inl hval =>
  cases hf with
  | fn =>
    apply Exists.intro (fn n)
    exact Step.appSucc
  | appSucc => cases hval
| inr hstep =>
  cases hstep with | intro f' hf' =>
  apply Exists.intro (app f' x)
  exact Step.appArg hf'
State after:
no goals

State before:
case appSucc.h.inl
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value f
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hf with
| fn =>
  apply Exists.intro (fn n)
  exact Step.appSucc
| appSucc => cases hval
State after:
no goals

State before:
case appSucc.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value (fn (Nat.succ n))
⊢ ∃ e', app (fn (Nat.succ n)) x ⇒ e'
Tactic:
apply Exists.intro (fn n)
State after:
case appSucc.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value (fn (Nat.succ n))
⊢ app (fn (Nat.succ n)) x ⇒ fn n

State before:
case appSucc.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value (fn (Nat.succ n))
⊢ app (fn (Nat.succ n)) x ⇒ fn n
Tactic:
exact Step.appSucc
State after:
no goals

State before:
case appSucc.h.inl.appSucc
e : FnExp
τ : FnType
x : FnExp
n : ℕ
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f✝ x✝ : FnExp
a✝¹ : x✝ ∶ argument
hval : Value (app f✝ x✝)
a✝ : f✝ ∶ function (Nat.succ (Nat.succ n))
⊢ ∃ e', app (app f✝ x✝) x ⇒ e'
Tactic:
cases hval
State after:
no goals

State before:
case appSucc.h.inr
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hstep : ∃ e', f ⇒ e'
⊢ ∃ e', app f x ⇒ e'
Tactic:
cases hstep with | intro f' hf' =>
apply Exists.intro (app f' x)
exact Step.appArg hf'
State after:
no goals

State before:
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ ∃ e', app f x ⇒ e'
Tactic:
apply Exists.intro (app f' x)
State after:
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x

State before:
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x
Tactic:
exact Step.appArg hf'
State after:
no goals