Stream: math-comp users

Topic: perm_eq for equal seqs


view this post on Zulip Florent Hivert (Aug 16 2021 at 18:23):

I'm trying to prove perm_eq of two complicated sequences. I looking for tactics saying that they are perm_eq because they are actualy equal. The best I've managed to come with is the following cumbersome commands. Is there any pattern matching wizardry which allows to to it better:

    set X := (X in perm_eq X _); set Y := (Y in perm_eq _ Y).
    suff -> : X = Y by apply: perm_refl.
    rewrite {}/X {}/Y.

view this post on Zulip Florent Hivert (Aug 17 2021 at 07:44):

Never mind. a simple rewrite (eq_map (f2 := ...)) does the job.

view this post on Zulip Notification Bot (Aug 17 2021 at 07:44):

Florent Hivert has marked this topic as resolved.

view this post on Zulip Yves Bertot (Aug 17 2021 at 07:47):

Too bad, I was looking at this problem, and I was thinking it might be useful to add a lemma to mathcomp, with the following statement.

reflE
     : forall (T : Type) (R : T -> T -> Prop),
       (forall x : T, R x x) -> forall x y : T, x = y -> R x y

view this post on Zulip Yves Bertot (Aug 17 2021 at 07:48):

But, then the usage is a bit complicated, because Coq's elaboration process has a hard time finding what the relation is. Here is the kind of command I had to write

apply: (@reflE _ perm_eq (@perm_refl T)).

view this post on Zulip Yves Bertot (Aug 17 2021 at 07:49):

where T is the type of elements of the sequences you are considering.

view this post on Zulip Yves Bertot (Aug 17 2021 at 07:53):

Here is the code for the whole experiment.

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section refl_sandbox.

Variables (T : Type)(R : T -> T -> Prop).
Hypothesis reflR : forall x: T, R x x.
Lemma reflE : forall x y, x = y -> R x y.
Proof.  move=> x y ->; apply: reflR. Qed.

End refl_sandbox.

Section perm_sandbox.

Variables (T : eqType) (X Y : seq T).
Hypothesis XY : X = Y.

Lemma sandbox : perm_eq X Y.
Proof.
apply: (@reflE _ perm_eq (@perm_refl T)).
apply: XY.
Qed.

view this post on Zulip Florent Hivert (Aug 17 2021 at 08:12):

Thanks for the suggestion. I did the experiment on my use case. I confirm that

apply: (@reflE _ perm_eq (@perm_refl _)).

or

apply: (@reflE _ perm_eq); first exact: perm_refl.

both work whereas

apply: (@reflE _ _ (@perm_refl _)).

fails.

view this post on Zulip Notification Bot (Aug 17 2021 at 08:14):

Florent Hivert has marked this topic as unresolved.

view this post on Zulip Florent Hivert (Aug 17 2021 at 08:18):

I'm unmarking the topic as resolved. A slightly more complicated usecase render my solution ugly.

view this post on Zulip YAMAMOTO Mitsuharu (Aug 18 2021 at 05:57):

Since perm_refl is in the core hint database,

apply: (@reflE _ perm_eq) => //.

or alternatively,

apply: (eq_ind _ (perm_eq _)) => //.

would work.

view this post on Zulip Florent Hivert (Aug 18 2021 at 12:10):

I don't understand how this second solution works. Consider the following setting:

Variables (X Y Z : seq T).
Hypothesis (XZ : X = Z) (YZ : Y = Z).

Lemma sandbox : perm_eq X Y.
Proof.

When writing

apply: (eq_ind _ (perm_eq _)).

one gets:

  XZ : X = Z
  YZ : Y = Z
  ============================
  perm_eq X ?Goal

subgoal 2 (ID 296) is:
 ?Goal = Y

If instead one writes:

apply: (eq_ind _ (perm_eq _)) => //.

one gets:

  XZ : X = Z
  YZ : Y = Z
  ============================
  X = Y

How comes that Coq decides by itself that the way to solve the second subgoal is eq_refl ?

view this post on Zulip YAMAMOTO Mitsuharu (Aug 19 2021 at 01:24):

// solves is the first subgoal perm_eq X ?Goal via unification with the type of perm_refl in the hint database. The unification yields the instantiation {Goal := X}, which is then applied to the second subgoal.

view this post on Zulip YAMAMOTO Mitsuharu (Aug 19 2021 at 02:17):

Actually, the order to process multiple subgoals is crucial here (trivial in // can also solve the second subgoal ?Goal = Y with {Goal := Y}, but that's not what we want). If Coq does not specify its order, then

apply: (eq_ind _ (perm_eq _)); first by [].

would be safer.

view this post on Zulip YAMAMOTO Mitsuharu (Aug 20 2021 at 01:28):

    set X := (X in perm_eq X _); set Y := (Y in perm_eq _ Y).
    suff -> : X = Y by apply: perm_refl.
    rewrite {}/X {}/Y.

A possible variant of your original commands above would be to use an extra feature of congr like:

    set X := (X in perm_eq X _).
    congr perm_eq: (perm_refl X); rewrite {}/X.

or

    evar (X : seq T).
    congr perm_eq: (perm_refl X); rewrite {}/X.

where X is a fresh name.

view this post on Zulip Enrico Tassi (Aug 20 2021 at 11:02):

Maybe I'm missing something, but I think you can easily prove, and then apply:, something like forall x y, x = y -> perm_eq x y.

view this post on Zulip YAMAMOTO Mitsuharu (Aug 20 2021 at 12:13):

Indeed. Probably I was thinking about the "pattern" that is composable on the fly too much.


Last updated: Jan 29 2023 at 18:03 UTC