(* TP1 Langages formels

   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
*)


(* DÉFINIR UN OBJET (entier, fonction, etc.) *)
(* Mot-clef "Definition" 
   suivi du nom de l'objet
   suivi de ":" 
   suivi du type de l'objet
   suivi de ":="
   suivi de la valeur de l'objet. *)
Definition a : nat := 3.
Definition b : nat := 6.

(* En Coq on donne TOUJOURS les types. *)

(* EFFECTUER UN CALCUL... dans l'interpréteur *)
(* Directive "Compute" *)
(* RÉSULTAT ATTENDU : 9 *)
Compute (a+b).

(* AFFICHER LE TYPE... dans l'interpréteur *)
(* Directive "Check" *)
Check (a+b).

Print a.



(* 1) TYPES ÉNUMÉRÉS et INDUCTIFS *)


(* Mots-clefs "Inductive" et "|" par cas. 
   C'est la définition d'un ensemble inductif, on donne des règles...
   Comme on définit un *type* de données, son propre type est Type. *)
Inductive jour : Type :=
  | lundi : jour
  | mardi : jour
  | mercredi : jour
  | jeudi : jour
  | vendredi: jour
  | samedi : jour
  | dimanche : jour.
(* ici uniquement des cas de base *)


(* On peut définir une FONCTION jour_suivant sur ce type.
   (jour_suivant e) s'évalue en le nom du jour suivant le jour e.
   Elle est réalisée suivant *la forme* du paramètre, c'est du
   "filtrage" ou "PATTERN MATCHING". C'est le mécanisme le plus
   confortable pour manipuler des structures inductives. *)
(* Mots-clef "match" "with" "end" *)
Definition jour_suivant (j : jour) : jour :=
  match j with
  | lundi => mardi
  | mardi => mercredi
  | mercredi => jeudi
  | jeudi => vendredi
  | vendredi => samedi
  | samedi => dimanche
  | dimanche => lundi
  end.

(* On teste. RÉSULTAT ATTENDU : jeudi *)
Compute (jour_suivant mercredi).


(* EXERCICE 2 *)
(* Définir la fonction qui retourne le surlendemain d'un jour donné *)
(* C'est une fonction qui APPLIQUÉE À un jour, RETOURNE un jour *)

(* On re-teste et on devrait obtenir vendredi*)
(* Compute (jour_suivant_le_jour_suivant mercredi). *)


(* On peut aussi définir les booléens... *)
(* Il n'y a que des cas de base et on va les appeler Vrai et Faux *)
Inductive booleens : Type :=
| Vrai : booleens
| Faux : booleens.

(* Ainsi que les fonctions logiques usuelles. *)
(* Le complémentaire : non. *)
Definition non (a : booleens) : booleens :=
  match a with
  | Vrai => Faux
  | Faux => Vrai
  end.


(* Directive d'affichage de type *)
Check non.

(* Directive d'affichage de valeur *)
Print non.


(* EXERCICE 3 *)
(* Définir la fonction "et" sur les booléens. *)
Definition et (a : booleens) (b : booleens) : booleens :=
Faux.

(* un petit test, RÉPONSE ATTENDUE : Faux *)
Compute (et Vrai (et Faux Vrai)).


(* EXERCICE 4 *)
(* Définir la fonction "ou" sur les booléens. *)

(* RÉPONSE ATTENDUE : Vrai *)
(* Compute (et Vrai (ou Faux Vrai)). *)


(* EXERCICE 5 *)
(* Définir une fonction bcompose : f -> g -> h telle que h est la composition des
deux fonctions booléennes f et g *)

(* Tester bcompose en définissant une fonction nonnon : booléens -> booléens qui
définit non o non *)

(* RÉSULTAT ATTENDU : Vrai *)
(* Compute (nonnon Vrai). *)


(* Le langage de Coq a bien sûr des booléens (dans le type prédéfini bool),
   ils sont en fait définis de la même façon que nos booleens. Pour l'instant
   nous allons continuer de travailler avec les nôtres. *)

(* On définit maintenant de façon inductive le type des entiers naturels.
   Un entier naturel est :
   - soit un élément particulier noté Z (pour zéro, c'est un cas de base ici),
   - soit le successeur d'un entier naturel.
 
   On a bien DEUX CONSTRUCTEURS pour les entiers : ils sont soit de la
   *forme* "Z" soit de la *forme* "Succ d'un entier".
*)
Inductive entiers : Type :=
| Z : entiers
| Succ : entiers -> entiers.

Definition un  := Succ Z.
Definition deux  := Succ un.
Definition trois  := Succ deux.


(* EXERCICE 6 *)
(* Définir la fonction prédécesseur *)
(* C'est une fonction qui APPLIQUÉE À un entier, RETOURNE un entier *)
(* On considère que le prédécesseur de quelque chose de la forme Z est... Z *)
(* Le prédécesseur de quelque chose de la forme Succ toto est bien sûr toto *)

(* RÉSULTAT ATTENDU :  Succ (Succ Z) *)
(* Compute (pred (Succ (Succ (Succ Z)))).*)


(* On veut écrire une FONCTION RÉCURSIVE pour ajouter deux entiers.
   Comme la fonction est récursive, on utilise le mot-clé Fixpoint (et
   non plus Definition).
   Elle se calcule selon la forme du premier paramètre *) 
Fixpoint plus (a : entiers) (b : entiers) : entiers :=
  match a with
  | Z => b
  | Succ n => Succ (plus n b)
  end.


(* EXERCICE 7 *)
(* Multiplication
   Elle se calcule selon la forme du premier paramètre *)

(* RÉSULTAT ATTENDU : 9 *)
(* Compute (mult trois trois). *)


(* EXERCICE 8 *)
(* Définir une fonction est_pair, telle que est_pair APPLIQUÉE À un entier a RETOURNE Vrai si a est pair, Faux sinon. *)

(* RÉSULTAT ATTENDU : Vrai *)
(* Compute (est_pair deux). *)

(* RÉSULTAT ATTENDU : Faux *)
(* Compute (est_pair trois). *)


(* EXERCICE 9 *)
(* Définir la fonction factorielle sur les entiers *)

(* RÉSULTAT ATTENDU : 24 sous forme de Succ( ... (Succ(Z) ...) *)
(* Compute (factorielle (plus trois un)). *)


(* EXERCICE 10 *)
(* Définir la fonction moins, soustraction non négative sur les entiers *)

(* RÉSULTAT ATTENDU : Succ Z *)
(* Compute (moins deux un).*)

(* RÉSULTAT ATTENDU : Z *)
(* Compute (moins deux trois).*)


(* EXERCICE 11 *)
(* Définir une fonction inf, tel que inf a b vaut/retourne Vrai si a est
   inférieur ou égal à b, Faux sinon. *)

(* RÉSULTAT ATTENDU : Vrai *)
(* Compute (inf trois trois). *)


(* EXERCICE 12 *)
(* Définir une fonction egal, tel que egal a b donne Vrai si les entiers
   a et b sont égaux, Faux sinon.*)

(* RÉSULTAT ATTENDU : Vrai *)
(* Compute (egal trois trois). *)

(* RÉSULTAT ATTENDU : Faux *)
(* Compute (egal un trois). *)


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


(* Précédemment, on a défini nos booléens et nos entiers naturels,
mais ils sont en fait déjà définis dans la bibliothèque que Coq charge
initialement au démarrage :

NE PAS DECOMMENTER CE QUI SUIT, CE SONT DES TYPES COQ PREDEFINIS

Inductive bool : Set :=
  | true : bool
  | false : bool.

avec les fonctions 

negb (le complémentaire)
andb (le et, (le min))
orb  (le ou, (le max))

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

avec les fonctions usuelles + , - , * , etc.
et les comparaisons :
Nat.eqb pour le test d'égalité
Nat.ltb pour le test plus petit
Nat.leb pour le test plus petit ou égal.


CE SONT EUX QU'ON UTILISERA DORÉNAVANT.

 *)



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


(* 3) ARBRES BINAIRES *)


(* EXERCICE 13 *)
(* Donner une définition par induction de l'ensemble nBin des arbres
binaires contenant des nat. On souhaite avoir une représentation de
l'arbre vide dans nBin. *)



(* Donner un exemple d'arbre, disons à 5 éléments *)

(*
Definition a1 := nNode
                      (nNode nEmpty 2 nEmpty)
                      1
                      (nNode
                            (nNode nEmpty 4 nEmpty)
                            3
                            (nNode nEmpty 5 nEmpty)
                      ).

Check a1.
Print a1.
*)

(* EXERCICE 14 *)
(* Définir la fonction nelements qui renvoie la liste des éléments
   contenus dans un arbre binaire de nat. Le faire naïvement avec un
   concat pour commencer. *)

(* RÉSULTAT ATTENDU : cons 1 (cons 2 (cons 3 (cons 4 (cons 5 vide)))) *)
(* Compute (nelements a1).*)


(* EXERCICE 15 *)
(* Définir la fonction nnelts qui renvoie le nombre de noeuds internes
   (portant une étiquette de type nat) dans un nBin. *)

(* RÉSULTAT ATTENDU : 5 *)
(* Compute (nnelts a1).*)


(* EXERCICE 16 *)
(* Définir la fonction nfeuilles qui renvoie le nombre de feuilles *)

(* RÉSULTAT ATTENDU : 6 *)
(* Compute nfeuilles a1. *)


(* EXERCICE 17 *)
(* Définir la fonction nsum qui renvoie la somme des valeurs portées
   par les noeuds internes d'un nBin. *)

(* RÉSULTAT ATTENDU : 15 *)
(* Compute (nsum a1).*)



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