Hoare triple notation

Question

The recent discussion of set notations re-motivates me to ask if anybody (Tej?) has a clever idea for getting Coq to accept a standard notation for Hoare triples -- something like this:

Notation "{ P }  c  { Q }" :=
  (hoare_triple P c Q) 
  (at level 0, P at level 99, c at level 99, Q at level 99) 
  : Hoare_scope.

Coq's error is "Error: A notation must include at least one symbol." Which I don't understand in light of the fact that

Notation "{ x }" := (x) (at level 0, x at level 99).

does work.

Any advice?

Answer 1

I'd recommend using another symbol somewhere to make this parseable. I've seen Adam Chlipala use Notation "{{ P }} c {{ Q }}" for example. You can also define { P } c { Q } as a printing-only notation, although I imagine that's less useful and potentially confusing to new users.

Curly braces are special; some of the ways they're special are documented in the manual (scroll down to the third note), but I confess I don't really understand that note beyond "here be dragons, ask Hugo Herbelin".

I can tell you mechanically why you're getting the error while "{ x }" works:

• curly braces don't count as symbols, because of a special remove_curly_brackets function
• if the notation is already in the parsing table, it doesn't need to include new symbols

This is checked in metasyntax.ml, which I found by looking for how the error message is thrown. You can also confirm what the Coq grammar is using Print Grammar constr (this is also how you figure out what level everything actually is).