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.