(* TP3 exercice 1 *)

Definition null (n:nat) := match n with O => True | S _ => False end.
Definition pred (n:nat) := match n with O => O | S p => p end.

Goal forall x y, S x = S y -> x = y.
intros.
change (pred (S x)=pred (S y)).
rewrite H; reflexivity.
Qed.


Goal forall x, S x <> 0.
intros; discriminate.
Qed.
 
Definition Even (n : nat) := exists p : nat, n = 2 * p.

Require Import Bool.

Fixpoint even (n : nat) : bool :=
  match n with
  | O => true
  | S p => negb (even p)          
  end.                           

Eval compute in even 2830.
Eval compute in even 5.

Lemma nat_ind2 :   forall P : nat -> Prop,
    P 0 -> P 1 ->
    (forall n : nat, P n -> P (S (S n))) ->
      forall n : nat, P n.
intros.
assert (P n /\ P (S n)).
induction n.
split; assumption.
destruct IHn.
split.
assumption.
apply H1; assumption.
destruct H2; assumption.
Qed.


Goal forall n, Even n <-> even n=true.
intros n; split.
intros (x, H).
rewrite H.
clear H; induction x.
reflexivity.
replace (2* S x) with (S (S (2*x))).
apply trans_eq with (negb (negb (even (2*x)))).
simpl; reflexivity.
rewrite IHx; reflexivity.
simpl.
rewrite plus_n_Sm; reflexivity.
apply nat_ind2 with (P:=fun n => even n = true -> Even n).
intros.
exists 0; reflexivity.
simpl; intros.
discriminate.
intros.
destruct H as (p,H1).
rewrite <- H0; simpl.
rewrite <- negb_involutive_reverse; reflexivity.
exists (S p).
rewrite H1.
simpl.
rewrite plus_n_Sm; reflexivity.
Qed.

(* TP3 exercice 2 *)

Parameter T : Set.
Definition EQ (x y : T) := forall P: T -> Prop, P x -> P y.


Lemma EQ_refl : forall x, EQ x x.
intros x P Px; assumption.
Qed.


Lemma EQ_trans : forall x y z, EQ x y -> EQ y z -> EQ x z.
intros x y z H1 H2 P H.
apply H2.
apply H1; assumption.
Qed.

Lemma EQ_sym : forall x y, EQ x y -> EQ y x.
intros x y; unfold EQ; intro Exy.
apply Exy.
intros P Px; assumption.
Qed.


Lemma EQ_eq_equiv : forall x y, EQ x y <-> x = y.
intros x y; unfold EQ; split.
intros H; apply H.
reflexivity.
intros H; rewrite H; intros; assumption.
Qed.

(* TP3 exercice 3 *)

Definition ET (A B : Prop) := forall X : Prop, (A -> B -> X) -> X.
Definition OU (A B : Prop) := forall X : Prop, (A -> X) -> (B -> X) -> X.

Lemma ET_intro :
  forall A B : Prop, A -> B -> ET A B.
intros; unfold ET.
intros X H1; apply H1; assumption.
Qed.

Lemma ET_elim1 :
  forall A B : Prop, ET A B -> A.
unfold ET; intros.
apply H.
intros; assumption.
Qed.

Lemma ET_elim2 :
  forall A B : Prop, ET A B -> B.
unfold ET; intros.
apply H.
intros; assumption.
Qed.

Lemma ET_and_equiv : forall A B : Prop, ET A B <-> A /\ B.
intros; unfold ET; split; intros.
split; apply H; intros; assumption.
destruct H; apply H0; assumption.
Qed.

Lemma OU_intro1 :
  forall A B : Prop, A -> OU A B.
unfold OU; intros.
apply H0; assumption.
Qed.

Lemma OU_intro2 :
  forall A B : Prop, B -> OU A B.
unfold OU; intros.
apply H1; assumption.
Qed.

Lemma OU_elim :
  forall A B C : Prop, (A -> C) -> (B -> C) -> OU A B -> C.
unfold OU; intros.
apply H1; assumption.
Qed.

Lemma OU_or_equiv :
  forall A B : Prop, OU A B <-> A \/ B.
unfold OU; split; intros.
apply H; intros.
left; assumption.
right; assumption.
case H; assumption.
Qed.

Definition BOT := forall X : Prop, X.

Lemma BOT_elim :
  forall A : Prop, BOT -> A.
intros; apply H.
Qed.


Lemma BOT_False_equiv : BOT <-> False.
split;intros.
apply H.
absurd False; auto.
Qed.

Definition TOP := forall X : Prop, X -> X.

Lemma TOP_intro :
  TOP.
unfold TOP; intros; assumption.
Qed.


Lemma TOP_True_equiv : TOP <-> True.
split; intros.
trivial.
apply TOP_intro.
Qed.


(* TP3 exercice 4 *)

Definition EX (P: T-> Prop) := forall (X: Prop), (forall (x:T), (P x -> X)) -> X.

Lemma EX_intro: forall (P:T -> Prop), forall x, P x -> EX P.
unfold EX; intros.
apply (H0 x); assumption.
Qed.

Lemma EX_elim :
  forall P : T -> Prop, forall A : Prop,
    (forall x : T, P x -> A) -> EX P -> A.
unfold EX; intros.
apply H0; assumption.
Qed.


Lemma EX_equiv :
  forall P : T -> Prop, EX P <-> exists x : T, P x.
intros; split; unfold EX; intros.
apply H.
intros x H1.
exists x; assumption.
destruct H.
apply (H0 x); assumption.
Qed.

(* TP3 exercice 5 *)

Parameter (o : T). 
Parameter (s : T -> T).

Definition N (x : T) :=
  forall P : T -> Prop, P o -> (forall y, P y -> P (s y)) -> P x.

Lemma No : N o.
unfold N; intros; assumption.
Qed.


Lemma Ns : forall x : T, N x -> N (s x).
unfold N; intros.
apply H1.
apply H; assumption.
Qed.

Lemma N_rec :
  forall A : T -> Prop,
    A o -> (forall x, N x -> A x -> A (s x)) -> forall x, N x -> A x.
intros.
assert (N x /\ A x).
apply H1.
split.
apply No.
apply H.
intros y (H2,H3).
split.
apply Ns; assumption.
apply H0; assumption.
destruct H2; assumption.
Qed.