Stream: math-comp users

Topic: Is there inversion and general induction in mathcomp ?


view this post on Zulip walker (Nov 04 2022 at 10:21):

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.

view this post on Zulip Ana de Almeida Borges (Nov 04 2022 at 11:40):

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

view this post on Zulip Ana de Almeida Borges (Nov 04 2022 at 11:42):

Why do you say elim doesn't work well here, though?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Ana de Almeida Borges (Nov 05 2022 at 16:26):

What is the difference between indexes and parameters?

view this post on Zulip Ana de Almeida Borges (Nov 05 2022 at 16:29):

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.

view this post on Zulip Alexander Gryzlov (Nov 07 2022 at 08:24):

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.

view this post on Zulip Enrico Tassi (Nov 07 2022 at 09:10):

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.

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (Nov 07 2022 at 13:33):

Hello @walker , what is the problem 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.

view this post on Zulip 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.


Last updated: Jan 29 2023 at 19:02 UTC