The Coq mailing list

[Frank Staals <f.staals AT student.tue.nl>]

On 2010-11-25 16:09, AUGER Cedric wrote:
> <snip>
> > CoFixpoint s : Stream A := x :: xs.
> ???
>
> That doesn't mean anything:
>
> I can assume that A is a Type, but
> AFAIK "::" is for lists (not Streams)
> I do not know what are x and xs (are they already been declared).
> What is the aim of defining a (co)fixpoint which is not involved in its
> definition?
Ah I'm sorry for not being clear enough. I'm working a lot with streams 
so I defined "::" as the Cons constructor using Coqs notation facilities:

Infix "::" := Cons (at level 60, right associativity) : richstream_scope.
Open Scope richstream_scope.

In the above definition 'x' and 'xs' can be arbitrary terms, possibly 
again depending on 's'. I simply wanted to name the head and the tail. 
The 'real' definitions can be any stream definition.

A nice example would be the following definition of the naturals. 
Unfortunately Coq cannot verify the guardedness of this definition.

CoFixpoint nats : Stream nat := 0 :: map S nats.

An other example is a definition of even. A function that takes a stream 
and retains only the elements on even indices.

CoFixpoint even(t: Stream A) : Stream A := hd t :: even (Str_nth_tl 2 t).

In both these examples the head (our term 'x') and the tail (our term 
'xs' ) can be some complicated term, possibly again depending on 's'. 
Hence we have a CoFixpoint. However, no matter what these terms look 
like the following two lemmas can be proven[1] (again using the 
generalized 's','x','xs' notation, and this time in the correct Coq 
syntax):

Lemma s_hd : hd s = x.
Lemma s_tl : tl s = xs.


[1] Note that in the case 's' is a function (like in the case with even) 
the lemma would become a bit more elaborate as the input variables would 
have to be universally quantified:

Lemma even_hd : forall t: Stream A, hd (even t) = hd t.

> I do not know if "Function" and "Program" can manage coinductive types,
> (if I well remember they require measure, so it shouldn't be the case);
> if not, maybe would it be a good idea to extend it for your purpouse.
From what I can see in the documentation both require some decreasing 
argument, which is unavailable in case of streams. I am affraid that 
extending them is out of the scope of my project.
> One last thing, you can use simply sigma types
>
> For instance:
>
> Record Cons_spec (A: Type) (x: A) (xs: Stream A): Type :=
> { s: Stream A;
>    s_hd: hd s = x;
>    s_tl: tl s = xs
> }.
>
> Definition ConsRich: forall A x xs, Cons_spec A x xs
>   := {|s := Cons x xs; s_hd := _; s_tl := _|}.
> Proof.
>   abstract prove_hd. (* since you tell you have such tactic *)
>   abstract prove_tl. (* since you tell you have such tactic *)
> Defined.
>
> Now you have the following:
> (ConsRich A x xs).(s_hd A x xs): hd (ConsRich A x xs).(s A x xs) = x
> and
> (ConsRich A x xs).(s_tl A x xs): tl (ConsRich A x xs).(s A x xs) = xs
This seems/seemed interesting. But I think this is no longer possible 
when 'x' and 'xs' are dependent on 's'. Or am I missing something.
> I hope I gave you some good idea(s)
> Regards
Thanks for your input.

Regards,

--

- Frank