(********************)
(*   EXERCICE 0.1   *)
(********************)

Lemma exemple :
  forall A : Prop, A -> A.

Proof.
auto. (* On laisse faire le système *)
Defined.

Print exemple.

(*
exemple = fun (A : Prop) (H : A) => H
     : forall A : Prop, A -> A
*)

(********************)
(*   EXERCICE 0.2   *)
(********************)

Check (forall n : nat, True).

(*
nat -> True
     : Prop
*) (* Le "forall" a été remplacé par "->" *)

Parameter T : Set.
Parameter c : T.
Parameter f : T -> T.
Parameter A B C : Prop.
Parameter P Q R : T -> Prop.

(************************************)
(*   EXERCICE 1: Logique minimale   *)
(************************************)

(* 1. Principe d'identité *)

Lemma imp_refl :
  A -> A.

Proof (fun (x : A) => x).

(* 2. Syllogisme Barbara *)

Lemma imp_trans :
  (A -> B) -> (B -> C) -> A -> C.

Proof (fun (f : A -> B) (g : B -> C) (x : A) => g (f x)).

(* 3. Axiome du combinateur K *)

Lemma K_axiom :
  A -> B -> A.

Proof (fun (x : A) (y : B) => x).

(* 4. Axiome du combinateur S *)

Lemma S_axiom :
  (A -> B -> C) -> (A -> B) -> A -> C.

Proof (fun (x : A -> B -> C) (y : A -> B) (z : A) => x z (y z)).

(*******************************)
(*   EXERCICE 2: La négation   *)
(*******************************)

(* 1. Introduction de la double négation: *)

Lemma not_not_intro :
  A -> ~~A.

Proof (fun (x : A) (f : A -> False) => f x).

(* 2. Élimination de la double négation: *)

(*    (Quand les poules auront des dents...) *)

(* 3. Contraposition: un cas particulier de Barbara *)

Lemma imp_contra :
  (A -> B) -> ~B -> ~A.

Proof (fun (f : A -> B) (g : B -> False) (x : A) => g (f x)).

(* 4. Non contradiction de l'élimination de la double négation: *)

Lemma weak_not_not_elim :
  ~~(~~A -> A).

Proof
  (fun (k : ~(~~A -> A)) =>
    k (fun (y : ~~A) =>
         False_ind A
           (y (fun (x : A) => k (fun (_ : ~~ A) => x)))
      )).

(*************************************************)
(*   EXERCICE 3: La quantification universelle   *)
(*************************************************)

(* 1. *)
Lemma separ :
  (forall x, P x -> Q x) -> (forall x, P x) -> forall x, Q x.

Proof (fun (f : forall x, P x -> Q x)
           (g : forall x, P x) (x : T) => f x (g x)).

(* 2. *)
Lemma Barbara :
  (forall x, P x -> Q x) -> (forall x, Q x -> R x) -> forall x, P x -> R x.

Proof (fun (f : forall x, P x -> Q x)
           (g : forall x, Q x -> R x)
           (x : T) (p : P x) => g x (f x p)).

(* 3. *)
Lemma double :
  (forall x, P x -> P (f x)) -> (forall x, P x -> P (f (f x))).

Proof (fun (h : forall x, P x -> P (f x))
           (x : T) (p : P x) => h (f x) (h x p)).

(* 4. *)
Lemma contre_exemple :
  (forall x, P x -> Q x) -> ~ Q c -> ~ (forall x, P x).

Proof (fun (f : forall x, P x -> Q x)
           (g : Q c -> False)
           (h : forall x, P x) => g (f c (h c))).

(**********************************)
(*   EXERCICE 4: La conjonction   *)
(**********************************)

(* 1. *)
Lemma and_sym :
  A /\ B -> B /\ A.

Proof (fun (p : A /\ B) => conj (proj2 p) (proj1 p)).

(* 2. *)
Lemma and_assoc :
  (A /\ B) /\ C -> A /\ (B /\ C).

Proof (fun (p : (A /\ B) /\ C) =>
         conj (proj1 (proj1 p)) (conj (proj2 (proj1 p)) (proj2 p))).

(* 3. *)
Lemma and_imp :
  (A -> B) /\ (A -> C) <-> (A -> B /\ C).

Proof (conj (fun (p : (A -> B) /\ (A -> C)) (x : A) =>
              (conj (proj1 p x) (proj2 p x)))
            (fun (p : (A -> B /\ C)) =>
              (conj (fun (x : A) => proj1 (p x))
                    (fun (x : A) => proj2 (p x))))).

(* 4. *)
Lemma forall_and :
  (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x).

Proof (conj
        (fun (h : forall x, P x /\ Q x) =>
          conj (fun x => proj1 (h x)) (fun x => proj2 (h x)))
        (fun (h : (forall x, P x) /\ (forall x, Q x)) =>
          fun (x : T) => conj (proj1 h x) (proj2 h x))).

(**********************************)
(*   EXERCICE 5: La disjonction   *)
(**********************************)

(*
  \begin{enumerate}
  \item\verb|A \/ B -> B \/ A|.
  \item\verb|(A \/ B) \/ C -> A \/ (B \/ C)|.
  \item\verb|(A \/ B -> C) <-> (A -> C) /\ (B -> C)|.
  \item\verb|~~ (A \/ ~A)|.
*)

(* 1. *)
Lemma or_sym :
  A \/ B -> B \/ A.

Proof (fun (s : A \/ B) =>
        (or_ind (fun (x : A) => or_intror B x)
                (fun (y : B) => or_introl A y) s)).

(* 2. *)
Lemma or_assoc :
  (A \/ B) \/ C -> A \/ (B \/ C).

Proof (fun (s : (A \/ B) \/ C) =>
         (or_ind
            (fun (t : A \/ B) =>
              (or_ind
                (fun (x : A) => or_introl (B \/ C) x)
                (fun (y : B) => or_intror A (or_introl C y))
                t))
            (fun (z : C) => or_intror A (or_intror B z))
            s)).

(* 3. *)
Lemma or_imp :
  (A \/ B -> C) <-> (A -> C) /\ (B -> C).

Proof (conj
        (fun (f : A \/ B -> C) =>
          (conj (fun (x : A) => f (or_introl B x))
                (fun (y : B) => f (or_intror A y))))
        (fun (p : (A -> C) /\ (B -> C)) (s : A \/ B) =>
          or_ind (proj1 p) (proj2 p) s)).

(* 4. *)
Lemma not_not_em :
  ~~ (A \/ ~A).

Proof (fun (k : A \/ ~A -> False) =>
        k (or_intror A (fun (x : A) => k (or_introl (~A) x)))).