James Wood (Mar 28 2022 at 12:58): 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.
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.
Paolo Giarrusso (Mar 28 2022 at 20:39):(but I guess you know the last bit)
Paolo Giarrusso (Mar 28 2022 at 20:42):Haven't used it myself but maybe Elpi could be nicer? We use it for metaprogramming
James Wood (Mar 28 2022 at 22:04):Thanks for the hints! I'll try them out tomorrow.
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).
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: Oct 03 2023 at 20:01 UTC