Stream: Coq users

Topic: Using one recursive notation from another?


view this post on Zulip Ralf Jung (Dec 03 2021 at 17:24):

We have defined a recursive notation as shorthand for writing a telescope type:

Notation "'[tele' x .. z ]" :=
  (TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))
  (x binder, z binder, format "[tele  '[hv' x  ..  z ']' ]").
Notation "'[tele' ]" := (TeleO)
  (format "[tele ]").

However, when I try to use that notation to define another notation, that does not work:

Definition test {TT : tele} (t : TT  Prop) : Prop :=
  ∀.. x, t x  t x.
Notation "'[TEST'  x .. z ,  P ']'" :=
  (test (TT:=[tele x .. z])
        (tele_app  x, ..  z, P) ..)))
  (x binder, z binder).
(* Error: x should only be used in the recursive part of a pattern. *)

Instead I have to write

Notation "'[TEST'  x .. z ,  P ']'" :=
  (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
        (tele_app  x, ..  z, P) ..)))
  (x binder, z binder).

Is there any way to use the [tele...] notation to abbreviate the (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))?

view this post on Zulip Ralf Jung (Dec 03 2021 at 17:27):

Here is a self-contained example:

From Coq Require Import Utf8.
Set Default Proof Using "Type".

Local Set Universe Polymorphism.

(** Telescopes *)
Inductive tele : Type :=
  | TeleO : tele
  | TeleS {X} (binder : X  tele) : tele.

Arguments TeleS {_} _.

(** The telescope version of Coq's function type *)
Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
  match TT with
  | TeleO => T
  | TeleS b =>  x, tele_fun (b x) T
  end.

Notation "TT -t> A" :=
  (tele_fun TT A) (at level 99, A at level 200, right associativity).

(** A sigma-like type for an "element" of a telescope, i.e. the data it
  takes to get a [T] from a [TT -t> T]. *)
Inductive tele_arg : tele  Type :=
| TargO : tele_arg TeleO
(* the [x] is the only relevant data here *)
| TargS {X} {binder} (x : X) : tele_arg (binder x)  tele_arg (TeleS binder).

Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT  T :=
  λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T)  T :=
     match a in tele_arg TT return (TT -t> T)  T with
     | TargO => λ t : T, t
     | TargS x a => λ f, rec a (f x)
     end) TT a f.
Arguments tele_app {!_ _} _ !_ /.

Coercion tele_arg : tele >-> Sortclass.
Coercion tele_app : tele_fun >-> Funclass.

(** The actual testcase *)
Notation "'[tele' x .. z ]" :=
  (TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))
  (x binder, z binder, format "[tele  '[hv' x  ..  z ']' ]").
Notation "'[tele' ]" := (TeleO)
  (format "[tele ]").

Definition test {TT : tele} (t : TT  Prop) : Prop.
Admitted.
Notation "'[TEST'  x .. z ,  P ']'" :=
  (test (TT:=[tele x .. z])
        (tele_app  x, ..  z, P) ..)))
  (x binder, z binder).

view this post on Zulip Ralf Jung (Dec 04 2021 at 02:16):

Cc @Hugo Herbelin

view this post on Zulip Hugo Herbelin (Dec 04 2021 at 15:10):

Looks like #7911! It is actually simpler than what I thought first and I made #15291. :smile:

view this post on Zulip Ralf Jung (Dec 05 2021 at 16:03):

Oh I had totally forgotten that I had reported this exact issue (with the same example) already oops

view this post on Zulip Ralf Jung (Dec 05 2021 at 16:03):

Thanks for looking into it :)


Last updated: Feb 01 2023 at 13:03 UTC