什么是最好的重写方式\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),但我需要将它用于(有界)自然数的减法。
提前感谢您的任何建议。
再见,
皮埃尔
最佳答案
这是一个更简短的证明,带有更一般的陈述,我会将其添加到库中。
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
取消.
关于coq - 在 bigop 上分配减法,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/61556710/