Удаление tcast для кортежей

Question

Я нахожусь в тупике с таким равенством целей (я думаю, детали не имеют значения):

tcast tc0
[tuple of take i (s_bs bs) ++ drop i.+1 (s_bs bs) ++ [:: [ffun⇒ 0]]] 
=
...

Как мне избавиться от tcast и tuple к go обратно к простому seq (я пробовал трюк val_inj, но это не помогло удалить приведение типов)?

Заранее спасибо.

Пока,

Пьер

Answer 1

Дать точный ответ немного сложно, так как вы не предоставили воспроизводимый тестовый сценарий. Но вы можете попробовать переписать свою цель, используя следующую лемму, как только вы применили val_inj.

Lemma val_tcast {T} m n (tc : n = m) (x : n.-tuple T) :
  val (tcast tc x) = val x.
Proof. now case tc. Qed.

Answer 2

Я полагал, что, по крайней мере, в тех случаях, которые мне приходилось обрабатывать, правильное использование перезаписи с использованием tcastE и tnth_nth (что вынудило приведение к nat) с последующей частичной оценкой через /= , избавляется от tcast.