Theorem: LoVe.BigStepEquiv.seq_skip_right (LoVe/Labs/Lab6Solution.lean)

State before:
S : Stmt
⊢ S; Stmt.skip ~ S
Tactic:
intro s t
State after:
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t ↔ (S, s) ⟹ t

State before:
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t ↔ (S, s) ⟹ t
Tactic:
apply Iff.intro
State after:
case mp
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t → (S, s) ⟹ t

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t

State before:
case mp
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t → (S, s) ⟹ t

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Tactic:
{ intro hseq
  cases hseq with
  | seq _ _ _ u _ hS hs =>
    cases hs
    assumption }
State after:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t

State before:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Tactic:
{ intro h
  apply BigStep.seq
  { assumption }
  { apply BigStep.skip } }
State after:
no goals

State before:
case mp
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t → (S, s) ⟹ t
Tactic:
intro hseq
State after:
case mp
S : Stmt
s t : State
hseq : (S; Stmt.skip, s) ⟹ t
⊢ (S, s) ⟹ t

State before:
case mp
S : Stmt
s t : State
hseq : (S; Stmt.skip, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
cases hseq with
| seq _ _ _ u _ hS hs =>
  cases hs
  assumption
State after:
no goals

State before:
case mp.seq
S : Stmt
s t u : State
hS : (S, s) ⟹ u
hs : (Stmt.skip, u) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
cases hs
State after:
case mp.seq.skip
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t

State before:
case mp.seq.skip
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
assumption
State after:
no goals

State before:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Tactic:
intro h
State after:
case mpr
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S; Stmt.skip, s) ⟹ t

State before:
case mpr
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S; Stmt.skip, s) ⟹ t
Tactic:
apply BigStep.seq
State after:
case mpr.hS
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S, s) ⟹ ?mpr.t

case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, ?mpr.t) ⟹ t

case mpr.t
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ State

State before:
case mpr.hS
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S, s) ⟹ ?mpr.t

case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, ?mpr.t) ⟹ t

case mpr.t
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ State
Tactic:
{ assumption }
State after:
case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, t) ⟹ t

State before:
case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, t) ⟹ t
Tactic:
{ apply BigStep.skip }
State after:
no goals

State before:
case mpr.hS
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S, s) ⟹ ?mpr.t
Tactic:
assumption
State after:
no goals

State before:
case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, t) ⟹ t
Tactic:
apply BigStep.skip
State after:
no goals