Pierre Jouvelot (Jun 12 2021 at 12:06): Pierre Jouvelot (Jun 12 2021 at 12:06):Is there a more elegant way to get to eq_from_tnth than what is done in this code snippet?
From Coq Require Import Unicode.Utf8.
From mathcomp Require Import all_ssreflect.
From mathcomp.fingroup Require Import perm.
From Coq Require Import ssrsearch.
Variable (n : nat).
Lemma foo (x y : n.-tuple nat) (p : 'S_n) : perm_eq x y.
Proof.
apply/tuple_permP.
exists p.
(**)
set xx := (X in val X = _); set yy := (X in _ = val X).
suff : xx = yy by move=> ->.
(**)
apply: eq_from_tnth => j.
Thanks.
Reynald Affeldt (Jun 12 2021 at 13:15):This could maybe replace the last 3 lines: rewrite -[X in _ = _ X](@eq_from_tnth _ _ x) // => j.
Pierre Jouvelot (Jun 12 2021 at 13:49):Nice :) Thanks a lot.
Enrico Tassi (Jun 13 2021 at 08:06):This should also work
congr (val _).
apply: eq_from_tnth => j.
Enrico Tassi said:
This should also work
congr (val _). apply: eq_from_tnth => j.
Damned, of course! congr val is even enough. Thanks a lot :)
Last updated: Apr 19 2024 at 12:02 UTC