Stream: Coq users

Topic: Notation for a coinductive type


view this post on Zulip Julin S (Oct 02 2021 at 12:15):

Hi.
I was trying to make a notation that would let me create instances of an infinite list made as a CoInductive type.

CoInductive ilist {A : Type} : Type :=
| icons : A -> ilist -> ilist.

CoFixpoint foo := (icons 3 (icons 4 foo)).

(*
So I tried doing it along the lines of how it's done for lists where it's:

[Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.]

as mentioned at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html
 *)

Notation "[ x , y , .. , z , 'nil' ]" := (icons x
                                           (icons y ..
                                             (icons z) .. )).

(*
But this gave error:

    Cannot find where the recursive pattern starts.

 *)

How can this be fixed? Are notations possible for coinductive types in coq?

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 12:21):

@Ju-sh the (icons z) part seems off, no? It's not clear how to fix that, but I suspect you'd need to use cofix so that you have a name to use in place of nil

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 12:22):

(but I'm not sure of the exact syntax, https://coq.inria.fr/refman/language/core/coinductive.html#co-recursive-functions-cofix has the grammar but not an example of cofix)

view this post on Zulip Julin S (Oct 02 2021 at 13:10):

Thanks, a way to reference the original variable is what I needed. cofix gave a way for that.

So I did

Notation "[ x , y , .. , z , 'NIL' ]" := (cofix Foo : ilist :=
  icons x (icons y .. (icons z Foo) .. )).
(*(at level 70, no associativity). *)

Compute [ 1 , 2 , 3 , NIL ].

(* Gets error on the last closing square bracket:

    Syntax error: ',' or ',' 'NIL' ']' expected (in [term]).

*)

Any idea where I am going off course?

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 13:23):

okay, now we're back to the usual challenges of defining notations. To get started, it might be easier to not overload existing symbols like [ and ] — otherwise, you'll have to understand how your rule composes with the existing grammar.


Last updated: Jan 28 2023 at 07:30 UTC