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

State before:
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut ↔ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
Tactic:
apply Iff.intro
State after:
case mp
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut → (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)

case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut

State before:
case mp
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut → (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)

case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Tactic:
{ intro hST
  cases hST with
  | seq_step _ S' _ _ s' hS =>
    apply Or.intro_left
    apply Exists.intro S'
    apply Exists.intro s'
    aesop
  | seq_skip =>
    apply Or.intro_right
    aesop }
State after:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut

State before:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Tactic:
{
  intro hor
  cases hor with
  | inl hex =>
    cases hex with
    | intro S' hex' =>
      cases hex' with
      | intro s' hand =>
        cases hand with
        | intro hS hUt =>
          rw [hUt]
          apply SmallStep.seq_step
          assumption
  | inr hand =>
    cases hand with
    | intro hS hUt =>
      rw [hS, hUt]
      apply SmallStep.seq_skip }
State after:
no goals

State before:
case mp
S T : Stmt
s : State
Ut : Stmt × State
⊢ (S; T, s) ⇒ Ut → (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
Tactic:
intro hST
State after:
case mp
S T : Stmt
s : State
Ut : Stmt × State
hST : (S; T, s) ⇒ Ut
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)

State before:
case mp
S T : Stmt
s : State
Ut : Stmt × State
hST : (S; T, s) ⇒ Ut
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
Tactic:
cases hST with
| seq_step _ S' _ _ s' hS =>
  apply Or.intro_left
  apply Exists.intro S'
  apply Exists.intro s'
  aesop
| seq_skip =>
  apply Or.intro_right
  aesop
State after:
no goals

State before:
case mp.seq_step
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (∃ S'_1 t, (S, s) ⇒ (S'_1, t) ∧ (S'; T, s') = (S'_1; T, t)) ∨ S = Stmt.skip ∧ (S'; T, s') = (T, s)
Tactic:
apply Or.intro_left
State after:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ S'_1 t, (S, s) ⇒ (S'_1, t) ∧ (S'; T, s') = (S'_1; T, t)

State before:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ S'_1 t, (S, s) ⇒ (S'_1, t) ∧ (S'; T, s') = (S'_1; T, t)
Tactic:
apply Exists.intro S'
State after:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ t, (S, s) ⇒ (S', t) ∧ (S'; T, s') = (S'; T, t)

State before:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ ∃ t, (S, s) ⇒ (S', t) ∧ (S'; T, s') = (S'; T, t)
Tactic:
apply Exists.intro s'
State after:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S, s) ⇒ (S', s') ∧ (S'; T, s') = (S'; T, s')

State before:
case mp.seq_step.h
S T : Stmt
s : State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
⊢ (S, s) ⇒ (S', s') ∧ (S'; T, s') = (S'; T, s')
Tactic:
aesop
State after:
no goals

State before:
case mp.seq_skip
T : Stmt
s : State
⊢ (∃ S' t, (Stmt.skip, s) ⇒ (S', t) ∧ (T, s) = (S'; T, t)) ∨ Stmt.skip = Stmt.skip ∧ (T, s) = (T, s)
Tactic:
apply Or.intro_right
State after:
case mp.seq_skip.h
T : Stmt
s : State
⊢ Stmt.skip = Stmt.skip ∧ (T, s) = (T, s)

State before:
case mp.seq_skip.h
T : Stmt
s : State
⊢ Stmt.skip = Stmt.skip ∧ (T, s) = (T, s)
Tactic:
aesop
State after:
no goals

State before:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
⊢ (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s) → (S; T, s) ⇒ Ut
Tactic:
intro hor
State after:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
hor : (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
⊢ (S; T, s) ⇒ Ut

State before:
case mpr
S T : Stmt
s : State
Ut : Stmt × State
hor : (∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)) ∨ S = Stmt.skip ∧ Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hor with
| inl hex =>
  cases hex with
  | intro S' hex' =>
    cases hex' with
    | intro s' hand =>
      cases hand with
      | intro hS hUt =>
        rw [hUt]
        apply SmallStep.seq_step
        assumption
| inr hand =>
  cases hand with
  | intro hS hUt =>
    rw [hS, hUt]
    apply SmallStep.seq_skip
State after:
no goals

State before:
case mpr.inl
S T : Stmt
s : State
Ut : Stmt × State
hex : ∃ S' t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hex with
| intro S' hex' =>
  cases hex' with
  | intro s' hand =>
    cases hand with
    | intro hS hUt =>
      rw [hUt]
      apply SmallStep.seq_step
      assumption
State after:
no goals

State before:
case mpr.inl.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
hex' : ∃ t, (S, s) ⇒ (S', t) ∧ Ut = (S'; T, t)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hex' with
| intro s' hand =>
  cases hand with
  | intro hS hUt =>
    rw [hUt]
    apply SmallStep.seq_step
    assumption
State after:
no goals

State before:
case mpr.inl.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hand : (S, s) ⇒ (S', s') ∧ Ut = (S'; T, s')
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hand with
| intro hS hUt =>
  rw [hUt]
  apply SmallStep.seq_step
  assumption
State after:
no goals

State before:
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ Ut
Tactic:
rw [hUt]
State after:
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ (S'; T, s')

State before:
case mpr.inl.intro.intro.intro
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S; T, s) ⇒ (S'; T, s')
Tactic:
apply SmallStep.seq_step
State after:
case mpr.inl.intro.intro.intro.hS
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S, s) ⇒ (S', s')

State before:
case mpr.inl.intro.intro.intro.hS
S T : Stmt
s : State
Ut : Stmt × State
S' : Stmt
s' : State
hS : (S, s) ⇒ (S', s')
hUt : Ut = (S'; T, s')
⊢ (S, s) ⇒ (S', s')
Tactic:
assumption
State after:
no goals

State before:
case mpr.inr
S T : Stmt
s : State
Ut : Stmt × State
hand : S = Stmt.skip ∧ Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
Tactic:
cases hand with
| intro hS hUt =>
  rw [hS, hUt]
  apply SmallStep.seq_skip
State after:
no goals

State before:
case mpr.inr.intro
S T : Stmt
s : State
Ut : Stmt × State
hS : S = Stmt.skip
hUt : Ut = (T, s)
⊢ (S; T, s) ⇒ Ut
Tactic:
rw [hS, hUt]
State after:
case mpr.inr.intro
S T : Stmt
s : State
Ut : Stmt × State
hS : S = Stmt.skip
hUt : Ut = (T, s)
⊢ (Stmt.skip; T, s) ⇒ (T, s)

State before:
case mpr.inr.intro
S T : Stmt
s : State
Ut : Stmt × State
hS : S = Stmt.skip
hUt : Ut = (T, s)
⊢ (Stmt.skip; T, s) ⇒ (T, s)
Tactic:
apply SmallStep.seq_skip
State after:
no goals