删除元组的tcast

Question

我在这样的目标平等中受束缚（我认为细节无关紧要：]

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

我如何摆脱tcast和tuple回到简单的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。