Stream: Coq users

Topic: notations

Jason Gross (Jun 06 2020 at 03:53):

Is there a way to get this to work without the parentheses? (cc @Hugo Herbelin )

Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn  'PRE'  [ ] P 'POST' [ ] Q" :=
  (((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
    (fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
    (fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. ))))
    (at level 200, x1 at level 0, x2t2 closed binder, xntn closed binder, P at level 100, Q at level 100).

Check WITH (x : nat) , (y : nat) , (z : unit) PRE [] (x, y, z) POST [] (z, y, x).

That is, I want

Check WITH x : nat , y : nat , z : unit PRE [] (x, y, z) POST [] (z, y, x).

to work. I can do

Notation "'WITH' x1 : t1 , x2t2 , .. , xntn  'PRE'  [ ] P 'POST' [ ] Q" :=
  (((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
    (fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
    (fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. ))))
    (at level 200, x1 at level 0, x2t2 closed binder, xntn closed binder, P at level 100, Q at level 100).

but I can't figure out a replacement for "closed binder" that removes the parentheses (I'm willing to have it be one that requires the : to always be present). If I remove closed, then I get the error message Error: as x2t2 is a non-closed binder, no such "," is allowed to occur. If I replace closed binder with at level 0, I get Anomaly "Inconsistent substitution of recursive notation." on the Check (reported at https://github.com/coq/coq/issues/12467). If I replace x1t1 with x1 : t1 and xntn with xn : tn, I get Cannot find where the recursive pattern starts.. Not sure what else to try here...

Hugo Herbelin (Jun 09 2020 at 21:27):

If we remove the restriction on closed binders (and allow it even in the presence of a ,), you'd be allowed to write things like Check WITH (x : nat) , y y' , (z : unit) PRE [] (x, y, z) POST [] (z, y, x). where y and y' are not separated by a ,. Is this what you'd really want?

I suspect that you'd like some unary binder incantation, which typically tells to allow any of x, x:T, x:=c, {x : T}, [x : T] as a binder. This is not implemented though...

Last updated: Oct 13 2024 at 01:02 UTC