Stream: Coq users

Topic: Notation with binder only in part of the right-hand side

Théo Winterhalter (Feb 24 2023 at 08:24):

Hello! I'm trying to define a notation with a binder that only should be bound in part of the right-hand side and I don't know how to do it. Here's a simple example where it fails:

From Coq Require Import Utf8.

Section Foo.

  Context (M : ∀ (A : Type) (B : A → Type), Type).

  Notation "∇ x , B" :=
    (∀ x, M _ B)
    (at level 200, x binder).

  Fail Check ∇ x, x = 0.

If I apply B to x explicitly in the notation it also complains.

Laurent Théry (Feb 24 2023 at 09:02):

you mean

 Notation "∇ x , B" :=
    (M _ (fun x => B))
    (at level 200, x binder).

?

Théo Winterhalter (Feb 24 2023 at 09:21):

I guess the problem is I want something weird. You made me realise, x in my notation is bound twice and what I want is:

Notation "∇ x , B" :=
  (∀ x, M _ (λ x, B))
  (at level 200, x binder).

and it seems to work. Thanks.

Théo Winterhalter (Feb 24 2023 at 09:27):

For some reason though, ∇ (x : nat), x = 0 is printed as ∇ x0, x0 = 0…
Also for ∇ x, x = 0 it doesn't infer the type of x is there any way to say the binders should have the same types?

Paolo Giarrusso (Feb 24 2023 at 12:17):

how's the first x possibly used before being shadowed? This prints without renaming:

  Notation "∇ x , B" :=
    (∀ _, M _ (λ x, B))
    (at level 200, x binder).

  Check ∇ x, x = 0.

Paolo Giarrusso (Feb 24 2023 at 12:25):

regarding shared types, it seems you can ask via named evars and refine, but type inference doesn't seem too happy.

This _might_ relate to the previous problem, but I thought the idea was maybe still worth sharing...

From Coq Require Import Utf8.

Section Foo.

  Context (M : ∀ (A : Type) (B : A → Type), Type).

  Notation "∇ x , B" :=
    (∀ x, M _ (λ x, B))
    (only printing, at level 200, x binder).
  Let x : Type.
    refine (∀ x : ?[T], M _ (λ x : ?T, x = 0)).
  Defined.
  Fail Notation "∇ x , B" :=
    (∀ x : ?T, M ?[T] (λ x, B))
    (only parsing, at level 200, x binder).

  Notation "∇ x , B" :=
    (* ltac:(refine (∀ x : ?[T], M _ (λ x : ?T, B))) *)
    ltac:(refine (∀ x : ?[T], M _ (λ x : ?T, x = 0)))
    (only parsing, at level 200, x binder).

  Fail Check (∇ x, x = 0).
(*
Error: In environment
M : ∀ A : Type, (A → Type) → Type
x := ∇ x0, x0 = 0 : Type
The term "0" has type "nat" while it is expected to have type "Type".
*)

EDIT: clarified snippet

Théo Winterhalter (Feb 24 2023 at 12:28):

Yeah, I guess what I wanted didn't make much sense, and that's reasonable that it's not properly supported.

Last updated: Oct 04 2023 at 23:01 UTC