(** NOM : ..... *)

(** Ce squelette comporte des éléments partiels pour la résolution de votre devoir, vous devez compléter les parties manquantes et répondre aux questions du sujet *)
(** Renommer le fichier en votre_nom.v *)
(** Rendre le devoir avant le lundi 11 avril 2016 à stefania.dumbrava@lri.fr *)

(** Exercice 1 *)

Section exo1.

Variables P Q R : Prop.

Lemma La : (~ P /\ ~ Q) -> Q -> P.
Proof.
(* compléter *)
Qed.

Lemma Lb : ~ (P -> Q) -> ~ P -> Q.
Proof.
(* compléter *)
Qed.

Lemma Lc : (P -> Q) -> ~ Q -> (~ P \/ Q).
Proof.
(* compléter *)
Qed.

Lemma Ld : (~ (P \/ Q) /\ R) -> (R /\ ~ P) \/ ~ Q.
Proof.
(* compléter *)
Qed.

Lemma Le : (P \/ Q) -> (P -> Q -> R) -> R.
Proof.
(* compléter *)
Qed.

Lemma Lf : (P -> Q) -> (P \/ R -> Q) -> R -> Q.
Proof.
(* compléter *)
Qed.

Lemma Lg : (P \/ Q) -> ~ Q -> P.
Proof.
(* compléter *)
Qed.

Lemma Lh : ((P -> Q) -> R) -> P -> (Q \/ R).
Proof.
(* compléter *)
Qed.


End exo1.

(** Exercice 2 *)

Section exo2.

Variable X : Type.
Variable p : X -> X -> Prop.

Lemma exist_swap :
  (exists x, exists y, p x y) <-> exists y, exists x, p x y.
Proof.
(* compléter*)
Qed.

End exo2.

(** Exercice 3 *)

Section exo3.
Variable X : Type.
Variables ami voisin : X -> X -> Prop.
Variable enfant : X -> Prop.

(* Q1 *)
Definition Pa := (*compléter*).
Definition Pb := (*compléter*).
Definition Pc := (*compléter*).
Definition Pd := (*compléter*).

Lemma prop : Pa -> Pb -> Pc -> Pd -> (*compléter*).
Proof.
(* compléter*)
Qed.

(* Q3 *)
Inductive table : X -> X -> Prop := (*compléter*)
.


End exo3.

(** Exercice 4 *)

Section exo4.

Require Import Arith Omega.

Fixpoint exp2 (n:nat) : nat := match n with 
   0 => 1 | S p => 2 * exp2 p end.

Lemma exp2S : forall n, exp2 (S n) = 2 * exp2 n.
Proof.
intros; reflexivity.
Qed.

Fixpoint div2 (n:nat) : nat := match n with 
   0 => 0 | 1 => 0 | S (S p) => S (div2 p) end.

Lemma div2S : forall n, div2 (S (S n)) = S (div2 n).
Proof.
intros; reflexivity.
Qed.

(* Q3 *)

Section ArtinInd.
Variable P : nat -> Prop.
Hypothesis H1: P 1.
Hypothesis H2 : forall n, P n -> P (2*n).
Hypothesis Hlt : forall n, P (S n) -> P n.

Lemma PA1 : forall n, P (exp2 n).
Proof.
(* compléter *)
Qed.

Lemma PA2 : forall n, P n -> forall k, k <= n -> P k.
Proof.
(* compléter *)
Qed.

Lemma PAn : forall n, P n.
Proof.
(* compléter *)
Qed.

End ArtinInd.

(* Q4a *)
Inductive F : nat -> nat -> Prop := 
(* compléter *)
.

(* Q4c *)
Lemma Fapp : forall n, exists p, F n p.
Proof.
apply PAn.
(* compléter *)
Qed.