(***********************************************************)
(* Natural semantics (or big steps operational semantics)  *)
(***********************************************************)

(* We import Coq libraries that may be useful.   *)

Require Import Bool Arith List.
Import ListNotations.

(** States are represented by lists of natural numbers. *)

Check list.
Check list nat.

Print list.

Check 0::1::3::[].

(* The notation for lists is the same as in OCaml. *)

Check [0;1;3].

Remark List_Notation: [0;1;3] = 0::1::3::nil.
Proof.
  (* complete here LEVEL 1 *)
Admitted.

(** * Preliminary material *)
(** Syntax of arithmetic expressions *)

Inductive aexp :=
| Aco : nat -> aexp
| Ava : nat -> aexp
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Asu : aexp -> aexp -> aexp
.

(** Syntax of Boolean expressions *)

Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp -> bexp
| Band : bexp -> bexp -> bexp
| Bor : bexp -> bexp -> bexp
| Beq : bexp -> bexp -> bexp
| Beqnat : aexp -> aexp -> bexp
.

(** Syntax of WHILE instructions *)

Inductive winstr :=
| Skip   : winstr
| Assign : nat -> aexp -> winstr
| Seq    : winstr -> winstr -> winstr
| If     : bexp -> winstr -> winstr -> winstr
| While  : bexp -> winstr -> winstr
.

(** Some states for testing *)
(** [S1] is a state etat where variable "x0" is mapped to 1, variable "x1"
    is mapped to 2 and all other variable are mapped to 0 (defaut value) *)
(** More generally, the value corresponding to variable [Ava i] 
    in state [s] is the ith element of the list that represents [s]. *)

Definition state := list nat.

Example S1 := [1; 2].
Example S2 := [0; 3].
Example S3 := [0; 7; 5; 41].

(** * Semantics *)
(** The functional semantics of arithmetic and Boolean expressions is as before. *)

Fixpoint get (i:nat) (s:state) : nat :=
  match i,s with
  | 0   ,  v :: _   => v
  | S i',  _ :: s'  => get i' s'
  | _   ,  _        => 0
  end.

(** Examples *)

Compute (get 0 S3).
Compute (get 1 S3).
Compute (get 2 S3).
Compute (get 3 S3).
Compute (get 4 S3).

(** [update s i v] returns the state where xi is mapped to [v],
    and the other variables are mapped to the same value as in [s].
    This function never fails, even when variable xi is not
    explicitly given in state [s].
 *)

Fixpoint update (s:state) (i:nat) (v:nat) : state :=
  match i,s with
  | 0   , a :: s' => v :: s'
  | 0   , []      => v :: nil
  | S i', a :: s' => a :: (update s' i' v)
  | S i', []      => 0 :: (update [] i' v)
  end.

Definition S4 := update (update (update (update (update S1 4 1) 3 2) 2 3) 1 4) 0 5.

Compute S1.
Compute S4.

(** Functional semantics of [aexp] *)
Fixpoint evalA (a: aexp) (s: state) : nat :=
  match a with
  | Aco n => n
  | Ava x => get x s
  | Apl a1 a2 =>  evalA a1 s + evalA a2 s
  | Amu a1 a2 =>  evalA a1 s * evalA a2 s
  | Asu a1 a2 =>  evalA a1 s - evalA a2 s
  end.

(** Functional semantics of [bexp] *)
Definition eqboolb b1 b2 : bool :=
  match b1, b2  with
  | true , true  => true
  | false, false => true
  | _    , _     => false
  end.

Fixpoint eqnatb n1 n2 : bool :=
  match n1, n2 with
  | O    , O     => true
  | S n1', S n2' => eqnatb n1' n2'
  | _    , _     => false
  end.

Fixpoint evalB (b : bexp) (s : state) : bool :=
  match b with
  | Btrue => true
  | Bfalse => false
  | Bnot b => negb (evalB b s)
  | Band e1 e2 => (evalB e1 s) && (evalB e2 s)
  | Bor e1 e2 => (evalB e1 s) || (evalB e2 s)
  | Beq e1 e2 => eqboolb (evalB e1 s) (evalB e2 s)
  | Beqnat n1 n2 => eqnatb (evalA n1 s) (evalA n2 s)
  end.

(** Integer constants, for convenience *)

Example N0 := Aco 0.
Example N1 := Aco 1.
Example N2 := Aco 2.
Example N3 := Aco 3.
Example N4 := Aco 4.

(** Variables, for convenience *)

Example X := Ava 1.
Example Y := Ava 2.
Example Z := Ava 3.

(** Arithmetic expressions *)

(** exp1 = x + 3 *)
Example E1 := Apl X N3.

(** exp2 = y - 1 *)
Example E2 := Asu Y N1.

(** exp3 = (x + y) * 2 *)
Example E3 := Amu (Apl X Y) N2.

Compute (evalA E1 S1).
Compute (evalA E1 S2).
Compute (evalA E2 S1).
Compute (evalA E2 S2).
Compute (evalA E3 S1).
Compute (evalA E3 S2).

(** Boolean expressions *)

(** B1 :=  exp1 = 4 *)
Definition B1 := Beqnat E1 N4.

(** B2 := not ( bexp1 /\ (exp1 = 7) *)
Definition B2 := Bnot (Band B1 (Beqnat X N2)).

Compute (evalB B1 S1).
Compute (evalB B1 S2).
Compute (evalB B2 S1).
Compute (evalB B2 S2).

(** Functional semantics of [winstr]: we get a failure *)

Fail Fixpoint evalW (i : winstr) (s : state) {struct i} : state :=
  match i with
  | Skip       => s
  | Assign x a => update s x (evalA a s)
  | Seq i1 i2  => let s1 := evalW i1 s in evalW i2 s1
               (*   (evalW i2 (evalW i1 s) *)
  | If e i1 i2 => match evalB e s with
                  | true  => evalW i1 s
                  | false => evalW i2 s
                  end
  | While e i1 => match evalB e s with
                  | true  =>
                    let s1 := evalW i1 s in evalW (While e i1) s1
               (*   let s1 := evalW i1 s in evalW i s1                *)
                  | false => s
                  end
  end.

(** Relational version, 
    called "natural semantics" or "big steps operational semantics".
    It is an inductive relation. *)

Inductive NS : winstr -> state -> state -> Prop :=
| NS_Skip        : forall s,
                   NS Skip s s
| NS_Assign      : forall x a s,
                   NS (Assign x a) s (update s x (evalA a s))
| NS_Seq         : forall i1 i2 s s1 s2,
                   NS i1 s s1 -> NS i2 s1 s2 -> NS (Seq i1 i2) s s2
| NS_If_true     : forall b i1 i2 s s1,
                   (evalB b s = true)  ->  NS i1 s s1 -> NS (If b i1 i2) s s1
| NS_If_false    : forall b i1 i2 s s2,
                   (evalB b s = false) ->  NS i2 s s2 -> NS (If b i1 i2) s s2
| NS_While_false : forall b i s,
                   (evalB b s = false) ->  NS (While b i) s s
| NS_While_true  : forall b i s s1 s2,
                   (evalB b s = true)  ->  NS i s s1 -> NS (While b i) s1 s2 ->
                   NS (While b i) s s2
.

(** A WHILE program [P1] corresponding to
    while not (i=0) do {i := i-1; x := 1+x} *)
Example Il := 0.
Example Ir := Ava Il.
Example Xl := 1.
Example Xr := Ava Xl.

Example body_loop := Seq (Assign Il (Asu Ir N1)) (Assign Xl (Apl N1 Xr)).
Example P1 := While (Bnot (Beqnat Ir N0)) body_loop.

(** We prove that [P1] transforms state [S1] into state [S2]  *)

Theorem reduction1 : NS P1 S1 S2.
(** Pay attention to the current state throughout the proof *)
Proof.
  cbv [P1]. cbv [S1]. cbv [S2].
  (** Equivalently:
  unfold P1. unfold S1. unfold S2. *)

  (** This goal should be proved by one of the two last rules of [NS],
      that relate to the [While] case.
      We can guess which one, or ask for help like this: *)
  Compute (evalB (Bnot (Beqnat Ir N0)) [1; 2]).
  (** Then [NS_While_true] is the right one.
      We can try to progress with [apply NS_While_true.]  ... but it fails.
      Here Coq cannot guess the intermediate state [s1]. *)
  Fail apply NS_While_true.
  (** A possible strategy could be to directly add the intermediate
      state using the [with] clause of [apply]: [apply ... with (s1:= ...)].
      We then have to guess the right parameters, which is not always that easy.
      In our situation it would be: *)
  apply NS_While_true with (s1:=[0;3]).
  (** We then propose another strategy. *)
  Undo 1.
  (** A first option is to use [refine] :
      here we provide a wildcard [_] for each one of the EIGHT arguments;
      [b], [i], [s] et [s2] are then determined by the form of the the goal,
      [s1] is determined by the proof of [NS s i s s1] and therefore does not 
      give rise to a sub-goal. It will remain to be proven:
      [evalB b s = true], [NS i s s1] and [NS (While b i) s1 s2].  *)
  refine (NS_While_true _ _ _ _ _ _ _ _).
  (** We obtain the same effect with tactic [eapply], more convenient. *)
  Undo 1.
  eapply NS_While_true.
  - cbn. reflexivity.
  - cbv [body_loop].
    (** A new intermediate state has to be guessed. *)
    eapply NS_Seq.
    + apply NS_Assign.
    (* By applying this rule we fixed the value of the arrival state. *)
    + (* the starting state comes from the previous sub-goal;
         as the states are known we can simplify. *)
      cbn [evalA Ir Il N1 get minus update].
      (** Or, more quickly: *)
      Undo 1.
      cbn.
      apply NS_Assign.
  - cbn.
    (** [NS_While_true] or [NS_While_false]? *)
    Compute (evalB (Bnot (Beqnat Ir N0)) [0; 3]).
    apply NS_While_false.
    cbn.
    reflexivity.
Qed.

(** Exercise on paper (LEVEL 1) :
    finish the presentation below of [reduction1] in the form of a tree *)

(*











 evalB "i<>0" [1; 2] = true          NS body [1; 2] [0; 3]                                  NS P1 [0; 3] [0; 3]
------------------------------------------------------------------------------------------------------------------ NS_While_true
                                     NS P1 [1; 2] [0; 3]

 *)

(** Here is another presentation of the script, structured by curly braces.
    This allows us to get another managing  of indentation
    (especially useful when the body of the loop runs several times. *)
Theorem reduction1_braces : NS P1 S1 S2.
Proof.
  cbv [P1]. cbv [S1]. cbv [S2].
  eapply NS_While_true.
  { cbn. reflexivity. }
  { cbv [body_loop].
    eapply NS_Seq.
    + apply NS_Assign.
    + cbn. apply NS_Assign. }
  cbn.
  Compute (evalB (Bnot (Beqnat Ir N0)) [0; 3]).
  apply NS_While_false.
  cbn. reflexivity.
Qed.

(** Training exercice *)

Theorem training_P1 : NS P1 [2; 5] [0; 7].
Proof.
  (* Complete here LEVEL 1 *)
Admitted.

(** Now we wnat to prove that whatever the initial state, [P1] returns a state
    where the value of [i] is 0 and the value of [x] was incremented by the
    initial value of [i]. *)

(** Recall that here, natural numbers are defined by an inductive type
    with the constructors O for zero and S for the successor. *)

Print nat.
Require Import Arith. (* for Nat.sub_0_r *)
Check Nat.sub_0_r.

(** The following lemmas of the Coq library can be useful:
    - Lemma Nat.sub_0_r : forall n, n - 0 = n.
    - Lemma minus_n_O :   forall n, n = n - 0. (* obsolete since coq.8.16.0 *)
    - Lemma plus_n_Sm :   forall n m, S (n + m) = n + S m. *)

Theorem reduction2 : forall x y, NS P1 [x;y] [0;x+y].
Proof.
  cbv [P1 Ir Il N1 Xr Xl]; intros x.
  induction x as [ | x IH_x];
    intros; cbn [evalA];cbn [evalB].
  (** complete here LEVEL 2 *)
Admitted.

(** *** Computation of the square of a number using only additions *)
(** Here is a While program Psquare corresponding to
    while not (i=n) do {i:= 1+i; x:= y+x ; y:= 2+y} *)
(* (* already defined *)
Example Il := 0.
Example Ir := Ava Il.
Example Xl := 1.
Example Xr := Ava Xl.*)
Example Yl := 2.
Example Yr := Ava Yl.

Example incrI := Assign Il (Apl N1 Ir).
Example incrX := Assign Xl (Apl Yr Xr).
Example incrY := Assign Yl (Apl N2 Yr).
Example body_square := Seq incrI (Seq incrX incrY).
Example Psquare_2 := While (Bnot (Beqnat Ir (Aco 2))) body_square.
Example Psquare n := While (Bnot (Beqnat Ir (Aco n))) body_square.

Theorem reduction_Psquare_2 : NS (Psquare_2) [0;0;1] [2;4;5].
Proof.
  (** complete here LEVEL 1 *)
Admitted.

(** State and prove that [Psquare n] computes the square of [n] *)
(* complete here LEVEL 4
   (no new technique, but requires a little bit of creativity *)

(** On the same scheme, find a program [Pcube] using only
    additions, state and prove its correctness. *)
(** complete here LEVEL 6 *)

(** A few useful lemmas. *)

Check Nat.add_comm.
Check Nat.add_assoc.
Check plus_assoc.

(* -------------------------------------------------------------------------- *)
(** ** Proofs by structural induction on an inductive predicate *)


(** A simple program transformation:
   -  [if true  then X else Y] ---> [X]
   -  [if false then X else Y] ---> [Y]  *)
Fixpoint simpl_test_Btrue_Bfalse (i: winstr) : winstr :=
  match i with
  | Skip => Skip
  | Assign v a => i
  | Seq w1 w2 => Seq (simpl_test_Btrue_Bfalse w1)
                     (simpl_test_Btrue_Bfalse w2)
  | If Btrue i1 i2 => simpl_test_Btrue_Bfalse i1
  | If Bfalse i1 i2 =>
      (* remove the fake [i] and the fake last case, then complete here LEVEL 1 *)
      i2
  | _ => i
  end.

(** Comme indicated in the title we will proceed by structural induction on
     the proof trees of [NS i s s'] *)
Theorem simpl_test_Btrue_Bfalse_correct :
  forall i s s', NS i s s' -> NS (simpl_test_Btrue_Bfalse i) s s'.
Proof.
  (** We first try an induction on [i].
      Even with care, in the most general possible way
      (states [s] and [s'], as well as hypothesis [NS i s s'] are
      introduced AFTER [induction i]), we will see that the goals are
      not as expected. *)
  intro i.
  induction i as [ | | | | ]; (** without naming the components to lighten the script *)
    intros s s' ns (** introductions are systematically performed
                       on each sub-goal *).
  (** Observe that the hypothesis [ns] should entail [s = s'],
      but we did not get it;
      similar issues occur on all other subgoals. *)
  Undo 2.
  (** It is much more appropriate to reason by structural induction on [ns] because
      we directly get not only the decomposition of [i] but, in addition,
      contraints dictated by the definition of [NS] *)
  intros i s s' ns.
  induction ns as  [ (* NS_Skip *) s
                   | (* NS_Assign *) x s a
                   | (* NS_Seq *) i1 i2 s s1 s' ns1 ih_ns1 ns2 ih_ns2
                   | (* NS_If_true *) cond i1 i2 s s' e ns ih_ns
                   | (* NS_If_false *) cond i1 i2 s s' e ns ih_ns
                   | (* NS_While_false *) (* complete here LEVEL 1 *)
                   | (* NS_While_true *) (* complete here LEVEL 1 *)
                   ]; cbn [simpl_test_Btrue_Bfalse].

 (** The proof to follow is somewhat tedious, we will see later some tricks
     allowing us to make it in a more clever way. *)
 (** A number of goals will contain a hypothesis convertible to
     [false = true] (use [cbn in ...] to make this appear).
     We can remember a technique seen before (contagious equalities).
  *)
(** complete here
     - many sub-goals LEVEL 2
     - some sub-goals LEVEL 3, you can use [admit] to move on *)
Admitted.

(* -------------------------------------------------------------------------- *)
(** Another simple transformation (optional, just training)
  -  if (Bnot b) then X else Y ---> if b then Y else X  *)

Fixpoint simpl_test_exchange (i: winstr) : winstr.
  (** complete here LEVEL 1 *)
Admitted.

Lemma negb_negb : forall b, b = negb (negb b).
Proof.
  (** complete here LEVEL 1 *)
Admitted.

Lemma Bnot_negb : forall {B s b}, evalB (Bnot B) s = b -> evalB B s = negb b.
Proof.
 (** complete here LEVEL 1 *)
Admitted.

(** Use the same approach as for [simpl_test_Btrue_Bfalse_correct]. *)
Theorem simpl_test_exchange_correct :
  forall i s s', NS i s s' -> NS (simpl_test_exchange i) s s'.
Proof.
(** complete here
     - many sub-goals LEVEL 2
     - some sub-goals LEVEL 3, you can use [admit] to move on *)
Admitted.

(* -------------------------------------------------------------------------- *)
(** ** Interlude on inversion *)

(** In the following exercise, we will get a goal containing
    a hypothesis of the form [NS i s s2],
    where [i] is itself of the form [Seq i1 i2]    (1).
    Without condition (1), it would be natural to proceed by
    case on the [NS] hypothesis, which would give rise to its seven cases;
    but with condition (1), we see that only a single case on the seven
    is relevant, correponding to [NS_Seq].
    This proof technique is called "by inversion".
    We will get a simpler situation thanks to the next auxiliary
    predicate, that isolates the relevant case of [NS].
 *)

Inductive NS1_Seq i1 i2 s s2 : Prop :=
| NS1_Seq_intro : forall s1,
                  NS i1 s s1 -> NS i2 s1 s2 -> NS1_Seq i1 i2 s s2
.

(** We can then prove the following consequence of an hypothesis
    respecting condition (1) above *)

Lemma inv_Seq' : forall {i1 i2 s s2}, NS (Seq i1 i2) s s2 -> NS1_Seq i1 i2 s s2.
Proof.
  intros i1 i2 s s2 ns.
  (** At the moment, let us first use a magic tactic of Coq. *)
  inversion ns.
  (** Then another, to clean equalities. *)
  subst.
  apply (NS1_Seq_intro _ _ _ _ _ H1 H4).
Qed.

(** Small inversions. Given a goal such as:

 H18 : NS (Seq i1 i2) s s2
 =========================
 conclusion

Instead of
  [destruct H18]
that yields 7 cases, observe that
[inv_Seq' H18]   is of type   [NS1_Seq i1 i2 s s2]
so we can more appropriately use
 [ destruct (inv_Seq' H18) as [s1 ns1 ns2] ]
that considers only one case, the relevant one.
 *)

(** ** Small inversions (advanced topic *)

(** You can skip this at first reading *)

(** Here is a proof of the same theorem using "small inversions",
    that uses only a knowledge of the elementary constructs see before
    -- and no magics!
    In particular, remember program "waow_woaw" (see coq01_init_theory2.v)
    It is not essential to understand it before its use.
    OPTIONAL EXERCISES:
    1) Explain how this proof works.
    2) In the following scripts, use [NS_inv] instead of [inv_Seq]
       (interest: this can be generalized).
 *)
Inductive NS1_trivial (s s1 : state) : Prop := Triv : NS1_trivial s s1.

Definition dispatch (i: winstr) : state -> state -> Prop :=
  match i with
  | Seq i1 i2 => NS1_Seq i1 i2
  | _         => NS1_trivial
  end.

Definition NS_inv {i s s2} (ns : NS i s s2) : dispatch i s s2 :=
  match ns with
  | NS_Seq i1 i2 s s1 s2 ns1 ns2 =>
    NS1_Seq_intro _ _ _ _ s1 ns1 ns2
  | _ => Triv _ _
  end.

Lemma inv_Seq : forall {i1 i2 s s2}, NS (Seq i1 i2) s s2 -> NS1_Seq i1 i2 s s2.
Proof.
  intros * ns. apply (NS_inv ns).
Qed.

(** *** Illustration *)
(** Here is another way to express the semantics of the WHILE language;
    we will prove that [NS] and [NS'] are equivalent. *)
Inductive NS' : winstr -> state -> state -> Prop :=
| NS'_Skip        : forall s,
                    NS' Skip s s
| NS'_Assign      : forall x a s,
                    NS' (Assign x a) s (update s x (evalA a s))
| NS'_Seq         : forall i1 i2 s s1 s2,
                    NS' i1 s s1 -> NS' i2 s1 s2 -> NS' (Seq i1 i2) s s2
| NS'_If_true     : forall b i1 i2 s s1,
                    (evalB b s = true)  ->  NS' i1 s s1 -> NS' (If b i1 i2) s s1
| NS'_If_false    : forall b i1 i2 s s2,
                    (evalB b s = false) ->  NS' i2 s s2 -> NS' (If b i1 i2) s s2
| NS'_While_false : forall b i s,
                    (evalB b s = false) ->  NS' (While b i) s s
| NS'_While_true  : forall b i s s1,
                    (evalB b s = true)  ->  NS' (Seq i (While b i)) s s1 ->
                    NS' (While b i) s s1
.


(** The following direction does not raise any new difficulty *)
Lemma NS_NS' : forall i s s1, NS i s s1 -> NS' i s s1.
Proof.
  intros i s s1 ns.
  induction ns as  [ (* NS_Skip *) s
                   | (* NS_Assign *) x s a
                   | (* NS_Seq *) i1 i2 s s1 s' ns1 ih_ns1 ns2 ih_ns2
                   | (* NS_If_true *) cond i1 i2 s s' e ns ih_ns
                   | (* NS_If_false *) cond i1 i2 s s' e ns ih_ns
                   | (* NS_While_false *) (* complete here LEVEL 1 *)
                   | (* NS_While_true *)  (* complete here LEVEL 1 *)
                   ].
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - (** The most interesting sub-goal, where [NS] and [NS'] are expressed
        in a different way. *)
    apply NS'_While_true.
    + admit (** complete here LEVEL 1 *).
    + eapply NS'_Seq.
      -- admit (** complete here LEVEL 2 *).
      -- admit (** complete here LEVEL 2 *).
Admitted.

(** The script of the converse is similar EXCEPT in the last sub-goal,
    that precisely requires an inversion. *)
Lemma NS'_NS : forall i s s1, NS' i s s1 -> NS i s s1.
Proof.
  intros i s s1 ns'.
  induction ns' as [ (* NS_Skip *) s
                   | (* NS_Assign *) x s a
                   | (* NS_Seq *) i1 i2 s s1 s' ns1 ih_ns1 ns2 ih_ns2
                   | (* NS_If_true *) cond i1 i2 s s' e ns ih_ns
                   | (* NS_If_false *) cond i1 i2 s s' e ns ih_ns
                   | (* NS_While_false *) cond i s e
                   | (* NS_While_true *)
                     cond i s s' e ns ih_ns
                   ].
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - admit (** complete here LEVEL 1 *).
  - (** LEVEL 4 *)
    (** Here we have to exploit hypothesis
        [ih_ns : NS (Seq i (While cond i)) s s'].
        Observe that this hypothesis is of the form [NS (Seq i1 i2) s s']
        which is a special case of [NS i s s']:
        however a [destruct ih_ns] would ignore that we are 
        in this special case *)
    destruct ih_ns as [ | | | | | | ].
    + (** The current sub-goal corresponds to the case where
          [Seq i (While cond i)] would be [Skip] at the same time,
          an irrelevant situation. *)
      Undo 1.
    Undo 1.
    (** This is solved by using the consequence of [ih_ns]
        obtained by [inv_Seq].
        See "small inversions" presented above.
     *)
    Check (inv_Seq ih_ns).
    destruct (inv_Seq ih_ns) as [s1 ns1 ns2].
    (** We solve the sub-goal by using [NS_While_true] *)
    + eapply NS_While_true.
      -- apply e.
      -- apply ns1.
      -- apply ns2.
Admitted.

(* -------------------------------------------------------------------------- *)
(** ** The REPEAT language *)
(** Now we consider an imperative language without the [While] construct,
    but containing instead another instruction for loops
                       [repeat i until b]
    that executes [i] then exits the loop if [b] evuluates to [true], and
    restarts the loop otherwise.
 *)

(** Here is the syntax of the REPEAT language
    (we define a new type with new constructor.    *)

Inductive rinstr :=
| RSkip   : rinstr
| RAssign : nat -> aexp -> rinstr
| RSeq    : rinstr -> rinstr -> rinstr
| RIf     : bexp -> rinstr -> rinstr -> rinstr
| Repeat  : rinstr -> bexp -> rinstr.

(** Define the natural semantics of the REPEAT language. *)

Inductive NSr: rinstr -> state -> state -> Prop :=
| NSr_Skip        : forall s,
                    NSr RSkip s s
| NSr_Assign      : forall x e s,
                    NSr (RAssign x e) s (update s x (evalA e s))
| NSr_Seq         : forall i1 i2 s s1 s2,
                    NSr i1 s s1 -> NSr i2 s1 s2 -> NSr (RSeq i1 i2) s s2
| NSr_If_true     : forall b i1 i2 s s1,
                    evalB b s = true -> NSr i1 s s1 -> NSr (RIf b i1 i2) s s1
| NSr_If_false    : forall b i1 i2 s s2,
    evalB b s = false -> NSr i2 s s2 -> NSr (RIf b i1 i2) s s2
(** (* uncomment and complete here *)
| NSr_Repeat_true : (** complete here LEVEL 2 *)
| NSr_Repeat_false: (** complete here LEVEL 2 *)
 *)
.

(** We encode in REPEAT a program [P2] corresponding to
    repeat {i := i-1; x := 1+x} until i=0 *)

Example body_loopR : rinstr. (** complete here LEVEL 1 *) Admitted.
Example P2 := Repeat body_loopR (Beqnat Ir N0).

Lemma P2_test : NSr P2 [2; 5] [0; 7].
Proof.
  (** complete here LEVEL 1 *)
Admitted.

(** You could draw [P2_test] in the form of a proof-tree *)

(** *** Proofs on [NSr] *)
(** We want to prove that:  [Repeat i until b]
    could be translated as: [i; while (not b) do i]     *)

(** Write a function that translates any [rinstr] expression into a [winstr]
    expression, by recursively replacing the Repeat constructs by the equivalent 
    expression above.
 *)

Fixpoint repeat_while (i:rinstr) : winstr :=
    match i with
    | RSkip        => Skip
    | RAssign v a  => Assign v a
      (* remove the fake last case, then complete here LEVEL 2 *)
    | _ => Skip
    end.

(** Before tackling the next proof, it is worth to check on a small
    REPEAT program that, after transformation, its execution from
    a concrete initial state indeed gives the same final state.
*)

(** Prove that this transformation preserves the semantics. *)

Theorem repeat_while_correct : forall i s1 s2, NSr i s1 s2 -> NS (repeat_while i) s1 s2.
Proof.
  intros i s1 s2 ns.
            (* complete here LEVEL 3 *)
Admitted.

(* -------------------------------------------------------------------------- *)
(** Converse transformation *)
Fixpoint while_repeat (i:winstr) : rinstr :=
    match i with
    | Skip        => RSkip
    | Assign v a  => RAssign v a
      (* remove the fake last case, then complete here LEVEL 2 *)
    | _ => RSkip
    end.

(** Before tackling the next proof, it is worth to check on a small
    REPEAT program that, after transformation, its execution from
    a concrete initial state indeed gives the same final state.
*)

(** Prove that this transformation preserves the semantics. *)
(** The next proof requires additional techniques,
    to be considered only after the nex lectures. *)

Theorem while_repeat_correct :
  forall i s1 s2, NS i s1 s2 -> NSr (while_repeat i) s1 s2.
Proof.
  intros i s_1 s_2 ns.
            (** complete here LEVEL 5 *)
Admitted.

(* -------------------------------------------------------------------------- *)
(** ** The language WHILE-REPEAT *)
(** Remark: we could also consider a WHILE_REPEAT language
    containing the two instructions [While] and [Repeat].
 *)