Stream: Coq users

Topic: ✔ Automatically generated names from `inversion` tactic.


view this post on Zulip Olivier Laurent (Nov 28 2023 at 10:04):

I think this behavior of inversion is explained in the as or_and_intropattern part of the doc of theinversion tactic:

If an equation splits into several equations (because inversion applies injection on the equalities it generates), the corresponding intropattern should be in the form [ intropattern* ] (or the equivalent ( simple_intropattern )*,), with the number of entries equal to the number of subequalities obtained from splitting the original equation.

I use it with no particular trouble when I want to name generated hypotheses (which is always tedious anyway, as with induction for example).

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:12):

The very frustrating thing with inversion is the need to give a pattern for every constructor. When your inductive type has 16 constructors but only one or two are possible, this is nightmarish.

view this post on Zulip Quinn Flavel (Nov 28 2023 at 10:14):

Olivier Laurent said:

I think this behavior of inversion is explained in [...]

Aah, so that's it. Thanks — I missed that reading over the docs earlier.

view this post on Zulip Karl Palmskog (Nov 28 2023 at 10:16):

the HOL approach is to have separate "inversion lemmas" for each inductive type. Couldn't something like this be used in Coq to get reasonable naming?

view this post on Zulip Notification Bot (Nov 28 2023 at 10:16):

Quinn Flavel has marked this topic as resolved.

view this post on Zulip Notification Bot (Nov 28 2023 at 10:16):

Karl Palmskog has marked this topic as resolved.

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:26):

That's what I usually do :) That way you can also fine tune the form of the lemma, typically what counts as "input" and "output" index

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:27):

But it is rather tedious to set one such lemma by hand for each inductive type when it is such a core reasoning principle

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:27):

(A relevant thing to quote here is the Braga method, which makes an industrial use of these ideas)

view this post on Zulip Karl Palmskog (Nov 28 2023 at 10:31):

I guess you mean https://github.com/DmxLarchey/The-Braga-Method

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:32):

Yes, this is the one I meant

view this post on Zulip Théo Winterhalter (Nov 28 2023 at 10:32):

A related tactic is Equations's depelim which uses patterns and not intropatterns, meaning you actually get to pick names in a nice way without having to mention impossible cases.

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:37):

Also relevant (on how to defined inductive predicates to get the most out of them): https://proofassistants.stackexchange.com/questions/2136/inductive-vs-recursive-definitions/2147#2147

view this post on Zulip Paolo Giarrusso (Nov 28 2023 at 10:46):

@Karl Palmskog Gonthier advocates inversion lemmas too, and both math-comp and stdpp do that. But I agree with others, it's not reasonable for inversion on typing derivations

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:49):

Well, about that… https://github.com/CoqHott/logrel-coq/blob/6fa27fdbbc627d49d1a553801342cb75c8d8fa1e/theories/TypeConstructorsInj.v#L560

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:49):

And it is exactly the point where we want a fancy ad-hoc inversion

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:50):

(This is usually called an "inversion lemma", especially in the PTS literature)

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 10:50):

(If you meant typing derivations of an object language)

view this post on Zulip Paolo Giarrusso (Nov 28 2023 at 11:03):

I meant to agree with you — so s/unreasonable/tedious/ I guess. And that's indeed a neat phrasing, but the goal of this inversion/generation seems far from just inversion, since you're bundling together conversions (presumably, only those at the top?)

view this post on Zulip Gaëtan Gilbert (Nov 28 2023 at 11:04):

maybe we could have a inversion variant which leaves the results in the goal instead of as hypotheses (ie like injection does)

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 11:06):

What it morally does is "inversion on the last rule which is not conversion"

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 11:06):

Which is the reasonable inversion you want for dependently typed derivations

view this post on Zulip Meven Lennon-Bertrand (Nov 28 2023 at 11:07):

Because you almost always want to go back to this "last non-conversion rule" to obtain relevant information

view this post on Zulip Pierre Courtieu (Nov 28 2023 at 14:12):

Gaëtan Gilbert said:

maybe we could have a inversion variant which leaves the results in the goal instead of as hypotheses (ie like injection does)

That is one of the goals of https://github.com/Matafou/LibHyps. More generally you want to be able to apply tactics on "new" hyps: revert is a possibility, but something like (fun H => progress subst_using_H + revert) is often nicer.


Last updated: Jun 22 2024 at 16:02 UTC