The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 27 Jun 2011 13:33:14 +0200,
AUGER Cedric 
<Cedric.Auger AT lri.fr>
 a écrit :

I was wrong with my second definition, it should have been:

 Record item2 (current_restriction: A -> Prop): Type := {
  current_function2: forall x, (A*(current_restriction x))+unit;
  next_restriction2 :=
    fun x => exists H, current_function2 x = inl unit (a, H)
 }.

> Section Refinement2.
>  Variable A: Type.
>  Variable a: A.
> 
>  Record item2 (current_restriction: A -> Prop): Type := {
>   current_function2: forall x, A+(~current_restriction x);
>   next_restriction2 :=
>     fun x => current_function2 x = inl (~current_restriction x) a
>  }.
> 
>  CoInductive Refinement2: (A->Prop) -> Type :=
>  Next2: forall current_restriction (f: item2 current_restriction),
>         Refinement2 f.(next_restriction2 current_restriction) ->
>         Refinement2 current_restriction.
> End Refinement2.
> 
> The second variant may not be as convenient, but using it, you won't
> have to worry about the use of a proof_irrelevance axiom.
> 
> That is in the environment:
> 
> P: A -> Prop
> f_n: {x|P A} -> A
> x: A
> Hx1: P x
> Hx2: P x
> b: A
> Hb: f_n (ex_intro _ x Hx1) = b
> c: A
> Hc: f_n (ex_intro _ x Hx2) = c
> ===============================
> b = c
> 
> is not axiom free provable.
> 
> But in the second variant,
> P: A -> Prop
> f_n: forall x:A, A+(~P x)
> x: A
> Hx1: P x
> Hx2: P x
> b: A
> Hb: f_n x = left (~P x) b
> c: A
> Hc: f_n x = left (~P x) c
> ===============================
> b = c
> 
> is axiom free provable
>