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

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

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

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

case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t
Tactic:
{ intro h
  cases h with
  | skip => rfl }
State after:
case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t

State before:
case mpr
s t : State
⊢ t = s → (Stmt.skip, s) ⟹ t
Tactic:
{ intro h
  rw [h]
  apply BigStep.skip }
State after:
no goals

State before:
case mp
s t : State
⊢ (Stmt.skip, s) ⟹ t → t = s
Tactic:
intro h
State after:
case mp
s t : State
h : (Stmt.skip, s) ⟹ t
⊢ t = s

State before:
case mp
s t : State
h : (Stmt.skip, s) ⟹ t
⊢ t = s
Tactic:
cases h with
| skip => rfl
State after:
no goals

State before:
case mp.skip
s : State
⊢ s = s
Tactic:
rfl
State after:
no goals

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

State before:
case mpr
s t : State
h : t = s
⊢ (Stmt.skip, s) ⟹ t
Tactic:
rw [h]
State after:
case mpr
s t : State
h : t = s
⊢ (Stmt.skip, s) ⟹ s

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