Stream: Coq users

Topic: Wildcards in Inductive definition


view this post on Zulip spaceloop (Mar 18 2021 at 15:04):

Is there a way to specify that I don't care about some values of specific indices of an Inductive type? e.g. something along the lines of:

Inductive A (a : Type) : list a -> list a -> Type :=
  |  C : A (_ :: _) (_ :: _)

I am aware of Generalizable vernacular which saves me the explicit binding, but I still have to come up with (unique) variable names.

view this post on Zulip Enrico Tassi (Mar 18 2021 at 15:28):

No, but what you ask for is a bit risky. In the sense that the order of arguments may matter later on, if you get an heuristic chose for you... you may be surprised.

view this post on Zulip spaceloop (Mar 18 2021 at 16:52):

Do you mean the arguments of C? I don't understand the risk you mean, could you give an example of a heuristic? I am only really interested in relating two terms that have a similar shape, but can have arbitrary (different) subterms.

view this post on Zulip Paolo Giarrusso (Mar 18 2021 at 19:46):

@spaceloop are you asking for how to do it at all, or a shortcut?

view this post on Zulip Paolo Giarrusso (Mar 18 2021 at 19:47):

ah, the latter. Still, I think I see what Enrico means.

view this post on Zulip Paolo Giarrusso (Mar 18 2021 at 19:48):

the expansion could be C a as a’ as’ : A (a :: as) (a’ :: as’), or it could take the arguments in another order — especially if C must take extra arguments than don’t match the underscores you wrote?

view this post on Zulip Gaëtan Gilbert (Mar 18 2021 at 20:53):

the hole for the type (hidden by the :: notation) needs to be filled by a, not a fresh name
sounds like a complicated spec


Last updated: Feb 04 2023 at 21:02 UTC