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

State before:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ RTC SmallStep (S; T, s) (Stmt.skip; T, u)
Tactic:
apply RTC.lift (fun Ss ↦ (Prod.fst Ss; T, Prod.snd Ss)) _ h
State after:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ ∀ (a b : Stmt × State), a ⇒ b → (fun Ss => (Ss.fst; T, Ss.snd)) a ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) b

State before:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
⊢ ∀ (a b : Stmt × State), a ⇒ b → (fun Ss => (Ss.fst; T, Ss.snd)) a ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) b
Tactic:
intro Ss Ss' hrtc
State after:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
Ss Ss' : Stmt × State
hrtc : Ss ⇒ Ss'
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) Ss ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) Ss'

State before:
S T : Stmt
s u : State
h : RTC SmallStep (S, s) (Stmt.skip, u)
Ss Ss' : Stmt × State
hrtc : Ss ⇒ Ss'
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) Ss ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) Ss'
Tactic:
cases Ss with
| mk S s =>
  cases Ss' with
  | mk S' s' =>
    apply SmallStep.seq_step
    assumption
State after:
no goals

State before:
case mk
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
Ss' : Stmt × State
S : Stmt
s : State
hrtc : (S, s) ⇒ Ss'
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) (S, s) ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) Ss'
Tactic:
cases Ss' with
| mk S' s' =>
  apply SmallStep.seq_step
  assumption
State after:
no goals

State before:
case mk.mk
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
S : Stmt
s : State
S' : Stmt
s' : State
hrtc : (S, s) ⇒ (S', s')
⊢ (fun Ss => (Ss.fst; T, Ss.snd)) (S, s) ⇒ (fun Ss => (Ss.fst; T, Ss.snd)) (S', s')
Tactic:
apply SmallStep.seq_step
State after:
case mk.mk.hS
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
S : Stmt
s : State
S' : Stmt
s' : State
hrtc : (S, s) ⇒ (S', s')
⊢ ((S, s).fst, (S, s).snd) ⇒ ((S', s').fst, (S', s').snd)

State before:
case mk.mk.hS
S✝ T : Stmt
s✝ u : State
h : RTC SmallStep (S✝, s✝) (Stmt.skip, u)
S : Stmt
s : State
S' : Stmt
s' : State
hrtc : (S, s) ⇒ (S', s')
⊢ ((S, s).fst, (S, s).snd) ⇒ ((S', s').fst, (S', s').snd)
Tactic:
assumption
State after:
no goals