How does Coq know what to do with conflicting notation? In the following two modules it seems the behavior is different based on the presence of implicit coercions. See *BadNotation* with implicit coercion, always `==>`

gets picked instead of `¬`

.

However, in the *GoodNotation* module, somehow Coq knows to pick the right notation.

So I guess two questions

- How does it know to pick the right one in GoodNotation.
- How to force the same thing to happen in BadNotation?

```
(* With the coercion, Coq always picks the long form notation [==>]. Tried changing levels, the order, nothing... *)
Module BadNotation.
Context {S: Type}.
Notation SP := (S -> Prop).
Definition cast_Prop (P : Prop) : SP := (fun _ => P).
Coercion cast_Prop : Sortclass >-> Funclass.
Definition IMPL(p q: SP) : SP :=
fun s => p s -> q s.
Notation "'¬' p" := (IMPL p False) (at level 70).
Notation "p '==>' q" := (IMPL p q) (at level 74).
Definition sat(s: S)(p: SP): Prop :=
p s.
Notation "s |= p" := (sat s p) (at level 80).
Goal forall p q s, s |= ¬ p ==> q.
intros. (* Shows as [s |= (p ==> False) ==> q *)
Admitted.
End BadNotation.
(* Without the coercion, I can get conflicting notations to work (but no idea how!) *)
Module GoodNotation.
Context {S: Type}.
Notation SP := (S -> Prop).
Definition IMPL(p q: SP) : SP :=
fun s => p s -> q s.
Notation "'¬' p" := (IMPL p (fun _ => False)) (at level 70).
Notation "p '==>' q" := (IMPL p q) (at level 74).
Definition sat(s: S)(p: SP): Prop :=
p s.
Notation "s |= p" := (sat s p) (at level 80).
Goal forall p q s, s |= ¬ p ==> q.
intros. (* WORKS! *)
Admitted.
End GoodNotation.
```

with the coercion, the notation needs to be:

```
Notation "'¬' p" := (IMPL (cast_Prop p) (cast_Prop False)) (at level 70).
```

oh, or `Notation "'¬' p" := (IMPL p (cast_Prop False)) (at level 70).`

depending on the type you intend!

since notations aren't typechecked, Coq can't insert coercions automatically in their bodies. With `Notation "'¬' p" := (IMPL p False)`

, `¬ p`

expands to an ill-typed term `IMPL p False`

and Coq must fix that to `IMPL p (cast_Prop False)`

. Syntactically, that does _not_ match `IMPL p False`

, so the pretty-printer won't use `¬`

for it!

but using `p ==> cast_Prop False`

is fine — and as usual, the coercion is not printed by default

in your original example, `Set Printing Coercions`

indeed reveals the first goal as `s |= (p ==> cast_Prop False) ==> q`

.

Paolo Giarrusso said:

since coercions aren't typechecked

You mean *notations*, right?

thanks, fixed!

Last updated: Jun 25 2024 at 14:01 UTC