coq - 删除元组的 tcast

Question

我陷入了这样的目标平等（我认为细节并不重要）：

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

我如何摆脱tcastandtuple回到简单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

我认为，至少在我必须处理的情况下，正确使用重写使用tcastEand tnth_nth（这迫使强制转换为nat），然后通过部分评估/=，摆脱tcast.