通过bigop分配减法

Question

假设适当地管理了下溢量，用\sum_(i...) (F i - G i)将普通的(\sum_(i...) F i - \sum_(i...) G i)重写为bigop的最佳方法是什么？

[似乎big_split应该用于加法（或在Z中减去，将big_distrl与-1一起使用，但我需要将其用于（有界）自然数的减法。

谢谢您的任何建议。

再见，

皮埃尔

Answer 1

如果我正确解析了您的问题，那么您将关注以下陈述（？）

forall (n : nat) (F G : 'I_n -> nat),
  \sum_(i < n) (F i - G i) = \sum_(i < n) F i - \sum_(i < n) G i.

但是在这种情况下，考虑到减法运算(_ - _)%N的行为，该语句不成立，因为您需要添加一个假设，证明(F i - G i)不会取消，以证明相等性。

因此，以下语句：

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop.

Lemma question (n : nat) (F G : 'I_n -> nat) :
  (forall i : 'I_n, G i <= F i) ->
  \sum_(i < n) (F i - G i) = \sum_(i < n) F i - \sum_(i < n) G i.

您是对的，big_split不能照原样适用，而且从big_split的相同证明开始就不能成功，因为我们得到：

Proof.
move=> Hmain.
elim/big_rec3: _ => [//|i x y z _ ->].

(* 1 subgoal (ID 113) *)


    (*   n : nat *)
    (*   F, G : 'I_n -> nat *)
    (*   Hmain : forall i : 'I_n, G i <= F i *)
    (*   i : ordinal_finType n *)
    (*   x, y, z : nat *)
    (*   ============================ *)
    (*   F i - G i + (y - x) = F i + y - (G i + x) *)

并且我们被困住了，因为(y - x)上没有假设。

但是，可以依靠manual induction结合以下引理来证明引理：

Check big_ord_recl.
(* big_ord_recl *)
(*      : forall (R : Type) (idx : R) (op : R -> R -> R) (n : nat) (F : 'I_n.+1 -> R), *)
(*        \big[op/idx]_(i < n.+1) F i = op (F ord0) (\big[op/idx]_(i < n) F (lift ord0 i)) *)
Search _ addn subn in ssrnat.

例如，这是该结果的可能证明：

Proof.
  elim: n F G => [|n IHn] F G Hmain; first by rewrite !big_ord0.
  rewrite !big_ord_recl IHn // addnBAC // subnDA //.
  rewrite -subnDA [in X in _ = _ - X]addnC subnDA.
  congr subn; rewrite addnBA //.
  exact: leq_sum.
Qed.