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

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

does the job.

Florent Hivert has marked this topic as resolved.

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

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

where `T`

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

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

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.

Florent Hivert has marked this topic as unresolved.

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

Since `perm_refl`

is in the core hint database,

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

or alternatively,

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

would work.

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`

?

`//`

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.

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.

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

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`

.

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

Last updated: Jul 23 2024 at 20:01 UTC