The Coq mailing list

[Tom Harke <harke AT cs.pdx.edu>]

Hi,

I'm new to Coq and a bit unclear on its limitations.

Suppose I have an infinite stream, and I'm looking for a special element
in it.  I don't know where it is, I only know that it definitely occurs.
In fact, I've got a Prop demonstrating its existence.

Is it possible to write a function in Set which will find this element?
I haven't been able to, and I can't tell whether I should be able to.

If I understand things correctly, the situation is this:
On one hand, since the logic is constructive, my Prop has a witness
which knows exactly which element it is.  On the other hand, this Prop
can't be used within the function, since it is erased when code
extraction happens.  But this Prop isn't being used directly,
it's only being used to prove termination.

Here's some concrete code:

== begin Coq ==
Require Import List.

Variable A:Set.
CoInductive Stream : Set := Seq : A -> Stream -> Stream . 
Definition head (s:Stream) := match s with Seq a s' => a  end.
Definition tail (s:Stream) := match s with Seq a s' => s' end.

CoInductive eqS : Stream -> Stream -> Prop :=
   eqst : forall s1 s2:Stream,
      head s1 = head s2 -> eqS (tail s1) (tail s2) -> eqS s1 s2.

Fixpoint nth (n:nat) (xs:Stream) {struct n} : A :=
   match n with
   | O   => head xs
   | S m => nth m (tail xs)
   end.

Fixpoint drop n (s:Stream) {struct n} : Stream :=
   match n with
   | O   => s
   | S m => drop m (tail s)
   end.

Definition Occurs (p:A -> Prop) (s:Stream) := exists j, p (nth j s).

Definition seek (p:A -> Prop) (s:Stream) (occ:Occurs p s):
   {  t:Stream
   |  p (head t)
   /\ exists n, eqS (drop n s) t
   }.
Abort.
== end Coq ==

It was not clear how to define seek so I was trying to use tactics.
But I couldn't figure out how to use the parameter/assumption occ.

I am also coding up the producer of the stream.  I had imagined it would
produce the proof of (Occurs p s) together with the stream s.
Instead I avoid the whole Prop thing by producing a triplet of objects:
the finite list preceeding the element; the special element itself; the
infinite tail.  But I'm curious if using Prop is possible, as it would
be more readable, more elegant, and efficient should I choose to extract
code.

Thanks for any advice or pointers you can provide!  (I've got access to
Coq'Art if there's anything relevant there)