(** ** 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. *)