删除元组的tcast [英] Removing tcast for tuples

问题描述

我陷入了这样的目标平等的困境(我认为细节无关紧要):

I'm in a bind with a goal equality like this (the details don't matter, I think):

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

如何摆脱 tcast 和 tuple 回到简单的 seq (我尝试了 val_inj 技巧，但这似乎并没有删除类型转换)?

How do I get rid of the tcast and tuple to go back to simple seq (I tried the val_inj trick, but this didn't seem to remove the type cast)?

谢谢.

再见

皮埃尔

推荐答案

给出准确的答案有些困难，因为您没有提供任何可重现的测试用例.但是，一旦您应用了 val_inj ，就可以尝试使用以下引理重写目标.

Giving a precise answer is a bit difficult, since you did not provide any reproducible testcase. But you could try rewriting your goal using the following lemma, once you have applied 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.

这篇关于删除元组的tcast的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！