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: Apr 19 2024 at 22:01 UTC