(*|
===========================
Week 6: Smallstep Semantics
===========================

:sortorder: 2
:status: hidden

Author
  `Aurèle Barrière <https://aurele-barriere.github.io>`__,
  `Adam Chlipala <http://adam.chlipala.net/frap/>`__,
  `Benjamin C. Pierce <https://softwarefoundations.cis.upenn.edu/lf-current/index.html>`__

License
  No redistribution allowed (usage by permission in CS-428).

.. contents::

.. coq:: none
|*)

Require Import String List Arith Lia.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.

Set Implicit Arguments.
Notation var := string.

(*|
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.
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).
  Notation "'while' e 'loop' body 'done'" :=
    (While e%arith body) (at level 75).

(*|
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.

(*|
Small-step Semantics
--------------------

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.
  Proof.
    intros v x k. unfold get, set.
    destruct string_dec; auto. contradiction.
  Qed.

  Lemma gso:
    forall v x y k, x <> y -> (v $+ (x,k)) $? y = v $? y.
  Proof.
    intros v x y k H. unfold get, set. destruct string_dec; auto.
    subst. 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.
  Proof.
    eexists.
    split.
    - econstructor.
      { unfold factorial. repeat econstructor. }
      econstructor.
      { simpl. apply StepSeq2. }
      econstructor.
      { apply StepWhileTrue. simpl. lia. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { econstructor. apply StepSeq2. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { apply StepSeq2. }
      econstructor.
      { apply StepWhileTrue. simpl. lia. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { econstructor. apply StepSeq2. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { apply StepSeq2. }
      econstructor.
      { apply StepWhileFalse. simpl. reflexivity. }
      simpl. constructor.
    - rewrite gso.
      2: { unfold not. intros H. inversion H. }
      rewrite gss. 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.
  Proof.
    intros v c v1 H. induction H; intros.
    - inversion H. subst. reflexivity.
    - inversion H. subst. reflexivity.
    - inversion H1. subst.
      apply IHeval1 in H5. subst. apply IHeval2 in H7. assumption.
    - inversion H1; subst.
      + apply IHeval in H8. assumption.
      + contradiction.
    - inversion H1; subst.
      + contradiction.
      + apply IHeval in H8. assumption.
    - inversion H2; subst.
      + apply IHeval1 in H7. subst.
        apply IHeval2 in H9. assumption.
      + contradiction.
    - inversion H0; subst.
      + contradiction.
      + reflexivity.
  Qed.

  Theorem step_det :
    forall s out1,
    step s out1 ->
    forall out2, step s out2 ->
            out1 = out2.
  Proof.
    intros s out1 H. induction H; intros.
    - inversion H. subst. constructor.
    - inversion H0; subst.
      + apply IHstep in H5. inversion H5. subst. reflexivity.
      + inversion H.
    - inversion H; subst.
      + inversion H4.
      + reflexivity.
    - inversion H0; subst.
      + reflexivity.
      + contradiction.
    - inversion H0; subst; try contradiction. reflexivity.
    - inversion H0; subst; try contradiction. reflexivity.
    - inversion H0; subst; try contradiction. 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).
  Proof.
    split.
    - apply TrcRefl.
    - eapply TrcFront. apply StepSeq2. 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').
  Proof.
    intros v c. induction c. 1:left. all:try right.
    - reflexivity.
    - eexists. eexists. constructor.
    - destruct IHc1 as [H | [v' [c' H]]].
      + subst. eexists. eexists. apply StepSeq2.
      + eexists. eexists. apply StepSeq1. apply H.
    - destruct (interp e v =? 0)%nat eqn:Hcond.
      (* if we forget eqn:, we forget what we destroyed *)
      + eexists. eexists.
        apply StepIfFalse. rewrite Nat.eqb_eq in Hcond. assumption.
      + eexists. eexists.
        (* if we did eexists before destruct, what would happen? *)
        apply StepIfTrue. rewrite Nat.eqb_neq in Hcond. assumption.
    - destruct (interp e v =? 0)%nat eqn:Hguard.
      + eexists. eexists.
        apply StepWhileFalse. rewrite Nat.eqb_eq in Hguard. assumption.
      + eexists. eexists.
        apply StepWhileTrue. rewrite Nat.eqb_neq in Hguard. 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).
  Proof.
    intros v c. split; intros.
    - subst. unfold normal_form, not. intros [s' STEP]. inversion STEP.
    - unfold normal_form, not in H.
      specialize (strong_progress_step v c) as STRONG.
      destruct STRONG as [SKIP | [v' [c' STEP]]].
      + assumption.
      + exfalso. (* replaces the current goal with false *)
        apply H. exists (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.
  Proof.
    intros A R a a' STAR NF. unfold normal_form in NF.
    destruct STAR.
    - reflexivity.
    - exfalso. apply NF. exists 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.
  Proof.
    intros A R RDET s f1 f2 STAR1 NF1 STAR2 NF2.
    induction STAR1.
    - apply trc_nf in STAR2; try assumption. subst. reflexivity.
    - destruct STAR2.
      + exfalso. apply NF2. eexists. eapply STEP.
      + specialize (RDET _ _ _ STEP STEP0). subst.
        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.
  Proof.
    intros v c vf1 vf2 STAR1 STAR2.
    assert ((vf1, Skip) = (vf2,Skip)).
    { eapply trc_determinism with (R:=step).
      - intros a a1 a2 H H0. eapply step_det. apply H. apply H0.
      - apply STAR1.
      - rewrite <- skip_normal_form. reflexivity.
      - apply STAR2.
      - rewrite <- skip_normal_form. reflexivity. }
    inversion H. 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).
  Proof.
    intros v start send H H0. induction H0.
    - assumption.
    - apply IHtrc. destruct H; subst.
      + right. eapply step_det. apply STEP. constructor. simpl. lia.
      + left. eapply step_det. apply STEP. constructor.
  Qed.

  Theorem not_normalizing:
    ~ (forall s,
        exists sfinal, step^* s sfinal /\ normal_form step sfinal).
  Proof.
    unfold not. intros H.
    specialize (H ($0,infinite)).
    destruct H as [[vfinal cfinal] [STAR NF]].
    eapply infinite_loop in STAR.
    2: { left. reflexivity. }
    rewrite <- skip_normal_form in NF. subst.
    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).
  Proof.
    intros v1 c1 v2 c2 v3 c3 STAR1 STAR2. induction STAR1; auto.
    econstructor. apply STEP.
    apply IHSTAR1. 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).
  Proof.
    intros s1 s2 c H.
    induction H.
    - constructor.
    - destruct y. econstructor.
      2: { eapply IHtrc. }
      constructor. destruct x. simpl. 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 <https://coq.inria.fr/doc/v8.18/refman/proofs/writing-proofs/reasoning-inductives.html#examples-of-dependent-destruction-dependent-induction>`_ 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).
  Proof.
    intros v c1 c2 v' c1' H.
    remember (v, c1) as x.
    remember (v', c1') as y.
    replace v with (fst x) by (subst;auto).
    replace v' with (fst y) by (subst;auto).
    replace c1 with (snd x) by (subst;auto).
    replace c1' with (snd y) by (subst;auto).
    (* if we don't clear we don't get the right induction! *)
    clear v v' c1 c1' Heqx Heqy.
    induction H; subst.
    - constructor.
    - econstructor.
      2: apply IHtrc.
      constructor. destruct x, y. assumption.
  Qed.

(*|
Not very convenient. Let's look at the `dependent induction` tactic.
|*)

  Require Import Coq.Program.Equality.

  Lemma step_star_Seq : forall v c1 c2 v' c1',
    step^* (v, c1) (v', c1')
    -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).
  Proof.
    intros.
    dependent induction H.
    - constructor.
    - destruct y. econstructor.
      2: { eapply IHtrc; reflexivity. }
      constructor.  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).
  Proof.
    intros v c v' H. induction H.
    - constructor.
    - econstructor; constructor.
    - apply step_star_Seq with (c2:=c2) in IHeval1.
      eapply multi_step_trans. apply IHeval1.
      econstructor. apply StepSeq2. assumption.
    - econstructor.
      { apply StepIfTrue. assumption. }
      assumption.
    - econstructor.
      { apply StepIfFalse. assumption. }
      assumption.
    - econstructor.
      { apply StepWhileTrue. assumption. }
      eapply multi_step_trans.
      2: { apply IHeval2. }
      eapply multi_step_trans.
      { apply step_star_Seq. apply IHeval1. }
      econstructor. apply StepSeq2. constructor.
    - econstructor.
      { apply StepWhileFalse. assumption. }
      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'.
  Proof.
    intros x y H. induction H; intros; simpl in *.
    - inversion H. subst. constructor.
    - inversion H0. subst. econstructor.
      + apply IHstep. eassumption.
      + assumption.
    - econstructor. constructor. assumption.
    - constructor; assumption.
    - apply EvalIfFalse; assumption.
    - inversion H0. subst. econstructor; eassumption.
    - inversion H0. subst. apply EvalWhileFalse. 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''.
  Proof.
    intros v c v' c' H v'' H0.
    eapply small_big_fs in H; simpl. 2: eassumption.
    simpl in H. 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''.
  Proof.
    intros v c v' c' H.
    dependent induction H; intros; try assumption.
    destruct y. eapply IHtrc in H0; auto.
    eapply small_big''; eauto.
  Qed.

  Theorem small_big :
    forall v c v',
       step^* (v, c) (v', Skip) ->
       eval v c v'.
  Proof.
    intros v c v' H. eapply small_big'; eauto. 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').
  Proof.
    intros v c v' c' H. induction H.
    - eapply CStep.
      2: constructor. apply PlugHole. apply PlugHole.
    - inversion IHstep. subst. econstructor. 2: apply H5.
      apply PlugSeq. apply H4. constructor. assumption.
    - econstructor; constructor.
    - econstructor; constructor. assumption.
    - econstructor. 2: apply Step0IfFalse.
      constructor. assumption. constructor.
    - econstructor; constructor. assumption.
    - econstructor. 2: apply Step0WhileFalse.
      constructor. assumption. constructor.
  Qed.

  Lemma step0_step :
    forall v c v' c',
      step0 (v, c) (v', c') ->
      step (v, c) (v', c').
  Proof.
    intros v c v' c' H. 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').
  Proof.
    intros C c0 c H.
    induction H; intros.
    - inversion H0. subst. apply step0_step. assumption.
    - inversion H1. subst. apply StepSeq1. eapply IHplug; eassumption.
  Qed.

  Theorem cstep_step :
    forall v c v' c',
    cstep (v, c) (v', c') ->
    step (v, c) (v', c').
  Proof.
    intros v c v' c' H. inversion H. subst.
    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.
  Proof.
    intros s out1 H out2 H0. destruct s, out1, out2.
    apply cstep_step in H0. apply cstep_step in H.
    eapply step_det in H. 2: apply H0. inversion H. 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.
  Proof.
    intros a v. induction a; simpl; auto.
    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)).
  Proof.
    intros s1 s2 STEP.
    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)).
  Proof.
    intros s1 s2 STAR. induction STAR.
    { constructor. }
    apply simplify_cmd_step in STEP.
    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).
  Notation "'while' e 'loop' body 'done'" :=
    (While e%arith body) (at level 75).
  Infix "||" := Parallel.

  Lemma gss:
    forall v x k, (v $+ (x,k)) $? x = Some k.
  Proof.
    intros v x k. unfold get, set.
    destruct string_dec; auto. contradiction.
  Qed.

  Lemma gso:
    forall v x y k, x <> y -> (v $+ (x,k)) $? y = v $? y.
  Proof.
    intros v x y k H. unfold get, set. destruct string_dec; auto.
    subst. 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).
  Proof.
    intros n. eexists. split. unfold prog.
    1: {
    econstructor.
    { eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto. }
    econstructor.
    { eapply CStep with (C := CPar1 Hole _); eauto. }
    econstructor.
    { eapply CStep with (C := CPar1 Hole _); eauto. }
    econstructor.
    { eapply CStep with (C := Hole); eauto. }
    econstructor.
    { eapply CStep with (C := CSeq Hole _); eauto. }
    econstructor.
    { eapply CStep with (C := Hole); eauto. }
    econstructor.
    { eapply CStep with (C := Hole); eauto. }
    econstructor. }
    simpl.
    rewrite gss. f_equal. 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).
  Proof.
    intros n. eexists. split. unfold prog.
    1: {
    econstructor.
    { eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto. }
    econstructor.
    { eapply CStep with (C := CPar2 _ (CSeq Hole _)); eauto. }
    econstructor.
    { eapply CStep with (C := CPar1 Hole _); eauto. }
    econstructor.
    { eapply CStep with (C := CPar2 _ Hole); eauto. }
    econstructor.
    { eapply CStep with (C := CPar1 Hole _); eauto. }
    econstructor.
    { eapply CStep with (C := Hole); eauto. }
    econstructor.
    { eapply CStep with (C := Hole); eauto. }

    econstructor. }
    simpl.
    rewrite gss. auto.
  Qed.

End Concurrent.