Consignes

Ce devoir est à rendre sur le dépôt moodle avant le : dimanche 20 septembre à 23h59 Vous rendrez un seul fichier appelé Devoir_1_2026.v et complèterez la déclaration suivante ci-dessous : NOM, prénom, numéro étudiant : Je déclare qu'il s'agit de mon propre travail et que ce travail a été intégralement réalisé par un être humain. C'est un travail individuel. Vous pouvez vous aider les uns les autres mais vous ne devez jamais vous montrer le code de votre solution. L'usage de ChatGPT ou de toute autre intelligence artificielle pour résoudre les exercices est interdit. N'hésitez pas à vous aider les uns les autres, mais sans jamais vous montrer le code de la solution. Il est possible aussi d'envoyer des mails à rousselin@univ-paris13.fr. Le premier but de ce très court premier devoir est de vous faire progresser en mathématiques et en informatique. Le deuxième est que tous les étudiants soient bien à jour dans la progression et aient un environnement suffisamment en place pour rendre les devoirs. Pour faire ce devoir, il faut avoir traité le sujet Logique1.v. Vous utiliserez les tactiques :

• intros
• exact
• split
• destruct pour : un /\, un \/
• left ou right
• apply

Logique de base en Rocq

Lemma ex1 : forall (P Q R : Prop), (P -> Q) -> (Q -> R) -> P -> R. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex2 : 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. *)

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.

Lemma ex3 : forall P Q : Prop, ((((P -> Q) -> P) -> P) -> Q) -> Q. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex4 : forall P Q R : Prop, P /\ (Q /\ R) -> (P /\ Q) /\ R. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex5 : forall (P Q R S : Prop), (P -> Q) -> (P -> R) -> (Q /\ R -> S) -> P -> S. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex6 : forall (P Q R : Prop), (P -> Q) -> (P -> R) -> P -> Q /\ R. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex7 : forall (P Q R : Prop), (P -> R) -> (Q -> R) -> P \/ Q -> R. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex8 : forall (P Q R : Prop), (P \/ Q) \/ R -> P \/ (Q \/ R). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex9 : forall (P Q R : Prop), ((P -> R) \/ (Q -> R)) -> P /\ Q -> R. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) Lemma ex10 : forall (P Q R : Prop), P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)