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.

Lemma ex2 : aeval (("x", 2)::("y", 4)::("z", 7)::nil)
                (aplus (aplus (anum 1) (avar "y")) 
                       (aplus (avar "x") (aplus (anum 2) (avar "z"))))
                16.
(* C'est votre tour. *)
Qed.