(* ---------------------------------------------------------------------- *)
(** * Sémantique naturelle du langage WHILE  *)

(** On se concentre sur winstr, sans prendre la peine de reprendre
    le travail fait auparavant sur aexp et bexp.
    NORMALEMENT IL FAUDRAIT LE𝕊RECOPIER
    (ou utiliser un mécanisme de compilation séparée)
    au lieu d'utiliser "Parameter", dont l'effet est analogue
    à "Admitted".
 *)
Parameter aexp : Set.
Parameter bexp : Set.

Inductive state :=
  | Nil : state
  | Cons : nat -> state -> state
.

(** On se donne des notations préalables pour faciliter la présentation *)
Notation "[]" := Nil.
Notation "x :: y" := (Cons x y).

Parameter evalA : aexp -> state -> nat.
Parameter evalB : bexp -> state -> bool.

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

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

(** Corrigé du travail effectué en TD *)
Fail Fixpoint evalW (i : winstr) (s : state) {struct i} : state :=
  match i with
  | Skip       => s
  | Assign x e => update x (evalA e s) 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) as i => 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.

(** Version relationnelle, appelée "sémantique naturelle" *)
Inductive SN: winstr -> state -> state -> Prop :=
| SN_Skip        : forall s,
                   SN Skip s s
| SN_Assign      : forall x e s,
                   SN (Assign x e) s (update x (evalA e s) s)
| SN_Seq         : forall i1 i2 s s1 s2,
                   SN i1 s s1 -> SN i2 s1 s2 -> SN (Seq i1 i2) s s2
| SN_If_true     : forall e i1 i2 s s1,
                   (evalB e s = true)  ->  SN i1 s s1 -> SN (If e i1 i2) s s1
| SN_If_false    : forall e i1 i2 s s2,
                   (evalB e s = false) ->  SN i2 s s2 -> SN (If e i1 i2) s s2
| SN_While_false : forall e i s,
                   (evalB e s = false) ->  SN (While e i) s s
| SN_While_true  : forall e i s s1 s2,
                   (evalB e s = true)  ->  SN i s s1 -> SN (While e i) s1 s2
               ->  SN (While e i) s s2
.