James Wood (Mar 16 2022 at 13:28): James Wood (Mar 16 2022 at 13:28):Is there a command I can use in proof mode, akin to About or Print, which can tell me, about a variable, what would happen if I eliminated it? For example, if I had a variable n : nat in scope, it would print out that it could be of the form O or the form S n' for n' : nat; and if I had a variable l : n <= 0, maybe it would show me that it could only be le_n n (or le_S n m l if S m = 0). I tend to find that just doing the elimination is not particularly helpful, because the relevant information is hidden behind multiple subgoals and potentially somewhere in the middle of a large context.
Meven Lennon-Bertrand (Mar 16 2022 at 13:30):If you Print the type of the variable (for instance Print nat or Print le), you can see the whole inductive type definition, including all its constructors. This seems to correspond with the information you are looking for?
James Wood (Mar 16 2022 at 13:32):Yeah, I guess that's the best thing I've found so far. It'd be nice if it could interpret indices a bit, though.
Meven Lennon-Bertrand (Mar 16 2022 at 13:33):What do you mean?
James Wood (Mar 16 2022 at 13:33):Like in my l : n <= 0 example
Ali Caglayan (Mar 16 2022 at 13:41):So your asking if you can get the constructors of a variable of an inductive type? I think the best thing to do would be Check l which would tell you the type and if it is inductive Print T.
Ali Caglayan (Mar 16 2022 at 13:42):Alternatively you can just do it with all with two Prints
James Wood (Mar 16 2022 at 13:43):Like, in simple examples like this one, it's easy enough to do the elimination and be pleased that there's only one subgoal, with n unified with 0, but in bigger examples the cases can be harder to work out, and what unifications will happen can get difficult to track (from a human perspective).
Require Import Coq.Program.Equality.
Lemma foo n (l : n <= 0) : n = 0.
Proof.
dependent destruction l.
- reflexivity.
Qed.
James Wood said:
Like in my
l : n <= 0example
Mmmmm I do not think you can do that… But what I often do in such situations is to focus on a specific goal using 3:{ (or another integer) to see how things look like there before going on. And I definitely do not take care of the goals in the order in which they appear, but rather use that focusing feature to work on the one that is the hardest/most dubious first to get an idea of what happens there.
James Wood (Mar 16 2022 at 13:47):Hmm, yeah, I probably could do with more practice with these.
Paolo Giarrusso (Mar 16 2022 at 14:28):@James Wood are you asking to generate the inversion principle for an arbitrary proposition, or just the one that destruct or inversion would "produce"?
James Wood (Mar 16 2022 at 14:30):The latter, I think, though I guess it complicates things that there are lots of different elimination tactics.
Paolo Giarrusso (Mar 16 2022 at 14:30):all I've seen is:
James Wood (Mar 16 2022 at 14:31):Ah, okay, good to know. :+1:
Paolo Giarrusso (Mar 16 2022 at 14:33):some examples:
https://gitlab.mpi-sws.org/iris/stdpp/-/blob/17d496753c8573d036e7f2b99792d7e5fcbe961c/theories/fin.v#L47-56
https://gitlab.mpi-sws.org/iris/stdpp/-/blob/17d496753c8573d036e7f2b99792d7e5fcbe961c/theories/telescopes.v#L57-66
Paolo Giarrusso (Mar 16 2022 at 14:34):of course that's somewhat time-consuming. And in part, it's needed because inversion Hfoo as [a b c|...] is very annoying to use.
Paolo Giarrusso (Mar 16 2022 at 14:35):OTOH, proving lemmas with nice statements sometimes needs nontrivial proofs — you must pick the right inversion tactic, maybe call subst, ... so having the lemmas can be nice if you use them enough.
James Wood (Mar 16 2022 at 14:36):Is the idea with these inversion lemmas to (possibly) shunt variables back into the goal and then eapply them?
Paolo Giarrusso (Mar 16 2022 at 14:46):usually it's destruct (inversion_lemma hyp) as intro_pattern, but I agree that fin_S_inv looks more interesting
Paolo Giarrusso (Mar 16 2022 at 14:48):sorry, I haven't used those fins up close (I've written sigma types instead for the job); they're interesting enough there's a special inv_fin tactic — which indeed works somewhat as you suggest and has snippets like
revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
Re: inversion, there’s a somewhat generic setting provided by small inversion. AFAIK Equations has some bits of it, although it’s not exactly as nice as proving exactly the "right" thing by hand. And there has been plans to ship (some of) this with the compilation of Coq’s pattern-matching directly, so a to provide a nicer entry point for e.g. inversion, but it’s been in the making for a long time…
Paolo Giarrusso (Mar 16 2022 at 14:48):(I don't think you can paste that, best use the tactic)
Paolo Giarrusso (Mar 16 2022 at 14:49):@Meven Lennon-Bertrand aren't small inversions about making inversion produce better proof terms?
Paolo Giarrusso (Mar 16 2022 at 14:50):And there has been plans to ship (some of) this with the compilation of Coq’s pattern-matching directly
would you want to do that without Equations? Nobody should look at the proof terms output by a pattern-matching compiler, so I think you need all the extra infrastructure to hide them.
Meven Lennon-Bertrand (Mar 16 2022 at 14:51):It is, but I think it gives a good generic setting for all those inductive types where indices are nice enough (typically, those where pattern-matching on the indices tells you which constructors are applicable), one where you could automate generation of the nice inversion lemmas such as the one you gave.
Paolo Giarrusso (Mar 16 2022 at 14:52):re pattern matching, AFAICT, the only sensible UX I've seen is "the equations you wrote hold" — propositionally in Coq, definitionally in Agda
Meven Lennon-Bertrand (Mar 16 2022 at 14:52):Paolo Giarrusso said:
would you want to do that without Equations? Nobody should look at the proof terms output by a pattern-matching compiler, so I think you need all the extra infrastructure to hide them.
If the pattern-matching compilation is good, then inversion can just rely on it when you are doing proofs. But I agree you never want to look at that compiled pattern-matching!
Meven Lennon-Bertrand (Mar 16 2022 at 14:54):Paolo Giarrusso said:
re pattern matching, AFAICT, the only sensible UX I've seen is "the equations you wrote hold" — propositionally in Coq, definitionally in Agda
If you care about computational content, for sure. But if you only care about the proof, having inversion which gives you the nice goal you expect, lets you use intro-patterns in a reasonable way, and so on is a slightly different issue
Paolo Giarrusso (Mar 16 2022 at 14:55):we agree, I just associate "dependent pattern matching" with match expressions and computational content.
Paolo Giarrusso (Mar 16 2022 at 14:55):as a technicality, dependent elimination is a bit stronger than inversion AFAICT — inversion only learns info about the indices, only elimination learns info about the actual witness
Paolo Giarrusso (Mar 16 2022 at 14:56):or at least that seems the difference when using the tactics?
Paolo Giarrusso (Mar 16 2022 at 14:57):but I guess we agree on the important points :-)
Last updated: Feb 04 2023 at 22:29 UTC