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: Jan 29 2023 at 18:03 UTC