(* Faire les preuves suivantes. *)

Lemma ex1 : forall A B C:Prop, A/\(B/\C)->(A/\B)/\C.
Qed.

Lemma ex2 : forall A B C D: Prop,(A->B)/\(C->D)/\A/\C -> B/\D.
Qed.

Lemma ex3 : forall A: Prop, ~(A/\~A).
Qed.

Lemma ex4 : forall A B C: Prop, A\/(B\/C)->(A\/B)\/C.
Qed.

Lemma ex5 : forall A B: Prop, (A\/B)/\~A -> B.
Qed.

(* Nous allons maintenant travailler sur les données représentant
  un petit langage de programmation. *)
Require Import String ZArith.  Open Scope Z_scope.

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


(* La fonction suivante peut être utilisée pour comparer deux chaines de
   caractères *)

Definition string_eq x y :=
  if string_dec x y then true else false.

(* Exemple de calcul. *)

Eval vm_compute in string_eq "a" "a".
Eval vm_compute in string_eq "a" "b".

(* Travail à faire: écrire une fonction subst_aexpr qui remplace
  toutes les occurrences de la variable de nom x par l'expression e_x
  dans e. *)

Fixpoint subst_aexpr (e : aexpr) (x : string) (e_x : aexpr) : aexpr :=
....

(* Si vous avez bien fait l'exercice, la preuve suivante doit passer
  sans modification. *)
Lemma example : subst_aexpr (aplus (avar "a") (avar "b")) "a" (avar "b") =
                aplus (avar "b") (avar "b").
reflexivity.
Qed.

(* Travail à faire: écrire une fonction qui évalue une expression
 arithmétique dans une valuation f, qui associe à toute chaine de caractère
 une valeur entière. *)

Fixpoint af' (g : string -> Z) (e : aexpr) : Z :=
....


(* Si vous avez bien fait l'exercice, la preuve suivante doit passer sans
  modification. *)

Lemma example2 : af' (fun s => if string_eq s "a" then 1
                               else if string_eq s "b" then 3
                               else 0) (aplus (avar "a") (avar "b")) = 4.
reflexivity.
Qed.