从元组中删除 tcast ...第 2 季

Question

我想删除 "lemma" 中的 tcast，如下所示。但由于依赖类型 "constraints"，这甚至没有进行类型检查。

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 和案例分析（参见前面的 post）进行处理时，解决这些表达式的正确方法是什么？在第一个例子中，我是否必须引入两个版本的 f，后来证明它们在序列上是相等的（如果是这样，最好的方法是什么）？

提前感谢您的任何建议。

皮埃尔

Answer 1

如果您 post，您可以使用标准技巧删除强制转换：

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.

从元组中删除 tcast ...第 2 季

Removing tcast from tuples... Season 2

coq

ssreflect