Is there inversion and general induction in mathcomp ? · math-comp users

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?

(* 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.

Ana de Almeida Borges (Nov 04 2022 at 11:40):

Ana de Almeida Borges (Nov 04 2022 at 11:42):

Ana de Almeida Borges (Nov 04 2022 at 11:44):

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.

Ana de Almeida Borges (Nov 04 2022 at 11:47):

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.

Paolo Giarrusso (Nov 04 2022 at 12:33):

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).

Alexander Gryzlov (Nov 04 2022 at 14:42):

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.

Ana de Almeida Borges (Nov 05 2022 at 15:51):

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.

Paolo Giarrusso (Nov 05 2022 at 16:19):

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.

Paolo Giarrusso (Nov 05 2022 at 16:21):

And the reason we must treat indexes specially is because case analysis on PIn a l can teach us constraints on a and l.

Paolo Giarrusso (Nov 05 2022 at 16:24):

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).

Ana de Almeida Borges (Nov 05 2022 at 16:26):

Ana de Almeida Borges (Nov 05 2022 at 16:29):

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.

Alexander Gryzlov (Nov 07 2022 at 08:24):

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.

Enrico Tassi (Nov 07 2022 at 09:10):

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.

Enrico Tassi (Nov 07 2022 at 09:14):

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.

Assia Mahboubi (Nov 07 2022 at 13:33):

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.

walker (Nov 08 2022 at 10:22):

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.

Stream: math-comp users

Topic: Is there inversion and general induction in mathcomp ?

walker (Nov 04 2022 at 10:21):