## Stream: math-comp users

### Topic: how to restore information after building a tuple

#### Andrey Klaus (Oct 21 2021 at 12:59):

Hello.
I'd like to restore somehow information about tuple's sequence. In example, I have next theorem

``````From mathcomp Require Import all_ssreflect.

Theorem test2 n (T : eqType) (t1 : n.+1.-tuple T) :
{ t : n.-tuple T | tval t == drop 1 (tval t1) }.
Proof.
have p : { s | s = drop 1 t1} by exists (drop 1 t1).
case: p => s H. rewrite <- H.
have t := (@Tuple _ _ s).
move : t => /(_ n).
``````

Context is

``````  n : nat
T : eqType
t1 : (n.+1).-tuple T
prf : uniq t1
s : seq T
H : s = drop 1 t1
============================
(size s == n -> n.-tuple T) -> {t : n.-tuple T | t == s}
``````

My problem here is that as far as I've created the tuple, I'm already not able to see that it is related somehow with the sequence from which it is built... in example when I provide proof that `size s == n`, I have just a tuple of size n and that is. It 'forgot' that it is built from `s ` and I'm not able to relate `tval (of new tuple)` and the `s` somehow.

So, the question: how would you proof the theorem?

#### Cyril Cohen (Oct 21 2021 at 13:06):

Hi! You should use `pose t := in_tuple s`

• `pose` is the "transparent equivalent" of `have`
• `in_tuple` is the injection of `seq` into `Tuple`.

#### Cyril Cohen (Oct 21 2021 at 13:08):

However, `behead` has a canonical structure of `tuple` and is "equal" to `drop 1`

#### Cyril Cohen (Oct 21 2021 at 13:08):

So the tuple you are looking for is simply `[tuple of behead t1]`.

#### Cyril Cohen (Oct 21 2021 at 13:09):

``````Theorem test2 n (T : eqType) (t1 : n.+1.-tuple T) :
{ t : n.-tuple T | tval t == drop 1 (tval t1) }.
Proof. by exists [tuple of behead t1]; rewrite drop1. Qed.
``````

#### Andrey Klaus (Oct 21 2021 at 13:12):

@Cyril Cohen , thank you!

Last updated: Feb 02 2023 at 13:03 UTC