On Tue, Sep 30, 2008 at 4:37 AM, Robin Green <[EMAIL PROTECTED]> wrote: > On Tue, 30 Sep 2008 03:27:09 -0600 > "Luke Palmer" <[EMAIL PROTECTED]> wrote: > >> But I *want* to do something like that with Coq (I prefer it to Agda >> for little more than personal taste). In particular, I'd like to see >> a reasoning framework for partial functions, so you could state and >> prove a property like: >> >> length [1..] = _|_ > > Bear in mind, in Coq, the equivalent of [1..] is a stream, whereas the > equivalent of [1,2,3] is a list.
You miss my point. Every value here is lifted to its domain before being reasoned about. So eg. [1,1..] is not the coinductive x = 1:x. Instead we model this example like so (this is my current direction, nothing tested or fully reasoned out, so I may be full of beans): [1..] is the limit [_|_, 1:_|_, 1:2:_|_, ...] length [1..] is the limit [_|_, _|_, _|_, ...] Every function we can write in Haskell is corecursive on this representation, because every such function is Scott-continuous. To prove the above property would amount to proving that every element of the resulting limit is _|_, so the whole limit is _|_. Luke _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
