(***********************************************************)
(* sémantique naturelle codée en Coq du petit langage      *)
(* impératif WHILE déjà vu précédemment.                   *)
(* On va l'utiliser pour faire des dérivations, montrer    *)
(* des propriétés, étudier des extensions.                 *)
(***********************************************************)

(* On importe les bibliothèques de Coq utiles   *)

Require Import Bool Arith List.
Import List.ListNotations.

(** * On choisit de définir ici un état comme une liste d'entiers naturels.
      On utilise ici le type list de la bibliothèque standard de Coq.
      Ce type est polymorphe. On le spécialise pour des éléments de type nat. *)

(* ============================================================================= *)
(** * On reprend ici les AST définis aux séances précédentes *)

(** ** Syntaxe des expressions arithmétiques *)

Inductive aexp :=
| Aco : nat -> aexp (** constantes *)
| Ava : nat -> aexp (** variables *)
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Amo : aexp -> aexp -> aexp
.

(** ** Syntaxe des expressions booléennes *)

Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp -> bexp
| Band : bexp -> bexp -> bexp
| Bor : bexp -> bexp -> bexp
| Beq : bexp -> bexp -> bexp (* test égalité de bexp *)
| Beqnat : aexp -> aexp -> bexp (* test égalité d'aexp *)
.

(** ** Syntaxe du langage impératif WHILE *)

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

(** ** Quelques listes/états pour faire des tests *)
(** S1 est un état dans lequel la variable '0' vaut 1 et la variable '1' vaut 2
    et toutes les autres '0' (valeur par défaut)                             *)
(** Une variable (Ava i) étant représentée par un entier naturel i,
    sa valeur dans l'état est la valeur de la ieme position de la liste *)

Definition state := list nat.

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

(* ============================================================================= *)
(** * Sémantique *)
(** On reprend les sémantiques fonctionnelles
    des expressions artihmétiques et booléennes      *)

(** La fonction get x s rend la valeur de x dans s. *)
(** Elle rend 0 par défaut, par exemple si la variable
    n'est pas définie/initialisée    *)

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

(** Exemples *)

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

(** La mise à jour d'une variable v par un nouvel entier n dans un état s
    s'écrit 'update s v n'
    Cette fonction n'échoue jamais et écrit la valeur à sa place même
    si elle n'est pas encore définie dans l'état *)

Fixpoint update (s:state) (v:nat) (n:nat): state :=
match v,s with
| 0   , a :: l1 => n :: l1
| 0   , nil     => n :: nil
| S v1, a :: l1 => a :: (update l1 v1 n)
| S v1, nil     => 0 :: (update nil v1 n) end.

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

Compute S1.
Compute S4.

(** ** Sémantique fonctionnelle de 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
  | Amo a1 a2 =>  evalA a1 s - evalA a2 s
  end.


(** ** Sémantique fonctionnelle de 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.

(** Pour définir plus facilement des expressions de test on prédéfinit
    des constantes entières ... *)

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

(** ...  et des variables *)

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


(** Quelques expressions arithmétiques pour tester *)

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

(** exp2 = y - 1 *)
Definition E2 := Amo Y N1.

(** exp3 = (x + y) * 2 *)
Definition 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).

(** Quelques expressions booléennes pour tester *)

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

(** ** Version relationnelle, appelée "sémantique naturelle" *)

(** Vu dans le CM précédent.
    La sémantique naturelle (ou sémantique opérationnelle à grands pas)
    du langage WHILE est donnée sous la forme d'un prédicat inductif. *)

Inductive SN : winstr -> state -> state -> Prop :=
| SN_Skip        : forall s,
                   SN Skip s s
| SN_Assign      : forall x a s,
                   SN (Assign x a) s (update s x (evalA a 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 b i1 i2 s s1,
                   (evalB b s = true)  ->  SN i1 s s1 -> SN (If b i1 i2) s s1
| SN_If_false    : forall b i1 i2 s s2,
                   (evalB b s = false) ->  SN i2 s s2 -> SN (If b i1 i2) s s2
| SN_While_false : forall b i s,
                   (evalB b s = false) ->  SN (While b i) s s
| SN_While_true  : forall b i s s1 s2,
                   (evalB b s = true)  ->  SN i s s1 -> SN (While b i) s1 s2 ->
                   SN (While b i) s s2
.

(** On code dans WHILE un programme P1 correspondant à
    while not (i=0) do {i:=i-1;x:=1+x} *)
Definition Il := 0.
Definition Ir := Ava Il.
Definition Xl := 1.
Definition Xr := Ava Xl.

Definition corps_boucle := Seq (Assign Il (Amo Ir N1)) (Assign Xl (Apl N1 Xr)).
Definition P1 := While (Bnot (Beqnat Ir N0)) corps_boucle.

(** On montre que P1 transforme l'état S1 en l'état S2  *)

Theorem reduction1 : SN P1 S1 S2.
(** Regarder les états courants tout au long de la preuve *)
Proof.
  cbv [P1]. cbv [S1]. cbv [S2].
  (** Ou de façon équivalente :
  unfold P1. unfold S1. unfold S2. *)

  (** Ce but devrait être prouvé par l'une des deux dernières règles de SN,
      qui portent sur le cas While.
      On peut deviner laquelle de tête, ou demander de l'aide ainsi : *)
  Compute (evalB (Bnot (Beqnat Ir N0)) [1; 2]).
  (** Ce sera donc avec SN_While_true.
      On peut essayer d'avancer avec 'apply SN_While_true.'  ... mais ça échoue.
      Ici Coq ne peut pas deviner ce que sera l'état intermédiaire s1. *)
  Fail apply SN_While_true.
  (** Une stratégie possible serait d'indiquer directement l'état
      intermédiaire avec la variante 'apply ... with (s1:= ...)'.
      Il faut deviner les paramètres corrects ce qui n'est pas toujours facile.
      Dans notre cas cela serait : *)
  apply SN_While_true with (s1:=[0;3]).
  (** On va donc proposer une autre stratégie· *)
  Undo 1.
  (** Une première possibilité est avec refine, déjà connu :
      ici on indique un joker '_' pour chacun des HUIT arguments ;
      [b], [i], [s] et [s2] se trouvent déterminés par la forme du but,
      [s1] sera déterminé par la preuve de [SN s i s s1] et ne donne donc
      pas lieu à un sous-but. Il restera à prouver :
      [evalB b s = true], [SN i s s1] et [SN (While b i) s1 s2].  *)
  refine (SN_While_true _ _ _ _ _ _ _ _).
  (** On obtient le même effet avec la tactique [eapply], plus commode. *)
  Undo 1.
  eapply SN_While_true.
  - reflexivity.
  - cbv [corps_boucle].
    (** Un nouvel état intermédiaire est à deviner *)
    eapply SN_Seq.
    + apply SN_Assign.
    (* En appliquant cette règle nous avons fixé la valeur de l'état d'arrivée *)
    + (* L'état de départ vient du cas précédent ;
         comme les états sont connus on peut simplifier. *)
      cbn [evalA Ir Il N1 get minus update].
      (** Ou, plus rapidement *)
      Undo 1.
      cbn.
      apply SN_Assign.
  - cbn.
    (** SN_While_true ou SN_While_false ? *)
    Compute (evalB (Bnot (Beqnat Ir N0)) [0; 3]).
    apply SN_While_false.
    cbn.
    reflexivity.
Qed.

(** ICI 1 : présenter reduction1 sous forme d'arbre *)

(*

          ------------------------- SN:=    ------------------------- SN:=
          SN "i:=i-1" [1; 2] [0; 2]         SN "x:=1+x" [0; 2] [0; 3]
          ----------------------------------------------------------- SN_Seq
                            SN corps [1; 2] [0; 3]
                                          \
                                           \
                                            \                   --------------------------- =refl
                                             \                  evalB "i<>0" [0; 3] = false
-------------------------- =refl    .....................       --------------------------- SN_While_false
evalB "i<>0" [1; 2] = true          SN corps [1; 2] [0; 3]         SN P1 [0; 3] [0; 3]
-------------------------------------------------------------------------------------- SN_While_true
                                    SN P1 [1; 2] [0; 3]



 *)


(** Une autre présentation de ce script, structurée par accolades.
    Cela permet de gérer l'indentation autrement
    (surtout utile quand le corps de boucle s'exécute plusieurs fois. *)
Theorem reduction1_accolades : SN P1 S1 S2.
Proof.
  cbv [P1]. cbv [S1]. cbv [S2].
  eapply SN_While_true.
  { cbn. reflexivity. }
  { cbv [corps_boucle].
    eapply SN_Seq.
    + apply SN_Assign.
    + cbn. apply SN_Assign. }
  cbn.
  Compute (evalB (Bnot (Beqnat Ir N0)) [0; 3]).
  apply SN_While_false.
  cbn. reflexivity.
Qed.