search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.87k stars 653 forks source link

Warn when one notation makes another notation unreachable #15779

Open samuelgruetter opened 2 years ago

samuelgruetter commented 2 years ago

This might be really (too?) difficult to implement, but even if it ends as a wontfix, I thought it might be at least worth suggesting it: It would be useful if Coq warned when one notation makes another notation unreachable, like in the following example:

Axiom shl: nat -> nat -> nat.

Notation "a << b" := (shl a b) (at level 32).

Check (3 << 4).

Axiom index: list nat -> nat -> nat.

Notation "a << i >>" := (index a i) (at level 32).

Check (fun l: list nat => l << 3 >>).

Check (3 << 4). (* Error: Syntax error: '>>' expected after [term level 200] (in [term]). *)

The desired behavior would be that when defining (or even more importantly, when importing) the second notation, Coq warned that this shadows the first notation. Would that be possible?

Coq version: 8.15-rc1

ppedrot commented 2 years ago

I think that this is a plain undecidable problem from grammar theory. We may be able to implement an approximation but given how the grammar engine works that's not going to be easy...

silene commented 2 years ago

This might be really (too?) difficult to implement

No, it is trivial to implement, since Coq has to detect this conflict anyway during rule factorization. But for some reason, someone forcefully disabled the warning in 9847448b5f9dbf32806decf676f415d584a2cddb.

ppedrot commented 2 years ago

@silene this is incomplete, the factorization of camlp5 is just a heuristic.

silene commented 2 years ago

Sure, but it would fix the above test case, wouldn't it?

I think that this is a plain undecidable problem from grammar theory.

It is true that deciding the equality of context-free grammars is undecidable in general. But Coq's grammar, even with user notations, is not arbitrary at all. Otherwise, we would not be able to recognize it with Camlp5 in the first place. So, the undecidability argument does not really apply.

ejgallego commented 2 years ago

I don't recall the discussion, but I think we deemed it was not very important, but for sure now that we have finished the refactoring the warning can be enabled again.

ejgallego commented 2 years ago

That refactoring was really a PITA!