The Coq mailing list

["Eelis van der Weegen" <coq-club AT contacts.eelis.net>]

harke AT cs.pdx.edu
 wrote:
> On Tue, Apr 22, 2008 at 09:00:17PM +0200, Eelis van der Weegen wrote:
> ]
> ] P.S. In the above, f is obviously a silly function. However, this is only 
> an
> ] isolated testcase; in my actual development I'm trying to define a monadic
> ] bind operation for Tree.
>
> How about:
>
> Fixpoint bind' (A B:Set) (k:A -> Tree B) (m:Tree A) : Tree B :=
>   match m with
>   | Leaf a => k a
>   | Node ts => Node _ (map (bind' _ _ k) ts)
>   end.
> Definition bind (A B:Set) m (k:A -> Tree B) := bind' A B k m.

That works perfectly, thanks!

This was actually what I had in my Haskell prototype that I was porting to
Coq. I didn't even try writing it in this form in Coq, though, since it seemed
obvious that it did not satisfy the principal argument decrease condition,
which I always thought was a strictly local syntactic check. I'm greatly
surprised (and pleased) to learn that the check can involve unfolding and
inspection of separate definitions (like map's). I must have overlooked the
bit in the manual that explains this. :-)  Coq also seems much more clever
w.r.t. nested fix's than I dared dream.

Thanks again.

Eelis