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

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

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

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

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

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, 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 → (Stmt.skip; S, s) ⟹ t

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

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

State before:
case mp
S : Stmt
s t : State
hseq : (Stmt.skip; S, 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 : (Stmt.skip, s) ⟹ u
hS : (S, 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 → (Stmt.skip; S, s) ⟹ t
Tactic:
intro hS
State after:
case mpr
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (Stmt.skip; S, s) ⟹ t

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

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

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

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

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

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

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

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

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