coq - 从元组中删除 tcast... 第 2 季
问题描述
我想删除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
, 后来证明在序列上是相等的(如果是,那么最好的方法是什么)?
提前感谢您的任何建议。
皮埃尔
解决方案
在您发布的情况下,您可以使用标准技巧删除演员表:
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.
推荐阅读
- python - 使用python从html文件中提取邮政编码
- javascript - 是否有任何方法可以滚动到确切的关键字,如果它在当前窗口中不可见,我正在使用 wd npm
- javascript - 用于实现淡入的 for 循环中的 setInterval
- matlab - 如何从文本文件 Matlab 创建散点图
- c++ - 在光线追踪器上进行 phong 着色的奇怪颜色
- observable - Promise.resolve 的 rxjs6 中的等价物是什么
- java - Apache FOP fox:使用 PDF 文件时外部文档不起作用
- android - 如何在Android中使线程重复
- graphviz - GraphViz:使用 pos 属性的网格布局问题
- php - php pdo 属性数组