« if _ is _ then _ else » notation

Using Coq
1

Just out of curiosity:

Require Import ssreflect.
Definition foo a := if a is S _ then true else false.
Print foo.  (* foo = fun a : nat => match a with … *)

Import IfNotations.
Definition bar a := if a is S _ then true else false.
Print bar.  (* bar = fun a : nat => if a is … *)

Note the difference, foo is apparently parsed by ssreflect plugin and desugared to a match, but bar is just a notation and printed as-is.
So

  1. Why ssreflect does’t use a Notation?
  2. What is the motive for IfNotations? To be used in vanilla (non-ssreflect) coq?
2
  1. Why ssreflect does’t use a Notation ?

At the time Georges Gonthier introduced the if t is pat then u else v syntax, the generic notation mechanism was not powerful enough to support it (because of the presence of a pattern in the notation, a feature which was introduced in 8.8.0 only).

  1. What is the motive for IfNotations ? To be used in vanilla (non-ssreflect) coq?

I personally liked the idea of the notation if t is pat then u else v a lot and wished that it was made available for all users, what was done in the IfNotations module introduced in 8.8.0. There was a discussion on github about going further in unifying Georges’ non-reprinted version of if t is pat then u else v in ssreflect and the printing-enabled version made available thanks to the support of patterns in the generic notation mechanism but it did not converge. If you think the merge effort should be continued to avoid the duplication, don’t hesitate to tell (see the discussion started here for more about what remains to be done to do a complete merge; it is mixed with other long and technical discussions though).

By the way, there are two reasons to have the “vanilla” if is in a module. First because it introduces a new keyword is and that may break compatibility in rare occasions (e.g. in fun is : input_state => ...). Second, precisely because of an absence of convergence on the two implementations. Personally, I’d be happy in having if is available by default for everyone (without requiring any Require or Import).

2 Likes