(* La première commande indique que nous manipulerons des listes et
   des entiers. *)
Require Import List ZArith.
(* La deuxième commande indique que les notations mathématiques porteront par
  défaut sur des entiers relatifs. *)
Open Scope Z_scope.

(* Voici une fonction qui insère un élément dans une liste de telle sorte que
 tous les élément avant l'élément insérés sont plus petits. *)

(* Le mot clef "Fixpoint" est utilisé pour indiquer que l'on définit une
  fonction récursive.  Le text {struct l} indique que la liste fournie dans
  l'appel récursif est une sous liste de l.  Ceci sert à garantir que la
  fonction récursive ne peut pas boucler indéfiniment. *)

(* Les mots clefs "match ... with ... end" permettent de définir la fonction
  en indiquant ce qui se passe pour chaque forme que peut prendre l'expression
  qui setrouve entre "match" et "with".  Les différentes formes possibles sont
  données par la définition de type inductif de cette expression. *)

Fixpoint insert (n:Z) (l:list Z) {struct l} : list Z :=
  match l with
  | nil => n::l
  | m::tl => if Zle_bool m n then m :: insert n tl else n :: m :: tl
  end.

(* La fonction suivante produit une liste triée à partir d'une liste 
  quelconque.  Il n'est pas nécessaire d'indiquer quel argument devient
  plus petit à chaque appel récursif, car il y a un seul argment. *)

Fixpoint sort (l:list Z) : list Z :=
  match l with
  | nil => l
  | n::tl => insert n (sort tl)
  end.

(* La fonction suivante calcule la somme des éléments d'une liste. *)
Fixpoint sum_list (l:list Z) : Z :=
  match l with
  | nil => 0
  | n::tl => n+sum_list tl
  end.

Eval vm_compute in
  sort (10 :: 2 :: 3 :: 7 :: 9 :: 5 :: 6 :: 4 :: 1 :: 8 :: nil).

(* En vous basant sur ces trois exemples, définissez une fonction list_as_poly
  qui prend en entrée une valeur x et une liste a_0 :: a_1 :: ... :: a_n et
  produit en sortie la valeur a_0 + x * (a_1 + x * (...   + x * a_n)...) *)


(* Définir un nouveau type inductif. *)

Inductive btree : Type :=
  bt1 : btree
| bt2 : Z -> btree -> btree -> btree.

(* The function that adds all the integer values present in a binary tree. *)

Fixpoint sum_btree (t:btree) : Z :=
  match t with
    bt1 => 0
  | bt2 n t1 t2 => n + sum_btree t1 + sum_btree t2
  end.

Check app.
Eval vm_compute in app (1 :: 2 :: nil) (3 :: 4 :: nil).
(* La commande suivante montre que la notation "_ ++ _" cache en fait un
appel à une fonction appelée app *)
Locate "_ ++ _".
(* La command suivante permet de voir la définition de la fonction app *)
Print app.

(* Voici un lemme (utilisé plus tard dans le même fichier), où l'on démontre
 une correspondance entre concaténer les lists et additionner leurs sommes. *)
Lemma sum_list_app : forall l1 l2, sum_list (l1++l2) =
   sum_list l1 + sum_list l2.
induction l1.
intros l2. 
(* puisque nous avons vu la définition de app, nous savons que nil++l2 se
  calcule en l2, nous pouvons demander à coq de faire le remplacement. *)
change (nil ++ l2) with l2.
change (sum_list nil) with 0.
(* Pouvez-vous m'expliquer ce qui se passe à la ligne suivante? *)
change (0 + sum_list l2) with (sum_list l2).
(* Lorsque l'on doit prouver une égalité dont les deux membres sont 
  visiblement les mêmes, on peut dire à coq que c'est trivial. *)
trivial.
intros l2.
change ((a :: l1) ++ l2) with (a :: (l1 ++ l2)).
change (sum_list (a :: l1)) with (a + sum_list l1).
change (sum_list (a :: l1 ++ l2)) with (a + sum_list (l1 ++ l2)).
(* Nous sommes en train de faire une preuve par récurrence et IHl1 est
   l'hypothèse de récurrence. *)
rewrite IHl1.
(* A cet endroit, la preuve semble terminée, mais les deux expressions
 de l'égalité ne sont pas exactement pareilles: il y a des parenthèses
 qui ne sont pas au même endroit.  Cherchons un théorème qui peut résoudre
 cette différence. *)
SearchRewrite (_ + _ + _).
rewrite Zplus_assoc.
trivial.
Qed.

(* Ecrivez une fonction qui retourne la liste de tous les éléments
 trouvés dans un arbre binaire.  Appelez cette fonction btree_to_list. *)
Fixpoint btree_to_list (t:btree) : list Z :=
  match t with
   bt1 => nil
  | bt2 n t1 t2 => n::btree_to_list t1++btree_to_list t2
  end.

(* Démontrez que la conbinaison de sum_list et btree_to_list fait le même
  calcul que sum_btree.  Utilisez le théorème sum_list_app donné ci-dessus. *)
Lemma sum_list_sum_btree :
  forall t, sum_list (btree_to_list t) = sum_btree t.
Qed.

(* Essayez maintenant de faire les preuves suivantes qui se concentrent
  sur les connecteurs logiques. *)
Lemma and1 : forall a b, a /\ b -> b /\ a.

Lemma or1 : forall a b, a \/ b -> b \/ a.

Lemma and_imp : forall a b c d:Prop, a /\ b -> (a->c) /\ (b->d) -> c/\d.

Lemma exist_imp : forall A:Type, forall P Q: A -> Prop,
   (forall y:A, P y -> Q y) ->
   (exists x: A, P x) -> exists z:A, Q z.

Lemma not_and_not : forall a, ~ (a /\ ~ a).