从tuple中移除tcast... 第二季

Question

我想去掉 tcast 的 "稃 "中，比如下面这个。但由于依赖型的 "约束"，这甚至没有进行类型检查。

Lemma foo : forall {T} m n (tc : n = m) (f : m.-tuple T -> 'I_n -> nat) (x : n.-tuple T),
    [seq f (tcast tc x) j | j <- enum 'I_n] =  
    [seq f x j | j <- enum 'I_n].

事实上，对于我心目中的应用来说，一个更重要的例子是下面的外稃，它可以进行类型检查。

Lemma bar n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
  \sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i = 
  \sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.

这将是简单的 seq但在这里我找不到如何使用tuple.v或fintype.v中的稃来进行。

那么，正确的处理方式是什么呢？tcast 当他们似乎不适合用 "大刀阔斧 "的方法来处理时，他们的表情就会变得很复杂。val_inj 和案例分析（见前文）？在第一个例子中，我是否必须引入两个版本的 f，后来证明在序列上是相等的（如果是，最好的方法是什么）？

先谢谢你的建议。

皮埃尔

Answer 1

在你发布的情况下，你可以使用标准的技巧来删除casts。

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

Lemma sum_tuple n (t : n.-tuple nat) :
 \sum_(i < n) tnth t i = \sum_(i < n) nth 0 (val t) i.
Proof. by apply: eq_bigr => ? ?; rewrite (tnth_nth 0). Qed.

Lemma bar n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
  \sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i =
  \sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.
Proof.
rewrite !sum_tuple val_tcast /=.

有一个直接的证明:

Lemma bar' n1 n2 n (tc : n1 + n2 = n) (l1 : n1.-tuple nat) (l2 : n2.-tuple nat) :
  \sum_(i < n) tnth (tcast tc [tuple of (l1 ++ l2)]) i =
  \sum_(i < n1) tnth l1 i + \sum_(i < n2) tnth l2 i.
Proof. by rewrite -!(big_tuple _ _ _ predT id) val_tcast big_cat. Qed.