4

假设下溢得到妥善管理，在序数上重写的最佳方法是\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 一起使用），但我需要将它用于（有界）自然的减法。

提前感谢您的任何建议。

再见，

皮埃尔

4

3 回答 3

5

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

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。

于 2021-01-18T17:10:34.840 回答
1

这是 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.
于 2020-05-30T17:41:57.787 回答
0

如果我正确解析了您的问题，您将关注以下相等性：

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

   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)。

但是，可以通过“手动归纳”结合以下引理来证明引理：

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)

但是它看起来不像我预期的那么简单：FYI 下面是一个几乎完整的脚本 - 剩下的两个承认处理重新索引函数的双射属性，希望这会有所帮助（也似乎有一些引理，例如mem_enumTand 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.
于 2020-05-02T12:44:09.503 回答