The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 6 Jun 2012 18:17:51 -0400,
Thomas Braibant 
<thomas.braibant AT gmail.com>
 a écrit :

> Hi,
> 
> I have some trouble using recursive notations in Coq 8.4 beta
> 
> The following snippet comes from the documentation and works
> perfectly well
> 
> Notation "’mylet’ f x .. y :=  t ’in’ u":=
>    (let f := fun x => .. (fun y => t) .. in u)
>    (x closed binder, y closed binder, at level 200, right
> associativity).
> 
> Now, the following works perfectly well:
> 
> Notation "'FUN' x => B" := (fun x => B) (at level 0).
> Notation "’mylet’ f x .. y :=  t ’in’ u":=
> (let f := FUN x => .. (FUN y => t) .. in u)
>       (x closed binder, y closed binder, at level 200, right
> associativity).
> 
> But, if the definition of FUN is more complicated, I cannot define the
> notation "mylet" anymore, and get the error message
> 
> Notation "'FUN' x => B" := (fun n R x => B n R).
> Notation "’mylet’ f x .. y :=  t ’in’ u":=
> (let f := FUN x => .. (FUN y => t) .. in u)
>       (x closed binder, y closed binder, at level 200, right
> associativity).
> 
> Toplevel input, characters 70-88:
> Error: Cannot find where the recursive pattern starts.

If you need a solution, I guess this does what you want (I unfolded
your FUN, and then β reduced it).

Notation "’mylet’ f x .. y :=  t ’in’ u":=
(let f := (fun n R => fun x => (.. (fun y => t n R) ..)) in u)
      (x closed binder, y closed binder, at level 200, right
      associativity).

I guess addition of binders confuse Coq.

> 
> From this I infer that (rightfully), the notation FUN is unfolded in
> the definition of mylet, and that it is indeed more complicated to
> find where this recursive pattern starts. Looking at the
> documentation, I would like to be able to define _exactly_ what are
> the recursive pattern, and the terminating expression. But I cannot
> find how to do it, nor to find encodings of my original problem such
> that the notation is accepted... Any ideas?
> 
> With best regards,
> Thomas