Set Printing Parentheses.
Require Import Unicode.Utf8.

Partie 1 : Prouver une implication.

La flèche représente l'implication. A -> B signifie intuitivement "Si A, alors B". Pour prouver un énoncé de ce type, on commence par supposer ce qui est à gauche de la flèche. Il faut alors prouver ce qui est à droite à l'aide de cette hypothèse supplémentaires.

Theorem manger (Pjaifaim : Prop) :
  Pjaifaim → Pjaifaim.
Proof.
(* On suppose (hypothèse H) que Pjaifaim est vraie *)
intros H.
(* On doit prouver que Pjaifaim est vrai, mais c'est exactement
   ce que dit l'hypothèse H. *)
exact H.
Qed.

Theorem mangerA (A : Prop): A → A.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Partie 2 : la conjonction (le "et" logique)

Le symbole /\ représente le "et logique". Dire que la proposition (A /\ B) est vraie signifie que A et B sont toutes les deux vraies. Pour UTILISER une telle hypothèse on utilise la tactique "destruct" pour la transformer en 2 hypothèses : l'une disant que A est vrai, l'autre que B est vrai.
Exemple : si j'ai faim et soif, alors en particulier j'ai faim.
Theorem manger_et_boire1 (Pjaifaim Pjaisoif : Prop) :
  Pjaifaim ∧ Pjaisoif → Pjaifaim.
Proof.
  intros Hyp.
  destruct Hyp as [H H0].
  exact H.
Qed.

(* À vous ! *)
Theorem manger_et_boire2 (Pjaifaim Pjaisoif : Prop) :
  Pjaifaim ∧ Pjaisoif → Pjaisoif.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Pour PROUVER un énoncé du type A /\ B, il faut apporter deux preuves :
   une preuve de A et une preuve de B.
   On informe coq qu'on veut le faire avec la tactique split. *)

Theorem faim_soif_soif_faim (Pjaifaim Pjaisoif : Prop) :
  Pjaifaim ∧ Pjaisoif → Pjaisoif ∧ Pjaifaim.
Proof.
  (* On suppose (hypothèse Hyp) que (Pjaifaim /\ Pjaisoif) est vraie *)
  intros Hyp.
  (* On en déduit que Pjaifaim (H) est vraie et que Pjaisoif (H0) est vraie. *)
  destruct Hyp as [H H0].
  (* On va prouver que Pjaisoif est vraie puis que Pjaifaim est vraie *)
  split.
  (* Preuve que Pjaisoif est vraie : *)
  exact H0.
  (* Preuve que Pjaifaim est vraie : *)
  exact H.
Qed.

(* À vous, avec un énoncé plus abstrait *)
Theorem et_commutatif (A B : Prop) :
   A ∧ B → B ∧ A.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Dans l'énoncé suivant, il y a deux prémisses, on peut faire
 * deux hypothèses, donc vous devez utiliser intros deux fois. *)

Theorem hypotheses_faim_soif (Pjaifaim Pjaisoif : Prop) :
  Pjaifaim → (Pjaisoif → Pjaifaim ∧ Pjaisoif).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Presque la même chose, pour voir que l'ordre des prémisses n'est pas
 * important. *)

Theorem hypotheses_soif_faim (Pjaifaim Pjaisoif : Prop) :
  Pjaisoif → (Pjaifaim → Pjaifaim ∧ Pjaisoif).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* On continue ce petit jeu.*)
Theorem si_alors_et2 (A B C : Prop) :
   A → (B → (C → A ∧ (B ∧ C))).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* On peut aussi utiliser un "et" dans un "et". Une fois les
hypothèses introduites, penser à utiliser "destruct". *)
Theorem utiliser_et_dans_et (A B C : Prop) :
  A ∧ (B ∧ C) → A ∧ B.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Partie 3 : la disjonction (le "ou" logique)

On en vient au connecteur de base le plus compliqué : le "ou", représenté ici par \/. Dire que A \/ B est vraie signifie que : A est vraie ou B est vraie (ou les deux). Pour prouver un tel énoncé, il faut faire un choix ! Lequel est vrai ? Ceci se fait avec les tactiques :
  • left (pour choisir de prouver ce qui est à gauche de \/) et
  • right (pour choisir de prouver ce qui est à droite de \/).
Exemple : si j'ai faim, alors j'ai faim ou soif

Theorem faim_faim_ou_soif (Pjaifaim Pjaisoif : Prop) :
  Pjaifaim → (Pjaifaim ∨ Pjaisoif).
Proof.
  (* On suppose (hypothèse (H)) que j'ai faim. *)
  intros H.
  (* Pour prouver que j'ai faim ou soif,
     on va fournir une preuve que j'ai faim. *)
  left.
  exact H.
Qed.

(* À vous ! *)
Theorem soif_faim_ou_soif (Pjaifaim Pjaisoif : Prop) :
  Pjaisoif → (Pjaifaim ∨ Pjaisoif).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Dans certains cas, les deux propositions sont vraies et qu'on choisisse left
 * ou right, la preuve fonctionne. *)

(* À vous ! *)
Theorem et_affaibli_en_ou (A B : Prop) :
  A ∧ B → A ∨ B.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Utiliser un "ou" : lorsqu'on a une hypothèse du type A \/ B, on sait seulement que l'une des deux propositions est vraie, mais on ne sait pas laquelle ! Il faut alors donner deux preuves :
  • l'une dans le cas où A est supposée vraie ;
  • l'autre dans le cas où B est supposée vraie.
Ceci se fait encore avec la tactique destruct.
Exemple : si nous sommes le lundi ou le mardi, alors nous sommes le mardi ou le lundi.

Theorem ou_commutatif_exemple (lundi mardi : Prop):
   lundi ∨ mardi → mardi ∨ lundi.
Proof.
  (* On suppose (hypothèse (H)) que nous sommes lundi ou mardi. *)
  intros H.
  (* On va séparer les cas : *)
  destruct H as [H1 | H2].
  (* Premier cas (H1) : on suppose qu'on est le lundi. *)
  right.
  exact H1.
  (* Deuxième cas (H2) : on suppose qu'on est le mardi. *)
  left.
  exact H2.
Qed.

(* À vous avec un énoncé plus abstrait. *)
Theorem ou_commutatif (A B : Prop):
   A ∨ B → B ∨ A.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Un exercice un peu plus dur avec des "ou" et des "et". *)
Theorem and_or_distr_l_1 (A B C : Prop) :
  A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Partie 4 : utiliser une implication.

Utiliser une implication. Pour utiliser une implication, on utilise la tactique apply, pour remplacer le but par ce qui est à gauche de l'implication.
L'exemple suivant dit :
  • j'ai un chocolat
  • tous les chocolats sont des desserts
  • donc j'ai un dessert.

Theorem miam (chocolat dessert : Prop) :
    chocolat → (chocolat → dessert) → dessert.
Proof.
(* On suppose (hypothèse (H1)) que j'ai un chocolat. *)
intros H1.
(* On suppose (hypothèse (H2)) qu'un chocolat est un dessert. *)
intros H2.
(* D'après (H2), pour prouver que j'ai un dessert, il suffit de prouver que
   j'ai un chocolat. *)
apply H2.
(* Or, c'est exactement ce que dit H1. *)
exact H1.
Qed.

(* À vous avec un énoncé un peu plus abstrait. *)
Theorem modus_ponens (A B : Prop) : A → (A → B) → B.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* On peut commencer à prouver des énoncés un peu plus compliqués. *)
Theorem imp_trans (A B C : Prop) :
  (A → B) → (B → C) → A → C.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem or_imp (A B C : Prop) :
  (A → C) → (B → C) → (A ∨ B) → C.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Voyons maintenant un exemple d'apply qui fait apparaître des sous-buts. *)
Theorem exple_sous_but (A B C : Prop) :
  (A → B → C) → A → B → C.
Proof.
  (* On suppose (hypothèse (H)) que A et B impliquent C. *)
  intros H.
  (* On suppose (hypothèses (H1) et (H2) que A et B sont vrais. *)
  intros H1 H2.
  (* D'après (H), pour prouver C, il suffit de prouver A et de prouver B. *)
  apply H.
  (* Preuve de A : *)
  exact H1.
  (* Preuve de B : *)
  exact H2.
Qed.

(* À vous ! *)
Theorem modus_ponens2 (A B C : Prop) :
   A → (A → B) → (A → B → C) → C.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Fin de partie 4 : exercices à faire en plus si vous avez le temps.


Theorem and_or_distr_l_2 (A B C : Prop) :
  (A ∧ B) ∨ (A ∧ C) → A ∧ (B ∨ C).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem and_imp_imp (A B C : Prop) :
  A ∧ B → (A → B → C) → C.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem plop (A B C : Prop) :
  (A ∨ B) → (B → C) → A ∨ C.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Partie 5 : la proposition False

En logique intuitionniste (et aussi en logique classique), si on a prouvé False (le faux, l'absurde) alors on a prouvé n'importe quoi. Ce principe s'appelle "exfalso quod libet", ce qui en latin signifie "à partir du faux, on peut déduire tout ce qu'on veut".
En coq, si l'on utilise la tactique destruct sur une preuve de faux, la preuve est tout simplement terminée.
Exemple : si False, alors je suis un super héros

Theorem faux_en_hypothese_exemple (je_suis_un_super_heros : Prop) :
  False → je_suis_un_super_heros.
Proof.
  (* On suppose (hypothèse (H)) que False est prouvée. *)
  intro H.
  (* Alors, de (H) on déduit n'importe quoi. *)
  destruct H.
Qed.

Theorem faux_en_hypothese (A : Prop): False → A.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Vraiment, dès qu'on a prouvé False, pas la peine d'insister,
   c'est terminé ! *)

Theorem faux_en_hypothese2 (A B C D E : Prop):
   A → False → (A → B → C) → (C ∨ D) → E.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

La tactique exfalso remplace le but par False. On dit simplement à coq : "je pense que mes hypothèses sont contradictoires, je vais prouver False vu que ça prouve tout."
On utilise exfalso lorsque nos hypothèses semblent contradictoire et le but impossible. On se ramène à prouver le faux avec "exfalso" et les hypothèses contradictoires, et tout devient possible.
Voici un exemple : Si (A -> False) et A, alors on a une preuve de n'importe quelle proposition B.

Theorem false_A_A (A B : Prop) :
  (A → False) → A → B.
Proof.
  (* On suppose (hypothèse (H)) que A implique False. *)
  intros H.
  (* On suppose (hypothèse (H1) que A est vraie. *)
  intros H1.
  (* Comme le False entraîne n'importe quoi, pour prouver B, il suffit de
     prouver False. *)
  exfalso.
  (* D'après (H), pour prouver False, il suffit de prouver A. *)
  apply H.
  (* Or, c'est exactement ce que dit l'hypothèse (H1). *)
  exact H1.
Qed.

(* À vous ! *)
Theorem false_imp (A B C : Prop) :
  (A → False) → (B → A) → B → C.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Partie 6 : la négation

En logique intuitionniste, la négation d'une proposition A, appelée "non A" et notée ~A ou ¬A est simplement la même chose que (A -> False).
Pour traduire une notation, on utilise la tactique unfold (en anglais, déplier).
Exemple, si un mur et blanc et non blanc, alors je mange des vers de terre.

Theorem idiot (mur_blanc je_mange_des_vers_de_terre : Prop):
    mur_blanc → ¬mur_blanc → je_mange_des_vers_de_terre.
Proof.
  (* On remplace ~mur_blanc par (mur_blanc -> False). *)
  unfold "~".
  (* On suppose (hypothèse (H1)) que le mur est blanc. *)
  intros H1.
  (* On suppose (hypothèse (H2)) qu'il n'est pas blanc. *)
  intros H2.
  (* Il suffit de prouver False. *)
  exfalso.
  (* Pour prouver False, par H2, il suffit de prouver que le mur est blanc. *)
  apply H2.
  (* Ce que dit exactement l'hypothèse H1. *)
  exact H1.
Qed.

(* À vous ! *)
Theorem absurd (A C : Prop): A → ¬A → C.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem contraposee (A B C : Prop) :
 (A → B) → ¬B → ¬A.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem AnnA (A : Prop) :
  A → ~~A.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem or_not (A B : Prop) :
  A ∨ B → ¬B → A.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem demorgan1 (A B : Prop) :
  ~(A ∨ B) → (¬A) ∧ (¬B).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)