There are cases where `inversion`

/`induction`

work but `case`

/`elim`

does not work (or they produce a huge mess). For instance when dealing with inductively defined propositions.

What will be the mathcomp way of dealing with that?

An example will be:

```
(* propositional version of \in this one does not require eqTypev*)
Inductive PIn {A}: A -> seq A -> Prop :=
| pin_here (a : A) l : PIn a (a::l)
| pin_future (a b : A) l : PIn a l -> PIn a (b::l).
Lemma PIn_in (A: eqType): forall (a: A) (l: seq A), PIn a l <-> a \in l.
Proof.
split.
move => HPIn.
induction HPIn as [a l| a b l HInd]. (* replacing induction with elim does not work as well *)
by apply: mem_head.
rewrite in_cons.
apply/orP.
by right.
move: a.
have ? := pin_here.
elim : l => [|a' l Hind] //= a /[!in_cons].
move /orP => [|a_in_l].
by move /eqP => ->.
apply: pin_future.
by apply: Hind.
Qed.
```

There's a way of automatically obtaining inversion lemmas that you can then use with `elim`

: https://stackoverflow.com/questions/69210037/ssreflect-inversion-i-need-two-equations-instead-of-one/69211639#69211639

Why do you say `elim`

doesn't work well here, though?

The main difference I see is that `elim`

doesn't use `a`

and `l`

; it instead invents new ones. So you can actually `elim: HPIn => {a l}`

and it will amount to the same.

I agree that `elim`

fails at this when it's needed (unless there's something I don't know about it). I've been using `dependent induction`

in cases where the information about the terms that appear in the inductive predicate is really important.

That tactic might use axiom K unnecessarily (tho often that's not a problem); I prefer the variant tactic from the coq-equations package (that you can use on standard definitions just fine).

I should say there is an ssreflect alternative using `elim`

case directly, but I consider that (intentionally) cumbersome; generated inversion lemmas and dependent induction are probably superior. Examples:

https://sympa.inria.fr/sympa/arc/ssreflect/2014-10/msg00006.html, https://sympa.inria.fr/sympa/arc/ssreflect/2010-04/msg00001.html and https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#type-families

For relatively simple cases you can do the manual type family elimination as described above, for more complicated stuff it's typically better to reformulate the whole thing via `Equations`

plugin.

Clarifying what is meant by type family elimination (because it took me a good while to parse given the above examples and the refman) (let me know if this understanding is wrong): if you want to do case analysis or induction on something which is not naturally on the top of your stack, you can do it with the `case: ... / ...`

syntax.

So, for example, walker wanted to do induction on `PIn a l`

, but even though we can place it on top of the stack, this is not natural since `a`

and `l`

have already been introduced. Thus, if the goal is `PIn a l -> a \in l`

, we can `elim: a l /`

, which will do induction on the top of the stack (`PIn a l`

) but only after generalizing `a`

and `l`

. Alternatively, if we introduce `PIn a l`

first with `move=> HPIn`

, we would use `elim: a l / HPIn`

instead.

First, I should have said upfront that I struggle with the manual as well. Second, I suspect this only applies to _indexes_ and not _parameters_, which is why induction on (xs : list A) needn't mention A.

And the reason we must treat indexes specially is because case analysis on `PIn a l`

can teach us constraints on `a`

and `l`

.

As a follow-up question (and I can try in a bit): here a is an index that could be turned into a parameter. Does ssreflect realize that automatically, and let you use `elim: l / HPin`

, or not? I think my doubt is because Agda here would automatically turn `a`

into a parameter (IIRC), but usually Coq doesn't (also because that would affect generated induction principles, a problem that in Agda doesn't show up).

What is the difference between indexes and parameters?

Paolo Giarrusso said:

As a follow-up question (and I can try in a bit): here a is an index that could be turned into a parameter. Does ssreflect realize that automatically, and let you use

`elim: l / HPin`

, or not?

It lets you do so, no problem. But it also lets you do `elim: HPIn`

directly, so perhaps that doesn't provide the information you were looking for.

Ana de Almeida Borges said:

What is the difference between indexes and parameters?

Indices change in constructors and parameters don't, e.g. here `A`

is a parameter, while the `nat`

is an index:

```
Inductive vect (A : Type) : nat -> Type :=
| nil : vect A 0
| cons n : forall x : A, vect A n -> vect A n.+1.
```

Paolo Giarrusso said:

First, I should have said upfront that I struggle with the manual as well. Second, I suspect this only applies to _indexes_ and not _parameters_, which is why induction on (xs : list A) needn't mention A.

Yes, the "dependent elimination switches" that come before `\`

are for indexes. I think the doc uses the maybe oldish terminology that considers a family of types being indexes on something, eg `vect A`

is a family, not a type, since you need to pass a `nat`

to it. I never liked this terminology (to me `list`

is a family as well), so I'm all for improving the doc.

About inversion, if your data type a few cases I'd say the best is to write an inversion lemma by hand. Otherwise my hope was to synthesize a pedantic one automatically, but I never finished, and it is not documented. Here the inversion and here the view lemma. I'm posting this just in case someone brave wants to pick this up. The idea was to generate an inductive with no index but equations, and then prove a view mapping one in the other. Eliminating (trivially) the non-indexed one is easier, e.g. you get the equations without a fancy generalization, and you can control the substitution with rewrite.

Hello @walker , what is the"huge mess" with `elim`

in this example?

```
From mathcomp Require Import all_ssreflect.
Inductive PIn {A}: A -> seq A -> Prop :=
| pin_here (a : A) l : PIn a (a::l)
| pin_future (a b : A) l : PIn a l -> PIn a (b::l).
Lemma PIn_in (A: eqType): forall (a: A) (l: seq A), PIn a l <-> a \in l.
Proof.
split.
- elim => {a l} [a l |a b l aPInl ainl]; first by rewrite inE eqxx.
by rewrite inE ainl orbT.
- elim: l a => // a l ihl b.
rewrite inE; case/orP; first by move/eqP->; constructor.
by move/ihl => {}ihl; constructor.
Qed.
```

Well this works, my problem in this case was the duplicate variables, I will let you know once I find additional similar issues that I couldn't solve.

Last updated: Mar 03 2024 at 16:02 UTC