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

State before:
⊢ (sillyLoop, State.update "x" 1 fun x => 0) ⟹ fun x => 0
Tactic:
rw [sillyLoop]
State after:
⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0) ⟹
    fun x => 0

State before:
⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" 1 fun x => 0) ⟹
    fun x => 0
Tactic:
apply BigStep.while_true
State after:
case hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"

case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State

State before:
case hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"

case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State
Tactic:
{ simp }
State after:
case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State

State before:
case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), ?t) ⟹ fun x => 0

case t

⊢ State
Tactic:
{ apply BigStep.seq
  { apply BigStep.skip }
  { apply BigStep.assign } }
State after:
case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⟹
    fun x => 0

State before:
case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⟹
    fun x => 0
Tactic:
{ simp
  apply BigStep.while_false
  simp }
State after:
no goals

State before:
case hcond

⊢ State.update "x" 1 (fun x => 0) "x" > State.update "x" 1 (fun x => 0) "y"
Tactic:
simp
State after:
no goals

State before:
case hbody

⊢ (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
Tactic:
apply BigStep.seq
State after:
case hbody.hS

⊢ (Stmt.skip, State.update "x" 1 fun x => 0) ⟹ ?hbody.t

case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, ?hbody.t) ⟹ ?t

case hbody.t

⊢ State

State before:
case hbody.hS

⊢ (Stmt.skip, State.update "x" 1 fun x => 0) ⟹ ?hbody.t

case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, ?hbody.t) ⟹ ?t

case hbody.t

⊢ State
Tactic:
{ apply BigStep.skip }
State after:
case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t

State before:
case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
Tactic:
{ apply BigStep.assign }
State after:
no goals

State before:
case hbody.hS

⊢ (Stmt.skip, State.update "x" 1 fun x => 0) ⟹ ?hbody.t
Tactic:
apply BigStep.skip
State after:
no goals

State before:
case hbody.hT

⊢ (Stmt.assign "x" fun s => s "x" - 1, State.update "x" 1 fun x => 0) ⟹ ?t
Tactic:
apply BigStep.assign
State after:
no goals

State before:
case hrest

⊢ (Stmt.whileDo (fun s => s "x" > s "y") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1),
      State.update "x" (State.update "x" 1 (fun x => 0) "x" - 1) (State.update "x" 1 fun x => 0)) ⟹
    fun x => 0
Tactic:
simp
State after:
case hrest

⊢ (Stmt.whileDo (fun s => s "y" < s "x") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), fun x => 0) ⟹ fun x => 0

State before:
case hrest

⊢ (Stmt.whileDo (fun s => s "y" < s "x") (Stmt.skip; Stmt.assign "x" fun s => s "x" - 1), fun x => 0) ⟹ fun x => 0
Tactic:
apply BigStep.while_false
State after:
case hrest.hcond

⊢ ¬0 < 0

State before:
case hrest.hcond

⊢ ¬0 < 0
Tactic:
simp
State after:
no goals