Require Import List ZArith String.
Open Scope Z_scope.
Open Scope string_scope.

Inductive aexpr : Type :=
 avar (x : string) | anum (n : Z) | aplus (e1 e2 : aexpr).

(* Nous encoderons les environnements par des listes de paires. *)

Definition env := list (string*Z).

(* Voici l'encodage en Coq des règles d'évaluation pour les expressions
  arithmétiques. *)

Inductive aeval : env -> aexpr -> Z -> Prop :=
  ae_int : forall r n, aeval r (anum n) n
| ae_var1 : forall r x v, aeval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' , x <> y -> aeval r (avar x) v' ->
              aeval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
              aeval r e1 v1 -> aeval r e2 v2 ->
              aeval r (aplus e1 e2) (v1 + v2).


(* exemple de preuve d'évaluation.  Faites exécuter cette preuve dans
  Coq pour voir dans quel cas chaque tactique s'utilise. *)

Lemma ex1 : aeval (("x",3)::("y", 5)::nil) (aplus (avar "x")(avar "y")) 8.
apply ae_plus with (v1:=3) (v2:=5).
apply ae_var1.
apply ae_var2.
discriminate.
apply ae_var1.
Qed.

(* Le type de données option permet de décrire des données optionnelles.
   La valeur None représente une donnée non définie. 
   La valeur Some x représente x, dans le type option.

   Pour récupérer une valeur dans un type option, il faut tenir compte
   du cas None.  Ceci se fait par filtrage.

   match opt_v with None => .... | Some v => ... v ... end

   Manipuler des valeurs optionnelles est difficile.  La solution passe
   pratiquement pour toujours.  Voir à la fin du fichier comment faire pour
   additionner deux valeurs optionnelles.
   
*)

     

(* Ecrivez une fonction qui calcule la valeur des expressions arithmétiques.
   Rappelez-vous qu'on peut tester l'égalité de deux chaines de caractères
   en utilisant la construction suivante:
   if string_dec s1 s2 then ... else ... *)

Fixpoint lookup (l:list (string*Z)) (x:string) {struct l} : option Z :=
  match l with nil =>
    None
  | (y,n)::tl => if string_dec x y then Some n else lookup tl x
  end.

Definition o_add (ov1 ov2 : option Z) : option Z :=
  match ov1 with
    Some v1 => match ov2 with Some v2 => Some (v1 + v2) | None => None end
  | None => None
  end.

Fixpoint af (l:list (string * Z)) (e:aexpr) {struct e} : option Z :=
  match e with
    avar x => lookup l x
  | anum n => Some n
  | aplus e1 e2 =>
    o_add (af l e1) (af l e2)
  end.

(* Faites la preuve que la fonction af est correcte. *)
Lemma lookup_correct : forall l x v, lookup l x = Some v -> aeval l (avar x) v.
induction l.
  simpl. 
  intros x v abs; discriminate.
simpl.
intros x v.
destruct a as [y n].
case (string_dec x y).
intros xy nv.
injection nv.
intros nv'; rewrite nv'.
rewrite xy.
apply ae_var1.
intros xny h.
apply ae_var2.
assumption.
apply IHl.
assumption.
Qed.

Lemma af_correct : forall l e v, af l e = Some v -> aeval l e v.
intros l e; induction e.
    simpl.
    intros v lk.
    apply lookup_correct.
    assumption.
  simpl. 
  intros v h.
  injection h.
  intros nv.
  rewrite nv.
  apply ae_int.
simpl.
intros v.
destruct (af l e1).
  destruct (af l e2).
    intros h; injection h.
    intros hv.
    rewrite <- hv.
    apply ae_plus.
      apply IHe1.
      reflexivity.
    apply IHe2.
    reflexivity.
  intros abs.
  discriminate.
intros abs.
discriminate.
Qed.

(* Deuxième partie.  Exécution des expressions booléennes. *)

Inductive bexpr := blt (e1 e2 : aexpr).

Inductive beval : env -> bexpr -> bool -> Prop :=
  b_true : forall r e1 e2 v1 v2,
     aeval r e1 v1 -> aeval r e2 v2 -> v1 < v2 ->
     beval r (blt e1 e2) true
| b_false : forall r e1 e2 v1 v2,
     aeval r e1 v1 -> aeval r e2 v2 -> v2 <= v1 ->
     beval r (blt e1 e2) false.

(* Exercice: construire une preuve pour l'énoncé suivant: *)

Lemma ex2:   beval (("x",2)::("y",3)::nil)
         (blt (aplus (avar "x") (anum 2)) (avar "y"))
         false.
apply b_false with (v1:= 4) (v2 := 3).
    apply ae_plus with (v1 := 2) (v2 := 2).
      apply ae_var1.
    apply ae_int.
  apply ae_var2.
  discriminate.
apply ae_var1.
omega.
Qed.

(* Annexe: comment additionner deux valeurs optionnelles. *)

(*
Definition o_add (ov1 ov2 : option Z) : option Z :=
  match ov1 with
    Some v1 => match ov2 with Some v2 => Some (v1 + v2) | None => None end
  | None => None
  end.
*)