(*
Adresses email des TDmen :
 alexandre.isoard@ens-lyon.fr
 antoine.plet@ens-lyon.fr
 jeanmarie.madiot@ens-lyon.fr

Pour avoir les raccourcis comme il faut :
- Lancer "coqide" dans un terminal
- Edit > Preferences > Shortcuts > Modifiers for Navigation Menu
- Changer vers <alt> (selon les versions:
  - Taper Alt+W dans le champ, ou,
  - Laisser le bouton <alt> seul enfonçé)
- Cliquer sur OK
- Quitter coqide
- Relancer coqide
*)


(* TP n°1 : Introduction à Coq *)

(* Toutes les expressions bien formées de Coq ont un type que l'on
peut demander à l'interpréteur grâce à la commande "Check" : *)

Check 2 + 2. (* "nat" : type des entiers naturels *)
Check plus.  (* fonction qui prend deux "nat"s et renvoie un "nat" *)


(* Les types sont eux-mêmes des expressions bien formées de Coq, elles
ont donc également un type. *)

Check nat -> nat -> nat. (* "Set" est le type des types de données. *)


(* On peut également demander à Coq de nous donner la définition d'une 
d'une expression déjà définie; on utilise pour ça la commande "Print". *) 

Print plus.


(* On peut bien sûr définir de nouvelles fonctions *) 

Definition times_two (n : nat) := 2 * n.
Check times_two.
Print times_two.


(* et on utilise la syntaxique suivante pour faire des définitions
récursives: *)

Fixpoint double (n : nat) :=
  match n with 
    | 0 => 0
    | S p => S (S (double p))
  end.

Print double.


(* Sur le même modèle implémentez la fonction [sum : nat -> nat] qui
calcule la somme des premiers entiers *)

Fixpoint sum (n : nat ) := ...
(* ... Complétez ici ... *)

Eval compute in sum 10.


(* En plus des types de données et des programmes, coq permet également 
de manipuler des formules. À commencer par les égalités : *)

Check 0 = 0. (* "Prop" : type des formules logiques. *)
Check 0 = 1. (* "Prop" : type des formules logiques fausses. *)


(* Enfin, Coq permet de prouver les formules à l'aide d'un système de 
"tactiques" de preuves. *)

Lemma zero_equals_zero : 0 = 0.
trivial. (* Cette tactique résout les égalités triviales *)
Qed.

Lemma two_plus_two_equals_four : 2 + 2 = 4.
simpl. (* Cette tactique effectue des pas de calcul dans les buts. *)
trivial.
Qed.


(* On dispose également de quantificateurs pour fabriquer les formules :*)

(* Formule qui énonce "+" est commutatif *)
Check (forall x y : nat, x + y = y + x).


(* Il y a tout un tas de tactiques qu'il faudra apprendre à utiliser.
Voici un exemple de preuve un peu moins triviales. Pouvez-vous
retranscrire cette preuve simple en "mathématiques informelles" ?  *)

Lemma f_double : forall n, double n = n * 2.
intros n.
induction n.
  simpl.
  trivial.
  
  simpl.
  rewrite IHn.
  trivial.
Qed.

(* Les deux tactiques centrales de Coq sont :

  [intros H]
    l'équivalent de "soit H" et de "supposons que..."  dans les maths
    informelles, [intros H] introduit une hypothèse H dans le
    contexte.

  [intros H1 H2 H3]
     est un raccourci pour [intros H1. intros H2. intros H3.]

  [apply H]
    permet d'invoquer l'hypothèse nommée H. *)

(* À vous de jouer maintenant ! *)

Lemma trivial1 : forall P : Prop, P -> P.

Qed.

Lemma trivial3 : forall P Q R : Prop,
  (P -> Q -> R) -> (P -> Q) -> P -> R.

Qed.


(* Pour chaque connecteur, Coq fournit une tactique pour l'utiliser
quand il est en hypothèse et une tactique pour le "construire" quand
il est en but:

    connecteur    | pour utiliser |  pour construire
  ----------------|---------------|---------------------
      P /\ Q      |  destruct H.  |  split.
      P \/ Q      |  destruct H.  |  left. / right.
  exists x:nat, P |  destruct H.  |  exists 17.     
      False       |  destruct H.  |  (pas de constructeur)
*)

Lemma conj1: forall P Q : Prop, P /\ Q -> P.

Qed.

Lemma conj2: forall P Q : Prop, P /\ Q -> Q.

Qed.

Lemma conj3: forall P Q : Prop, P -> Q -> P /\ Q.

Qed.

Lemma or1 : forall P Q : Prop, P -> P \/ Q.

Qed.

Lemma or2 : forall P Q : Prop, Q -> P \/ Q.

Qed.

Lemma or3 : forall P Q R : Prop,
  P \/ Q -> (P -> R) -> (Q -> R) -> R.

Qed.

Lemma ex_falso: forall P : Prop, False -> P.

Qed.

Notation "~ P" := (P -> False).

Lemma not_not : forall P : Prop, P -> ~~P.

Qed.

Lemma morgan1 : forall P Q : Prop, 
  ~P \/ ~Q -> ~(P /\ Q).

Qed.

Lemma morgan2 : forall P Q : Prop, 
  ~P /\ ~Q -> ~(P \/ Q).

Qed.


(* On dispose également d'une égalité entre les termes de Coq qui
vient avec trois tactiques pour les manipuler, l'une d'entre elles étant:
  [rewrite H]
    si H est une hypothèse de la forme "t₁ = t₂" remplace dans le but
    courant les sous-termes de la forme t₁ par t₂.

  [rewrite <-H]
    dans l'autre sens: remplace t₂ par t₁.
*)

Lemma eq_trans : forall (x y z : nat), x = y -> y = z -> x = z.

Qed.


(* Arithmétique *)

(* Rappel: on utilise la tactique simpl, pour simplifier les calculs. *)
Lemma zero_plus : forall x : nat, 0 + x = x.

Qed.

Lemma exists_factor : 
  exists n, exists m , n * (m + 1) = 36.

Qed.


(* La tactique simpl ne marche par pour prouver la proposition
suivante. Pourquoi ? *)

Lemma plus_zero : forall x:nat, x + 0 = x.

(* Il va nous faloir démontrer le résultat par récurrence sur de x.

  [induction x]
    invoque automatiquement le principe d'induction pour prouver un
    but par récurrence sur la variable x. *)
induction x.
  (* Il faut prouver le cas de base (zéro) .. *)

  (* ... et l'hérédité.*)
Qed.

Lemma plus_assoc : forall a b c, (a + b) + c = a + (b + c).

Qed.

Lemma mult_zero : forall a, a * 0 = 0.

Qed.



(* En coq on peut également définition des propositions qui dépendent
de paramètres. Cela permet de représenter d'autres relations que
l'égalité *)

Definition less_or_equal (n m : nat) := exists k, n+k = m.

Check less_or_equal. (* Méditez le type de la relation. *)

Infix "<=" := less_or_equal. (* On déclare "<=" comme étant une
                                  notation pour cette relation. *)

Lemma less_or_equal_refl : forall x, x <= x.

Qed.

Lemma less_or_equal_trans : 
  forall x y z, x <= y -> y <= z -> x <= z.

Qed.

(* Pour finir, quelques exercices pour occuper les plus rapides
d'entre vous. N'hésitez pas à faire des lemmes intermédiaires ! *)

(* Ce n'est pas aussi trivial qu'il n'y paraît. *)
Lemma plus_comm : forall a b, a + b = b + a.

Qed.

Lemma sum_formula: forall n, 2 * (sum n) = n * (n + 1).

Qed.

Lemma identite : forall a b,
  (a + b) * (a + b) = a*a + 2*a*b + b*b.

Qed.

(* Écrivez la fonction [power] qui calcule les puissances entières : *)
Fixpoint power a b := 
...

Infix "^" := power.

Lemma power_exp: forall a n m, a^(n + m) = a^n * a^m.

Qed.

Lemma closed:
  forall n a b c, 3 <= n -> a^n + b^n = c^n -> a = c \/ b = c.

Qed.