coq - 在 bigop 上分配减法

Question

什么是最好的重写方式\sum_(i...) (F i - G i)如 (\sum_(i...) F i - \sum_(i...) G i)在序数上 bigop ，假设下溢得到妥善管理？

更准确地说，关于这些下溢，我对以下引理感兴趣:
Lemma big_split_subn (n : nat) (P : 'I_n -> bool) (F G : 'I_n -> nat) :
(forall i : 'I_n, P i -> G i <= F i) ->
\sum_(i < n | P i) (F i - G i) = \sum_(i < n | P i) F i - \sum_(i < n | P i) G i.
看来big_split应该适用于加法(或 Z 中的减法，使用 big_distrl 和 -1)，但我需要将它用于(有界)自然数的减法。

提前感谢您的任何建议。

再见，

皮埃尔

Answer 1

这是一个更简短的证明，带有更一般的陈述，我会将其添加到库中。

Lemma sumnB I r (P : pred I) (E1 E2 : I -> nat) :
     (forall i, P i -> E1 i <= E2 i) ->
  \sum_(i <- r | P i) (E2 i - E1 i) =
  \sum_(i <- r | P i) E2 i - \sum_(i <- r | P i) E1 i.
Proof. by move=> /(_ _ _)/subnK-/(eq_bigr _)<-; rewrite big_split addnK. Qed.

编辑:实际上，甚至有一个类轮。
这是介绍模式的解释，从 move=> 开始

/(_ _ _)填充假设的两个参数 forall i, P i -> E1 i <= E2 i)带有两个元变量(让我们将第一个命名为 ?i )，

然后 /subnK链接它以将比较结果变为 E2 ?i - E1 ?i + E1 ?i = E2 ?i .

-释放元变量，将顶部假设变为 forall i, P i -> E2 i - E1 i + E1 i = E2 i

/(eq_bigr _)<-具有同余引理的链，使用 _作为第一
参数(应该是右手边的形状
我们不想提供)，这导致了假设forall idx op P l, \big[op/idx]_(i <- l | P i) (E2 i - E1 i + E1 i) = \big[op/idx]_(i <- l | P i) E2 i)我们可以用它来重写权利
离开使用 <- .

我们以通常的 big_split 结束并用 addnK 取消.