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

(* Coq est un langage de programmation fourni avec un interpréteur
   que l'on peut interroger -entre autre- pour faire des calculs: *)

Eval compute in 2+2.
Eval compute in 6*8.

(* 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. (* 2+2 a le type "nat" des entiers naturels *)
Check plus. (* l'addition "plus" prends deux entiers en paramètre et retourne 
             un entier. *)
(* 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.

(* 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 ) := 
  match n with
  | 0 => 0
  | S n => S n + sum n
  end.

Eval compute in sum 3.

(* 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" est le type des formules logiques. *)
Check 0 = 1. (* Les formules fausses sont aussi des expressions valides ! *)

(* Enfin, Coq permet de prouver les formules à l'aide d'un système de 
   "tactiques" de preuves. *)
Lemma zero_equals_zero :
  0 = 0.
reflexivity. (* Comme on le verra plus tard, c'est la tactique qui
                  résout les égalités triviales. *)
Qed.

Lemma two_plus_two_equals_four : 
  2+2 = 4.
simpl. (* Cette tactique nous sera très utile dans la suite, elle
                  sert à effectuer les pas de calcul dans les buts. *)
reflexivity.
Qed.

(* On dispose également de quantificateurs pour fabriquer les formules :*)
Check (forall x y : nat, x+y = y + x). (* Une formule qui nous dit que + est commutatif. *)

(* 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.
  reflexivity.
simpl.
rewrite IHn.
reflexivity.
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.
       (notez qu'il est également permis d'invoquer [intros H1 H2 H3]
       à la place de [intros A. intros B. intros C.]  pour faire des 
       intros successifs)
     - [apply H] : permet d'invoquer l'hypothèse nommée H. *)

(* À vous de jouer maintenant ! *)

Lemma trivial1 : forall P:Prop, P -> P.
intros P.
intros H.
apply H.
Qed.

Lemma trivial3: forall P Q R:Prop, (P -> Q -> R) -> (P -> Q) -> P -> R.
intros P Q R H I J.
apply H.
apply J.
apply I.
apply J.
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.
intros P Q pq.
destruct pq.
apply H.
Qed.

Lemma conj2: forall P Q:Prop, P /\ Q -> Q.
intros P Q pq.
destruct pq.
apply H0.
Qed.

Lemma conj3: forall P Q:Prop, P -> Q -> P /\ Q.
intros P Q p q.
split.
apply p.
apply q.
Qed.

Lemma or1 : forall P Q:Prop, P -> P \/ Q.
intros P Q p.
left.
apply p.
Qed.

Lemma or2 : forall P Q:Prop, Q -> P \/ Q.
intros P Q q.
right.
apply q.
Qed.

Lemma or3 : forall P Q R:Prop, P \/ Q -> (P -> R) -> (Q -> R) -> R.
intros P Q R poq pr qr.
destruct poq.
apply pr.
apply H.
apply qr.
apply H.
Qed.

Lemma ex_falso: forall P:Prop, False -> P.
intros P F.
destruct F.
Qed.

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

Lemma not_not : forall P:Prop, P -> ~~P.
intros P H.
intros I.
apply I.
apply H.
Qed.

Lemma morgan1 : forall P Q:Prop, 
  ~P \/ ~Q -> ~(P /\ Q).
intros P Q nponq paq.
destruct paq.
destruct nponq.
apply H1.
apply H.
apply H1.
apply H0.
Qed.

Lemma morgan2 : forall P Q:Prop, 
  ~P /\ ~Q -> ~(P \/ Q).
intros P Q npanq poq.
destruct npanq.
destruct poq.
apply H.
apply H1.
apply H0.
apply H1.
Qed.

(* On dispose également d'une égalité entre les termes de 
   coq qui vient avec trois tactiques pour les manipuler: 
      - [reflexivity] : permet de prouver les but de la forme t=t. 
      - [symmetry] : permet de transformer un but t₁ = t₂ en t₂ = t₁.
      - [rewrite H] : si H est une hypothèse de la forme "t₁ = t₂"
        cette tactique remplace dans le but courant les sous-termes
        de la forme t₁ par t₂.
      - [rewrite <-H] : si H est une hypothèse de la forme "t₁ = t₂"
        cette tactique remplace dans le but courant les sous-termes
        de la forme t₂ par t₁.  *)


Lemma eq_trans : forall (x y z:nat), x = y -> y = z -> x = z.
intros x y z xy yz.
rewrite xy.
apply yz.
Qed.

(* Arithmétique *)

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

Lemma exists_factor : 
  exists n, exists m , n * (m+1) = 36.
exists 12.
exists 2.
simpl.
reflexivity.
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 la
   forme de x. 
   La tactique [induction x] invoque automatiquement le 
   principe d'induction pour prouver un but par induction sur 
   la variable x. *)

induction x.
(* Il faut ensuite prouver le cas de base et l'hérédité...*) 
  simpl.
  reflexivity.
  
  simpl.
  rewrite IHx.
  reflexivity.
Qed.

Lemma plus_assoc : forall a b c, (a + b) + c = a + (b + c).
intros a b c.
induction a.
  simpl.
  reflexivity.
  
  simpl.
  rewrite IHa.
  reflexivity.
Qed.

Lemma mult_zero : forall a, a*0 = 0.
intros a.
induction a.
  simpl.
  reflexivity.
  
  simpl.
  apply IHa.
Qed.


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

Definition lesser_or_equal (n m : nat) := exists k, n+k = m.
Check lesser_or_equal. (* Méditez le types de la relation. *)

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

Lemma lesser_or_equal_refl : 
  forall x, x <= x.
exists 0.
apply plus_zero.
Qed.

Lemma lesser_or_equal_trans : 
  forall x y z, x <= y -> y <= z -> x <= z.
intros x y z xy yz.
destruct xy as [ymx xy].
destruct yz as [zmy yz].
exists (ymx + zmy).
rewrite <- plus_assoc.
rewrite xy.
apply yz.
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.
intros a b.
induction a.
  simpl.
  symmetry.
  apply plus_zero.
  
  simpl.
  rewrite IHa.
  Lemma plus_S_a_b : forall a b, a + S b = S (a + b).
  intros a b.
  induction a.
    simpl.
    reflexivity.
    
    simpl.
    rewrite IHa.
    reflexivity.
  Qed.
  
  rewrite plus_S_a_b.
  reflexivity.
Qed.

Lemma sum_formula: 
  forall n, 2 * (sum n) = n * (n+1).
intros n.
simpl.
rewrite plus_zero.
induction n.
  simpl.
  reflexivity.
  
  simpl.
  rewrite plus_assoc.
  Lemma sum_formula_sub_proof : forall n, sum n + S (n + sum n) = S (n + (sum n + sum n)).
  intros n.
  rewrite plus_comm.
  simpl.
  rewrite plus_assoc.
  reflexivity.
  Qed.
  rewrite sum_formula_sub_proof.
  rewrite IHn.
  clear IHn.
  
  Lemma plus_1_S : forall a, a + 1 = S a.
  intros a.
  rewrite plus_S_a_b.
  rewrite plus_zero.
  reflexivity.
  Qed.
  
  rewrite plus_1_S.
  
  Lemma mult_a_S_b : forall a b, a * (S b) = a * b + a.
  intros a b.
  induction a.
    simpl.
    reflexivity.
    
    simpl.
    rewrite IHa.
    rewrite <- plus_assoc.
    rewrite plus_S_a_b.
    reflexivity.
  Qed.
  
  rewrite plus_S_a_b.
  rewrite (mult_a_S_b n (S n)).
  rewrite (plus_comm _ n).
  reflexivity.
Qed.

Lemma identite : 
  forall a b, (a + b)*(a+b) = a*a + 2*a*b + b*b.
  Lemma distributivité : forall a b c, a * (b + c) = a * b + a * c.
  intros a b c.
  induction a.
    simpl.
    reflexivity.
    
    simpl.
    rewrite IHa.
    repeat rewrite plus_assoc.
    f_equal.
    rewrite plus_comm.
    repeat rewrite plus_assoc.
    f_equal.
    apply plus_comm.
  Qed.
  Lemma mult_comm : forall a b, a * b = b * a.
  intros a b.
  induction a.
    simpl.
    rewrite mult_zero.
    reflexivity.
    
    simpl.
    rewrite IHa.
    rewrite mult_a_S_b.
    apply plus_comm.
  Qed.
  Lemma distributivité_r : forall a b c, (b + c) * a = b * a + c * a.
  intros a b c.
  rewrite mult_comm.
  rewrite distributivité.
  f_equal.
    apply mult_comm.
    apply mult_comm.
  Qed.
  intros a b.
  rewrite distributivité.
  rewrite mult_comm.
  rewrite distributivité.
  rewrite (mult_comm (a + b)).
  rewrite distributivité.
  repeat rewrite <- plus_assoc.
  f_equal.
  repeat rewrite plus_assoc.
  f_equal.
  rewrite (mult_comm b).
  Lemma mult_assoc : forall a b c, a * b * c = a * (b * c).
  intros a b c.
  induction a.
    simpl.
    reflexivity.
    
    simpl.
    rewrite distributivité_r.
    rewrite IHa.
    reflexivity.
  Qed.
  rewrite mult_assoc.
  simpl.
  rewrite plus_zero.
  reflexivity.
Qed.

(* Écrivez la fonction [power] qui calcule les puissances entières : *)
Fixpoint power a b :=
  match b with
  | 0 => 1
  | S b => a * power a b
  end.

Infix "^" := power.

Lemma power_exp: 
  forall a n m, a^(n + m) = a^n * a^m.
intros x a b.
induction a.
  simpl.
  symmetry.
  apply plus_zero.
  
  simpl.
  rewrite IHa.
  symmetry.
  apply mult_assoc.
Qed.

Lemma closed:
  forall n a b c, 3 <= n -> a^n + b^n = c^n -> a = c \/ b = c.
(* Exercise *)
Admitted.