Week 6: Smallstep Semantics

Display all goals and responses

Author: Aurèle Barrière, Adam Chlipala, Benjamin C. Pierce
License: No redistribution allowed (usage by permission in CS-428).

Definitions from last week

We define a simple imperative language. It uses arithmetic expressions. We define notations and big-step semantics (eval).

Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).

Coercion Const : nat >-> arith.
Coercion Var : var >-> arith.
Infix "+" := Plus : arith_scope.Declaring a scope implicitly is deprecated; use in
advance an explicit "Declare Scope arith_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope.
Delimit Scope arith_scope with arith.

Definition valuation := var -> option nat.

Definition empty : valuation := fun _ => None.
Notation "$0" := (empty).

Definition get (x:var) (v:valuation) : option nat := v x.
Notation "v $? x" := (get x v) (at level 50, left associativity).

Definition set (x:var) (n:nat) (v:valuation) : valuation :=
  fun y =>
    match string_dec x y with
        | left H => Some n
        | right H' => get y v
    end.
Notation "v $+ ( x , k )" :=
  (set x k v) (at level 50, left associativity).

Fixpoint interp (e : arith) (v : valuation) : nat :=
  match e with
  | Const n => n
  | Var x =>
    match get x v with
    | None => 0
    | Some n => n
    end
  | Plus e1 e2 => interp e1 v + interp e2 v
  | Minus e1 e2 => interp e1 v - interp e2 v
  | Times e1 e2 => interp e1 v * interp e2 v
  end.

Module Simple.
  Inductive cmd :=
  | Skip
  | Assign (x : var) (e : arith)
  | Sequence (c1 c2 : cmd)
  | If (e : arith) (then_ else_ : cmd)
  | While (e : arith) (body : cmd).

Here are some notations for the language, which again we won't really explain.

  Notation "x <- e" := (Assign x e%arith) (at level 75).
  Infix ";;" := Sequence (at level 76).
  Notation "'when' e 'then' then_ 'else' else_ 'done'" :=
    (If e%arith then_ else_) (at level 75, e at level 0).Identifier 'when' now a keyword
Identifier 'done' now a keyword
  Notation "'while' e 'loop' body 'done'" :=
    (While e%arith body) (at level 75).Identifier 'while' now a keyword
Identifier 'loop' now a keyword

Here's an adaptation of our factorial example.

  Example factorial :=
    "output" <- 1;;
    while "input" loop
      "output" <- "output" * "input";;
      "input" <- "input" - 1
    done.

And the big-step semantics as an inductive proposition:

  Inductive eval : valuation -> cmd -> valuation -> Prop :=
  | EvalSkip : forall v,
    eval v Skip v
  | EvalAssign : forall v x e,
    eval v (Assign x e) (v $+ (x, interp e v))
  | EvalSeq : forall v c1 v1 c2 v2,
    eval v c1 v1
    -> eval v1 c2 v2
    -> eval v (Sequence c1 c2) v2
  | EvalIfTrue : forall v e then_ else_ v',
    interp e v <> 0
    -> eval v then_ v'
    -> eval v (If e then_ else_) v'
  | EvalIfFalse : forall v e then_ else_ v',
    interp e v = 0
    -> eval v else_ v'
    -> eval v (If e then_ else_) v'
  | EvalWhileTrue : forall v e body v' v'',
    interp e v <> 0
    -> eval v body v'
    -> eval v' (While e body) v''
    -> eval v (While e body) v''
  | EvalWhileFalse : forall v e body,
    interp e v = 0
    -> eval v (While e body) v.

Big-step semantics only tells us something about the behavior of terminating programs. Our imperative language clearly supports nontermination, thanks to the inclusion of general "while" loops. A switch to small-step semantics lets us also explain what happens with nonterminating executions, and this style will also come in handy for more advanced features like concurrency.

In general, the small-step style has the following advantages:

Defines a finer-grained "abstract machine", closer to real implementations
Extends smoothly to concurrent languages and languages with other sorts of computational effects.
Clearly separates divergence (nontermination) from being stuck (run-time error).

  Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
  | StepAssign : forall v x e,
    step (v, Assign x e) (v $+ (x, interp e v), Skip)
  | StepSeq1 : forall v c1 c2 v' c1',
    step (v, c1) (v', c1')
    -> step (v, Sequence c1 c2) (v', Sequence c1' c2)
  | StepSeq2 : forall v c2,
    step (v, Sequence Skip c2) (v, c2)
  | StepIfTrue : forall v e then_ else_,
    interp e v <> 0
    -> step (v, If e then_ else_) (v, then_)
  | StepIfFalse : forall v e then_ else_,
    interp e v = 0
    -> step (v, If e then_ else_) (v, else_)
  | StepWhileTrue : forall v e body,
    interp e v <> 0
    -> step (v, While e body) (v, Sequence body (While e body))
  | StepWhileFalse : forall v e body,
    interp e v = 0
    -> step (v, While e body) (v, Skip).

Next we define the multi-step relation, using the transitive reflexive closure of the step relation:

  Inductive trc {A:Type} {R:A -> A -> Prop}: A -> A -> Prop :=
  | TrcRefl : forall x, trc x x
  | TrcFront : forall x y z
    (STEP: R x y)
    (STAR: trc y z),
      trc x z.

  Notation "R ^*" := (@trc _ R) (at level 0).

Here we define some useful lemmas about valuation operations.

  Lemma gss:
    forall v x k, (v $+ (x,k)) $? x = Some k.forall (v : valuation) (x : var) (k : nat),
v $+ (x, k) $? x = Some k
  Proof.forall (v : valuation) (x : var) (k : nat),
v $+ (x, k) $? x = Some k
    intros v x k.v: valuation
x: var
k: nat
v $+ (x, k) $? x = Some k unfold get, set.v: valuation
x: var
k: nat
(if string_dec x x then Some k else v $? x) = Some k
    destruct string_dec; auto.v: valuation
x: var
k: nat
n: x <> x
v $? x = Some k contradiction.
  Qed.

  Lemma gso:
    forall v x y k, x <> y -> (v $+ (x,k)) $? y = v $? y.forall (v : valuation) (x y : var) (k : nat),
x <> y -> v $+ (x, k) $? y = v $? y
  Proof.forall (v : valuation) (x y : var) (k : nat),
x <> y -> v $+ (x, k) $? y = v $? y
    intros v x y k H.v: valuation
x, y: var
k: nat
H: x <> y
v $+ (x, k) $? y = v $? y unfold get, set.v: valuation
x, y: var
k: nat
H: x <> y
(if string_dec x y then Some k else v $? y) = v y destruct string_dec; auto.v: valuation
x, y: var
k: nat
H: x <> y
e: x = y
Some k = v y
    subst.v: valuation
y: var
k: nat
H: y <> y
Some k = v y contradiction.
  Qed.

And now we can show show our mall-step semantics relation evaluates:

  Theorem factorial_2_small :
    exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip)
         /\ v $? "output" = Some 2.exists v : valuation,
  (step) ^* ($0 $+ ("input", 2), factorial) (v, Skip) /\
  v $? "output" = Some 2
  Proof.exists v : valuation,
  (step) ^* ($0 $+ ("input", 2), factorial) (v, Skip) /\
  v $? "output" = Some 2
    eexists.(step) ^* ($0 $+ ("input", 2), factorial) (?v, Skip) /\
?v $? "output" = Some 2
    split.(step) ^* ($0 $+ ("input", 2), factorial) (?v, Skip)
?v $? "output" = Some 2
    -(step) ^* ($0 $+ ("input", 2), factorial) (?v, Skip) econstructor.step ($0 $+ ("input", 2), factorial) ?y
(step) ^* ?y (?v, Skip)
      {step ($0 $+ ("input", 2), factorial) ?y unfold factorial.step
  ($0 $+ ("input", 2),
   "output" <- 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y repeat econstructor. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output",
   interp 1 ($0 $+ ("input", 2))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output",
   interp 1 ($0 $+ ("input", 2))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output",
   interp 1 ($0 $+ ("input", 2))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y simpl.step
  ($0 $+ ("input", 2) $+ ("output", 1),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y apply StepSeq2. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y apply StepWhileTrue.interp "input" ($0 $+ ("input", 2) $+ ("output", 1)) <>
0 simpl.2 <> 0 lia. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1),
   ("output" <- "output" * "input";;
    "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1),
   ("output" <- "output" * "input";;
    "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1),
   ("output" <- "output" * "input";;
    "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y repeat econstructor. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))),
   (Skip;; "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))),
   (Skip;; "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))),
   (Skip;; "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))),
   Skip;; "input" <- "input" - 1) (?v', ?c1') apply StepSeq2. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))),
   "input" <- "input" - 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))),
   "input" <- "input" - 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))),
   "input" <- "input" - 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y repeat econstructor. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y apply StepSeq2. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y apply StepWhileTrue.interp "input"
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1)))))) <> 0 simpl.1 <> 0 lia. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   ("output" <- "output" * "input";;
    "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   ("output" <- "output" * "input";;
    "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))),
   ("output" <- "output" * "input";;
    "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y repeat econstructor. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))),
   (Skip;; "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))),
   (Skip;; "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))),
   (Skip;; "input" <- "input" - 1);;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))),
   Skip;; "input" <- "input" - 1) (?v', ?c1') apply StepSeq2. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))),
   "input" <- "input" - 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))),
   "input" <- "input" - 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))),
   "input" <- "input" - 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y repeat econstructor. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1))))))))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1))))))))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1))))))))),
   Skip;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y apply StepSeq2. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1))))))))),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) (?v, Skip)
      econstructor.step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1))))))))),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y
(step) ^* ?y (?v, Skip)
      {step
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1))))))))),
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?y apply StepWhileFalse.interp "input"
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1)))))))))) =
0 simpl.0 = 0 reflexivity. }(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))))) $+
   ("output",
   interp ("output" * "input")%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))))) $+
   ("input",
   interp ("input" - 1)%arith
     ($0 $+ ("input", 2) $+ ("output", 1) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1))) $+
      ("input",
      interp ("input" - 1)%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))))) $+
      ("output",
      interp ("output" * "input")%arith
        ($0 $+ ("input", 2) $+ ("output", 1) $+
         ("output",
         interp ("output" * "input")%arith
           ($0 $+ ("input", 2) $+ ("output", 1))) $+
         ("input",
         interp ("input" - 1)%arith
           ($0 $+ ("input", 2) $+ ("output", 1) $+
            ("output",
            interp ("output" * "input")%arith
              ($0 $+ ("input", 2) $+ ("output", 1))))))))),
   Skip) (?v, Skip)
      simpl.(step) ^*
  ($0 $+ ("input", 2) $+ ("output", 1) $+ ("output",
   2) $+ ("input", 1) $+ ("output", 2) $+ ("input", 0),
   Skip) (?v, Skip) constructor.
    -$0 $+ ("input", 2) $+ ("output", 1) $+ ("output", 2) $+
("input", 1) $+ ("output", 2) $+ ("input", 0) $?
"output" = Some 2 rewrite gso.$0 $+ ("input", 2) $+ ("output", 1) $+ ("output", 2) $+
("input", 1) $+ ("output", 2) $? "output" = Some 2
"input" <> "output"
      2: {"input" <> "output" unfold not."input" = "output" -> False intros H.H: "input" = "output"
False inversion H. }$0 $+ ("input", 2) $+ ("output", 1) $+ ("output", 2) $+
("input", 1) $+ ("output", 2) $? "output" = Some 2
      rewrite gss.Some 2 = Some 2 reflexivity.
  Qed.

Determinism

Each of the semantics (big-step and small-step) we have defined turn out to be deterministic. Let's prove it.

  Theorem eval_det :
    forall v c v1,
    eval v c v1 ->
    forall v2, eval v c v2 ->
          v1 = v2.forall (v : valuation) (c : cmd) (v1 : valuation),
eval v c v1 ->
forall v2 : valuation, eval v c v2 -> v1 = v2
  Proof.forall (v : valuation) (c : cmd) (v1 : valuation),
eval v c v1 ->
forall v2 : valuation, eval v c v2 -> v1 = v2
    intros v c v1 H.v: valuation
c: cmd
v1: valuation
H: eval v c v1
forall v2 : valuation, eval v c v2 -> v1 = v2 induction H; intros.v, v2: valuation
H: eval v Skip v2
v = v2
v: valuation
x: var
e: arith
v2: valuation
H: eval v (x <- e) v2
v $+ (x, interp e v) = v2
v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: forall v2 : valuation,
eval v c1 v2 -> v1 = v2
IHeval2: forall v3 : valuation,
eval v1 c2 v3 -> v2 = v3
v0: valuation
H1: eval v (c1;; c2) v0
v2 = v0
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: forall v2 : valuation,
eval v then_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
v' = v2
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: forall v2 : valuation,
eval v else_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
v' = v2
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: forall v2 : valuation,
eval v body v2 -> v' = v2
IHeval2: forall v2 : valuation,
eval v' (while e loop body done) v2 ->
v'' = v2
v2: valuation
H2: eval v (while e loop body done) v2
v'' = v2
v: valuation
e: arith
body: cmd
H: interp e v = 0
v2: valuation
H0: eval v (while e loop body done) v2
v = v2
    -v, v2: valuation
H: eval v Skip v2
v = v2 inversion H.v, v2: valuation
H: eval v Skip v2
v0: valuation
H0: v0 = v
H2: v = v2
v2 = v2 subst.v2: valuation
H: eval v2 Skip v2
v2 = v2 reflexivity.
    -v: valuation
x: var
e: arith
v2: valuation
H: eval v (x <- e) v2
v $+ (x, interp e v) = v2 inversion H.v: valuation
x: var
e: arith
v2: valuation
H: eval v (x <- e) v2
v0: valuation
x0: var
e0: arith
H0: v0 = v
H2: x0 = x
H3: e0 = e
H1: v $+ (x, interp e v) = v2
v $+ (x, interp e v) = v $+ (x, interp e v) subst.v: valuation
x: var
e: arith
H: eval v (x <- e) (v $+ (x, interp e v))
v $+ (x, interp e v) = v $+ (x, interp e v) reflexivity.
    -v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: forall v2 : valuation,
eval v c1 v2 -> v1 = v2
IHeval2: forall v3 : valuation,
eval v1 c2 v3 -> v2 = v3
v0: valuation
H1: eval v (c1;; c2) v0
v2 = v0 inversion H1.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: forall v2 : valuation,
eval v c1 v2 -> v1 = v2
IHeval2: forall v3 : valuation,
eval v1 c2 v3 -> v2 = v3
v0: valuation
H1: eval v (c1;; c2) v0
v3: valuation
c0: cmd
v4: valuation
c3: cmd
v5: valuation
H5: eval v c1 v4
H7: eval v4 c2 v0
H4: v3 = v
H2: c0 = c1
H3: c3 = c2
H6: v5 = v0
v2 = v0 subst.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: forall v2 : valuation,
eval v c1 v2 -> v1 = v2
IHeval2: forall v3 : valuation,
eval v1 c2 v3 -> v2 = v3
v0: valuation
H1: eval v (c1;; c2) v0
v4: valuation
H5: eval v c1 v4
H7: eval v4 c2 v0
v2 = v0
      apply IHeval1 in H5.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: forall v2 : valuation,
eval v c1 v2 -> v1 = v2
IHeval2: forall v3 : valuation,
eval v1 c2 v3 -> v2 = v3
v0: valuation
H1: eval v (c1;; c2) v0
v4: valuation
H5: v1 = v4
H7: eval v4 c2 v0
v2 = v0 subst.v: valuation
c1, c2: cmd
v2, v4: valuation
IHeval2: forall v3 : valuation,
eval v4 c2 v3 -> v2 = v3
IHeval1: forall v2 : valuation,
eval v c1 v2 -> v4 = v2
H0: eval v4 c2 v2
H: eval v c1 v4
v0: valuation
H1: eval v (c1;; c2) v0
H7: eval v4 c2 v0
v2 = v0 apply IHeval2 in H7.v: valuation
c1, c2: cmd
v2, v4: valuation
IHeval2: forall v3 : valuation,
eval v4 c2 v3 -> v2 = v3
IHeval1: forall v2 : valuation,
eval v c1 v2 -> v4 = v2
H0: eval v4 c2 v2
H: eval v c1 v4
v0: valuation
H1: eval v (c1;; c2) v0
H7: v2 = v0
v2 = v0 assumption.
    -v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: forall v2 : valuation,
eval v then_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
v' = v2 inversion H1; subst.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: forall v2 : valuation,
eval v then_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v <> 0
H8: eval v then_ v2
v' = v2
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: forall v2 : valuation,
eval v then_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v = 0
H8: eval v else_ v2
v' = v2
      +v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: forall v2 : valuation,
eval v then_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v <> 0
H8: eval v then_ v2
v' = v2 apply IHeval in H8.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: forall v2 : valuation,
eval v then_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v <> 0
H8: v' = v2
v' = v2 assumption.
      +v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: forall v2 : valuation,
eval v then_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v = 0
H8: eval v else_ v2
v' = v2 contradiction.
    -v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: forall v2 : valuation,
eval v else_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
v' = v2 inversion H1; subst.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: forall v2 : valuation,
eval v else_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v <> 0
H8: eval v then_ v2
v' = v2
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: forall v2 : valuation,
eval v else_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v = 0
H8: eval v else_ v2
v' = v2
      +v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: forall v2 : valuation,
eval v else_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v <> 0
H8: eval v then_ v2
v' = v2 contradiction.
      +v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: forall v2 : valuation,
eval v else_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v = 0
H8: eval v else_ v2
v' = v2 apply IHeval in H8.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: forall v2 : valuation,
eval v else_ v2 -> v' = v2
v2: valuation
H1: eval v (when e then then_ else else_ done) v2
H7: interp e v = 0
H8: v' = v2
v' = v2 assumption.
    -v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: forall v2 : valuation,
eval v body v2 -> v' = v2
IHeval2: forall v2 : valuation,
eval v' (while e loop body done) v2 ->
v'' = v2
v2: valuation
H2: eval v (while e loop body done) v2
v'' = v2 inversion H2; subst.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: forall v2 : valuation,
eval v body v2 -> v' = v2
IHeval2: forall v2 : valuation,
eval v' (while e loop body done) v2 ->
v'' = v2
v2: valuation
H2: eval v (while e loop body done) v2
v'0: valuation
H5: interp e v <> 0
H7: eval v body v'0
H9: eval v'0 (while e loop body done) v2
v'' = v2
e: arith
body: cmd
v', v'', v2: valuation
H2: eval v2 (while e loop body done) v2
H0: eval v2 body v'
H: interp e v2 <> 0
H1: eval v' (while e loop body done) v''
IHeval1: forall v3 : valuation,
eval v2 body v3 -> v' = v3
IHeval2: forall v2 : valuation,
eval v' (while e loop body done) v2 ->
v'' = v2
H7: interp e v2 = 0
v'' = v2
      +v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: forall v2 : valuation,
eval v body v2 -> v' = v2
IHeval2: forall v2 : valuation,
eval v' (while e loop body done) v2 ->
v'' = v2
v2: valuation
H2: eval v (while e loop body done) v2
v'0: valuation
H5: interp e v <> 0
H7: eval v body v'0
H9: eval v'0 (while e loop body done) v2
v'' = v2 apply IHeval1 in H7.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: forall v2 : valuation,
eval v body v2 -> v' = v2
IHeval2: forall v2 : valuation,
eval v' (while e loop body done) v2 ->
v'' = v2
v2: valuation
H2: eval v (while e loop body done) v2
v'0: valuation
H5: interp e v <> 0
H7: v' = v'0
H9: eval v'0 (while e loop body done) v2
v'' = v2 subst.v: valuation
e: arith
body: cmd
v'': valuation
H: interp e v <> 0
v'0: valuation
IHeval2: forall v2 : valuation,
eval v'0 (while e loop body done) v2 ->
v'' = v2
IHeval1: forall v2 : valuation,
eval v body v2 -> v'0 = v2
H1: eval v'0 (while e loop body done) v''
H0: eval v body v'0
v2: valuation
H2: eval v (while e loop body done) v2
H5: interp e v <> 0
H9: eval v'0 (while e loop body done) v2
v'' = v2
        apply IHeval2 in H9.v: valuation
e: arith
body: cmd
v'': valuation
H: interp e v <> 0
v'0: valuation
IHeval2: forall v2 : valuation,
eval v'0 (while e loop body done) v2 ->
v'' = v2
IHeval1: forall v2 : valuation,
eval v body v2 -> v'0 = v2
H1: eval v'0 (while e loop body done) v''
H0: eval v body v'0
v2: valuation
H2: eval v (while e loop body done) v2
H5: interp e v <> 0
H9: v'' = v2
v'' = v2 assumption.
      +e: arith
body: cmd
v', v'', v2: valuation
H2: eval v2 (while e loop body done) v2
H0: eval v2 body v'
H: interp e v2 <> 0
H1: eval v' (while e loop body done) v''
IHeval1: forall v3 : valuation,
eval v2 body v3 -> v' = v3
IHeval2: forall v2 : valuation,
eval v' (while e loop body done) v2 ->
v'' = v2
H7: interp e v2 = 0
v'' = v2 contradiction.
    -v: valuation
e: arith
body: cmd
H: interp e v = 0
v2: valuation
H0: eval v (while e loop body done) v2
v = v2 inversion H0; subst.v: valuation
e: arith
body: cmd
H: interp e v = 0
v2: valuation
H0: eval v (while e loop body done) v2
v': valuation
H3: interp e v <> 0
H5: eval v body v'
H7: eval v' (while e loop body done) v2
v = v2
e: arith
body: cmd
v2: valuation
H0: eval v2 (while e loop body done) v2
H, H5: interp e v2 = 0
v2 = v2
      +v: valuation
e: arith
body: cmd
H: interp e v = 0
v2: valuation
H0: eval v (while e loop body done) v2
v': valuation
H3: interp e v <> 0
H5: eval v body v'
H7: eval v' (while e loop body done) v2
v = v2 contradiction.
      +e: arith
body: cmd
v2: valuation
H0: eval v2 (while e loop body done) v2
H, H5: interp e v2 = 0
v2 = v2 reflexivity.
  Qed.

  Theorem step_det :
    forall s out1,
    step s out1 ->
    forall out2, step s out2 ->
            out1 = out2.forall s out1 : valuation * cmd,
step s out1 ->
forall out2 : valuation * cmd,
step s out2 -> out1 = out2
  Proof.forall s out1 : valuation * cmd,
step s out1 ->
forall out2 : valuation * cmd,
step s out2 -> out1 = out2
    intros s out1 H.s, out1: (valuation * cmd)%type
H: step s out1
forall out2 : valuation * cmd,
step s out2 -> out1 = out2 induction H; intros.v: valuation
x: var
e: arith
out2: (valuation * cmd)%type
H: step (v, x <- e) out2
(v $+ (x, interp e v), Skip) = out2
v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall out2 : valuation * cmd,
step (v, c1) out2 -> (v', c1') = out2
out2: (valuation * cmd)%type
H0: step (v, c1;; c2) out2
(v', c1';; c2) = out2
v: valuation
c2: cmd
out2: (valuation * cmd)%type
H: step (v, Skip;; c2) out2
(v, c2) = out2
v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
out2: (valuation * cmd)%type
H0: step (v, when e then then_ else else_ done) out2
(v, then_) = out2
v: valuation
e: arith
then_, else_: cmd
H: interp e v = 0
out2: (valuation * cmd)%type
H0: step (v, when e then then_ else else_ done) out2
(v, else_) = out2
v: valuation
e: arith
body: cmd
H: interp e v <> 0
out2: (valuation * cmd)%type
H0: step (v, while e loop body done) out2
(v, body;; while e loop body done) = out2
v: valuation
e: arith
body: cmd
H: interp e v = 0
out2: (valuation * cmd)%type
H0: step (v, while e loop body done) out2
(v, Skip) = out2
    -v: valuation
x: var
e: arith
out2: (valuation * cmd)%type
H: step (v, x <- e) out2
(v $+ (x, interp e v), Skip) = out2 inversion H.v: valuation
x: var
e: arith
out2: (valuation * cmd)%type
H: step (v, x <- e) out2
v0: valuation
x0: var
e0: arith
H1: v0 = v
H2: x0 = x
H3: e0 = e
H0: (v $+ (x, interp e v), Skip) = out2
(v $+ (x, interp e v), Skip) =
(v $+ (x, interp e v), Skip) subst.v: valuation
x: var
e: arith
H: step (v, x <- e) (v $+ (x, interp e v), Skip)
(v $+ (x, interp e v), Skip) =
(v $+ (x, interp e v), Skip) constructor.
    -v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall out2 : valuation * cmd,
step (v, c1) out2 -> (v', c1') = out2
out2: (valuation * cmd)%type
H0: step (v, c1;; c2) out2
(v', c1';; c2) = out2 inversion H0; subst.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall out2 : valuation * cmd,
step (v, c1) out2 -> (v', c1') = out2
v'0: valuation
c1'0: cmd
H0: step (v, c1;; c2) (v'0, c1'0;; c2)
H5: step (v, c1) (v'0, c1'0)
(v', c1';; c2) = (v'0, c1'0;; c2)
v: valuation
c2: cmd
v': valuation
c1': cmd
IHstep: forall out2 : valuation * cmd,
step (v, Skip) out2 -> (v', c1') = out2
H: step (v, Skip) (v', c1')
H0: step (v, Skip;; c2) (v, c2)
(v', c1';; c2) = (v, c2)
      +v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall out2 : valuation * cmd,
step (v, c1) out2 -> (v', c1') = out2
v'0: valuation
c1'0: cmd
H0: step (v, c1;; c2) (v'0, c1'0;; c2)
H5: step (v, c1) (v'0, c1'0)
(v', c1';; c2) = (v'0, c1'0;; c2) apply IHstep in H5.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall out2 : valuation * cmd,
step (v, c1) out2 -> (v', c1') = out2
v'0: valuation
c1'0: cmd
H0: step (v, c1;; c2) (v'0, c1'0;; c2)
H5: (v', c1') = (v'0, c1'0)
(v', c1';; c2) = (v'0, c1'0;; c2) inversion H5.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall out2 : valuation * cmd,
step (v, c1) out2 -> (v', c1') = out2
v'0: valuation
c1'0: cmd
H0: step (v, c1;; c2) (v'0, c1'0;; c2)
H5: (v', c1') = (v'0, c1'0)
H2: v' = v'0
H3: c1' = c1'0
(v'0, c1'0;; c2) = (v'0, c1'0;; c2) subst.v: valuation
c1, c2: cmd
v'0: valuation
c1'0: cmd
H: step (v, c1) (v'0, c1'0)
IHstep: forall out2 : valuation * cmd,
step (v, c1) out2 -> (v'0, c1'0) = out2
H0: step (v, c1;; c2) (v'0, c1'0;; c2)
H5: (v'0, c1'0) = (v'0, c1'0)
(v'0, c1'0;; c2) = (v'0, c1'0;; c2) reflexivity.
      +v: valuation
c2: cmd
v': valuation
c1': cmd
IHstep: forall out2 : valuation * cmd,
step (v, Skip) out2 -> (v', c1') = out2
H: step (v, Skip) (v', c1')
H0: step (v, Skip;; c2) (v, c2)
(v', c1';; c2) = (v, c2) inversion H.
    -v: valuation
c2: cmd
out2: (valuation * cmd)%type
H: step (v, Skip;; c2) out2
(v, c2) = out2 inversion H; subst.v: valuation
c2: cmd
v': valuation
c1': cmd
H: step (v, Skip;; c2) (v', c1';; c2)
H4: step (v, Skip) (v', c1')
(v, c2) = (v', c1';; c2)
v: valuation
c2: cmd
H: step (v, Skip;; c2) (v, c2)
(v, c2) = (v, c2)
      +v: valuation
c2: cmd
v': valuation
c1': cmd
H: step (v, Skip;; c2) (v', c1';; c2)
H4: step (v, Skip) (v', c1')
(v, c2) = (v', c1';; c2) inversion H4.
      +v: valuation
c2: cmd
H: step (v, Skip;; c2) (v, c2)
(v, c2) = (v, c2) reflexivity.
    -v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
out2: (valuation * cmd)%type
H0: step (v, when e then then_ else else_ done) out2
(v, then_) = out2 inversion H0; subst.v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
H0: step (v, when e then then_ else else_ done)
  (v, then_)
H6: interp e v <> 0
(v, then_) = (v, then_)
v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
H0: step (v, when e then then_ else else_ done)
  (v, else_)
H6: interp e v = 0
(v, then_) = (v, else_)
      +v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
H0: step (v, when e then then_ else else_ done)
  (v, then_)
H6: interp e v <> 0
(v, then_) = (v, then_) reflexivity.
      +v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
H0: step (v, when e then then_ else else_ done)
  (v, else_)
H6: interp e v = 0
(v, then_) = (v, else_) contradiction.
    -v: valuation
e: arith
then_, else_: cmd
H: interp e v = 0
out2: (valuation * cmd)%type
H0: step (v, when e then then_ else else_ done) out2
(v, else_) = out2 inversion H0; subst; try contradiction.v: valuation
e: arith
then_, else_: cmd
H: interp e v = 0
H0: step (v, when e then then_ else else_ done)
  (v, else_)
H6: interp e v = 0
(v, else_) = (v, else_) reflexivity.
    -v: valuation
e: arith
body: cmd
H: interp e v <> 0
out2: (valuation * cmd)%type
H0: step (v, while e loop body done) out2
(v, body;; while e loop body done) = out2 inversion H0; subst; try contradiction.v: valuation
e: arith
body: cmd
H: interp e v <> 0
H0: step (v, while e loop body done)
  (v, body;; while e loop body done)
H5: interp e v <> 0
(v, body;; while e loop body done) =
(v, body;; while e loop body done) reflexivity.
    -v: valuation
e: arith
body: cmd
H: interp e v = 0
out2: (valuation * cmd)%type
H0: step (v, while e loop body done) out2
(v, Skip) = out2 inversion H0; subst; try contradiction.v: valuation
e: arith
body: cmd
H: interp e v = 0
H0: step (v, while e loop body done) (v, Skip)
H5: interp e v = 0
(v, Skip) = (v, Skip) reflexivity.
  Qed.

Bonus question: step is deterministic. Is the multi-step relation step^* also deterministic? No! Since it relates the original state to every reachable state.

  Lemma trc_nondet:
    step^* ($0, Skip;;Skip) ($0, Skip;; Skip) /\
      step^* ($0, Skip;;Skip) ($0, Skip).(step) ^* ($0, Skip;; Skip) ($0, Skip;; Skip) /\
(step) ^* ($0, Skip;; Skip) ($0, Skip)
  Proof.(step) ^* ($0, Skip;; Skip) ($0, Skip;; Skip) /\
(step) ^* ($0, Skip;; Skip) ($0, Skip)
    split.(step) ^* ($0, Skip;; Skip) ($0, Skip;; Skip)
(step) ^* ($0, Skip;; Skip) ($0, Skip)
    -(step) ^* ($0, Skip;; Skip) ($0, Skip;; Skip) apply TrcRefl.
    -(step) ^* ($0, Skip;; Skip) ($0, Skip) eapply TrcFront.step ($0, Skip;; Skip) ?y
(step) ^* ?y ($0, Skip) apply StepSeq2.(step) ^* ($0, Skip) ($0, Skip) apply TrcRefl.
  Qed.

This might feel underwhelming: did we change this notion of determinism while going from big-step to small-step? Sure, we get local non-determinism, but what if we want to talk about the final value reached by the program? We will see below that we can define a similar lemma for the multi-step relation and reason about these final values.

Strong Progress

In fact, we have another interesting property of this small-step semantics. Any program that is not Skip should reduce to something. This is a strong property, either a state is in a final state (a syntactical property) or it can progress (a semantic property). In other words, the semantics cannot get stuck. This is called strong progress to differentiate it from a weaker property, as this version is often too strong for more complex languages. We'll see more about this when talking about typed languages.

  Theorem strong_progress_step:
    forall v c,
      c = Skip \/ exists v' c', step (v, c) (v', c').forall (v : valuation) (c : cmd),
c = Skip \/
(exists (v' : valuation) (c' : cmd),
   step (v, c) (v', c'))
  Proof.forall (v : valuation) (c : cmd),
c = Skip \/
(exists (v' : valuation) (c' : cmd),
   step (v, c) (v', c'))
    intros v c.v: valuation
c: cmd
c = Skip \/
(exists (v' : valuation) (c' : cmd),
   step (v, c) (v', c')) induction c.v: valuation
Skip = Skip \/
(exists (v' : valuation) (c' : cmd),
   step (v, Skip) (v', c'))
v: valuation
x: var
e: arith
(x <- e) = Skip \/
(exists (v' : valuation) (c' : cmd),
   step (v, x <- e) (v', c'))
v: valuation
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
(c1;; c2) = Skip \/
(exists (v' : valuation) (c' : cmd),
   step (v, c1;; c2) (v', c'))
v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
(when e then c1 else c2 done) = Skip \/
(exists (v' : valuation) 
 (c' : cmd),
   step (v, when e then c1 else c2 done) (v', c'))
v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
(while e loop c done) = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, while e loop c done) (v', c')) 1:left.v: valuation
Skip = Skip
v: valuation
x: var
e: arith
(x <- e) = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, x <- e) (v', c'))
v: valuation
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
(c1;; c2) = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1;; c2) (v', c'))
v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
(when e then c1 else c2 done) = Skip \/
(exists (v' : valuation) 
 (c' : cmd),
   step (v, when e then c1 else c2 done) (v', c'))
v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
(while e loop c done) = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, while e loop c done) (v', c')) all:try right.v: valuation
Skip = Skip
v: valuation
x: var
e: arith
exists (v' : valuation) (c' : cmd),
  step (v, x <- e) (v', c')
v: valuation
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, c1;; c2) (v', c')
v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, when e then c1 else c2 done) (v', c')
v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, while e loop c done) (v', c')
    -v: valuation
Skip = Skip reflexivity.
    -v: valuation
x: var
e: arith
exists (v' : valuation) (c' : cmd),
  step (v, x <- e) (v', c') eexists.v: valuation
x: var
e: arith
exists c' : cmd, step (v, x <- e) (?v', c') eexists.v: valuation
x: var
e: arith
step (v, x <- e) (?v', ?c') constructor.
    -v: valuation
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, c1;; c2) (v', c') destruct IHc1 as [H | [v' [c' H]]].v: valuation
c1, c2: cmd
H: c1 = Skip
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, c1;; c2) (v', c')
v: valuation
c1, c2: cmd
v': valuation
c': cmd
H: step (v, c1) (v', c')
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, c1;; c2) (v', c')
      +v: valuation
c1, c2: cmd
H: c1 = Skip
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, c1;; c2) (v', c') subst.v: valuation
c2: cmd
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, Skip;; c2) (v', c') eexists.v: valuation
c2: cmd
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists c' : cmd, step (v, Skip;; c2) (?v', c') eexists.v: valuation
c2: cmd
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
step (v, Skip;; c2) (?v', ?c') apply StepSeq2.
      +v: valuation
c1, c2: cmd
v': valuation
c': cmd
H: step (v, c1) (v', c')
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, c1;; c2) (v', c') eexists.v: valuation
c1, c2: cmd
v': valuation
c': cmd
H: step (v, c1) (v', c')
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists c'0 : cmd, step (v, c1;; c2) (?v', c'0) eexists.v: valuation
c1, c2: cmd
v': valuation
c': cmd
H: step (v, c1) (v', c')
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
step (v, c1;; c2) (?v', ?c') apply StepSeq1.v: valuation
c1, c2: cmd
v': valuation
c': cmd
H: step (v, c1) (v', c')
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
step (v, c1) (?v', ?c1') apply H.
    -v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, when e then c1 else c2 done) (v', c') destruct (interp e v =? 0)%nat eqn:Hcond.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = true
exists (v' : valuation) (c' : cmd),
  step (v, when e then c1 else c2 done) (v', c')
v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = false
exists (v' : valuation) (c' : cmd),
  step (v, when e then c1 else c2 done) (v', c')
      (* if we forget eqn:, we forget what we destroyed *)
      +v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = true
exists (v' : valuation) (c' : cmd),
  step (v, when e then c1 else c2 done) (v', c') eexists.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = true
exists c' : cmd,
  step (v, when e then c1 else c2 done) (?v', c') eexists.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = true
step (v, when e then c1 else c2 done) (?v', ?c')
        apply StepIfFalse.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = true
interp e v = 0 rewrite Nat.eqb_eq in Hcond.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: interp e v = 0
interp e v = 0 assumption.
      +v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = false
exists (v' : valuation) (c' : cmd),
  step (v, when e then c1 else c2 done) (v', c') eexists.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = false
exists c' : cmd,
  step (v, when e then c1 else c2 done) (?v', c') eexists.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = false
step (v, when e then c1 else c2 done) (?v', ?c')
        (* if we did eexists before destruct, what would happen? *)
        apply StepIfTrue.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: (interp e v =? 0)%nat = false
interp e v <> 0 rewrite Nat.eqb_neq in Hcond.v: valuation
e: arith
c1, c2: cmd
IHc1: c1 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c1) (v', c'))
IHc2: c2 = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c2) (v', c'))
Hcond: interp e v <> 0
interp e v <> 0 assumption.
    -v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
exists (v' : valuation) (c' : cmd),
  step (v, while e loop c done) (v', c') destruct (interp e v =? 0)%nat eqn:Hguard.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = true
exists (v' : valuation) (c' : cmd),
  step (v, while e loop c done) (v', c')
v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = false
exists (v' : valuation) (c' : cmd),
  step (v, while e loop c done) (v', c')
      +v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = true
exists (v' : valuation) (c' : cmd),
  step (v, while e loop c done) (v', c') eexists.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = true
exists c' : cmd,
  step (v, while e loop c done) (?v', c') eexists.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = true
step (v, while e loop c done) (?v', ?c')
        apply StepWhileFalse.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = true
interp e v = 0 rewrite Nat.eqb_eq in Hguard.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: interp e v = 0
interp e v = 0 assumption.
      +v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = false
exists (v' : valuation) (c' : cmd),
  step (v, while e loop c done) (v', c') eexists.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = false
exists c' : cmd,
  step (v, while e loop c done) (?v', c') eexists.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = false
step (v, while e loop c done) (?v', ?c')
        apply StepWhileTrue.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: (interp e v =? 0)%nat = false
interp e v <> 0 rewrite Nat.eqb_neq in Hguard.v: valuation
e: arith
c: cmd
IHc: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
Hguard: interp e v <> 0
interp e v <> 0 assumption.
  Qed.

More precisely, we say that such irreducible states of the small-step semantics are normal forms.

  Definition normal_form {A:Type} (R:A -> A-> Prop) (a:A) : Prop :=
    ~ exists a', R a a'.

With strong progress, we have actually proven that normal forms are exactly states where the command is Skip. This relates a semantic property (being a normal form) to a syntactical one (being Skip).

  Theorem skip_normal_form:
    forall v c,
      c = Skip <-> normal_form step (v,c).forall (v : valuation) (c : cmd),
c = Skip <-> normal_form step (v, c)
  Proof.forall (v : valuation) (c : cmd),
c = Skip <-> normal_form step (v, c)
    intros v c.v: valuation
c: cmd
c = Skip <-> normal_form step (v, c) split; intros.v: valuation
c: cmd
H: c = Skip
normal_form step (v, c)
v: valuation
c: cmd
H: normal_form step (v, c)
c = Skip
    -v: valuation
c: cmd
H: c = Skip
normal_form step (v, c) subst.v: valuation
normal_form step (v, Skip) unfold normal_form, not.v: valuation
(exists a' : valuation * cmd, step (v, Skip) a') ->
False intros [s' STEP].v: valuation
s': (valuation * cmd)%type
STEP: step (v, Skip) s'
False inversion STEP.
    -v: valuation
c: cmd
H: normal_form step (v, c)
c = Skip unfold normal_form, not in H.v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
c = Skip
      specialize (strong_progress_step v c) as STRONG.v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
STRONG: c = Skip \/
(exists (v' : valuation) 
 (c' : cmd), step (v, c) (v', c'))
c = Skip
      destruct STRONG as [SKIP | [v' [c' STEP]]].v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
SKIP: c = Skip
c = Skip
v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
v': valuation
c': cmd
STEP: step (v, c) (v', c')
c = Skip
      +v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
SKIP: c = Skip
c = Skip assumption.
      +v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
v': valuation
c': cmd
STEP: step (v, c) (v', c')
c = Skip exfalso. (* replaces the current goal with false *)v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
v': valuation
c': cmd
STEP: step (v, c) (v', c')
False
        apply H.v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
v': valuation
c': cmd
STEP: step (v, c) (v', c')
exists a' : valuation * cmd, step (v, c) a' exists (v', c').v: valuation
c: cmd
H: (exists a' : valuation * cmd, step (v, c) a') ->
False
v': valuation
c': cmd
STEP: step (v, c) (v', c')
step (v, c) (v', c') assumption.
  Qed.

Now that we have identified the final values of our small-step semantics, we can use it to rephrase the determinism property of the multi-step relation: a program should only evaluate to a single final value!

This should not only be true for step^*, but also for the transitive reflexive closure of any dterministic relation.

  Lemma trc_nf:
    forall A (R:A -> A -> Prop) a a'
      (STAR: R^* a a')
      (NF: normal_form R a),
      a' = a.forall (A : Type) (R : A -> A -> Prop) (a a' : A),
(R) ^* a a' -> normal_form R a -> a' = a
  Proof.forall (A : Type) (R : A -> A -> Prop) (a a' : A),
(R) ^* a a' -> normal_form R a -> a' = a
    intros A R a a' STAR NF.A: Type
R: A -> A -> Prop
a, a': A
STAR: (R) ^* a a'
NF: normal_form R a
a' = a unfold normal_form in NF.A: Type
R: A -> A -> Prop
a, a': A
STAR: (R) ^* a a'
NF: ~ (exists a' : A, R a a')
a' = a
    destruct STAR.A: Type
R: A -> A -> Prop
x: A
NF: ~ (exists a' : A, R x a')
x = x
A: Type
R: A -> A -> Prop
x, y, z: A
STEP: R x y
STAR: (R) ^* y z
NF: ~ (exists a' : A, R x a')
z = x
    -A: Type
R: A -> A -> Prop
x: A
NF: ~ (exists a' : A, R x a')
x = x reflexivity.
    -A: Type
R: A -> A -> Prop
x, y, z: A
STEP: R x y
STAR: (R) ^* y z
NF: ~ (exists a' : A, R x a')
z = x exfalso.A: Type
R: A -> A -> Prop
x, y, z: A
STEP: R x y
STAR: (R) ^* y z
NF: ~ (exists a' : A, R x a')
False apply NF.A: Type
R: A -> A -> Prop
x, y, z: A
STEP: R x y
STAR: (R) ^* y z
NF: ~ (exists a' : A, R x a')
exists a' : A, R x a' exists y.A: Type
R: A -> A -> Prop
x, y, z: A
STEP: R x y
STAR: (R) ^* y z
NF: ~ (exists a' : A, R x a')
R x y assumption.
  Qed.


  Theorem trc_determinism:
    forall A (R:A -> A -> Prop)
      (RDET: forall a a1 a2, R a a1 -> R a a2 -> a1 = a2)
      (s f1 f2: A)
      (STAR1: R^* s f1)
      (NF1: normal_form R f1)
      (STAR2: R^* s f2)
      (NF2: normal_form R f2),
      f1 = f2.forall (A : Type) (R : A -> A -> Prop),
(forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2) ->
forall s f1 f2 : A,
(R) ^* s f1 ->
normal_form R f1 ->
(R) ^* s f2 -> normal_form R f2 -> f1 = f2
  Proof.forall (A : Type) (R : A -> A -> Prop),
(forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2) ->
forall s f1 f2 : A,
(R) ^* s f1 ->
normal_form R f1 ->
(R) ^* s f2 -> normal_form R f2 -> f1 = f2
    intros A R RDET s f1 f2 STAR1 NF1 STAR2 NF2.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
s, f1, f2: A
STAR1: (R) ^* s f1
NF1: normal_form R f1
STAR2: (R) ^* s f2
NF2: normal_form R f2
f1 = f2
    induction STAR1.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
f2, x: A
NF1: normal_form R x
STAR2: (R) ^* x f2
NF2: normal_form R f2
x = f2
A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
f2, x, y, z: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
STAR2: (R) ^* x f2
NF2: normal_form R f2
IHSTAR1: normal_form R z -> (R) ^* y f2 -> z = f2
z = f2
    -A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
f2, x: A
NF1: normal_form R x
STAR2: (R) ^* x f2
NF2: normal_form R f2
x = f2 apply trc_nf in STAR2; try assumption.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
f2, x: A
NF1: normal_form R x
STAR2: f2 = x
NF2: normal_form R f2
x = f2 subst.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
x: A
NF1, NF2: normal_form R x
x = x reflexivity.
    -A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
f2, x, y, z: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
STAR2: (R) ^* x f2
NF2: normal_form R f2
IHSTAR1: normal_form R z -> (R) ^* y f2 -> z = f2
z = f2 destruct STAR2.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
y, z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
NF2: normal_form R x
IHSTAR1: normal_form R z -> (R) ^* y x -> z = x
z = x
A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
y, z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
y0, z0: A
STEP0: R x y0
STAR2: (R) ^* y0 z0
NF2: normal_form R z0
IHSTAR1: normal_form R z -> (R) ^* y z0 -> z = z0
z = z0
      +A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
y, z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
NF2: normal_form R x
IHSTAR1: normal_form R z -> (R) ^* y x -> z = x
z = x exfalso.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
y, z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
NF2: normal_form R x
IHSTAR1: normal_form R z -> (R) ^* y x -> z = x
False apply NF2.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
y, z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
NF2: normal_form R x
IHSTAR1: normal_form R z -> (R) ^* y x -> z = x
exists a' : A, R x a' eexists.A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
y, z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
NF2: normal_form R x
IHSTAR1: normal_form R z -> (R) ^* y x -> z = x
R x ?a' eapply STEP.
      +A: Type
R: A -> A -> Prop
RDET: forall a a1 a2 : A, R a a1 -> R a a2 -> a1 = a2
y, z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
y0, z0: A
STEP0: R x y0
STAR2: (R) ^* y0 z0
NF2: normal_form R z0
IHSTAR1: normal_form R z -> (R) ^* y z0 -> z = z0
z = z0 specialize (RDET _ _ _ STEP STEP0).A: Type
R: A -> A -> Prop
y, y0: A
RDET: y = y0
z, x: A
STEP: R x y
STAR1: (R) ^* y z
NF1: normal_form R z
z0: A
STEP0: R x y0
STAR2: (R) ^* y0 z0
NF2: normal_form R z0
IHSTAR1: normal_form R z -> (R) ^* y z0 -> z = z0
z = z0 subst.A: Type
R: A -> A -> Prop
y0, z, x: A
STAR1: (R) ^* y0 z
STEP: R x y0
NF1: normal_form R z
z0: A
STEP0: R x y0
STAR2: (R) ^* y0 z0
NF2: normal_form R z0
IHSTAR1: normal_form R z -> (R) ^* y0 z0 -> z = z0
z = z0
        apply IHSTAR1; assumption.
  Qed.

  Corollary multistep_determinism :
    forall v c vf1 vf2
      (STAR1: step^* (v,c) (vf1, Skip))
      (STAR2: step^* (v,c) (vf2, Skip)),
      vf1 = vf2.forall (v : valuation) (c : cmd) (vf1 vf2 : valuation),
(step) ^* (v, c) (vf1, Skip) ->
(step) ^* (v, c) (vf2, Skip) -> vf1 = vf2
  Proof.forall (v : valuation) (c : cmd) (vf1 vf2 : valuation),
(step) ^* (v, c) (vf1, Skip) ->
(step) ^* (v, c) (vf2, Skip) -> vf1 = vf2
    intros v c vf1 vf2 STAR1 STAR2.v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
vf1 = vf2
    assert ((vf1, Skip) = (vf2,Skip)).v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
(vf1, Skip) = (vf2, Skip)
v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
H: (vf1, Skip) = (vf2, Skip)
vf1 = vf2
    {v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
(vf1, Skip) = (vf2, Skip) eapply trc_determinism with (R:=step).v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
forall a a1 a2 : valuation * cmd,
step a a1 -> step a a2 -> a1 = a2
v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
(step) ^* ?s (vf1, Skip)
v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
normal_form step (vf1, Skip)
v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
(step) ^* ?s (vf2, Skip)
v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
normal_form step (vf2, Skip)
      -v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
forall a a1 a2 : valuation * cmd,
step a a1 -> step a a2 -> a1 = a2 intros a a1 a2 H H0.v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
a, a1, a2: (valuation * cmd)%type
H: step a a1
H0: step a a2
a1 = a2 eapply step_det.v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
a, a1, a2: (valuation * cmd)%type
H: step a a1
H0: step a a2
step ?s0 a1
v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
a, a1, a2: (valuation * cmd)%type
H: step a a1
H0: step a a2
step ?s0 a2 apply H.v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
a, a1, a2: (valuation * cmd)%type
H: step a a1
H0: step a a2
step a a2 apply H0.
      -v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
(step) ^* ?s (vf1, Skip) apply STAR1.
      -v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
normal_form step (vf1, Skip) rewrite <- skip_normal_form.v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
Skip = Skip reflexivity.
      -v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
(step) ^* (v, c) (vf2, Skip) apply STAR2.
      -v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
normal_form step (vf2, Skip) rewrite <- skip_normal_form.v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
Skip = Skip reflexivity. }v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
H: (vf1, Skip) = (vf2, Skip)
vf1 = vf2
    inversion H.v: valuation
c: cmd
vf1, vf2: valuation
STAR1: (step) ^* (v, c) (vf1, Skip)
STAR2: (step) ^* (v, c) (vf2, Skip)
H: (vf1, Skip) = (vf2, Skip)
H1: vf1 = vf2
vf2 = vf2 reflexivity.
  Qed.

Normalization

We've seen that our small-step semantics is both deterministic and has strong progress. We can wonder now if this language is normalizing, meaning that every program eventually reaches a normal form. Is this true of this language? No! Because of possible non-termination.

  Example infinite :=
    while (Const 1) loop
      Skip
    done.

  Lemma infinite_loop:
    forall v start send,
      start = (v, infinite) \/ start = (v, Skip;;infinite) ->
      step ^* start send ->
      send = (v,infinite) \/ send = (v, Skip;;infinite).forall (v : valuation) (start send : valuation * cmd),
start = (v, infinite) \/ start = (v, Skip;; infinite) ->
(step) ^* start send ->
send = (v, infinite) \/ send = (v, Skip;; infinite)
  Proof.forall (v : valuation) (start send : valuation * cmd),
start = (v, infinite) \/ start = (v, Skip;; infinite) ->
(step) ^* start send ->
send = (v, infinite) \/ send = (v, Skip;; infinite)
    intros v start send H H0.v: valuation
start, send: (valuation * cmd)%type
H: start = (v, infinite) \/
start = (v, Skip;; infinite)
H0: (step) ^* start send
send = (v, infinite) \/ send = (v, Skip;; infinite) induction H0.v: valuation
x: (valuation * cmd)%type
H: x = (v, infinite) \/ x = (v, Skip;; infinite)
x = (v, infinite) \/ x = (v, Skip;; infinite)
v: valuation
x: (valuation * cmd)%type
H: x = (v, infinite) \/ x = (v, Skip;; infinite)
y, z: (valuation * cmd)%type
STEP: step x y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
z = (v, infinite) \/ z = (v, Skip;; infinite)
    -v: valuation
x: (valuation * cmd)%type
H: x = (v, infinite) \/ x = (v, Skip;; infinite)
x = (v, infinite) \/ x = (v, Skip;; infinite) assumption.
    -v: valuation
x: (valuation * cmd)%type
H: x = (v, infinite) \/ x = (v, Skip;; infinite)
y, z: (valuation * cmd)%type
STEP: step x y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
z = (v, infinite) \/ z = (v, Skip;; infinite) apply IHtrc.v: valuation
x: (valuation * cmd)%type
H: x = (v, infinite) \/ x = (v, Skip;; infinite)
y, z: (valuation * cmd)%type
STEP: step x y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
y = (v, infinite) \/ y = (v, Skip;; infinite) destruct H; subst.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
y = (v, infinite) \/ y = (v, Skip;; infinite)
v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, Skip;; infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
y = (v, infinite) \/ y = (v, Skip;; infinite)
      +v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
y = (v, infinite) \/ y = (v, Skip;; infinite) right.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
y = (v, Skip;; infinite) eapply step_det.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
step ?s y
v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
step ?s (v, Skip;; infinite) apply STEP.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
step (v, infinite) (v, Skip;; infinite) constructor.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
interp 1 v <> 0 simpl.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
1 <> 0 lia.
      +v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, Skip;; infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
y = (v, infinite) \/ y = (v, Skip;; infinite) left.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, Skip;; infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
y = (v, infinite) eapply step_det.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, Skip;; infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
step ?s y
v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, Skip;; infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
step ?s (v, infinite) apply STEP.v: valuation
y, z: (valuation * cmd)%type
STEP: step (v, Skip;; infinite) y
H0: (step) ^* y z
IHtrc: y = (v, infinite) \/ y = (v, Skip;; infinite) ->
z = (v, infinite) \/ z = (v, Skip;; infinite)
step (v, Skip;; infinite) (v, infinite) constructor.
  Qed.

  Theorem not_normalizing:
    ~ (forall s,
        exists sfinal, step^* s sfinal /\ normal_form step sfinal).~
(forall s : valuation * cmd,
 exists sfinal : valuation * cmd,
   (step) ^* s sfinal /\ normal_form step sfinal)
  Proof.~
(forall s : valuation * cmd,
 exists sfinal : valuation * cmd,
   (step) ^* s sfinal /\ normal_form step sfinal)
    unfold not.(forall s : valuation * cmd,
 exists sfinal : valuation * cmd,
   (step) ^* s sfinal /\ normal_form step sfinal) ->
False intros H.H: forall s : valuation * cmd,
exists sfinal : valuation * cmd,
  (step) ^* s sfinal /\ normal_form step sfinal
False
    specialize (H ($0,infinite)).H: exists sfinal : valuation * cmd,
  (step) ^* ($0, infinite) sfinal /\
  normal_form step sfinal
False
    destruct H as [[vfinal cfinal] [STAR NF]].vfinal: valuation
cfinal: cmd
STAR: (step) ^* ($0, infinite) (vfinal, cfinal)
NF: normal_form step (vfinal, cfinal)
False
    eapply infinite_loop in STAR.vfinal: valuation
cfinal: cmd
NF: normal_form step (vfinal, cfinal)
STAR: (vfinal, cfinal) = (?v, infinite) \/
(vfinal, cfinal) = (?v, Skip;; infinite)
False
vfinal: valuation
cfinal: cmd
STAR: (step) ^* ($0, infinite) (vfinal, cfinal)
NF: normal_form step (vfinal, cfinal)
($0, infinite) = (?v, infinite) \/
($0, infinite) = (?v, Skip;; infinite)
    2: {vfinal: valuation
cfinal: cmd
STAR: (step) ^* ($0, infinite) (vfinal, cfinal)
NF: normal_form step (vfinal, cfinal)
($0, infinite) = (?v, infinite) \/
($0, infinite) = (?v, Skip;; infinite) left.vfinal: valuation
cfinal: cmd
STAR: (step) ^* ($0, infinite) (vfinal, cfinal)
NF: normal_form step (vfinal, cfinal)
($0, infinite) = (?v, infinite) reflexivity. }vfinal: valuation
cfinal: cmd
NF: normal_form step (vfinal, cfinal)
STAR: (vfinal, cfinal) = ($0, infinite) \/
(vfinal, cfinal) = ($0, Skip;; infinite)
False
    rewrite <- skip_normal_form in NF.vfinal: valuation
cfinal: cmd
NF: cfinal = Skip
STAR: (vfinal, cfinal) = ($0, infinite) \/
(vfinal, cfinal) = ($0, Skip;; infinite)
False subst.vfinal: valuation
STAR: (vfinal, Skip) = ($0, infinite) \/
(vfinal, Skip) = ($0, Skip;; infinite)
False
    destruct STAR; inversion H.
  Qed.

Bonus question: what would be wrong if we tried to prove not_normalizing directly by induction on H ?

Big-step / Small-step Equivalence

We have seen two styles of defining semantics for the same language. Each has their own advantages. It also turns out that these two semantics styles are equivalent. Let's prove it.

First, we need some intermediate lemmas.

  Lemma multi_step_trans:
    forall v1 c1 v2 c2 v3 c3
      (STAR1: step^* (v1,c1) (v2,c2))
      (STAR2: step^* (v2,c2) (v3,c3)),
      step^* (v1,c1) (v3,c3).forall (v1 : valuation) (c1 : cmd) (v2 : valuation)
  (c2 : cmd) (v3 : valuation) (c3 : cmd),
(step) ^* (v1, c1) (v2, c2) ->
(step) ^* (v2, c2) (v3, c3) ->
(step) ^* (v1, c1) (v3, c3)
  Proof.forall (v1 : valuation) (c1 : cmd) (v2 : valuation)
  (c2 : cmd) (v3 : valuation) (c3 : cmd),
(step) ^* (v1, c1) (v2, c2) ->
(step) ^* (v2, c2) (v3, c3) ->
(step) ^* (v1, c1) (v3, c3)
    intros v1 c1 v2 c2 v3 c3 STAR1 STAR2.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
STAR1: (step) ^* (v1, c1) (v2, c2)
STAR2: (step) ^* (v2, c2) (v3, c3)
(step) ^* (v1, c1) (v3, c3) induction STAR1; auto.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* x (v3, c3)
    econstructor.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
step x ?y
v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* ?y (v3, c3) apply STEP.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* y (v3, c3)
    apply IHSTAR1.v1: valuation
c1: cmd
v2: valuation
c2: cmd
v3: valuation
c3: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
STAR1: (step) ^* y z
STAR2: (step) ^* z (v3, c3)
IHSTAR1: (step) ^* z (v3, c3) -> (step) ^* y (v3, c3)
(step) ^* z (v3, c3) assumption.
  Qed.

  Lemma step_star_Seq1 :
    forall s1 s2 c,
    step^* s1 s2 ->
    step^* (fst s1, Sequence (snd s1) c) (fst s2, Sequence (snd s2) c).forall (s1 s2 : valuation * cmd) (c : cmd),
(step) ^* s1 s2 ->
(step) ^* (fst s1, snd s1;; c) (fst s2, snd s2;; c)
  Proof.forall (s1 s2 : valuation * cmd) (c : cmd),
(step) ^* s1 s2 ->
(step) ^* (fst s1, snd s1;; c) (fst s2, snd s2;; c)
    intros s1 s2 c H.s1, s2: (valuation * cmd)%type
c: cmd
H: (step) ^* s1 s2
(step) ^* (fst s1, snd s1;; c) (fst s2, snd s2;; c)
    induction H.c: cmd
x: (valuation * cmd)%type
(step) ^* (fst x, snd x;; c) (fst x, snd x;; c)
c: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c)
  (fst z, snd z;; c)
(step) ^* (fst x, snd x;; c) (fst z, snd z;; c)
    -c: cmd
x: (valuation * cmd)%type
(step) ^* (fst x, snd x;; c) (fst x, snd x;; c) constructor.
    -c: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c)
  (fst z, snd z;; c)
(step) ^* (fst x, snd x;; c) (fst z, snd z;; c) destruct y.c: cmd
x: (valuation * cmd)%type
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
(step) ^* (fst x, snd x;; c) (fst z, snd z;; c) econstructor.c: cmd
x: (valuation * cmd)%type
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst x, snd x;; c) ?y
c: cmd
x: (valuation * cmd)%type
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
(step) ^* ?y (fst z, snd z;; c)
      2: {c: cmd
x: (valuation * cmd)%type
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
(step) ^* ?y (fst z, snd z;; c) eapply IHtrc. }c: cmd
x: (valuation * cmd)%type
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst x, snd x;; c) (fst (v, c0), snd (v, c0);; c)
      constructor.c: cmd
x: (valuation * cmd)%type
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step x (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst x, snd x) (fst (v, c0), snd (v, c0)) destruct x.c: cmd
v0: valuation
c1: cmd
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step (v0, c1) (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (fst (v0, c1), snd (v0, c1))
  (fst (v, c0), snd (v, c0)) simpl.c: cmd
v0: valuation
c1: cmd
v: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step (v0, c1) (v, c0)
H: (step) ^* (v, c0) z
IHtrc: (step) ^* (fst (v, c0), snd (v, c0);; c)
  (fst z, snd z;; c)
step (v0, c1) (v, c0) assumption.
  Qed.

This works well, but why did we state the theorem using fst and snd instead of giving a name to each element of each state? That would have been a more straightforward statement.

This is once again because induction is going to forget about some much needed equalities. We will look at three possible solutions:

State the theorems on pairs and use fst and snd as shown above.
Use the remember tactic as we saw two weeks ago.
Use the dependent induction tactic which generalizes as much as possible. See the reference manual for more details and examples.

  Lemma step_star_Seq_remember : forall v c1 c2 v' c1',
      step^* (v, c1) (v', c1')
      -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).forall (v : valuation) (c1 c2 : cmd) (v' : valuation)
  (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)
  Proof.forall (v : valuation) (c1 c2 : cmd) (v' : valuation)
  (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)
    intros v c1 c2 v' c1' H.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: (step) ^* (v, c1) (v', c1')
(step) ^* (v, c1;; c2) (v', c1';; c2)
    remember (v, c1) as x.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: (valuation * cmd)%type
Heqx: x = (v, c1)
H: (step) ^* x (v', c1')
(step) ^* (v, c1;; c2) (v', c1';; c2)
    remember (v', c1') as y.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: (valuation * cmd)%type
Heqx: x = (v, c1)
y: (valuation * cmd)%type
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (v, c1;; c2) (v', c1';; c2)
    replace v with (fst x) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: (valuation * cmd)%type
Heqx: x = (v, c1)
y: (valuation * cmd)%type
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, c1;; c2) (v', c1';; c2)
    replace v' with (fst y) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: (valuation * cmd)%type
Heqx: x = (v, c1)
y: (valuation * cmd)%type
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, c1;; c2) (fst y, c1';; c2)
    replace c1 with (snd x) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: (valuation * cmd)%type
Heqx: x = (v, c1)
y: (valuation * cmd)%type
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, snd x;; c2) (fst y, c1';; c2)
    replace c1' with (snd y) by (subst;auto).v: valuation
c1, c2: cmd
v': valuation
c1': cmd
x: (valuation * cmd)%type
Heqx: x = (v, c1)
y: (valuation * cmd)%type
Heqy: y = (v', c1')
H: (step) ^* x y
(step) ^* (fst x, snd x;; c2) (fst y, snd y;; c2)
    (* if we don't clear we don't get the right induction! *)
    clear v v' c1 c1' Heqx Heqy.c2: cmd
x, y: (valuation * cmd)%type
H: (step) ^* x y
(step) ^* (fst x, snd x;; c2) (fst y, snd y;; c2)
    induction H; subst.c2: cmd
x: (valuation * cmd)%type
(step) ^* (fst x, snd x;; c2) (fst x, snd x;; c2)
c2: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2)
  (fst z, snd z;; c2)
(step) ^* (fst x, snd x;; c2) (fst z, snd z;; c2)
    -c2: cmd
x: (valuation * cmd)%type
(step) ^* (fst x, snd x;; c2) (fst x, snd x;; c2) constructor.
    -c2: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2)
  (fst z, snd z;; c2)
(step) ^* (fst x, snd x;; c2) (fst z, snd z;; c2) econstructor.c2: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2)
  (fst z, snd z;; c2)
step (fst x, snd x;; c2) ?y
c2: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2)
  (fst z, snd z;; c2)
(step) ^* ?y (fst z, snd z;; c2)
      2: apply IHtrc.c2: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2)
  (fst z, snd z;; c2)
step (fst x, snd x;; c2) (fst y, snd y;; c2)
      constructor.c2: cmd
x, y, z: (valuation * cmd)%type
STEP: step x y
H: (step) ^* y z
IHtrc: (step) ^* (fst y, snd y;; c2)
  (fst z, snd z;; c2)
step (fst x, snd x) (fst y, snd y) destruct x, y.c2: cmd
v: valuation
c: cmd
v0: valuation
c0: cmd
z: (valuation * cmd)%type
STEP: step (v, c) (v0, c0)
H: (step) ^* (v0, c0) z
IHtrc: (step) ^* (fst (v0, c0), snd (v0, c0);; c2)
  (fst z, snd z;; c2)
step (fst (v, c), snd (v, c))
  (fst (v0, c0), snd (v0, c0)) assumption.
  Qed.

Not very convenient. Let's look at the dependent induction tactic.

  Require Import Coq.Program.Equality.Use of “Require” inside a module is fragile. It is not
recommended to use this functionality in finished
proof scripts. [require-in-module,fragile,default]

  Lemma step_star_Seq : forall v c1 c2 v' c1',
    step^* (v, c1) (v', c1')
    -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).forall (v : valuation) (c1 c2 : cmd) (v' : valuation)
  (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)
  Proof.forall (v : valuation) (c1 c2 : cmd) (v' : valuation)
  (c1' : cmd),
(step) ^* (v, c1) (v', c1') ->
(step) ^* (v, c1;; c2) (v', c1';; c2)
    intros.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: (step) ^* (v, c1) (v', c1')
(step) ^* (v, c1;; c2) (v', c1';; c2)
    dependent induction H.c2: cmd
v': valuation
c1': cmd
(step) ^* (v', c1';; c2) (v', c1';; c2)
c2: cmd
v: valuation
c1: cmd
y: (valuation * cmd)%type
v': valuation
c1': cmd
STEP: step (v, c1) y
H: (step) ^* y (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
y = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* (v, c1;; c2) (v', c1';; c2)
    -c2: cmd
v': valuation
c1': cmd
(step) ^* (v', c1';; c2) (v', c1';; c2) constructor.
    -c2: cmd
v: valuation
c1: cmd
y: (valuation * cmd)%type
v': valuation
c1': cmd
STEP: step (v, c1) y
H: (step) ^* y (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
y = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* (v, c1;; c2) (v', c1';; c2) destruct y.c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* (v, c1;; c2) (v', c1';; c2) econstructor.c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
step (v, c1;; c2) ?y
c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* ?y (v', c1';; c2)
      2: {c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
(step) ^* ?y (v', c1';; c2) eapply IHtrc; reflexivity. }c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
step (v, c1;; c2) (v0, c;; c2)
      constructor.c2: cmd
v: valuation
c1: cmd
v0: valuation
c: cmd
v': valuation
c1': cmd
STEP: step (v, c1) (v0, c)
H: (step) ^* (v0, c) (v', c1')
IHtrc: forall (v : valuation) (c1 : cmd)
  (v'0 : valuation) (c1'0 : cmd),
(v0, c) = (v, c1) ->
(v', c1') = (v'0, c1'0) ->
(step) ^* (v, c1;; c2) (v'0, c1'0;; c2)
step (v, c1) (v0, c)  assumption.
  Qed.

We can now resume our proof. First, let's show that a big-step reduction implies a multi-step small-step reduction to a final state.

  Theorem big_small :
    forall v c v',
      eval v c v' ->
      step^* (v, c) (v', Skip).forall (v : valuation) (c : cmd) (v' : valuation),
eval v c v' -> (step) ^* (v, c) (v', Skip)
  Proof.forall (v : valuation) (c : cmd) (v' : valuation),
eval v c v' -> (step) ^* (v, c) (v', Skip)
    intros v c v' H.v: valuation
c: cmd
v': valuation
H: eval v c v'
(step) ^* (v, c) (v', Skip) induction H.v: valuation
(step) ^* (v, Skip) (v, Skip)
v: valuation
x: var
e: arith
(step) ^* (v, x <- e) (v $+ (x, interp e v), Skip)
v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1) (v1, Skip)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (v2, Skip)
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip)
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip)
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, while e loop body done) (v'', Skip)
v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* (v, while e loop body done) (v, Skip)
    -v: valuation
(step) ^* (v, Skip) (v, Skip) constructor.
    -v: valuation
x: var
e: arith
(step) ^* (v, x <- e) (v $+ (x, interp e v), Skip) econstructor; constructor.
    -v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1) (v1, Skip)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (v2, Skip) apply step_star_Seq with (c2:=c2) in IHeval1.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (v2, Skip)
      eapply multi_step_trans.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v, c1;; c2) (?v2, ?c2)
v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (?v2, ?c2) (v2, Skip) apply IHeval1.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v1, Skip;; c2) (v2, Skip)
      econstructor.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
step (v1, Skip;; c2) ?y
v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* ?y (v2, Skip) apply StepSeq2.v: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H: eval v c1 v1
H0: eval v1 c2 v2
IHeval1: (step) ^* (v, c1;; c2) (v1, Skip;; c2)
IHeval2: (step) ^* (v1, c2) (v2, Skip)
(step) ^* (v1, c2) (v2, Skip) assumption.
    -v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip) econstructor.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
step (v, when e then then_ else else_ done) ?y
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* ?y (v', Skip)
      {v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
step (v, when e then then_ else else_ done) ?y apply StepIfTrue.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
interp e v <> 0 assumption. }v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v <> 0
H0: eval v then_ v'
IHeval: (step) ^* (v, then_) (v', Skip)
(step) ^* (v, then_) (v', Skip)
      assumption.
    -v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* (v, when e then then_ else else_ done)
  (v', Skip) econstructor.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
step (v, when e then then_ else else_ done) ?y
v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* ?y (v', Skip)
      {v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
step (v, when e then then_ else else_ done) ?y apply StepIfFalse.v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
interp e v = 0 assumption. }v: valuation
e: arith
then_, else_: cmd
v': valuation
H: interp e v = 0
H0: eval v else_ v'
IHeval: (step) ^* (v, else_) (v', Skip)
(step) ^* (v, else_) (v', Skip)
      assumption.
    -v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, while e loop body done) (v'', Skip) econstructor.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
step (v, while e loop body done) ?y
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* ?y (v'', Skip)
      {v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
step (v, while e loop body done) ?y apply StepWhileTrue.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
interp e v <> 0 assumption. }v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (v'', Skip)
      eapply multi_step_trans.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (?v2, ?c2)
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (?v2, ?c2) (v'', Skip)
      2: {v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (?v2, ?c2) (v'', Skip) apply IHeval2. }v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (v', while e loop body done)
      eapply multi_step_trans.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (?v2, ?c2)
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (?v2, ?c2) (v', while e loop body done)
      {v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, body;; while e loop body done)
  (?v2, ?c2) apply step_star_Seq.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v, body) (?v2, ?c1') apply IHeval1. }v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v', Skip;; while e loop body done)
  (v', while e loop body done)
      econstructor.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
step (v', Skip;; while e loop body done) ?y
v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* ?y (v', while e loop body done) apply StepSeq2.v: valuation
e: arith
body: cmd
v', v'': valuation
H: interp e v <> 0
H0: eval v body v'
H1: eval v' (while e loop body done) v''
IHeval1: (step) ^* (v, body) (v', Skip)
IHeval2: (step) ^* (v', while e loop body done)
  (v'', Skip)
(step) ^* (v', while e loop body done)
  (v', while e loop body done) constructor.
    -v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* (v, while e loop body done) (v, Skip) econstructor.v: valuation
e: arith
body: cmd
H: interp e v = 0
step (v, while e loop body done) ?y
v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* ?y (v, Skip)
      {v: valuation
e: arith
body: cmd
H: interp e v = 0
step (v, while e loop body done) ?y apply StepWhileFalse.v: valuation
e: arith
body: cmd
H: interp e v = 0
interp e v = 0 assumption. }v: valuation
e: arith
body: cmd
H: interp e v = 0
(step) ^* (v, Skip) (v, Skip)
      constructor.
  Qed.

Now for the other direction, we start at the level of the fine-grain step then work our way to the multi-step relation.

  Lemma small_big_fs: forall x y,
      step x y ->
      forall v', eval (fst y) (snd y) v' ->
            eval (fst x) (snd x) v'.forall x y : valuation * cmd,
step x y ->
forall v' : valuation,
eval (fst y) (snd y) v' -> eval (fst x) (snd x) v'
  Proof.forall x y : valuation * cmd,
step x y ->
forall v' : valuation,
eval (fst y) (snd y) v' -> eval (fst x) (snd x) v'
    intros x y H.x, y: (valuation * cmd)%type
H: step x y
forall v' : valuation,
eval (fst y) (snd y) v' -> eval (fst x) (snd x) v' induction H; intros; simpl in *.v: valuation
x: var
e: arith
v': valuation
H: eval (v $+ (x, interp e v)) Skip v'
eval v (x <- e) v'
v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
eval v (c1;; c2) v'0
v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v (Skip;; c2) v'
v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
v': valuation
H0: eval v then_ v'
eval v (when e then then_ else else_ done) v'
v: valuation
e: arith
then_, else_: cmd
H: interp e v = 0
v': valuation
H0: eval v else_ v'
eval v (when e then then_ else else_ done) v'
v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
eval v (while e loop body done) v'
v: valuation
e: arith
body: cmd
H: interp e v = 0
v': valuation
H0: eval v Skip v'
eval v (while e loop body done) v'
    -v: valuation
x: var
e: arith
v': valuation
H: eval (v $+ (x, interp e v)) Skip v'
eval v (x <- e) v' inversion H.v: valuation
x: var
e: arith
v': valuation
H: eval (v $+ (x, interp e v)) Skip v'
v0: valuation
H0: v0 = v $+ (x, interp e v)
H2: v $+ (x, interp e v) = v'
eval v (x <- e) (v $+ (x, interp e v)) subst.v: valuation
x: var
e: arith
H: eval (v $+ (x, interp e v)) Skip
  (v $+ (x, interp e v))
eval v (x <- e) (v $+ (x, interp e v)) constructor.
    -v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
eval v (c1;; c2) v'0 inversion H0.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v0: valuation
c0: cmd
v1: valuation
c3: cmd
v2: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
H3: v0 = v'
H1: c0 = c1'
H2: c3 = c2
H5: v2 = v'0
eval v (c1;; c2) v'0 subst.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v (c1;; c2) v'0 econstructor.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v c1 ?v1
v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval ?v1 c2 v'0
      +v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v c1 ?v1 apply IHstep.v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v' c1' ?v1 eassumption.
      +v: valuation
c1, c2: cmd
v': valuation
c1': cmd
H: step (v, c1) (v', c1')
IHstep: forall v'0 : valuation,
eval v' c1' v'0 -> eval v c1 v'0
v'0: valuation
H0: eval v' (c1';; c2) v'0
v1: valuation
H4: eval v' c1' v1
H6: eval v1 c2 v'0
eval v1 c2 v'0 assumption.
    -v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v (Skip;; c2) v' econstructor.v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v Skip ?v1
v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval ?v1 c2 v' constructor.v: valuation
c2: cmd
v': valuation
H: eval v c2 v'
eval v c2 v' assumption.
    -v: valuation
e: arith
then_, else_: cmd
H: interp e v <> 0
v': valuation
H0: eval v then_ v'
eval v (when e then then_ else else_ done) v' constructor; assumption.
    -v: valuation
e: arith
then_, else_: cmd
H: interp e v = 0
v': valuation
H0: eval v else_ v'
eval v (when e then then_ else else_ done) v' apply EvalIfFalse; assumption.
    -v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
eval v (while e loop body done) v' inversion H0.v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
v0: valuation
c1: cmd
v1: valuation
c2: cmd
v2: valuation
H4: eval v body v1
H6: eval v1 (while e loop body done) v'
H3: v0 = v
H1: c1 = body
H2: c2 = (while e loop body done)
H5: v2 = v'
eval v (while e loop body done) v' subst.v: valuation
e: arith
body: cmd
H: interp e v <> 0
v': valuation
H0: eval v (body;; while e loop body done) v'
v1: valuation
H4: eval v body v1
H6: eval v1 (while e loop body done) v'
eval v (while e loop body done) v' econstructor; eassumption.
    -v: valuation
e: arith
body: cmd
H: interp e v = 0
v': valuation
H0: eval v Skip v'
eval v (while e loop body done) v' inversion H0.v: valuation
e: arith
body: cmd
H: interp e v = 0
v': valuation
H0: eval v Skip v'
v0: valuation
H1: v0 = v
H3: v = v'
eval v' (while e loop body done) v' subst.e: arith
body: cmd
v': valuation
H0: eval v' Skip v'
H: interp e v' = 0
eval v' (while e loop body done) v' apply EvalWhileFalse.e: arith
body: cmd
v': valuation
H0: eval v' Skip v'
H: interp e v' = 0
interp e v' = 0 assumption.
  Qed.

  Lemma small_big'' : forall v c v' c',
      step (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''
  Proof.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''
    intros v c v' c' H v'' H0.v: valuation
c: cmd
v': valuation
c': cmd
H: step (v, c) (v', c')
v'': valuation
H0: eval v' c' v''
eval v c v''
    eapply small_big_fs in H; simpl.v: valuation
c: cmd
v': valuation
c': cmd
v'': valuation
H0: eval v' c' v''
H: eval (fst (v, c)) (snd (v, c)) ?v'
eval v c v''
v: valuation
c: cmd
v': valuation
c': cmd
H: step (v, c) (v', c')
v'': valuation
H0: eval v' c' v''
eval v' c' ?v' 2: eassumption.v: valuation
c: cmd
v': valuation
c': cmd
v'': valuation
H0: eval v' c' v''
H: eval (fst (v, c)) (snd (v, c)) v''
eval v c v''
    simpl in H.v: valuation
c: cmd
v': valuation
c': cmd
v'': valuation
H0: eval v' c' v''
H: eval v c v''
eval v c v'' assumption.
  Qed.

  Lemma small_big' :
    forall v c v' c',
      step^* (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
(step) ^* (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''
  Proof.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
(step) ^* (v, c) (v', c') ->
forall v'' : valuation, eval v' c' v'' -> eval v c v''
    intros v c v' c' H.v: valuation
c: cmd
v': valuation
c': cmd
H: (step) ^* (v, c) (v', c')
forall v'' : valuation, eval v' c' v'' -> eval v c v''
    dependent induction H; intros; try assumption.v: valuation
c: cmd
y: (valuation * cmd)%type
v': valuation
c': cmd
STEP: step (v, c) y
H: (step) ^* y (v', c')
IHtrc: forall (v : valuation) (c : cmd)
  (v'0 : valuation) (c'0 : cmd),
y = (v, c) ->
(v', c') = (v'0, c'0) ->
forall v'' : valuation,
eval v'0 c'0 v'' -> eval v c v''
v'': valuation
H0: eval v' c' v''
eval v c v''
    destruct y.v: valuation
c: cmd
v0: valuation
c0: cmd
v': valuation
c': cmd
STEP: step (v, c) (v0, c0)
H: (step) ^* (v0, c0) (v', c')
IHtrc: forall (v : valuation) (c : cmd)
  (v'0 : valuation) (c'0 : cmd),
(v0, c0) = (v, c) ->
(v', c') = (v'0, c'0) ->
forall v'' : valuation,
eval v'0 c'0 v'' -> eval v c v''
v'': valuation
H0: eval v' c' v''
eval v c v'' eapply IHtrc in H0; auto.v: valuation
c: cmd
v0: valuation
c0: cmd
v': valuation
c': cmd
STEP: step (v, c) (v0, c0)
H: (step) ^* (v0, c0) (v', c')
IHtrc: forall (v : valuation) (c : cmd)
  (v'0 : valuation) (c'0 : cmd),
(v0, c0) = (v, c) ->
(v', c') = (v'0, c'0) ->
forall v'' : valuation,
eval v'0 c'0 v'' -> eval v c v''
v'': valuation
H0: eval v0 c0 v''
eval v c v''
    eapply small_big''; eauto.
  Qed.

  Theorem small_big :
    forall v c v',
       step^* (v, c) (v', Skip) ->
       eval v c v'.forall (v : valuation) (c : cmd) (v' : valuation),
(step) ^* (v, c) (v', Skip) -> eval v c v'
  Proof.forall (v : valuation) (c : cmd) (v' : valuation),
(step) ^* (v, c) (v', Skip) -> eval v c v'
    intros v c v' H.v: valuation
c: cmd
v': valuation
H: (step) ^* (v, c) (v', Skip)
eval v c v' eapply small_big'; eauto.v: valuation
c: cmd
v': valuation
H: (step) ^* (v, c) (v', Skip)
eval v' Skip v' constructor.
  Qed.

Contextual small-step semantics

There is a common way to factor a small-step semantics into different parts, to make the semantics easier to understand and extend. First, we define a notion of evaluation contexts, which are commands with holes in them.

  Inductive context :=
  | Hole
  | CSeq (C : context) (c : cmd).

This relation explains how to plug the hole in a context with a specific term. Note that we use an inductive relation instead of a recursive definition, because Coq's proof automation is better at working with relations.

  Inductive plug : context -> cmd -> cmd -> Prop :=
  | PlugHole : forall c, plug Hole c c
  | PlugSeq : forall c C c' c2,
    plug C c c'
    -> plug (CSeq C c2) c (Sequence c' c2).

Now we define almost the same step relation as before, with one omission: only the more trivial of the [Sequence] rules remains. This simplifies all other rules, which do not need c2 anymore.

  Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
  | Step0Assign : forall v x e,
    step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
  | Step0Seq : forall v c2,
    step0 (v, Sequence Skip c2) (v, c2)
  | Step0IfTrue : forall v e then_ else_,
    interp e v <> 0
    -> step0 (v, If e then_ else_) (v, then_)
  | Step0IfFalse : forall v e then_ else_,
    interp e v = 0
    -> step0 (v, If e then_ else_) (v, else_)
  | Step0WhileTrue : forall v e body,
    interp e v <> 0
    -> step0 (v, While e body) (v, Sequence body (While e body))
  | Step0WhileFalse : forall v e body,
    interp e v = 0
    -> step0 (v, While e body) (v, Skip).

We recover the meaning of the original with one top-level rule, combining plugging of contexts with basic steps.

  Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
  | CStep : forall C v c v' c' c1 c2,
      plug C c c1 ->
      step0 (v, c) (v', c') ->
      plug C c' c2 ->
      cstep (v, c1) (v', c2).

We can prove equivalence between the two formulations.

  Theorem step_cstep :
    forall v c v' c',
    step (v, c) (v', c') ->
    cstep (v, c) (v', c').forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step (v, c) (v', c') -> cstep (v, c) (v', c')
  Proof.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step (v, c) (v', c') -> cstep (v, c) (v', c')
    intros v c v' c' H.v: valuation
c: cmd
v': valuation
c': cmd
H: step (v, c) (v', c')
cstep (v, c) (v', c') induction H.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
cstep (v0, x <- e) (v0 $+ (x, interp e v0), Skip)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
cstep (v0, c1;; c2) (v'0, c1';; c2)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c2: cmd
cstep (v0, Skip;; c2) (v0, c2)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 <> 0
cstep (v0, when e then then_ else else_ done)
  (v0, then_)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
cstep (v0, when e then then_ else else_ done)
  (v0, else_)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 <> 0
cstep (v0, while e loop body done)
  (v0, body;; while e loop body done)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
cstep (v0, while e loop body done) (v0, Skip)
    -v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
cstep (v0, x <- e) (v0 $+ (x, interp e v0), Skip) eapply CStep.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
plug ?C ?c (x <- e)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
step0 (v0, ?c) (v0 $+ (x, interp e v0), ?c')
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
plug ?C ?c' Skip
      2: constructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
plug ?C (x <- e) (x <- e)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
plug ?C Skip Skip apply PlugHole.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
x: var
e: arith
plug Hole Skip Skip apply PlugHole.
    -v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
cstep (v0, c1;; c2) (v'0, c1';; c2) inversion IHstep.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
v1: valuation
c0: cmd
v'1: valuation
c'0, c3, c4: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
H0: v1 = v0
H1: c3 = c1
H2: v'1 = v'0
H3: c4 = c1'
cstep (v0, c1;; c2) (v'0, c1';; c2) subst.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
cstep (v0, c1;; c2) (v'0, c1';; c2) econstructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug ?C ?c (c1;; c2)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
step0 (v0, ?c) (v'0, ?c')
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug ?C ?c' (c1';; c2) 2: apply H5.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug ?C c0 (c1;; c2)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug ?C c'0 (c1';; c2)
      apply PlugSeq.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug ?C c0 c1
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug (CSeq ?C c2) c'0 (c1';; c2) apply H4.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug (CSeq C c2) c'0 (c1';; c2) constructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c1, c2: cmd
v'0: valuation
c1': cmd
H: step (v0, c1) (v'0, c1')
IHstep: cstep (v0, c1) (v'0, c1')
C: context
c0, c'0: cmd
H4: plug C c0 c1
H5: step0 (v0, c0) (v'0, c'0)
H6: plug C c'0 c1'
plug C c'0 c1' assumption.
    -v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
c2: cmd
cstep (v0, Skip;; c2) (v0, c2) econstructor; constructor.
    -v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 <> 0
cstep (v0, when e then then_ else else_ done)
  (v0, then_) econstructor; constructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 <> 0
interp e v0 <> 0 assumption.
    -v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
cstep (v0, when e then then_ else else_ done)
  (v0, else_) econstructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
plug ?C ?c (when e then then_ else else_ done)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
step0 (v0, ?c) (v0, ?c')
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
plug ?C ?c' else_ 2: apply Step0IfFalse.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
plug ?C (when ?e then ?then_ else ?c' done)
  (when e then then_ else else_ done)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
interp ?e v0 = 0
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
plug ?C ?c' else_
      constructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
interp e v0 = 0
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
plug Hole else_ else_ assumption.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
then_, else_: cmd
H: interp e v0 = 0
plug Hole else_ else_ constructor.
    -v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 <> 0
cstep (v0, while e loop body done)
  (v0, body;; while e loop body done) econstructor; constructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 <> 0
interp e v0 <> 0 assumption.
    -v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
cstep (v0, while e loop body done) (v0, Skip) econstructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
plug ?C ?c (while e loop body done)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
step0 (v0, ?c) (v0, ?c')
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
plug ?C ?c' Skip 2: apply Step0WhileFalse.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
plug ?C (while ?e loop ?body done)
  (while e loop body done)
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
interp ?e v0 = 0
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
plug ?C Skip Skip
      constructor.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
interp e v0 = 0
v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
plug Hole Skip Skip assumption.v: valuation
c: cmd
v': valuation
c': cmd
v0: valuation
e: arith
body: cmd
H: interp e v0 = 0
plug Hole Skip Skip constructor.
  Qed.

  Lemma step0_step :
    forall v c v' c',
      step0 (v, c) (v', c') ->
      step (v, c) (v', c').forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step0 (v, c) (v', c') -> step (v, c) (v', c')
  Proof.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
step0 (v, c) (v', c') -> step (v, c) (v', c')
    intros v c v' c' H.v: valuation
c: cmd
v': valuation
c': cmd
H: step0 (v, c) (v', c')
step (v, c) (v', c') inversion H; constructor; assumption.
  Qed.

  Lemma cstep_step' :
    forall C c0 c,
      plug C c0 c  ->
      forall v' c'0 v c',
        step0 (v, c0) (v', c'0) ->
        plug C c'0 c' ->
        step (v, c) (v', c').forall (C : context) (c0 c : cmd),
plug C c0 c ->
forall (v' : valuation) (c'0 : cmd) (v : valuation)
  (c' : cmd),
step0 (v, c0) (v', c'0) ->
plug C c'0 c' -> step (v, c) (v', c')
  Proof.forall (C : context) (c0 c : cmd),
plug C c0 c ->
forall (v' : valuation) (c'0 : cmd) (v : valuation)
  (c' : cmd),
step0 (v, c0) (v', c'0) ->
plug C c'0 c' -> step (v, c) (v', c')
    intros C c0 c H.C: context
c0, c: cmd
H: plug C c0 c
forall (v' : valuation) (c'0 : cmd) (v : valuation)
  (c' : cmd),
step0 (v, c0) (v', c'0) ->
plug C c'0 c' -> step (v, c) (v', c')
    induction H; intros.c: cmd
v': valuation
c'0: cmd
v: valuation
c': cmd
H: step0 (v, c) (v', c'0)
H0: plug Hole c'0 c'
step (v, c) (v', c')
c: cmd
C: context
c', c2: cmd
H: plug C c c'
IHplug: forall (v' : valuation) 
  (c'0 : cmd) (v : valuation) 
  (c'1 : cmd),
step0 (v, c) (v', c'0) ->
plug C c'0 c'1 -> step (v, c') (v', c'1)
v': valuation
c'0: cmd
v: valuation
c'1: cmd
H0: step0 (v, c) (v', c'0)
H1: plug (CSeq C c2) c'0 c'1
step (v, c';; c2) (v', c'1)
    -c: cmd
v': valuation
c'0: cmd
v: valuation
c': cmd
H: step0 (v, c) (v', c'0)
H0: plug Hole c'0 c'
step (v, c) (v', c') inversion H0.c: cmd
v': valuation
c'0: cmd
v: valuation
c': cmd
H: step0 (v, c) (v', c'0)
H0: plug Hole c'0 c'
c0: cmd
H2: c0 = c'0
H3: c'0 = c'
step (v, c) (v', c') subst.c: cmd
v', v: valuation
c': cmd
H0: plug Hole c' c'
H: step0 (v, c) (v', c')
step (v, c) (v', c') apply step0_step.c: cmd
v', v: valuation
c': cmd
H0: plug Hole c' c'
H: step0 (v, c) (v', c')
step0 (v, c) (v', c') assumption.
    -c: cmd
C: context
c', c2: cmd
H: plug C c c'
IHplug: forall (v' : valuation) 
  (c'0 : cmd) (v : valuation) 
  (c'1 : cmd),
step0 (v, c) (v', c'0) ->
plug C c'0 c'1 -> step (v, c') (v', c'1)
v': valuation
c'0: cmd
v: valuation
c'1: cmd
H0: step0 (v, c) (v', c'0)
H1: plug (CSeq C c2) c'0 c'1
step (v, c';; c2) (v', c'1) inversion H1.c: cmd
C: context
c', c2: cmd
H: plug C c c'
IHplug: forall (v' : valuation) 
  (c'0 : cmd) (v : valuation) 
  (c'1 : cmd),
step0 (v, c) (v', c'0) ->
plug C c'0 c'1 -> step (v, c') (v', c'1)
v': valuation
c'0: cmd
v: valuation
c'1: cmd
H0: step0 (v, c) (v', c'0)
H1: plug (CSeq C c2) c'0 c'1
c0: cmd
C0: context
c'2, c1: cmd
H6: plug C c'0 c'2
H2: C0 = C
H4: c1 = c2
H3: c0 = c'0
H5: (c'2;; c2) = c'1
step (v, c';; c2) (v', c'2;; c2) subst.c: cmd
C: context
c', c2: cmd
H: plug C c c'
IHplug: forall (v' : valuation) 
  (c'0 : cmd) (v : valuation) 
  (c'1 : cmd),
step0 (v, c) (v', c'0) ->
plug C c'0 c'1 -> step (v, c') (v', c'1)
v': valuation
c'0: cmd
v: valuation
H0: step0 (v, c) (v', c'0)
c'2: cmd
H1: plug (CSeq C c2) c'0 (c'2;; c2)
H6: plug C c'0 c'2
step (v, c';; c2) (v', c'2;; c2) apply StepSeq1.c: cmd
C: context
c', c2: cmd
H: plug C c c'
IHplug: forall (v' : valuation) 
  (c'0 : cmd) (v : valuation) 
  (c'1 : cmd),
step0 (v, c) (v', c'0) ->
plug C c'0 c'1 -> step (v, c') (v', c'1)
v': valuation
c'0: cmd
v: valuation
H0: step0 (v, c) (v', c'0)
c'2: cmd
H1: plug (CSeq C c2) c'0 (c'2;; c2)
H6: plug C c'0 c'2
step (v, c') (v', c'2) eapply IHplug; eassumption.
  Qed.

  Theorem cstep_step :
    forall v c v' c',
    cstep (v, c) (v', c') ->
    step (v, c) (v', c').forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
cstep (v, c) (v', c') -> step (v, c) (v', c')
  Proof.forall (v : valuation) (c : cmd) (v' : valuation)
  (c' : cmd),
cstep (v, c) (v', c') -> step (v, c) (v', c')
    intros v c v' c' H.v: valuation
c: cmd
v': valuation
c': cmd
H: cstep (v, c) (v', c')
step (v, c) (v', c') inversion H.v: valuation
c: cmd
v': valuation
c': cmd
H: cstep (v, c) (v', c')
C: context
v0: valuation
c0: cmd
v'0: valuation
c'0, c1, c2: cmd
H4: plug C c0 c
H5: step0 (v, c0) (v', c'0)
H6: plug C c'0 c'
H0: v0 = v
H1: c1 = c
H2: v'0 = v'
H3: c2 = c'
step (v, c) (v', c') subst.v: valuation
c: cmd
v': valuation
c': cmd
H: cstep (v, c) (v', c')
C: context
c0, c'0: cmd
H4: plug C c0 c
H5: step0 (v, c0) (v', c'0)
H6: plug C c'0 c'
step (v, c) (v', c')
    eapply cstep_step'; eassumption.
  Qed.

We can also re-prove determinism. This is simpler if we use the equivalence.

  Theorem cstep_det :
    forall s out1,
    cstep s out1 ->
    forall out2, cstep s out2 ->
            out1 = out2.forall s out1 : valuation * cmd,
cstep s out1 ->
forall out2 : valuation * cmd,
cstep s out2 -> out1 = out2
  Proof.forall s out1 : valuation * cmd,
cstep s out1 ->
forall out2 : valuation * cmd,
cstep s out2 -> out1 = out2
    intros s out1 H out2 H0.s, out1: (valuation * cmd)%type
H: cstep s out1
out2: (valuation * cmd)%type
H0: cstep s out2
out1 = out2 destruct s, out1, out2.v: valuation
c: cmd
v0: valuation
c0: cmd
H: cstep (v, c) (v0, c0)
v1: valuation
c1: cmd
H0: cstep (v, c) (v1, c1)
(v0, c0) = (v1, c1)
    apply cstep_step in H0.v: valuation
c: cmd
v0: valuation
c0: cmd
H: cstep (v, c) (v0, c0)
v1: valuation
c1: cmd
H0: step (v, c) (v1, c1)
(v0, c0) = (v1, c1) apply cstep_step in H.v: valuation
c: cmd
v0: valuation
c0: cmd
H: step (v, c) (v0, c0)
v1: valuation
c1: cmd
H0: step (v, c) (v1, c1)
(v0, c0) = (v1, c1)
    eapply step_det in H.v: valuation
c: cmd
v0: valuation
c0: cmd
v1: valuation
c1: cmd
H0: step (v, c) (v1, c1)
H: ?out1 = (v0, c0)
(v0, c0) = (v1, c1)
v: valuation
c: cmd
v0: valuation
c0: cmd
H: step (v, c) (v0, c0)
v1: valuation
c1: cmd
H0: step (v, c) (v1, c1)
step (v, c) ?out1 2: apply H0.v: valuation
c: cmd
v0: valuation
c0: cmd
v1: valuation
c1: cmd
H0: step (v, c) (v1, c1)
H: (v1, c1) = (v0, c0)
(v0, c0) = (v1, c1) inversion H.v: valuation
c: cmd
v0: valuation
c0: cmd
v1: valuation
c1: cmd
H0: step (v, c) (v1, c1)
H: (v1, c1) = (v0, c0)
H2: v1 = v0
H3: c1 = c0
(v0, c0) = (v0, c0) reflexivity.
  Qed.

Proving program Optimizations

Let's begin with a simple optimization that simplifies a bit some arithmetic expressions.

  Fixpoint simplify_arith (a:arith) : arith :=
    match a with
    | Plus a1 a2 =>
        let s1 := simplify_arith a1 in
        let s2 := simplify_arith a2 in
        match s1,s2 with
        | Const n1, Const n2 => Const (n1 + n2)
        | Const 0, e => e
        | e, Const 0 => e
        | _, _ => Plus s1 s2
        end
    | _ => a
            (* we could do other simplifications *)
    end.

  Fixpoint simplify_cmd (c:cmd) : cmd :=
    match c with
    | Skip => Skip
    | Assign v a => Assign v (simplify_arith a)
    | Sequence c1 c2 =>
        Sequence (simplify_cmd c1) (simplify_cmd c2)
    | If a c1 c2 =>
        If (simplify_arith a) (simplify_cmd c1) (simplify_cmd c2)
    | While a c1 =>
        While (simplify_arith a) (simplify_cmd c1)
    end.

  Lemma simplify_arith_correct:
    forall a v,
      interp a v = interp (simplify_arith a) v.forall (a : arith) (v : valuation),
interp a v = interp (simplify_arith a) v
  Proof.forall (a : arith) (v : valuation),
interp a v = interp (simplify_arith a) v
    intros a v.a: arith
v: valuation
interp a v = interp (simplify_arith a) v induction a; simpl; auto.a1, a2: arith
v: valuation
IHa1: interp a1 v = interp (simplify_arith a1) v
IHa2: interp a2 v = interp (simplify_arith a2) v
interp a1 v + interp a2 v =
interp
  match simplify_arith a1 with
  | Const (0 as n1) =>
      match simplify_arith a2 with
      | Const n2 => n1 + n2
      | _ => simplify_arith a2
      end
  | Const (S _ as n1) =>
      match simplify_arith a2 with
      | Const n2 => n1 + n2
      | _ =>
          (simplify_arith a1 + simplify_arith a2)%arith
      end
  | _ =>
      match simplify_arith a2 with
      | Const 0 => simplify_arith a1
      | _ =>
          (simplify_arith a1 + simplify_arith a2)%arith
      end
  end v
    destruct (simplify_arith a1) eqn:S1; rewrite IHa1; rewrite IHa2;
      try destruct n; destruct (simplify_arith a2);
      try destruct n; auto.
  Qed.

  Lemma simplify_cmd_step:
    forall s1 s2 (STEP: step s1 s2),
      step (fst s1, simplify_cmd (snd s1))
        (fst s2, simplify_cmd (snd s2)).forall s1 s2 : valuation * cmd,
step s1 s2 ->
step (fst s1, simplify_cmd (snd s1))
  (fst s2, simplify_cmd (snd s2))
  Proof.forall s1 s2 : valuation * cmd,
step s1 s2 ->
step (fst s1, simplify_cmd (snd s1))
  (fst s2, simplify_cmd (snd s2))
    intros s1 s2 STEP.s1, s2: (valuation * cmd)%type
STEP: step s1 s2
step (fst s1, simplify_cmd (snd s1))
  (fst s2, simplify_cmd (snd s2))
    induction STEP; simpl in *; try rewrite simplify_arith_correct;
      constructor; try rewrite <- simplify_arith_correct; auto.
  Qed.

  Theorem simplify_cmd_correct:
    forall s1 s2 (STAR: step^* s1 s2),
      step^* (fst s1, simplify_cmd (snd s1))
        (fst s2, simplify_cmd (snd s2)).forall s1 s2 : valuation * cmd,
(step) ^* s1 s2 ->
(step) ^* (fst s1, simplify_cmd (snd s1))
  (fst s2, simplify_cmd (snd s2))
  Proof.forall s1 s2 : valuation * cmd,
(step) ^* s1 s2 ->
(step) ^* (fst s1, simplify_cmd (snd s1))
  (fst s2, simplify_cmd (snd s2))
    intros s1 s2 STAR.s1, s2: (valuation * cmd)%type
STAR: (step) ^* s1 s2
(step) ^* (fst s1, simplify_cmd (snd s1))
  (fst s2, simplify_cmd (snd s2)) induction STAR.x: (valuation * cmd)%type
(step) ^* (fst x, simplify_cmd (snd x))
  (fst x, simplify_cmd (snd x))
x, y, z: (valuation * cmd)%type
STEP: step x y
STAR: (step) ^* y z
IHSTAR: (step) ^* (fst y, simplify_cmd (snd y))
  (fst z, simplify_cmd (snd z))
(step) ^* (fst x, simplify_cmd (snd x))
  (fst z, simplify_cmd (snd z))
    {x: (valuation * cmd)%type
(step) ^* (fst x, simplify_cmd (snd x))
  (fst x, simplify_cmd (snd x)) constructor. }x, y, z: (valuation * cmd)%type
STEP: step x y
STAR: (step) ^* y z
IHSTAR: (step) ^* (fst y, simplify_cmd (snd y))
  (fst z, simplify_cmd (snd z))
(step) ^* (fst x, simplify_cmd (snd x))
  (fst z, simplify_cmd (snd z))
    apply simplify_cmd_step in STEP.x, y, z: (valuation * cmd)%type
STEP: step (fst x, simplify_cmd (snd x))
  (fst y, simplify_cmd (snd y))
STAR: (step) ^* y z
IHSTAR: (step) ^* (fst y, simplify_cmd (snd y))
  (fst z, simplify_cmd (snd z))
(step) ^* (fst x, simplify_cmd (snd x))
  (fst z, simplify_cmd (snd z))
    econstructor; eauto.
  Qed.

This one was particularly simple, because each step of the original program corresponds to one similar step of the optimized program. Here the invariant of the program transfomation is that at any point during program execution, a state of the original program execution can be related to a state of the optimized program execution where the valuation is the same and the program left to be executed is the same but simplified.

What if we have an optimization that changes the number of steps? We will revisit this topic in another lecture.

  End Simple.

Concurrency Example

To see one advantage of the small-step style, let's add a construct for parallel execution of two commands. Such parallelism may be nested arbitrarily.

Module Concurrent.
  Inductive cmd :=
  | Skip
  | Assign (x : var) (e : arith)
  | Sequence (c1 c2 : cmd)
  | If (e : arith) (then_ else_ : cmd)
  | While (e : arith) (body : cmd)
  | Parallel (c1 c2 : cmd).

  Notation "x <- e" := (Assign x e%arith) (at level 75).
  (* This one changed slightly, to avoid parsing clashes. *)
  Infix ";;" := Sequence (at level 76).
  Notation "'when' e 'then' then_ 'else' else_ 'done'" :=
    (If e%arith then_ else_) (at level 75, e at level 0).Identifier 'when' now a keyword
Identifier 'done' now a keyword
  Notation "'while' e 'loop' body 'done'" :=
    (While e%arith body) (at level 75).Identifier 'while' now a keyword
Identifier 'loop' now a keyword
  Infix "||" := Parallel.

  Lemma gss:
    forall v x k, (v $+ (x,k)) $? x = Some k.forall (v : valuation) (x : var) (k : nat),
v $+ (x, k) $? x = Some k
  Proof.forall (v : valuation) (x : var) (k : nat),
v $+ (x, k) $? x = Some k
    intros v x k.v: valuation
x: var
k: nat
v $+ (x, k) $? x = Some k unfold get, set.v: valuation
x: var
k: nat
(if string_dec x x then Some k else v $? x) = Some k
    destruct string_dec; auto.v: valuation
x: var
k: nat
n: x <> x
v $? x = Some k contradiction.
  Qed.

  Lemma gso:
    forall v x y k, x <> y -> (v $+ (x,k)) $? y = v $? y.forall (v : valuation) (x y : var) (k : nat),
x <> y -> v $+ (x, k) $? y = v $? y
  Proof.forall (v : valuation) (x y : var) (k : nat),
x <> y -> v $+ (x, k) $? y = v $? y
    intros v x y k H.v: valuation
x, y: var
k: nat
H: x <> y
v $+ (x, k) $? y = v $? y unfold get, set.v: valuation
x, y: var
k: nat
H: x <> y
(if string_dec x y then Some k else v $? y) = v y destruct string_dec; auto.v: valuation
x, y: var
k: nat
H: x <> y
e: x = y
Some k = v y
    subst.v: valuation
y: var
k: nat
H: y <> y
Some k = v y contradiction.
  Qed.

We need surprisingly few changes to the contextual semantics, to explain this new feature. First, we allow a hole to appear on either side of a Parallel. In other words, the "scheduler" may choose either "thread" to run next.

  Inductive context :=
  | Hole
  | CSeq (C : context) (c : cmd)
  | CPar1 (C : context) (c : cmd)
  | CPar2 (c : cmd) (C : context).

We explain the meaning of plugging the new contexts in the obvious way.

  Inductive plug : context -> cmd -> cmd -> Prop :=
  | PlugHole : forall c, plug Hole c c
  | PlugSeq : forall c C c' c2,
    plug C c c'
    -> plug (CSeq C c2) c (Sequence c' c2)
  | PlugPar1 : forall c C c' c2,
    plug C c c'
    -> plug (CPar1 C c2) c (Parallel c' c2)
  | PlugPar2 : forall c C c' c1,
    plug C c c'
    -> plug (CPar2 c1 C) c (Parallel c1 c').

The only new step rules are for "cleaning up" finished "threads," which have reached the point of being Skip commands.

  Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
  | Step0Assign : forall v x e,
    step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
  | Step0Seq : forall v c2,
    step0 (v, Sequence Skip c2) (v, c2)
  | Step0IfTrue : forall v e then_ else_,
    interp e v <> 0
    -> step0 (v, If e then_ else_) (v, then_)
  | Step0IfFalse : forall v e then_ else_,
    interp e v = 0
    -> step0 (v, If e then_ else_) (v, else_)
  | Step0WhileTrue : forall v e body,
    interp e v <> 0
    -> step0 (v, While e body) (v, Sequence body (While e body))
  | Step0WhileFalse : forall v e body,
    interp e v = 0
    -> step0 (v, While e body) (v, Skip)
  | Step0Par1 : forall v c,
    step0 (v, Parallel Skip c) (v, c).

  Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
  | CStep : forall C v c v' c' c1 c2,
    plug C c c1
    -> step0 (v, c) (v', c')
    -> plug C c' c2
    -> cstep (v, c1) (v', c2).

  Inductive trc {A:Type} {R:A -> A -> Prop}: A -> A -> Prop :=
  | TrcRefl : forall x, trc x x
  | TrcFront : forall x y z
    (STEP: R x y)
    (STAR: trc y z),
      trc x z.

  Notation "R ^*" := (@trc _ R) (at level 0).

Example: Stepping a specific program.

Here's the classic cautionary-tale program about remembering to lock your concurrent threads.

  Definition prog :=
    ("a" <- "n";;
     "n" <- "a" + 1)
    || ("b" <- "n";;
        "n" <- "b" + 1).

  Local Hint Constructors plug step0 cstep : core.

The naive "expected" answer is attainable.

  Theorem correctAnswer :
    forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
              /\ v $? "n" = Some (n + 2).forall n : nat,
exists v : valuation,
  (cstep) ^* ($0 $+ ("n", n), prog) (v, Skip) /\
  v $? "n" = Some (n + 2)
  Proof.forall n : nat,
exists v : valuation,
  (cstep) ^* ($0 $+ ("n", n), prog) (v, Skip) /\
  v $? "n" = Some (n + 2)
    intros n.n: nat
exists v : valuation,
  (cstep) ^* ($0 $+ ("n", n), prog) (v, Skip) /\
  v $? "n" = Some (n + 2) eexists.n: nat
(cstep) ^* ($0 $+ ("n", n), prog) (?v, Skip) /\
?v $? "n" = Some (n + 2) split.n: nat
(cstep) ^* ($0 $+ ("n", n), prog) (?v, Skip)
n: nat
?v $? "n" = Some (n + 2) unfold prog.n: nat
(cstep) ^*
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) (?v, Skip)
n: nat
?v $? "n" = Some (n + 2)
    1: {n: nat
(cstep) ^*
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   (Skip;; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   (Skip;; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   (Skip;; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y eapply CStep with (C := CPar1 Hole _); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   ("n" <- "a" + 1) || ("b" <- "n";; "n" <- "b" + 1))
  (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   ("n" <- "a" + 1) || ("b" <- "n";; "n" <- "b" + 1))
  ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   ("n" <- "a" + 1) || ("b" <- "n";; "n" <- "b" + 1))
  ?y eapply CStep with (C := CPar1 Hole _); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   Skip || ("b" <- "n";; "n" <- "b" + 1)) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   Skip || ("b" <- "n";; "n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   Skip || ("b" <- "n";; "n" <- "b" + 1)) ?y eapply CStep with (C := Hole); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   "b" <- "n";; "n" <- "b" + 1) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   "b" <- "n";; "n" <- "b" + 1) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   "b" <- "n";; "n" <- "b" + 1) ?y eapply CStep with (C := CSeq Hole _); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   Skip;; "n" <- "b" + 1) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   Skip;; "n" <- "b" + 1) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   Skip;; "n" <- "b" + 1) ?y eapply CStep with (C := Hole); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   "n" <- "b" + 1) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   "n" <- "b" + 1) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   "n" <- "b" + 1) ?y eapply CStep with (C := Hole); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))) $+ ("n",
   interp ("b" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))) $+ ("n",
         interp ("a" + 1)%arith
           ($0 $+ ("n", n) $+ ("a",
            interp "n" ($0 $+ ("n", n))))))))), Skip)
  (?v, Skip)
    econstructor. }n: nat
$0 $+ ("n", n) $+ ("a", interp "n" ($0 $+ ("n", n))) $+
("n",
interp ("a" + 1)%arith
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))))) $+ ("b",
interp "n"
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))))) $+ ("n",
interp ("b" + 1)%arith
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))))) $? "n" =
Some (n + 2)
    simpl.n: nat
$0 $+ ("n", n) $+ ("a", n) $+ ("n", n + 1) $+ ("b",
n + 1) $+ ("n", n + 1 + 1) $? "n" = Some (n + 2)
    rewrite gss.n: nat
Some (n + 1 + 1) = Some (n + 2) f_equal.n: nat
n + 1 + 1 = n + 2 lia.
  Qed.

But so is the "wrong" answer!

  Theorem wrongAnswer :
    forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
              /\ v $? "n" = Some (n + 1).forall n : nat,
exists v : valuation,
  (cstep) ^* ($0 $+ ("n", n), prog) (v, Skip) /\
  v $? "n" = Some (n + 1)
  Proof.forall n : nat,
exists v : valuation,
  (cstep) ^* ($0 $+ ("n", n), prog) (v, Skip) /\
  v $? "n" = Some (n + 1)
    intros n.n: nat
exists v : valuation,
  (cstep) ^* ($0 $+ ("n", n), prog) (v, Skip) /\
  v $? "n" = Some (n + 1) eexists.n: nat
(cstep) ^* ($0 $+ ("n", n), prog) (?v, Skip) /\
?v $? "n" = Some (n + 1) split.n: nat
(cstep) ^* ($0 $+ ("n", n), prog) (?v, Skip)
n: nat
?v $? "n" = Some (n + 1) unfold prog.n: nat
(cstep) ^*
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) (?v, Skip)
n: nat
?v $? "n" = Some (n + 1)
    1: {n: nat
(cstep) ^*
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n),
   ("a" <- "n";; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   (Skip;; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   (Skip;; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))),
   (Skip;; "n" <- "a" + 1)
   || ("b" <- "n";; "n" <- "b" + 1)) ?y eapply CStep with (C := CPar2 _ (CSeq Hole _)); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   (Skip;; "n" <- "a" + 1) || (Skip;; "n" <- "b" + 1))
  (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   (Skip;; "n" <- "a" + 1) || (Skip;; "n" <- "b" + 1))
  ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   (Skip;; "n" <- "a" + 1) || (Skip;; "n" <- "b" + 1))
  ?y eapply CStep with (C := CPar1 Hole _); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   ("n" <- "a" + 1) || (Skip;; "n" <- "b" + 1))
  (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   ("n" <- "a" + 1) || (Skip;; "n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   ("n" <- "a" + 1) || (Skip;; "n" <- "b" + 1)) ?y eapply CStep with (C := CPar2 _ Hole); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   ("n" <- "a" + 1) || ("n" <- "b" + 1)) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   ("n" <- "a" + 1) || ("n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))),
   ("n" <- "a" + 1) || ("n" <- "b" + 1)) ?y eapply CStep with (C := CPar1 Hole _); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   Skip || ("n" <- "b" + 1)) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   Skip || ("n" <- "b" + 1)) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   Skip || ("n" <- "b" + 1)) ?y eapply CStep with (C := Hole); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   "n" <- "b" + 1) (?v, Skip)
    econstructor.n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   "n" <- "b" + 1) ?y
n: nat
(cstep) ^* ?y (?v, Skip)
    {n: nat
cstep
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))),
   "n" <- "b" + 1) ?y eapply CStep with (C := Hole); eauto. }n: nat
(cstep) ^*
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))) $+ ("n",
   interp ("b" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))) $+ ("n",
      interp ("a" + 1)%arith
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))) $+ ("b",
         interp "n"
           ($0 $+ ("n", n) $+ ("a",
            interp "n" ($0 $+ ("n", n))))))))), Skip)
  (?v, Skip)

    econstructor. }n: nat
$0 $+ ("n", n) $+ ("a", interp "n" ($0 $+ ("n", n))) $+
("b",
interp "n"
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))))) $+ ("n",
interp ("a" + 1)%arith
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))))) $+ ("n",
interp ("b" + 1)%arith
  ($0 $+ ("n", n) $+ ("a",
   interp "n" ($0 $+ ("n", n))) $+ ("b",
   interp "n"
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))))) $+ ("n",
   interp ("a" + 1)%arith
     ($0 $+ ("n", n) $+ ("a",
      interp "n" ($0 $+ ("n", n))) $+ ("b",
      interp "n"
        ($0 $+ ("n", n) $+ ("a",
         interp "n" ($0 $+ ("n", n))))))))) $? "n" =
Some (n + 1)
    simpl.n: nat
$0 $+ ("n", n) $+ ("a", n) $+ ("b", n) $+ ("n", n + 1) $+
("n", n + 1) $? "n" = Some (n + 1)
    rewrite gss.n: nat
Some (n + 1) = Some (n + 1) auto.
  Qed.

End Concurrent.

Systems and
Formalisms Lab