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

State before:
⊢ ¬∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
Tactic:
intro hneg
State after:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
⊢ False

State before:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
⊢ False
Tactic:
have htp : app (app (fn 1) arg) arg ∶ argument :=
  HasType.appZero (HasType.appSucc HasType.fn HasType.arg) HasType.arg
State after:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
⊢ False

State before:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
⊢ False
Tactic:
have hexp_step := hneg htp
State after:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hexp_step : Value (app (app (fn 1) arg) arg) ∨ ∃ e', BadStep (app (app (fn 1) arg) arg) e'
⊢ False

State before:
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hexp_step : Value (app (app (fn 1) arg) arg) ∨ ∃ e', BadStep (app (app (fn 1) arg) arg) e'
⊢ False
Tactic:
cases hexp_step with
| inl hval =>  cases hval
| inr hstep =>
  cases hstep with | intro e' he' =>
  cases he'
State after:
no goals

State before:
case inl
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hval : Value (app (app (fn 1) arg) arg)
⊢ False
Tactic:
cases hval
State after:
no goals

State before:
case inr
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hstep : ∃ e', BadStep (app (app (fn 1) arg) arg) e'
⊢ False
Tactic:
cases hstep with | intro e' he' =>
cases he'
State after:
no goals

State before:
case inr.intro
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
e' : FnExp
he' : BadStep (app (app (fn 1) arg) arg) e'
⊢ False
Tactic:
cases he'
State after:
no goals