(* TP1 exercice 1 *)

Goal forall A B:Prop, A -> B -> A.
intros A B H1 H2; exact H1.
Qed.

Goal forall A B C : Prop, (A -> B ->  C) -> (A ->  B) -> A ->  C.
intros A B C H1 H2 H3.
apply H1;[idtac|apply H2];exact H3.
Qed.

Goal forall A B C : Prop, (B -> C) -> (A ->  B) -> A ->  C.
intros A B C H1 H2 H3.
apply H1.
apply H2; exact H3.
Qed.

Goal forall A B : Prop, A /\ B ->  B /\ A.
intros A B (H1,H2).
split; assumption.
Qed.

Goal forall A B : Prop, A \/ B ->  B \/ A.
intros A B [H1|H1].
right; assumption.
left; assumption.
Qed.

Goal forall A B C D : Prop, (A ->  C) /\ (B ->  D) -> A /\ B ->  C /\ D.
intros A B C D (H1,H2) (H3,H4).
split.
apply H1; exact H3.
apply H2; exact H4.
Qed.

Goal forall A : Prop,  A ->  ~ ~ A.
intros A H1 H2.
apply H2; exact H1.
Qed.

Goal forall A B : Prop, (A \/ ~ B) /\ B ->  A.
intros A B (H1,H2).
case H1; intros H3.
exact H3.
absurd B; assumption.
Qed.

Goal forall (X:Set) (A B: X -> Prop), (forall x: X, A x /\ B x) 
    <-> (forall x:X, A x) /\ (forall x:X, B x).
intros X A B; split.
intros H; split; intros x; destruct (H x); assumption.
intros (H1,H2) x; split;[apply H1|apply H2].
Qed.


(* TP1 exercice 2 *)
(* on pourrait avoir des propriétés Set->Prop "être écossais", mais il est plus
 * facile de ne considérer que des Prop correspondant à la personne "écossaise" 
 * E = écossais, R = a des chaussette rouges, K = porte un kilt
 *  M = être marié, D = sortir le dimanche *)

(* Ceci est une preuve intuitionniste qui ne nécessite pas le tiers exclus *)

Goal forall E R K M D:Prop,
  (~E -> R) ->
  (K \/ ~R) ->
  (M -> ~D) ->
  (D <-> E) ->
  (K -> E /\M) ->
  (E -> K) ->
   False.
(* la preuve peut être résolue immédiatement par la tactique intuition *)
intros E R K M D H1 H2 H3 (H4,H5) H6 H7.
(* à la main, l'idée est de se rendre compte que D=E=K, ce qui simplifie bien *)
(* on commence par prouver que K -> False *)
assert (~K).
intros H8.
apply H3.
apply H6; exact H8.
apply H5; apply H6; exact H8.
(* on n'a plus qu'à couper le ou et montrer l'absurde dans les 2 cas *)
case H2.
exact H.
intros H8.
apply H8.
apply H1; intros H9.
apply H.
apply H7; exact H9.
Qed.