## Stream: Coq users

### Topic: ✔ Conflicting notation & coercions weird interaction

#### Lef Ioannidis (Apr 05 2023 at 01:09):

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

1. How does it know to pick the right one in GoodNotation.
2. 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... *)
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 *)

(* 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! *)
End GoodNotation.
``````

#### Paolo Giarrusso (Apr 05 2023 at 09:32):

with the coercion, the notation needs to be:

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

#### Paolo Giarrusso (Apr 05 2023 at 09:35):

oh, or `Notation "'¬' p" := (IMPL p (cast_Prop False)) (at level 70).` depending on the type you intend!

#### Paolo Giarrusso (Apr 05 2023 at 09:37):

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!

#### Paolo Giarrusso (Apr 05 2023 at 09:38):

but using `p ==> cast_Prop False` is fine — and as usual, the coercion is not printed by default

#### Paolo Giarrusso (Apr 05 2023 at 09:38):

in your original example, `Set Printing Coercions` indeed reveals the first goal as `s |= (p ==> cast_Prop False) ==> q`.

#### Meven Lennon-Bertrand (Apr 05 2023 at 09:40):

Paolo Giarrusso said:

since coercions aren't typechecked

You mean notations, right?

thanks, fixed!

#### Notification Bot (Apr 05 2023 at 19:56):

Lef Ioannidis has marked this topic as resolved.

Last updated: Jun 16 2024 at 01:42 UTC