Removing the _CoqProject compile option -notation-incompatible-prefix

[DmxLarchey]

Solved Warning issues related to the -notation-incompatible-prefix compile option:

1. in FOL/TRAKHTENBROT/*, replaced (object level) FOL quantifier ∀₁/∃₁, instead of ∀/∃ which was obviously in conflict with Coq (meta) level quantifiers;
2. in membership.v, changed notations for pairs, orderedpairs etc, changing ≋ to ≅;
3. in ILL/*, change priority for £ letting Coq decide for itself, avoiding warning about wrong level;
4. in MuRec removed the (globally defined) notation [ f ; v ] ▹ x for ra_bs f v x, ie big step semantics for recalg, because of incompatibilities with ListNotations. Notice that the notation is kept ONLY (locally) for the definition of ra_bs to make it more readable.

As far I as checked, there are no remaining warnings.

[mrhaandi]

Btw, what about -notation-overridden? (Most of it comes from ILL.)

[Edit: DmxLarchey] Sorry I made a mess editing your comment instead of commenting it ...

[DmxLarchey]

Btw, what about -notation-overridden? (Most of it comes from ILL.)

There is some from ILL for sure, but not only there.

What is wrong with "overriding" notations? For instance £ _ is used as notation for the constructor of atoms in several logics, incl. ILL CLL EILL, but also FOL etc. Sometimes for terms, sometimes for propositions. Possibly we could localize it more to avoid overriding but I don't think it would be a good thing to invent a different notation for each of those use cases.

Hence you have to look in the context to understand what £ _ means, irrelevant of whether it was overridden or just given a different definition compared to its use at other locations in the code.

[DmxLarchey]

@mrhaandi Btw thinking a bit more about it, I find it bizarre to push for having NOT -notation-overridden as a default compile option, ie to check for overridden notations by default. I do not know who makes such decisions.

While I understand why such an option exists, Coq itself uses overridden or ambiguous notations all over the place. For instance:

1. [ ... ] are used with at least 3 different meanings:
   • intros [ H1 H2 ]
   • the list [0;1]
   • rewrite [LHS]equation
2. the case of _ is worse. It can be used with at least 3 different but related meanings as, in the following script:

Goal forall (X : Type) (P : X -> Prop) x, P x -> False.
Proof.
  intros X P.
  Fail intros _ H.       (* introduce then discards. Fails if dependencies prevents discarding *)
  refine (fun _ H => _). (* introduce w/o specifying a name, hence same as intros ? H. *)
  Check (exist _ _ H).   (* let unification fill the gaps *)
Admitted.

Hence I think we should not accept w/o criticism every new warning that pops up just become some developer had a new idea of what "ideal code" should be.

[mrhaandi]

Possibly we could localize it more to avoid overriding but I don't think it would be a good thing to invent a different notation for each of those use cases.

I agree that it is a bad idea to have to invent alternatives to £ _ for each individual logic.
For modularity, notations chosen by individual problems should not be dictated by some existing notations in the library.
The warning probably means that some notations which are not needed for the problem are not opt-in, or incorrectly scoped.

I also agree that [ ... ] Notations from the Coq stdlib are all over the place. This is somewhat mitigated by ListNotations.

My main motivation to have warning-free code that it does avoid some pitfalls when composing reductions.
In the past I wasn't even able to use ssreflect in some code due to notations which I did not care about, but was not able to suppress.