(* On s'échauffe avec quelques démonstrations simples *)
(* Utilisez les tactiques intro, apply et exact pour  *)
(* démontrer les théorèmes suivants.                  *)

Section Exercice1.

Variables P Q R S:Prop.

Theorem id_P : P->P.
Proof.
Qed.

Theorem id_PP : (P -> P) -> (P -> P).
Proof.
Qed.

Theorem imp_trans : (P->Q) -> (Q->R) -> (P->R).
Proof.
Qed.

Theorem imp_perm : (P -> Q -> R) -> (Q -> P -> R).
Proof.
Qed.

Theorem ignore_q : (P -> R) -> P -> Q -> R.
Proof.
Qed.

Theorem delta_imp: (P -> P -> Q) -> P -> Q.
Proof.
Qed.

Theorem delta_impR : (P-> Q) -> (P -> P -> Q).
Proof.
Qed.

Theorem losange: (P-> Q) -> (P -> R) -> (Q -> R -> S) -> P -> S.
Proof.
Qed.


Theorem weak_peirce : ((((P->Q)->P)->P)->Q)->Q.
Proof.
Qed.

End Exercice1.


(* Apprenons à nous servir des tactiques cut et assert *)

Section Cut.

Variables P Q R T : Prop.
Hypothesis Hpq : P -> Q.
Hypothesis Hqr : Q -> R.
Hypothesis Hprtq : (P -> R) -> T -> Q.
Hypothesis Hprt : (P -> R) -> T.

(* Démontrez une première fois Q comme à l'exercice 1 *)
Theorem Q_naif : Q.
Proof.
Qed.

(* Nous avons faits deux fois le même travail. Pour factoriser *)
(* ce travail, on peut préalablement définir un lemme.         *)
Lemma Lpr : P -> R.
Proof.
Qed.

(* Redémontrez Q en utilisant un lemme judicieusement choisi. *)
Theorem Q_lemma: Q.
Proof.
Qed.

(* On n'est pas obligé de définir un lemme à chaque fois que l'on *)
(* veut démontrer un résultat intermédiaire. Découvrez avec       *)
(* émerveillement l'usage de la tactique cut.                     *)
(* Redémontrez Q.                                                 *)
Theorem Q_cut : Q.
Proof.
Qed.

(* Je m'interroge : Q est-elle vraiment vraie ?   *)
(* Découvrez avec non moins d'émerveillement      *)
(* l'usage de la tactique assert.                 *)
(* Quelle différence y a-t-il entre les tactiques *)
(* assert et cut ?                                *)
Theorem Q_assert: Q.
assert (Hpr:P -> R).
Qed.

(* Les quatre preuves obtenues sont-elles identiques ? *)
(* Comment pouvez-vous le déterminer dans Coq ?        *)

End Cut.


(* Nous allons à présent définir de manière "imprédicative"     *)
(* les divers connecteurs logiques (en système F), et nous      *)
(* allons construire les outils nécessaires à leur utilisation. *)

Section Impredication.

(* Le vrai (quel programme !) *)
Definition my_true : Prop := forall X:Prop, X -> X.

(* Il y a bien une vérité en ce bas monde *)
Lemma tauto : my_true.
Proof.
Qed.

(* Comment définiriez-vous le faux ? *)
Definition my_false ?????


Lemma ex_falso : forall X: Prop, my_false -> X.
Proof.
Qed.

(* Une fausse définition du faux ? *)
Definition my_false_prime : Prop := forall P Q:Prop, P->Q .

Theorem false_prime_is_false : my_false_prime -> my_false.
Proof.
Qed.

(* Le non, qui n'appelle pas de réponse *)
Definition my_not : Prop -> Prop :=
  fun (P:Prop) => P -> my_false.


(* Passons aux choses sérieuses *)

(* Le and (sans les mains) *)
Definition my_and : Prop -> Prop -> Prop := fun P Q:Prop => forall R:Prop, (P->Q->R)->R.


(* Introduction du et        *)
(*     |- A     |- B         *) 
(*     --------------        *)
(*        |- A/\B            *)

Lemma and_split : forall A B:Prop, A->B->(my_and A B).
Proof.
Qed.


(* Élimination du et       *)
(*  |- A /\ B              *)
(*  ----------             *)
(*     |- A                *)
Lemma and_elim_l : forall A B:Prop, (my_and A B) -> A.
Proof.
Qed.

(* Élimination des gens de droite *)
Lemma and_elim_r : forall A B:Prop, (my_and A B) -> B.
Proof.
Qed.



(* Le ou (attention, c'est toxique) *)
Definition my_or : Prop -> Prop -> Prop :=
   fun P Q:Prop => forall R:Prop, (P->R)->(Q->R)->R.


(* Introduction droite du or *)
(*    |- B                   *)
(*  ---------                *)
(*  |- A\/B                  *)
Lemma or_right : forall A B:Prop, B -> my_or A B. 
Proof.
Qed.

(* Introduction des gens de gauche *)
Lemma or_left : forall A B:Prop, A -> my_or A B. 
Proof.
Qed.




(* Un humanisme *)
Definition my_exists : forall A:Set, (A->Prop) -> Prop :=
  fun A P => forall Q:Prop, (forall a:A, (P a)-> Q) -> Q.


(* Manipulons un peu le exists *)
(* Appel à témoins *)
Lemma exists_witness : forall A:Set, forall P:A->Prop, forall a:A,
                            (P a -> my_exists A P).
Proof.
Qed.


(* Quel connecteur manque à l'appel ? Pourquoi ? *)


(* À présent amusons-nous un peu : démontrez Q...           *)
(* NON.... C'est une blague... :-)                          *)
(* Démontrez les théorèmes suivants (beaucoup plus rigolos) *)

Theorem Th1 : forall A:Set, forall P Q : A -> Prop, forall a:A,
                  (P a -> (forall x :A, (P x -> Q x)) -> Q a). 
Proof.
Qed.


Theorem and_comm : forall P Q:Prop, (my_and P Q) -> (my_and Q P).
Proof.
Qed.


Theorem or_comm : forall P Q:Prop, (my_or P Q) -> (my_or Q P).
Proof.
Qed.

Theorem arrow_under_and : forall P Q R S:Prop,
         my_and (P->Q) (R->S) -> (my_and P R) -> my_and Q S.
Proof.
Qed.

Lemma trans_sym_refl : forall A:Set, forall R:A->A->Prop,
(forall x y z, (R x y) -> (R y z) -> (R x z)) ->
(forall x y, (R x y) -> (R y x)) ->
(forall x y, (R x y) -> (R x x)).
Proof.
Qed.

Theorem trans_sym_exists_refl : forall A:Set, forall R:A->A->Prop,
(forall x y z, (R x y) -> (R y z) -> (R x z)) ->
(forall x y, (R x y) -> (R y x)) ->
(forall x, (my_exists A (fun y => (R x y))) -> (R x x)).
Proof.
Qed.

Theorem Th2 : forall A:Set, forall P Q:A->Prop,
 (my_exists A (fun x => my_and (P x) (Q x))) -> 
     my_and (my_exists A P) (my_exists A Q).
Proof.
Qed.

Theorem Th3 : forall P:Prop, P -> my_not (my_not P).
Proof.
Qed.

Theorem impl_with_or : forall P Q: Prop,
                         my_and (my_or P (my_not Q)) Q -> P.
Proof.
Qed.



(* Et quelques questions bonus pour les plus rapides *)
(* d'entre vous.                                     *)

Theorem  and_assoc : forall P Q R:Prop,
  my_and P (my_and Q R) -> my_and (my_and P Q) R.
Proof.
Qed.


Theorem Th4: forall A:Set ,forall P Q : A -> Prop,
(forall x:A, P x) -> (forall y:A, Q y) ->  forall x:A, my_and (P x) (Q x).
Proof.
Qed.

Theorem morgan1 : forall P Q:Prop,
             my_not (my_or P Q) -> my_and (my_not P) (my_not Q).
Proof.
Qed.

Theorem morgan2 : forall P Q : Prop,
             my_or (my_not P) (my_not Q) -> my_not (my_and P Q).
Proof.
Qed.


Theorem weak_excluded_middle : forall P : Prop,
             my_not (my_not (my_or P (my_not P))).
Proof.
Qed.