## Stream: math-comp users

### Topic: perm_eq for equal seqs

#### 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.
``````

#### Florent Hivert (Aug 17 2021 at 07:44):

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

#### Notification Bot (Aug 17 2021 at 07:44):

Florent Hivert has marked this topic as resolved.

#### 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
``````

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

#### Yves Bertot (Aug 17 2021 at 07:49):

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

#### 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.
``````

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

#### Notification Bot (Aug 17 2021 at 08:14):

Florent Hivert has marked this topic as unresolved.

#### Florent Hivert (Aug 17 2021 at 08:18):

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

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

#### 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
``````

``````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` ?

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

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

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

#### 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`.

#### 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