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

State before:
e e' : FnExp
τ : FnType
⊢ e ∶ τ → e ⇒ e' → e' ∶ τ
Tactic:
intro htp hstep
State after:
e e' : FnExp
τ : FnType
htp : e ∶ τ
hstep : e ⇒ e'
⊢ e' ∶ τ

State before:
e e' : FnExp
τ : FnType
htp : e ∶ τ
hstep : e ⇒ e'
⊢ e' ∶ τ
Tactic:
induction hstep generalizing τ with
| @appArg f f' x h ih =>
  cases htp with
  | appZero hf hx =>
    apply HasType.appZero
    . exact ih hf
    . exact hx
  | @appSucc _ _ n hf hx =>
    apply HasType.appSucc
    . exact ih hf
    . exact hx
| @appZero x =>
  cases htp with
  | appZero => assumption
  | appSucc hf hx => cases hf
| @appSucc _ n =>
  cases htp with
  | appZero hf hx => cases hf
  | appSucc hf hx =>
    cases hf
    exact HasType.fn
State after:
no goals

State before:
case appArg
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
τ : FnType
htp : app f x ∶ τ
⊢ app f' x ∶ τ
Tactic:
cases htp with
| appZero hf hx =>
  apply HasType.appZero
  . exact ih hf
  . exact hx
| @appSucc _ _ n hf hx =>
  apply HasType.appSucc
  . exact ih hf
  . exact hx
State after:
no goals

State before:
case appArg.appZero
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ app f' x ∶ argument
Tactic:
apply HasType.appZero
State after:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ f' ∶ function 0

case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument

State before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ f' ∶ function 0

case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact ih hf
State after:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument

State before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact hx
State after:
no goals

State before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ f' ∶ function 0
Tactic:
exact ih hf
State after:
no goals

State before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
exact hx
State after:
no goals

State before:
case appArg.appSucc
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ app f' x ∶ function n
Tactic:
apply HasType.appSucc
State after:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ f' ∶ function (Nat.succ n)

case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument

State before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ f' ∶ function (Nat.succ n)

case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact ih hf
State after:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument

State before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact hx
State after:
no goals

State before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ f' ∶ function (Nat.succ n)
Tactic:
exact ih hf
State after:
no goals

State before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
exact hx
State after:
no goals

State before:
case appZero
e e' x : FnExp
τ : FnType
htp : app (fn 0) x ∶ τ
⊢ x ∶ τ
Tactic:
cases htp with
| appZero => assumption
| appSucc hf hx => cases hf
State after:
no goals

State before:
case appZero.appZero
e e' x : FnExp
a✝¹ : fn 0 ∶ function 0
a✝ : x ∶ argument
⊢ x ∶ argument
Tactic:
assumption
State after:
no goals

State before:
case appZero.appSucc
e e' x : FnExp
n✝ : ℕ
hf : fn 0 ∶ function (Nat.succ n✝)
hx : x ∶ argument
⊢ x ∶ function n✝
Tactic:
cases hf
State after:
no goals

State before:
case appSucc
e e' x✝ : FnExp
n : ℕ
τ : FnType
htp : app (fn (Nat.succ n)) x✝ ∶ τ
⊢ fn n ∶ τ
Tactic:
cases htp with
| appZero hf hx => cases hf
| appSucc hf hx =>
  cases hf
  exact HasType.fn
State after:
no goals

State before:
case appSucc.appZero
e e' x✝ : FnExp
n : ℕ
hf : fn (Nat.succ n) ∶ function 0
hx : x✝ ∶ argument
⊢ fn n ∶ argument
Tactic:
cases hf
State after:
no goals

State before:
case appSucc.appSucc
e e' x✝ : FnExp
n n✝ : ℕ
hf : fn (Nat.succ n) ∶ function (Nat.succ n✝)
hx : x✝ ∶ argument
⊢ fn n ∶ function n✝
Tactic:
cases hf
State after:
case appSucc.appSucc.fn
e e' x✝ : FnExp
n : ℕ
hx : x✝ ∶ argument
⊢ fn n ∶ function n

State before:
case appSucc.appSucc.fn
e e' x✝ : FnExp
n : ℕ
hx : x✝ ∶ argument
⊢ fn n ∶ function n
Tactic:
exact HasType.fn
State after:
no goals