(* TP1 Logique classique

   ATTENTION
   Pour le bon affichage des caractères accentués, précisez que l'encodage par défaut de votre NAVIGATEUR doit être Unicode (UTF-8)

   BUT DU TP
     - Manipuler Coq / Gallina
     - Se familiariser avec 4 mots-clés :
        + Definition
        + Definition avec match ... with
        + Inductive
        + Fixpoint
     - Premières preuves en logique propositionnelle
*)
        
(* -------------------------------------------------------------------------- *)

(* 1) LISTES D'OBJETS DE TYPE NAT *)

(* On considère ici des listes d'objets de type nat. *)

(* On peut définir de façon inductive un type nliste pour les listes d'objets de type nat. 
  Le cas de base est bien sûr la liste vide, l'autre règle de construction applique cons
  à un nat et une liste de l'ensemble inductif pour créer un nouvel élément de cet ensemble
*)
Inductive nliste : Type :=
  | vide : nliste
  | cons : nat -> nliste -> nliste.

Definition liste0 := vide.
Definition liste1 := cons 1 vide.
Definition liste2 := cons 2 (cons 1 vide).
Definition liste3 := cons 3 (cons 2 (cons 1 vide)).
Definition liste4 := cons 4 (cons 3 (cons 2 (cons 1 vide))).
Print liste0.
Print liste1.
Print liste2.


(* EXERCICE 2 *)
(* Écrire une fonction ajoute: nat -> nliste -> nliste telle que ajoute n l
   retourne une liste correspondant à l'ajout de l'élément n à la liste l.
   C'est bien sûr juste la fonction qui applique cons
*)

(* RÉSULTAT ATTENDU : cons 3 (cons 2 (cons 1 vide)) *)
(* Compute (ajoute 3 liste2). *)


(* EXERCICE 3 *)
(* Écrire une fonction longueur telle que longueur APPLIQUÉE À l
   RETOURNE le nombre (nat) d'éléments de la liste l.  On l'a vue en
   cours.
  C'est bien sûr une fonction qui travaille selon la FORME de l : si
  c'est vide, la longueur vaut zéro, et si l est de la forme cons n l'
*)

(* RÉSULTAT ATTENDU : 2 *)
(* Compute (longueur liste2).*)

(* EXERCICE 4 *)
(* Écrire une fonction concat: nliste -> nliste -> nliste telle que concat l l'
   retourne une liste correspondant à l'ajout des éléments de l en tête de la liste l'. *)

(* RÉSULTAT ATTENDU : cons 2 (cons 1 (cons 2 (cons 1 vide))) *)
(* Compute (concat liste2 liste2).*)

(* EXERCICE 5 *)
(* Écrire une fonction recherche: nat -> nliste -> bool telle que recherche n l
   retourne Vrai si un élément n appartient à la liste l et Faux sinon. *)
(* Pour l'égalité entre éléments du type nat, soit on la redéfinit, soit on utilise Nat.eqb *)
Require Import Nat.
Check (eqb 3 4).
Compute (eqb 3 4).

(* RÉSULTAT ATTENDU : true *)
(* Compute (recherche 1 liste2).*)

(* RÉSULTAT ATTENDU : false *)
(* Compute (recherche 3 liste2).*)


(* EXERCICE 6 *)
(* Écrire une fonction miroir: nliste -> nliste, qui
   retourne une liste correspondant à son argument dans l'ordre
   inverse. Dans un premier temps, on pourra utiliser la fonction de
   concaténation vue précédemment. *)

(* RÉSULTAT ATTENDU : cons 1 (cons 2 (cons 3 (cons 4 vide))) *)
(* Compute (miroir liste4).*)

(* RÉSULTAT ATTENDU : cons 1 (cons 2 (cons 3 (cons 4 vide))) *)
(* Compute (miroir' liste4).*)


(* EXERCICE 7 A FAIRE CHEZ VOUS *)
(* Écrire une fonction supprime: nat -> nliste -> nliste telle que
   supprime n l retourne une liste d'objets de type nat correspondant
   à l sans la première occurrence de n (le cas échéant), à l
   sinon. *)

(* RÉSULTAT ATTENDU : cons 4 (cons 2 (cons 1 vide)) *)
(* Compute (supprime 3 liste4). *)


(* EXERCICE 8 A FAIRE CHEZ VOUS *)
(* Écrire une fonction supprime_tout: nat -> nliste -> nliste telle
   que supprime_tout n l retourne une liste correspondant à l sans
   occurrence d'un nat n (le cas échéant), à l sinon. *)


(* EXERCICE 9 A FAIRE CHEZ VOUS *)
(* Écrire une fonction il_existe_pair: nliste -> booleens, telle que
   il_existe_pair l retourne Vrai si un élément de l est pair, Faux
   sinon. *)

(* RÉSULTAT ATTENDU : true *)
(* Compute (il_existe_pair liste4).*)


(* EXERCICE 10 A FAIRE CHEZ VOUS *)
(* Insertion triée *)
(* Écrire dans un premier temps une fonction leq : nat -> nat -> bool qui teste si le
premier entier est inférieur ou égal au second *)

(* RÉSULTAT ATTENDU : true *)
(* Compute (leq 2 2).*)

(* RÉSULTAT ATTENDU : true *)
(* Compute (leq 2 3).*)

(* RÉSULTAT ATTENDU : false *)
(* Compute (leq 3 2).*)


(* Écrire une fonction insertion_triee : nat -> nliste -> nliste qui effectue
une insertion triée dans une liste *)

(* RÉSULTAT ATTENDU : cons 1 (cons 2 (cons 2 (cons 3 (cons 4 vide)))) *)
(* Compute (insertion_triee 2 (miroir liste4)).*)

(* RÉSULTAT ATTENDU : cons 4 (cons 3 (cons 2 (cons 1 (cons 6 vide)))) *)
(* Compute (insertion_triee 6 liste4).*)


(* EXERCICE 11 A FAIRE CHEZ VOUS *)
(* Tri par insertion d'une liste *)
(* Écrire une fonction tri_insertion : nliste -> nliste qui effectue
le tri par insertion d'une liste *)

(* RÉSULTAT ATTENDU : cons 1 (cons 1 (cons 2 (cons 2 (cons 3 (cons 3 (cons 4 (cons 4 vide)))))) *)
(* Compute (tri_insertion (concat liste4 liste4)).*)




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

(* 2. PREMIÈRES PREUVES EN LOGIQUE PROPOSITIONNELLE *)

(* Introduction des mots-clés 
    - assumption
    - intro
    - apply
    - destruct
    - split
    - left / right *)

(* On introduit les variables propositionnelles avec lesquelles 
   on va travailler par la suite *)
Section logique_propositionnelle.
Context (P Q R S T U: Prop).

(* LA FLÈCHE *)
(* - axiome : assumption
   - introduction de la flèche : intro [nom qu'on donne à l'hypothèse] 
   - élimination de la flèche : apply [nom de l'hypothèse utilisée] *)

(* EXERCICE 12 *)
Theorem exercice_12: P -> (P -> Q) -> Q.
Proof.
Admitted.


(* EXERCICE 13 *)
Theorem exercice_13: (P -> Q) -> (Q -> R) -> (P -> R).
Proof.
Admitted.

(* LE ET *)
(* Une variante de la question précédente avec /\ *)
(* - décomposition du /\ en hypothèse : destruct [nom de l'hypothèse avec /\] *)

(* EXERCICE 14 *)
Theorem exercice_14: (P -> Q) /\ (Q -> R) -> (P -> R).
Proof.
Admitted.

(* - introduction du /\ : split *)
(* On obtient bien deux sous-buts *)

(* EXERCICE 15 *)
Theorem exercice_15: P -> Q -> P /\ Q.
Proof.
Admitted.
  
(* LE OU *)
(* - introduction du \/ :
       - depuis la droite : right
       - depuis la gauche : left
   - decomposition du \/ en hypothèse : destruct [nom de l'hypothèse avec \/]*)

(* EXERCICE 16 *)
Theorem exercice_16: (P \/ Q) -> (Q \/ P).
Proof.
Admitted.


(* zéro constructeur *)
Print False. 
(* un seul constructeur car une seule règle d'intro *)
Print and.
(* deux constructeurs car deux règles d'intro *)
Print or.  

(* destruct donne bien un sous but par constructeur *)


(* EXERCICE 17 *)
(* On remarque que comme False n'a aucun constructeur : le destruct résout le but *)
Theorem ex_falso_quodlibet : False ->  P.
Proof.
Admitted.

(* EXERCICE 18 *)
(** un peu difficile **)
(* Plus généralement, la tactique exfalso remplace tout but par False. *)
(* Si on peut déduire False des hypothèses, c'est alors gagné ! *)
Theorem ex_falso_quodlibet_Q : (P -> False) -> P -> (Q \/ (R -> S /\ T) -> U).
Proof.
Admitted.
  
End logique_propositionnelle.
(* -------------------------------------------------------------------------- *)