(**** on peut utiliser destruct sur A->B/\C et A->B\/C ****)

(*** preuves de toutes les implications possibles ;
 donc beaucoup plus que ce qui est nécessaire ! ***)


Definition peirce := forall P Q: Prop, ((P->Q)->P)->P.

Definition nono := forall P: Prop, ~~P -> P.

Definition tiers := forall P: Prop, P\/~P.

Definition demorgan := forall P Q: Prop, ~(~P/\~Q)->P\/Q.

Definition fleche := forall P Q: Prop, (P->Q) -> (Q\/~P).

Definition demorganbis := forall P Q: Prop, ~(~P\/~Q) -> P/\Q.

(* --------------------------------------------------------------------------------------------- *)
(* peirce -> ...*)
(* Indication : intros puis utiliser peirce avec apply with Q:=~P, pas toujours facile *)

Theorem peirce_nono: peirce -> nono.
unfold peirce, nono.
intros.
apply H with (Q:=~P).
intros.
destruct H0.
intro. apply H1.
apply H0.
apply H0.
Qed.

Theorem peirce_tiers: peirce -> tiers.
unfold peirce, tiers. intros.
apply H with (Q:=~(P\/~P)).
intros.
right.
intro.
apply H0.
left.
apply H1.
left. apply H1.
Qed.

Theorem peirce_demorgan: peirce-> demorgan.
unfold peirce, demorgan.
intros.
apply H with (Q:=~(P\/Q)).
intros.
destruct H0.
split.
intro.
apply H1.
left. apply H0.
left. apply H0.
intro. apply H1.
right. apply H0.
right. apply H0.
Qed.

Theorem peirce_fleche: peirce->fleche.
unfold peirce, fleche.
intros.
apply H with (Q:=~(Q\/~P)).
intros.
right.
intro.
apply H1.
left. apply H0. apply H2.
left. apply H0. apply H2.
Qed.

Theorem peirce_demorganbis : peirce -> demorganbis.
unfold peirce ; unfold demorganbis.
intros.
split.
apply H with (Q:=Q).
intros.

destruct H0.



(* --------------------------------------------------------------------------------------------- *)
(* nono -> ... *)
(* Indications : intros puis utiliser nono avec apply *)

Theorem nono_peirce: nono->peirce.
unfold nono, peirce. intros.
apply H.
intro.
apply H1.
apply H0.
intro.
destruct H1.
apply H2.
Qed.

Theorem nono_tiers: nono->tiers.
unfold nono, tiers. intros.
apply H.
intro. 
apply H0.
right.
intro.
apply H0.
left.
apply H1.
Qed.

Theorem nono_demorgan: nono->demorgan.
unfold nono,demorgan. intros.
apply H.
intro.
apply H0.
split.
intro. apply H1. left.   apply H2.
intro. apply H1. right. apply H2.
Qed.

Theorem nono_fleche: nono->fleche.
unfold nono, fleche. intros.
apply H.
intro.
apply H1.
right.
intro.
apply H1.
left.
apply H0.
apply H2.
Qed.


Theorem classique_demorganbis: nono -> demorganbis.
unfold nono. unfold demorganbis.
intros.
split.
apply H.
intro.
apply H0.
left.
apply H1.
apply H. intro.
apply H0.
right.
apply H1.
Qed.




(* --------------------------------------------------------------------------------------------- *)
(* tiers -> ... *)
(* Indication : intros puis preuve par cas avec destruct "tiers" with *)

Theorem tiers_peirce: tiers -> peirce.
unfold tiers, peirce.
intros.
destruct H with (P:=P).
apply H1.
apply H0.
intro.
destruct H1.
apply H2.
Qed.

Theorem tiers_nono: tiers->nono.
unfold tiers, nono.
intros.
destruct H with (P:=P).
apply H1.
destruct H0.
apply H1.
Qed.
 
Theorem t1: tiers->demorgan.
unfold tiers.
unfold demorgan.
intros.
destruct H with (P:=P\/Q).
apply H1.
destruct H0.
split.
intro.
apply H1.
left.
apply H0.
intro.
apply H1.
right.
apply H0.
Qed.

Theorem tiers_fleche: tiers -> fleche.
unfold tiers, fleche.
intros.
destruct H with (P:=(Q\/~P)).
apply H1.
right.
intro.
apply H1.
left.
apply H0.
apply H2.
Qed.

(* --------------------------------------------------------------------------------------------- *)
(* demorgan -> ... *)
(* Indication : intros puis utiliser demorgan *)

Theorem demorgan_peirce: demorgan->peirce.
unfold demorgan, peirce.
intros.
destruct H with (P:=P)(Q:=~P).
intro.
destruct H1.
apply H2. apply H1.
apply H1.
apply H0.
intro.
destruct H1.
apply H2.
Qed.

Theorem demorgan_nono: demorgan->nono.
unfold demorgan, nono. intros.
destruct H with (P:=P)(Q:=~P).
intro. destruct H1. apply H2. apply H1.
apply H1.
destruct H0. apply H1.
Qed.

Theorem demorgan_tiers: demorgan -> tiers.
unfold demorgan, tiers. intros.
destruct H with (P:=P)(Q:=~P).
intro. destruct H0. apply H1. apply H0.
left. apply H0.
right. apply H0.
Qed.

Theorem demorgan_fleche: demorgan->fleche.
unfold demorgan, fleche. intros.
destruct H with (P:=Q)(Q:=~P).
intro. destruct H1. apply H2. intro. apply H1.
apply H0. apply H3.
left. apply H1.
right. apply H1.
Qed.

Theorem demorgan_demorganbis: demorgan -> demorganbis.
unfold demorgan. unfold demorganbis.
intros.
split.
destruct (H P False).
intro.
destruct H1.
clear H2.
apply H0.
left.
apply H1.
apply H1.
destruct H1.
destruct (H False Q).
intro.
destruct H1.
apply H0.
right.
apply H2.
destruct H1.
apply H1.
Qed.


(* --------------------------------------------------------------------------------------------- *)
(* fleche -> ... *)
(* Hint : intros puis utiliser fleche pour faire preuve par cas *)
(* SAUF : fleche -> demorgan *)

Theorem fleche_peirce: fleche->peirce.
unfold fleche, peirce. intros.
destruct H with (P:=P)(Q:=P).
intro. apply H1.
apply H1.
apply H0.
intro.
destruct H1.
apply H2.
Qed.

Theorem fleche_nono: fleche->nono.
unfold fleche, nono. intros.
destruct H with (P:=P)(Q:=P).
intro. apply H1.
apply H1.
destruct H0. apply H1.
Qed.

Theorem fleche_tiers: fleche->tiers.
unfold fleche, tiers. intros.
destruct H with (P:=P)(Q:=P).
intro.
apply H0.
left. apply H0.
right. apply H0.
Qed.

Theorem fleche_demorgan: fleche -> demorgan.
unfold fleche, demorgan. intros.
destruct H with (P:=P)(Q:=P).
intro. apply H1.
left. apply H1.
destruct H with (Q:=Q)(P:=Q).
intro. apply H2.
right. apply H2.
destruct H0.
split.
apply H1. apply H2.
Qed.


(* --------------------------------------------------------------------------------------------- *)
(* demorganbis -> ... *)

Theorem demorganbis_classique: demorganbis->nono.
unfold nono ; unfold demorganbis ;intros.
destruct (H P True).
intro.
destruct H1.
apply H0. apply H1.
apply H1. split.
apply H1.
Qed.


(*
Theorem demorganbis_demorgan: demorganbis -> demorgan.
unfold demorganbis. unfold demorgan.
intros.
*)