Stream: Coq users

Topic: ✔ Conflicting notation & coercions weird interaction


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Meven Lennon-Bertrand (Apr 05 2023 at 09:40):

Paolo Giarrusso said:

since coercions aren't typechecked

You mean notations, right?

view this post on Zulip Paolo Giarrusso (Apr 05 2023 at 09:45):

thanks, fixed!

view this post on Zulip 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