Lemma id_proof : forall A : Prop, A -> A.
Proof.
intros A a; exact a.
Qed.

Print id_proof.

Check (forall n : nat, True).

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

(* Exercice 1 : Logique Minimale *)
Lemma imp_refl : A -> A.
Proof (fun (x : A) => x).

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

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

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 : négation *)


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

(* Lemma not_not_elim : ~~A -> A. : est-ce bien raisonnable? *)

Lemma contra : (A -> B) -> ~B -> ~A.
Proof (fun (x : A -> B) (y : B -> False) (z : A) => y (x z)).

Lemma weak_not_not_elim : ~~( ~~A -> A).
Proof
  (fun x : ~(~~A -> A) => 
    x (fun y : ~~A => False_ind A (y (fun z : A => (x (fun t : ~~A => z)))))).

(* Exercice 3 : quantification universelle *)
Lemma forall_distr : (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)).

Lemma forall_distr_gen :
  (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)).

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)).

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))).

(* Conjonction *)

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

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))).

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))))).

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))).

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


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)).

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)).


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