The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

Adam Chlipala writes:
 > Tom Harke wrote:
 > 
 > > 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.
 > 
 > My intuition is that this is impossible.  Since you aren't allowed to 
 > eliminate values of types in Prop to construct values of types in Set, I 
 > can't see how you could get any "information flow" from the existential 
 > witness to the return value of your function.  I don't know how to prove 
 > that it's impossible to write your function, though.

The situation is not so simple because the fixpoint rule allows to
define a function in Set with a decreasing argument in Prop. This is
used for well-founded recursion and can be used in that case as well.

The trick is to define exists j, p (nth j s) as an inductive relation

Inductive ok (p:A -> Prop) : Stream -> Prop := 
     ok_direct : forall s,p (head s) -> ok p s
   | ok_next : forall s, ok p (tail s) -> ok p s.

It is easy to prove the equivalence with your definition.

Then the following lemma is such that (ok_inv p s occ H) is a term
structurally smaller than occ

Lemma ok_inv : forall p s, ok p s ->~p (head s) ->  ok p (tail s).
destruct 1; intro; trivial.
case H0; auto.
Defined.

It is then possible to define your seek function by structural
induction over the proof of ok p s. 

Fixpoint seek (p:A -> Prop) (pdec : forall x, {p x}+{~p x})
                     (s:Stream) (occ:ok p s) {struct occ}: A := 
match pdec (head s) with 
               left _ => head s
           |   right H => seek p pdec (tail s) (ok_inv p s occ H)
       end.

You may have a look at Yves Bertot paper TLCA 95 on filters on
CoInductive Streams.

Best regards
Christine Paulin



 > 
 > > I'm new to Coq and a bit unclear on its limitations.
 > 
 > I wouldn't call this a limitation.  Especially if you turn on 
 > impredicativity of Set, you can ignore Prop altogether and not have this 
 > problem.  The reason to choose Prop versions of constructs in the first 
 > place is because you _want_ to prevent functions like yours from being 
 > written!
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  INRIA Futurs - PROVAL
        Parc club Orsay Université, Bat N, Zac des Vignes
        4, rue Jacques Monod, 91893 Orsay cedex
  &     LRI, Bat 490, UMR 8623 CNRS, 
        Université Paris Sud,  91405 Orsay Cedex 
  tel : (+33) (0)1 72 92 59 05         fax : (+33) (0)1 60 19 69 63