The Coq mailing list

[roconnor AT theorem.ca]

In the Streams library, the inductive type Exists is defined as:

Variable P : Stream -> Prop.

Inductive Exists  ( x: Stream ) : Prop :=
  | Here : P x -> Exists x
  | Further : Exists (tl x) -> Exists x.

Suppose that one as an (opaque) theorem (forall x, P x -> Q x) and one 
wants to create a function f : (Exists P x) -> (Exists Q x).  Such a 
function would necessarily be O(n) because the types of each Further 
constructor must be modified to change the P to a Q.

Suppose Exists had instead been defined as

Definition Exists' (x:Stream) : Prop := exists n:nat, P (Str_nth_tl n x).

The the function f : (Exists' P x) -> (Exists' Q x) could easily be 
defined as O(1).

Is this correct, or is there some way defining f using the orginal 
definition that can be done on O(1) time?

(BTW, I require the f be transpartent because I want to use the
(Exists Q x) as a witness of termination for another function.  This 
witness must be transpartent so that computation can proceed inside Coq.)

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''