(* 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 imp_trans : (P->Q) -> (Q->R) -> (P->R).
Proof.
Qed.

Theorem imp_perm : (P -> Q -> R) -> (Q -> P -> R).
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.
cut (P->R).
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.
Proof.
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.



(* Pour définir le connecteur 'il existe', les choses se corsent     *)
(* un peu. Considérons la formule 'il existe a dans A tel que P(a)'  *)
(* le connecteur 'il existe' prend donc comme arguments un           *)
(* ensemble A, un prédicat P : A->Prop et renvoie un objet de        *)
(* type Prop.                                                        *)
(* À présent comment utilise-t-on une formule existentielle pour     *)
(* démontrer une formule Q ? Nous nous servons du témoin a qu'elle   *)
(* nous fournit pour montrer Q. Ce témoin est anonyme, au sens où    *)
(* nous ne savons rien sur lui, hormis qu'il satisfait P(a).         *)
(* Autrement dit, si, pour a quelconque vérifiant P(a), on sait      *)
(* démontrer Q, alors Q est vrai. C'est ce que traduit la définition *)
(* imprédiative de ce connecteur.                                    *)

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

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.

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

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


End Impredication.



Section TypeEnumere.

(* Dans cette section, nous allons définir la logique booléenne à l'aide du *)
(* type énuméré bool défini dans Coq.                                       *)

(* Comment regardez la définition du type bool en Coq ? *)


Definition and : bool -> bool -> bool := fun a b =>
  match a with
    | true => b
    | false => false
  end.

(* Définissez or *)
Definition or : bool -> bool -> bool := .

Definition not : bool -> bool := fun a =>
  match a with
    | true => false
    | false => true
  end.

Definition impl : bool -> bool -> bool := fun a b => or (not a) b.

(* Redémontrons un théorème ou deux... *)
Theorem and_comm_bool : forall P Q:bool, impl (and P Q) (and Q P) = true.
Proof.
Qed.

Theorem morgan1_bool : forall P Q:bool,
          impl   (not (or P Q))    (and (not P) (not Q)) = true.
Proof.
Qed.

Theorem weak_excluded_middle_bool : forall P : bool,
             not (not (or P (not P))) = true.
Proof.
Qed.

(* Et comme on est en logique classique, *)
(* on peut même démontrer le tiers-exclu *)
Theorem excluded_middle_bool : forall P : bool,
             or P (not P) = true.
Proof.
Qed.

End TypeEnumere.



Section LogiquePropositionnelleEnCoq.

(* Nous avons vu comment définir les connecteurs logiques *)
(* de façon imprédicative. En Coq, les connecteurs sont   *)
(* fournis dans le langage (en réalité, ils sont définis  *)
(* de façon inductive, mais nous verrons ça plus tard).   *)

(* Le 'et' s'écrit avec l'opérateur infixe /\             *)
(* Le 'ou' s'écrit avec l'opérateur infixe \/             *)
(* Le 'non' s'écrit avec l'opérateur préfixe ~            *)
(* 'Il existe a:A tel que (P a)' s'écrit exists a:A, (P a)*)

(* Nous avions défini les lemmes d'introduction et        *)
(* éventuellement d'élimination pour chaque connecteur.   *)
(* On retrouve ces lemmes sous forme de tactique dans Coq.*)
(* Les voici résumées :                                   *)

(*  - les éliminations de tous les connecteurs se font par un elim.   *)
(*  - introduction du et : tactique split. L'usage de cette tactique  *)
(*    casse le but en deux sous-buts.                                 *)
(*  - introduction du ou : tactiques left et right. Servent à choisir *)
(*    quelle membre de l'alternative on va prouver.                   *)
(*  - introduction du non : tactique intro                            *)
(*    (~P est un raccourci pour P -> False).                          *)
(*  - introduction du il existe : tactique exists. Permet de          *)
(*    désigner un témoin                                              *)

(* Récrivez et démontrez les théorèmes suivants en utilisant les *)
(* connecteurs de Coq                                            *)

Theorem or_comm_Prop : ??????.
Proof.
Qed.

Theorem Th2_Prop : ??????.
Proof.
Qed.

Theorem Th3_Prop : ??????.
Proof.
Qed.

End LogiquePropositionnelleEnCoq.