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... *)
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.

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?

Paolo Giarrusso (Apr 05 2023 at 09:45):

thanks, fixed!

Last updated: Apr 20 2024 at 13:01 UTC