Partie 7 : Une histoire de desserts

Section Dessert.
On va maintenant utiliser l'ensemble de nos connaissances pour résoudre un exercice assez classique de logique propositionnelle : une histoire de desserts.
Trois amis (Jihane, Mehdi et Orane) ont l'habitude de déjeuner ensemble. À la fin du repas ils prennent ou non un dessert.
Les habitudes des amis sont les suivantes :
  • Si Jihane prend un dessert, alors Mehdi en prend un aussi.
  • Si Orane prend un dessert, alors Jihane en prend un aussi.
De plus, on sait que ce jour-là, Jihane ou Orane ont pris un dessert, mais Mehdi et Orane n'en ont pas tous les deux pris.
On modélise la situation de la façon suivante :
Variables Jihane_dessert Mehdi_dessert Orane_dessert : Prop.
Hypothesis H1 : Jihane_dessert → Mehdi_dessert.
Hypothesis H2 : ~(Mehdi_dessert ∧ Orane_dessert).
Hypothesis H3 : Jihane_dessert ∨ Orane_dessert.
Hypothesis H4 : Orane_dessert → Jihane_dessert.

Vous avez appris à utiliser les tactiques "destruct" ou "apply" sur des hypothèses que vous aviez dans votre contexte, au dessus de la barre dans le carré en haut à droite de Coqide. En fait, vous pouvez toujours utiliser les hypothès qui sont globales, comme H1 H2 H3 et H4 ci-dessus. Une fois énoncées, elles sont vraies tout le temps, dans toutes les preuves qui les suivent.
Voici un exemple à compléter
Theorem T1 : Jihane_dessert.
Proof.
  (* Une des hypothèse est un "ou", une disjonction, que l'on peut
  utiliser. Soit la proposition à gauche de \/ est vraie, soit la
  proposition à droite du \/ est vraie *)
  destruct H3 as [H | H'].
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Remarque : vous pouvez utiliser un théorème en utilisant son nom, de la même manière que vous l'avez fait avec des hypothèses. Par exemple, à partir de maintenant, si vous devez prouver que Jihane a pris un dessert, vous pouvez utiliser la tactique "exact T1".

Theorem T2 : Mehdi_dessert.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem T3 : ¬Orane_dessert.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Orane, ne vous en faîtes pas, vous pouvez tout de même prendre un dessert, ce n'est qu'un exercice...
End Dessert.

Partie 8 : Une histoire d'amitié


Section Amis.
(* On considère des élèves, qui peuvent être amis ou non*)
Variable (Eleve : Type).
Variables (Ylian Krystoffer Nakshatra Wael : Eleve).
Variable (Amis : Eleve → Eleve → Prop).

(* On va faire certaines hypothèses sur qui est ami avec qui. *)

(* On suppose que Krystoffer est amie avec Ylian. *)
Hypothesis CB : Amis Krystoffer Ylian.
(* Mais qu'Nakshatra n'est pas ami avec Ylian. *)
Hypothesis nEB : ~(Amis Nakshatra Ylian).
(* Nakshatra est ami avec Wael. *)
Hypothesis ED : Amis Nakshatra Wael.

(* Maintenant, on suppose que l'amitié est toujours réciproque, en maths on dit
   que c'est une relation symétrique. *)
Hypothesis amis_amis :
  ∀ (e1 e2 : Eleve), (Amis e1 e2) → (Amis e2 e1).
(* Ceci dit que, quels que soient les élèves e1 et e2, si e1 est ami
   avec e2, alors e2 est ami avec e1.
   forall signifie "pour tous" en anglais, c'est comme si e1 et e2
   étaient à gauche des ":" dans l'énoncé amis_amis.

   On va maintenant prouver un premier théorème simple :
   Ylian est amie avec Krystoffer.
*)

Theorem BC : Amis Ylian Krystoffer.
Proof.
  (* D'après amis_amis, pour prouver que Ylian est amie de Krystoffer,
     il suffit de prouver que Krystoffer est amie avec Ylian. *)
  apply amis_amis.
  exact CB.
Qed.

(* À vous ! *)
Theorem DE : Amis Wael Nakshatra.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem nBE : ~(Amis Ylian Nakshatra).
Proof.
intro H.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Maintenant, on introduit des groupes d'amis. Il y a le groupe 1 et
   le groupe 2 et chaque élève appartient à l'un des groupes. *)
Variable (groupe1 : Eleve → Prop).
Variable (groupe2 : Eleve → Prop).

On va donner des axiomes qui expliquent à notre sens ce que veut dire être dans un groupe d'amis
Deux amis appartiennent toujours au même groupe
Hypothesis groupe_amis :
  ∀ (groupe : Eleve → Prop), ∀ (e1 e2 : Eleve),
    (Amis e1 e2) ∧ (groupe e1) → (groupe e2).

Deux personnes dans le même groupe sont amies
Hypothesis amis_groupe :
  ∀ (groupe : Eleve → Prop), ∀ (e1 e2 : Eleve),
    (groupe e2) ∧ (groupe e1) → (Amis e1 e2).

Theorem Nakshatra_et_Ylian : groupe1 Ylian → ~(groupe1 Nakshatra).
Proof.
  intros H0 H1.
  (* on va montrer que Ylian et Nakshatra sont amis *)
  assert (Amis Ylian Nakshatra).
    (* c'est parce que ils sont dans le même groupe *)
    apply (amis_groupe groupe1).
    split; assumption.
  (* Or on savait que ils n'etaient pas amis, c'est de là qu'on va
  prouver l'absurde *)
  apply nEB.
  (* il faut juste qu'on applique le fait qu'une relation d'amitié est
  symmétrique *)
  apply amis_amis.
  assumption.
Qed.

Observez la preuve ci-dessus: on se sert du "assert" pour prouver des petits résultats intermédiaires qui nous aident à avancer. Vous pouvez désormais vous servir du assert aussi dans les preuves.
Observez aussi comment on applique les axiomes (ici amis_groupe). Souvent ils demandent un paramètre (ici groupe1) qu'il faut leur donner explicitement

(* À vous ! *)
Theorem Nakshatra_et_Krystoffer : groupe1 Krystoffer → ~(groupe1 Nakshatra).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Theorem pas_amis: (groupe1 Wael) → ~(Amis Wael Ylian).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

On peut prouver que les amis de mes amis sont mes amis, pour peu que l'on soit dans un groupe

Theorem amis_des_amis (e1 e2 e3 : Eleve) :
  groupe1 e1 → Amis e1 e2 → Amis e2 e3 → Amis e1 e3.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Les ennemis de mes amis sont mes ennemis
Theorem les_amis_de_mes_ennemis (A B C : Eleve):
  groupe1 A → ¬ (Amis A B) → (Amis C B) → ¬ (Amis A C).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Pour prouver que les ennemis de mes ennemis sont mes amis, il faut un peu plus d'hypotheses
(* On suppose maintenant que tout élève est forcément dans un groupe *)

Hypothesis deux_groupes : ∀ (E : Eleve), groupe1 E ∨ groupe2 E.

(* Ça implique que si tu n'es pas dans un groupe, tu es dans l'autre *)

Theorem pas_group2_groupe1 (E : Eleve): ¬ groupe2 E → groupe1 E.
Proof.
  intro.
  (*Tout comme on peut faire un apply avec un théorème prouvé avant,
  on peut aussi faire un destruct un theoreme prouvé avant. Observez
  ce qu'il se passe. *)
  destruct (deux_groupes E).
  assumption.
  exfalso.
  apply H; assumption.
Qed.

Prouver le symmétrique dont vous aurez besoin
(* À vous de jouer *)
Theorem pas_group1_groupe2 (E : Eleve): ¬ groupe1 E → groupe2 E.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

(* Voici un preuve à trous, où on vous propose de prouver des lemmes
intermédiaires au cours de la preuve *)

Theorem les_ennemis_de_mes_ennemis (A B C : Eleve):
  groupe1 A → ¬ (Amis A B) ∧ ¬ (Amis C B) → Amis A C.
Proof.
  Proof.

 intros GA [nAB nCB].
 assert (groupe2 B).
 (* prouvez que B est dans le groupe2 *)
 assert (groupe1 C).
 (* prouvez que C est dans le groupe1 *)
 (* puis servez vous de ces deux lemmes qui sont maintenant des
 hypotheses pour prouver votre but *)
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Qu'est ce qui se passe si l'on suppose

Hypothesis amis_ou_pas :
  ∀ (e1 e2 : Eleve), (Amis e1 e2) ∨ ~(Amis e1 e2).

C'est la même chose de supposer :
Theorem pas_pas_amis (e1 e2 : Eleve):
  ~~(Amis e1 e2) → (Amis e1 e2).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

End Amis.