(* This file is part of the "Initiation aux preuves formelles" course in Villetaneuse, France. Copyright (C) Kerjean, Mayero, Rousselin This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *)

Logique 1 : exercices à faire à la maison

Ces exercices d'entraînement sont à faire à la maison (ou en classe si vous avez terminé). Ils sont en général un peu plus difficiles que ceux vus en classe. Il est très important que vous preniez le temps de les faire.

Exercices sur l'implication

Exercice : Prouver le théorème suivant

Indice : en vérité, il n'y a pas tellement à réfléchir, mais à un moment, vous aurez l'impression d'avoir fait du surplace alors que non, un nouvel élément sera apparu dans le contexte.

Theorem weak_peirce : forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) -> Q. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Rien de bien difficile ici, un apply fera juste apparaître deux sous-buts.

Theorem diamond : forall P Q R T : Prop, (P -> Q) -> (P -> R) -> (Q -> R -> T) -> P -> T. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercices sur la conjonction et la disjonction

Exercice : Prouver le théorème suivant.

Theorem and_assoc2 : forall P Q R : Prop, P /\ Q /\ R -> (P /\ Q) /\ R. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem or_assoc1 : forall P Q R: Prop, (P \/ Q) \/ R -> P \/ Q \/ R. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)