The Coq mailing list

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

Le Mon, 27 Jun 2011 11:14:09 +0200,
Andreas Abel 
<andreas.abel AT ifi.lmu.de>
 a écrit :

> Hello Vladimir,
> 
> does this serve your purpose?
> 
> Variable A : Type.
> Variable a : A.
> 
> CoInductive Stream (P : A -> Prop) : Type :=
>    cons : forall
>            (head : { x : A | P x } -> A)
>            (tail : Stream (fun x => forall (p : P x),
>                              head (exist (fun x => P x) x p) = a)),
>           Stream P.
> 
> Definition VS := Stream (fun x => True).
> 
> Cheers,
> Andreas
> 
> On 27.06.11 2:30 AM, Vladimir Voevodsky wrote:
> > Is there a way to define in Coq the type which can be informally
> > described as follows:
> >
> > 1. Given parameters A : Type , a : A .
> >
> > 2. I want to define the type of (infinite) sequences f_0 ,..., f_n,
> > .... where
> >
> > 2a. f_0 : A ->  A .
> >
> > 2b. f_{S n} : {| x : A ; f_n x = a |} ->  A .
> >
> > Is there a way to define the type of such sequences ?
> >
> 

Here are 2 variants of Andreas solution
 (the first one is just defining a separate type for the contents of
 a stream).

Section Refinement.
 Variable A: Type.
 Variable a: A.

 Record item (current_restriction: A -> Prop): Type := {
  current_function: forall x, current_restriction x -> A;
  next_restriction := fun x => exists h, current_function x h = a
 }.

 CoInductive Refinement: (A->Prop) -> Type :=
 Next: forall current_restriction (f: item current_restriction),
       Refinement f.(next_restriction current_restriction) ->
       Refinement current_restriction.
End Refinement.

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