(*|
============================================
Exercises: Big-step / Small-step Equivalence
============================================

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

From Stdlib Require Import String List Arith Lia.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.
Set Implicit Arguments.

(*|
.. details:: Definitions and notations

   Here are the definitions and notations from the small-step semantics lecture.
|*)

Notation var := string.

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.
Declare Scope arith_scope.
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.

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

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).

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.

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).

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).

(*|
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).
(*|
.. solution::

   .. coq::
|*)
  Proof.
    intros v1 c1 v2 c2 v3 c3 STAR1 STAR2. induction STAR1; auto.
    econstructor. apply STEP.
    apply IHSTAR1. assumption.
  Qed.

(*|
.. coq::
|*)

  Lemma step_star_Seq1 :
    forall s1 s2 c,
    step^* s1 s2 ->
    step^* (fst s1, Sequence (snd s1) c) (fst s2, Sequence (snd s2) c).
(*|
.. solution::

   .. coq::
|*)
  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://rocq-prover.org/doc/V9.0.1/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).
(*|
.. solution::

   .. coq::
|*)
  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.
|*)

  #[warnings="-require-in-module"]
  From Stdlib Require Import 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).
(*|
.. solution::

   .. coq::
|*)
  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).
(*|
.. solution::

   .. coq::
|*)
  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'.
(*|
.. solution::

   .. coq::
|*)
  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.

(*|
.. coq::
|*)

  Lemma small_big'' : forall v c v' c',
      step (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.
(*|
.. solution::

   .. coq::
|*)
  Proof.
    intros v c v' c' H v'' H0.
    eapply small_big_fs in H; simpl. 2: eassumption.
    simpl in H. assumption.
  Qed.

(*|
.. coq::
|*)

  Lemma small_big' :
    forall v c v' c',
      step^* (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.
(*|
.. solution::

   .. coq::
|*)
  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.