Library hilbert.more_relations
Require Import Epsilon.
Section essai.
Variable U : Type.
Definition elagage (V:Type)(R S : V -> U -> Prop):Prop :=
(forall n y, S n y -> R n y) /\
(forall n p y, S n y -> S p y -> n = p) /\
(forall n y, R n y -> exists p, S p y).
Definition elaguer_mini (R: nat -> U -> Prop)(n:nat)(u:U):Prop :=
R n u /\ (forall p, R p u -> n <= p).
Require Import Classical.
Require Import Omega.
Require Import Arith.
Require Import Compare_dec.
Lemma L1 : forall R, elagage _ R (elaguer_mini R).
Proof.
repeat split.
destruct 1.
auto.
destruct 1.
destruct 1.
apply le_antisym;auto.
assert (forall (n : nat) (y : U), (exists q:nat, q<= n /\ R q y) ->
exists p : nat, elaguer_mini R p y).
induction n.
intros y (q,(H1,H2)).
exists 0.
split;auto with arith.
inversion H1.
subst q;auto.
intros y (q,(H1,H2)).
case (classic (exists r, r <= n /\ R r y)).
intro H';case (IHn y H').
intros;exists x;auto.
exists q.
split.
auto.
intros.
case (le_lt_dec q p).
auto.
intro.
case H.
exists p.
split;auto with arith.
omega.
intros.
eapply H with n.
exists n;auto with arith.
Qed.
Definition elagage_choisi (V:Type)(v:V)(R : V -> U -> Prop)(x:V)(y:U) : Prop
:= R x y /\ x = epsilon v (fun x' => R x' y).
Lemma L2 : forall (V:Type)(v:V)(R:V->U->Prop),
(elagage _ R (elagage_choisi _ v R)).
Proof.
repeat split.
destruct 1;auto.
destruct 1.
destruct 1.
subst p;auto.
intros; exists (epsilon v (fun x' => R x' y)).
split.
pattern (epsilon v (fun x' : V => R x' y)).
hilbert_e.
exists n;assumption.
trivial.
Qed.
End essai.