在 bigop 上分配减法

Question

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

更准确地说，关于这些下溢，我对以下引理感兴趣：

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

如果我正确地解析了你的问题，你将关注以下等式：

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 不适用，而且从 proof of big_split 重新开始也不会成功，因为我们得到：

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

(* 1 subgoal

   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.

（另见 https://github.com/math-comp/math-comp/wiki/Search）

特别是，这里是该结果的可能证明：

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.
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.

编辑： 概括确实可以使用这个引理来完成：

reindex
     : forall (R : Type) (idx : R) (op : Monoid.com_law idx) (I J : finType) 
         (h : J -> I) (P : pred I) (F : I -> R),
       {on [pred i | P i], bijective h} ->
       \big[op/idx]_(i | P i) F i = \big[op/idx]_(j | P (h j)) F (h j)

然而它似乎并不像我预期的那么简单：仅供参考，下面是一个几乎完整的脚本 − 其中两个剩余承认处理重新索引函数的双射属性，希望这有助于（也是它似乎有一些引理，例如 mem_enumT 和 filter_predI，可能会添加到 MathComp 中，所以我可能会打开一个 PR 来提议：

From mathcomp Require Import all_ssreflect.

Lemma mem_enumT (T : finType) (x : T) : (x \in enum T).
Proof. by rewrite enumT mem_index_enum. Qed.

Lemma predII T (P : pred T) :
  predI P P =1 P.
Proof. by move=> x; rewrite /predI /= andbb. Qed.

Lemma filter_predI T (s : seq T) (P1 P2 : pred T) :
  filter P1 (filter P2 s) = filter (predI P1 P2) s.
Proof.
elim: s => [//|x s IHs] /=.
case: (P2 x); rewrite ?andbT /=.
{ by rewrite IHs. }
by case: (P1 x) =>/=; rewrite IHs.
Qed.

Lemma nth_filter_enum
  (I : finType) (P : pred I) (s := filter P (enum I)) (j : 'I_(size s)) x0 :
  P (nth x0 [seq x <- enum I | P x] j).
Proof.
suff: P (nth x0 s j) && (nth x0 s j \in s) by case/andP.
rewrite -mem_filter /s /= filter_predI.
under [filter (predI P P) _]eq_filter do rewrite predII. (* needs Coq 8.10+ *)
exact: mem_nth.
Qed.

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.
Proof.
  move=> Hmain.
  (* Prepare the reindexation on the indices satisfying the pred. P *)
  set s := filter P (enum 'I_n).
  set t := in_tuple s.
  (* We need to exclude the case where the sums are empty *)
  case Es: s => [|x0 s'].
  { suff Hpred0: forall i : 'I_n, P i = false by rewrite !big_pred0 //.
    move: Es; rewrite /s; move/eqP.
    rewrite -[_ == [::]]negbK -has_filter => /hasPn HP i.
    move/(_ i) in HP.
    apply: negbTE; apply: HP; exact: mem_enumT.
  }
  (* Coercions to go back and forth betwen 'I_(size s) and 'I_(size s).-1.+1 *)
  have Hsize1 : (size s).-1.+1 = size s by rewrite Es.
  have Hsize2 : size s = (size s).-1.+1 by rewrite Es.
  pose cast1 i := ecast n 'I_n Hsize1 i.
  pose cast2 i := ecast n 'I_n Hsize2 i.
  set inj := fun (i : 'I_(size s).-1.+1) => tnth t (cast1 i).
  have Hinj1 : forall i : 'I_(size s).-1.+1, P (inj i).
  { move=> j.
    rewrite /inj (tnth_nth (tnth t (cast1 j)) t (cast1 j)) /t /s in_tupleE /=.
    exact: nth_filter_enum. }
  have Hinj : {on [pred i | P i], bijective inj}.
  { (* example inverse function; not the only possible definition *)
    pose inj' :=
      (fun n : 'I_n => if ~~ P n then @ord0 (size s).-1 (* dummy value *)
                       else @inord (size s).-1 (index n (filter P s))).
    exists inj'; move=> x Hx; rewrite /inj /inj'.
    admit. admit. (* exercise left to the reader :) *)
  }
  (* Perform the reindexation *)
  rewrite !(reindex inj).
  do ![under [\sum_(_ | P _) _]eq_bigl do rewrite Hinj1]. (* needs Coq 8.10+ *)
  apply: question => i; exact: Hmain.
  all: exact: Hinj.
Admitted.

Answer 2

这是 Emilio Gallego Arias（用户：1955696）写的一个很好的答案（谢谢，Emilio）。

Lemma big_split_subn (P : 'I_k -> bool) F1 F2
      (H : forall s : 'I_k, P s -> F2 s <= F1 s) :
  \sum_(s < k | P s) (F1 s - F2 s) =
  \sum_(s < k | P s) F1 s - \sum_(s < k | P s) F2 s.
Proof.
suff:
  \sum_(s < k | P s) (F1 s - F2 s) =
    \sum_(s < k | P s) F1 s - \sum_(s < k | P s) F2 s /\
    \sum_(s < k | P s) F2 s <= \sum_(s < k | P s) F1 s by case.
pose K x y z := x = y - z /\ z <= y. 
apply: (big_rec3 K); first by []; rewrite {}/K.
move=> i b_x b_y b_z /H Pi [] -> Hz; split; last exact: leq_add.
by rewrite addnBA ?addnBAC ?subnDA.
Qed.

Answer 3

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

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 取消。

在 bigop 上分配减法

Distributing subtraction over bigop

coq

ssreflect