(* Faire les preuves suivantes. *)

Lemma ex1 : forall A B C:Prop, A/\(B/\C)->(A/\B)/\C.
intros A B C h.
destruct h as [ha h].
destruct h as [hb hc].
split.
 split.
  exact ha.
 exact hb.
exact hc.
Qed.

Lemma ex2 : forall A B C D: Prop,(A->B)/\(C->D)/\A/\C -> B/\D.
intros A B C D h.
destruct h as [hb h].
destruct h as [hd h].
destruct h as [ha hc].
split.
 apply hb.
 exact ha.
apply hd.
exact hc.
Qed.

Lemma ex3 : forall A: Prop, ~(A/\~A).
intros A h.
destruct h as [ha hna].
case hna.
exact ha.
Qed.

Lemma ex4 : forall A B C: Prop, A\/(B\/C)->(A\/B)\/C.
intros A B C h.
destruct h as [ha | h].
 left.
 left.
 exact ha.
destruct h as [hb | hc].
 left.
 right.
 exact hb.
right.
exact hc.
Qed.

Lemma ex5 : forall A B: Prop, (A\/B)/\~A -> B.
intros A B h.
destruct h as [h hna].
destruct h as [ha | hb].
 case hna.
 exact ha.
exact hb.
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 :=
 match e with
   avar y => if string_eq x y then e_x else e
 | anum n => e
 | aplus e1 e2 => aplus (subst_aexpr e1 x e_x) (subst_aexpr e2 x e_x)
 end.

(* 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 :=
  match e with
    avar x => g x
  | anum n => n
  | aplus e1 e2 => af' g e1 + af' g e2
  end.


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