(* TP4 LOGIQUE CLASSIQUE

   LISEZ BIEN TOUT CE QUI EST PRÉCISÉ EN COMMENTAIRES

*)

Require Import Nat.
Require Import Arith.


(* 1. LE QUANTIFICATEUR EXISTENTIEL *)


(* Pour écrire une quantification existentielle, on utilise le mot-clé "exists".
   Par exemple : forall (l : nlist), length l <> 0 -> exists (n : nat), exists (l' : nlist), l = n::l'. *)

(* La tactique utilisée pour la règle d'introduction de l'existentiel est "exists terme_particulier". *)

(* EXERCICE 1 *)
(* Montrez qu'il existe un x tel que la fonction plus appliquée à ce x et à 0 retourne 0. *)
Lemma ex_exists1 : exists (x : nat), plus x 0 = 0.
Admitted.


(* EXERCICE 2 *)
(* Montrez que pour tout x, il existe un y tel que la fonction appliquée à x et y retourne x + 1. *)
Lemma ex_exists2 : forall (x : nat), exists (y : nat), plus x y = x + 1.
Admitted.


(* -------------------------------------------------------------------------- *)


(* 2. FONCTIONS RECURSIVES ET INDUCTION *)

(* FONCTIONS RECURSIVES ET INDUCTION SUR LES ENTIER *)
(* ------------------------------------------------------------ *)

(* On rappelle que les objets de type nat sont définis inductivement de façon similaire à 
   Inductive entiers : Set :=
   | Z : entiers
   | Succ : entiers -> entiers. *)

(* Print nat. *)

(* On dispose donc d'un principe d'induction nat_ind, construit à peu près comme vu en cours *)
(* Check nat_ind. *)

(* Si on omet le "forall P" qui n'est PAS du premier ordre, on se retrouve bien avec deux branches :
   - Une branche qui demande de prouver sur le cas de base des nat, c'est-à-dire 0
   - Une branche qui demande de prouver sur un nat construit par S à partir d'un nat sur lequel
     on sait déjà prouver la propriété
   On peut en déduire la propriété sur tout nat obtenu par 0 et S. *)

(* EN COQ : l'application de la tactique "induction" sur un nom d'entier
  produira donc DEUX sous-buts (il y a bien 2 règles de construction des entiers...) :
   - Le sous-but correspondant au cas de base O, 
   - Le sous-but correspondant au cas inductif où l'hypothèse d'induction apparaît dans le contexte.

   COMME ON SAIT que ça va mettre deux nouvelles choses dans la branche de droite
     et rien de nouveau dans celle de gauche on peut nommer directement :
               induction "n" as [ | "m" "Hyp_Ind_m"].
     Où n est dans le cas de droite l'entier Succ m
     avec comme hypothèse d'induction que la propriété est vraie pour m (hypothèse nommée ici Hyp_Ind_m).
*)

(* EXERCICE 3 *)
(* Montrez que la fonction plus appliquée à 0 et à un y quelconque retourne ce y. *)
(* La définition de plus est récursive sur le paramètre de gauche,
   donc pas de problème ici, c'est juste un calcul (simpl) *)
Lemma plus_Z_l : forall (y : nat), plus 0 y = y.
Admitted.


(* EXERCICE 4 *)
(* Montrez que la fonction plus appliquée un x quelconque et 0 retourne ce x. *)
(* Là il faut travailler par induction sur x. On utilise "induction x as..." qui invoque la règle nat_ind. *)
Lemma plus_Z_r : forall (x : nat), plus x 0 = x.
Admitted.


(* EXERCICE 5 *)
(* Montrez que le successeur du résultat de la fonction plus appliquée à x et y quelconques,
   c'est la fonction plus appliquée au successeur de x et à y.
   Comme avant, comme plus est récursive à gauche, c'est juste un calcul. *)
Lemma plus_Succ_l : forall x y, S (plus x y) = plus (S x) y.
Admitted.


(* EXERCICE 6 *)
(* Montrez que le successeur du résultat de la fonction plus appliquée à x et y quelconques,
   c'est la fonction plus appliquée à x et au successeur de y.
   Pareil qu'avant, on procède par induction sur x. *)
Lemma plus_Succ_r : forall x y, S (plus x y) = plus x (S y).
Admitted.


(* On peut ajouter une hypothèse provenant d'une propriété extérieure à la preuve courante, SI ON EN A BESOIN.
   
   On SPÉCIALISE une propriété : "specialize propriété with (univ1:=spé1) (univ2:=spé2) ... as Hspé_propriété"
     où univ1 est le premier universel instancié par la valeur spécialisée spé1 ...
     et a pour effet de créer une nouvelle hypothèse Hspé_propriété, qui est donc la spécialisation de propriété.

   Par exemple, si on a un y en hypothèse, "specialize plus_Z_r with (x:=y) as Hspe_plus_Z_r"
     crée l'hypothèse Hspe_plus_Z_r : y + 0 = y.
*)

(* Check plus_Z_r. *)

(* EXERCICE 7 *)
(* Montrez que la fonction plus est commutative. *)
(* On pourra utiliser les propriétés montrées ci-dessus. *)


(* FONCTIONS RECURSIVES ET INDUCTION SUR LES LISTES D'ENTIERS *)
(* ------------------------------------------------------------ *)

(* On reprend les listes de nat du TP précédent *)
Inductive nlist : Set :=
| nnil : nlist
| ncons : nat -> nlist -> nlist.

(* ... avec des notations confortables *)
Infix "::" := ncons.
Notation "[]" := nnil.

(* Check nlist_ind. *)

(* C'est tout à fait similaire au cas des nat.
   Si on omet le "forall P" qui n'est PAS du premier ordre, on se retrouve bien avec deux branches :
   - Une branche qui demande de prouver sur le cas de base des listes,
   - Une branche qui demande de prouver sur une liste construite par :: à partir d'une liste
     sur laquelle on sait déjà prouver la propriété
   On peut en déduire la propriété sur toute liste obtenue par [] et ::. 
   
   Comme pour les entiers, on sait qu'il n'y a rien dans la branche de gauche (cas de base) et
   qu'il y aura TROIS nouvelles choses dans la branche de droite, on les nomme directement :
               induction "l" as [ | "n" "l'" "IHl'"].
   Où l est dans le cas de droite la liste n::l' (n est un élément quelconque qui ne nous intéresse pas)
     avec comme hypothèse d'induction que la propriété est vraie pour l', hypothèse nommée ici IHl'.
   
   
   *)

Fixpoint concat (l1 l2 : nlist) : nlist := 
  match l1 with
  | []     => l2
  | x :: l => x::(concat l l2)
  end.

(* On note ++ en notation infix pour la concatenation *)
Infix "++" := concat.

Fixpoint length (l : nlist) : nat :=
  match l with
  | []     => 0
  | x :: l => S(length l)
  end.

Fixpoint appartient (x : nat) (l : nlist) : bool :=
match l with
| [] => false
| h::rl => (Nat.eqb x h) || (appartient x rl)
end.


(* EXERCICE 8 *)
(* Montrez que la fonction length retourne 0 SEULEMENT SI la liste est vide *)
Lemma length_zero_seulement_si_vide : forall (l : nlist), length l = 0 -> l = [].
Admitted.


(* EXERCICE 9 *)
(* Prouvez que pour tout nat x et toute liste de nat l,
   la liste vide n'est pas obtenue par l'ajout de x en tête de l. *)
Lemma nil_neq_cons : forall (x:nat), forall (l:nlist), [] = x :: l -> False.
Admitted.


(* EXERCICE 10 *)
(* Exprimez et montrez que pour tout élément x et toutes listes l1 et l2, ajouter x en tête
   de la concaténation de l1 et l2 est la même chose que concaténer l1 avec x en tête et l2. *)


(* EXERCICE 11 *)
(* Exprimez et montrez que la fonction length appliquée à la concaténation de deux listes quelconques l1 et l2
   retourne la somme des applications de cette fonction à chacune des deux listes. *)


(* EXERCICE 12 *)
(* Exprimez et montrez que pour toute liste l2, concaténer la liste vide à l2 renvoie exactement la liste l2. *)


(* EXERCICE 13 *)
(* Exprimez et montrez que pour toute liste l1, concaténer l1 à la liste vide renvoie exactement la liste l1. *)


(* EXERCICE 14 *)
(* Exprimez et prouvez la propriété que l'appartenance d'un élément à une liste vide est fausse *)


(* EXERCICE 15 *)
(* Exprimez et prouvez la propriété que l'appartenance d'un élément à une liste singleton est vraie
        SSI l'élément recherché et celui du singleton sont égaux
   On utilisera les théorèmes suivants :
   "Bool.orb_false_r : forall b : bool, (b || false)%bool = b"
   "PeanoNat.Nat.eqb_eq : forall n m : nat, PeanoNat.Nat.eqb n m = true <-> n = m"
*)
(* Check Bool.orb_false_r.
   Check PeanoNat.Nat.eqb.
   Check PeanoNat.Nat.eqb_eq. *)


(* EXERCICE 16 *)
(* Montrez que la fonction appartient est correcte et complète.
   On exprimera que (appartient x l) est vrai
     SI ET SEULEMENT SI il existe une décomposition de l de la forme l = l1 ++ x :: l2.
   On utilisera le théorème suivant :
   "Bool.orb_prop : forall a b : bool, (a || b)%bool = true -> a = true \/ b = true"
*)
(* Check Bool.orb_prop. *)

(* Pour la complétion on pourra se servir du lemme suivant *)
Lemma cons_injective : forall (x : nat) (l : nlist) (l' : nlist), x::l = x::l' -> l = l'.
Proof.
intro x.
intro l.
intro l'.
intro Heq.
injection Heq as Heq'.
assumption.
Qed.

(* ------------------------------------------------------------ *)