0

我想删除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, 后来证明在序列上是相等的（如果是，那么最好的方法是什么）？

提前感谢您的任何建议。

皮埃尔

4

1 回答 1

1

在您发布的情况下，您可以使用标准技巧删除演员表：

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.
于 2020-05-13T02:12:44.663 回答