在 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=>

1. /(_ _ _)forall i, P i -> E1 i <= E2 i)用两个元变量填充假设的两个参数（让我们命名第一个?i），
2. 然后/subnK链接它以将比较转换为E2 ?i - E1 ?i + E1 ?i = E2 ?i.
3. - 释放元变量，将顶部假设转化为 forall i, P i -> E2 i - E1 i + E1 i = E2 i
4. /(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。