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.

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?

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.

What do you mean?

Like in my `l : n <= 0`

example

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`

.

Alternatively you can just do it with all with two Prints

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 <= 0`

example

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.

Hmm, yeah, I probably could do with more practice with these.

@James Wood are you asking to generate the inversion principle for an arbitrary proposition, or just the one that `destruct`

or `inversion`

would "produce"?

The latter, I think, though I guess it complicates things that there are lots of different elimination tactics.

all I've seen is:

- just use the tactic and look at the result (and follow Meven's tips I guess?).
- in math-comp style, invest the time to state manual inversion lemmas.

Ah, okay, good to know. :+1:

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

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.

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.

Is the idea with these inversion lemmas to (possibly) shunt variables back into the goal and then `eapply`

them?

usually it's `destruct (inversion_lemma hyp) as intro_pattern`

, but I agree that `fin_S_inv`

looks more interesting

sorry, I haven't used those `fin`

s 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…

(I don't think you can paste that, best use the tactic)

@Meven Lennon-Bertrand aren't small inversions about making `inversion`

produce better proof terms?

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.

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.

re pattern matching, AFAICT, the only sensible UX I've seen is "the equations you wrote hold" — propositionally in Coq, definitionally in Agda

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!

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

we agree, I just associate "dependent pattern matching" with match expressions and computational content.

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

or at least that seems the difference when using the tactics?

but I guess we agree on the important points :-)

Last updated: Jun 23 2024 at 01:02 UTC