Stream: math-comp users

Topic: how to restore information after building a tuple


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

view this post on Zulip Cyril Cohen (Oct 21 2021 at 13:06):

Hi! You should use pose t := in_tuple s

view this post on Zulip Cyril Cohen (Oct 21 2021 at 13:08):

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

view this post on Zulip Cyril Cohen (Oct 21 2021 at 13:08):

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

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

view this post on Zulip Andrey Klaus (Oct 21 2021 at 13:12):

@Cyril Cohen , thank you!


Last updated: Feb 02 2023 at 13:03 UTC