Theorem: LoVe.BigStep_of_RTC_SmallStep (LoVe/Lectures/LoVe09_OperationalSemantics_Demo.lean)

State before:
Ss : Stmt × State
t : State
⊢ RTC SmallStep Ss (Stmt.skip, t) → Ss ⟹ t
Tactic:
intro hS
State after:
Ss : Stmt × State
t : State
hS : RTC SmallStep Ss (Stmt.skip, t)
⊢ Ss ⟹ t

State before:
Ss : Stmt × State
t : State
hS : RTC SmallStep Ss (Stmt.skip, t)
⊢ Ss ⟹ t
Tactic:
induction hS using RTC.head_induction_on with
| refl =>
  apply BigStep.skip
| head Ss Ss' hST hsmallT ih =>
  cases Ss' with
  | mk S' s' =>
    apply BigStep_of_SmallStep_of_BigStep hST
    apply ih
State after:
no goals

State before:
case refl
Ss : Stmt × State
t : State
⊢ (Stmt.skip, t) ⟹ t
Tactic:
apply BigStep.skip
State after:
no goals

State before:
case head
Ss✝ : Stmt × State
t : State
Ss Ss' : Stmt × State
hST : Ss ⇒ Ss'
hsmallT : RTC SmallStep Ss' (Stmt.skip, t)
ih : Ss' ⟹ t
⊢ Ss ⟹ t
Tactic:
cases Ss' with
| mk S' s' =>
  apply BigStep_of_SmallStep_of_BigStep hST
  apply ih
State after:
no goals

State before:
case head.mk
Ss✝ : Stmt × State
t : State
Ss : Stmt × State
S' : Stmt
s' : State
hST : Ss ⇒ (S', s')
hsmallT : RTC SmallStep (S', s') (Stmt.skip, t)
ih : (S', s') ⟹ t
⊢ Ss ⟹ t
Tactic:
apply BigStep_of_SmallStep_of_BigStep hST
State after:
case head.mk
Ss✝ : Stmt × State
t : State
Ss : Stmt × State
S' : Stmt
s' : State
hST : Ss ⇒ (S', s')
hsmallT : RTC SmallStep (S', s') (Stmt.skip, t)
ih : (S', s') ⟹ t
⊢ (S', s') ⟹ t

State before:
case head.mk
Ss✝ : Stmt × State
t : State
Ss : Stmt × State
S' : Stmt
s' : State
hST : Ss ⇒ (S', s')
hsmallT : RTC SmallStep (S', s') (Stmt.skip, t)
ih : (S', s') ⟹ t
⊢ (S', s') ⟹ t
Tactic:
apply ih
State after:
no goals