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?

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`

.

However, `behead`

has a canonical structure of `tuple`

and is "equal" to `drop 1`

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

.

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

@Cyril Cohen , thank you!

Last updated: Jul 25 2024 at 16:02 UTC