(* TP5 *)

Theorem toto: forall A:Prop, A -> A.
intros; assumption.
Defined.

Check toto.
Print toto.

Check (forall n:nat, True).

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

(* TP5 exercice 1 *)

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

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

Goal A -> B -> A.
Proof (fun a b => a).

Goal (A -> B -> C) -> (A -> B) -> A -> C.
Proof (fun f g a => f a (g a)).

(* TP5 exercice 2 *)

Goal A -> ~~A.
Proof (fun a b => b a). 

(* Goal ~~A -> A.
   Pas vrai en logique intuitionniste ! *) 
Goal (A -> B) -> (~B -> ~A).
Proof (fun (f:A->B) (g:B->False) (a:A) => g (f a)).

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


(* TP5 exercice 3 *)

Goal (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) (i:T)
   => f i (g i)).

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

Goal  (forall x, P x -> P (f x)) -> (forall x, P x -> P (f (f x))).
Proof (fun m i h => m (f i) (m i h)).

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


(* TP5 exercice 4 *)

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

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

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

Goal (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x).
Proof (conj
  (fun f => conj (fun x => proj1 (f x)) (fun x => proj2 (f x)))
  (fun f x => conj ((proj1 f) x) ((proj2 f) x))).


(* TP5 exercice 5 *)

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

Goal (A \/ B) \/ C -> A \/ (B \/ C).
Proof (fun x => or_ind
   (fun y:A\/B => or_ind
        (fun a => or_introl (B\/C) a)
        (fun b => or_intror A (or_introl C b))
        y)
   (fun c => or_intror A (or_intror B c))
    x).

Goal (A \/ B -> C) <-> (A -> C) /\ (B -> C).
Proof (conj
  (fun (x:A\/B->C) => conj (fun a => (x (or_introl B a)))
                           (fun b => (x (or_intror A b))))
  (fun (x:(A -> C) /\ (B -> C)) (y:A\/B) => or_ind 
       (fun a => (proj1 x) a)
       (fun b => (proj2 x) b)
       y)).

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