Stream: math-comp users

Topic: val/tval handling


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre Jouvelot (Jun 12 2021 at 13:49):

Nice :) Thanks a lot.

view this post on Zulip Enrico Tassi (Jun 13 2021 at 08:06):

This should also work

congr (val _).
apply: eq_from_tnth => j.

view this post on Zulip Pierre Jouvelot (Jun 13 2021 at 10:38):

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: Feb 08 2023 at 08:02 UTC