Stream: Coq users

Topic: Repeated destruction


view this post on Zulip James Wood (Mar 28 2022 at 12:58):

What's a better (more generalisable and robust) way of writing view in the following? I'd like to be able to deal with arbitrary-ary choices of constructors and preferably constructors with an arbitrary number of arguments.

Variable A B C D : Type.

Variant View : (A + (Empty_set + B)) + (C + D) -> Type :=
| view0 : forall x, View (inl (inl x))
| view1 : forall x, View (inl (inr (inr x)))
| view2 : forall x, View (inr (inl x))
| view3 : forall x, View (inr (inr x)).

Lemma view x : View x.
Proof.
  repeat destruct x as [x|x]; try econstructor; destruct x.
Defined.

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 20:37):

you can use match goal, and match hypotheses by type, to find what to destruct. For construction I’d recommend eauto + Local Hint Constructors (with a separate hint db). But doing any of this in Defined is… somewhat dangerous.

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 20:39):

(but I guess you know the last bit)

view this post on Zulip Paolo Giarrusso (Mar 28 2022 at 20:42):

Haven't used it myself but maybe Elpi could be nicer? We use it for metaprogramming

view this post on Zulip James Wood (Mar 28 2022 at 22:04):

Thanks for the hints! I'll try them out tomorrow.

view this post on Zulip James Wood (Mar 29 2022 at 08:43):

Maybe if I'm doing more than a one-liner, I can do something better and more general. What sort of information can I get about types, in Elpi or otherwise? For example, I'd like to be able to tell whether a given type normalises to a Variant or Record, and not an Inductive (to avoid infinitely destructing nats, for example).

view this post on Zulip Enrico Tassi (Mar 29 2022 at 08:55):

Under the disclaimer that I don't get exactly what you are trying to do ;-) all the info about Elpi is on its website, including tutorials.
The APIs you way use are probably these and that one where you can query if an inductive is a recursive type and all its info.
You also have APIs for reducing a term, or typing it.


Last updated: Jan 28 2023 at 06:30 UTC