Distributing subtraction over bigop

What is the best way to rewrite \sum_(i...) (F i - G i) as (\sum_(i...) F i - \sum_(i...) G i) on ordinals with bigop, assuming that underflows are properly managed?

More precisely, regarding these underflows, I'm interested in the following lemma:

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.

It seems that big_split should work for an addition (or subtraction in Z, using big_distrl with -1), but I need to use it for a subtraction on (bounded) naturals.

Thanks in advance for any suggestion.

Bye,

Pierre

Solution

If I correctly parse your question, you focus on the following equality:

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.

Obviously, given the behavior of the truncated subtraction (_ - _)%N, this statement doesn't hold as is, we need an hypothesis saying that no (F i - G i) cancels, in order to prove the equality.

Hence the following statement:

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.

Then you're right that big_split is not applicable as is, and moreover starting over from the proof of big_split can't be successful, as we get:

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

and we are stuck because there is no hypothesis on (y - x).

However, it is possible to prove the lemma by relying on a "manual induction", combined with the following lemmas:

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.

In particular, here is a possible proof of that result:

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.

EDIT: the generalization could indeed be done using this lemma:

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)

however it appears not as straightforward as I expected: FYI below is an almost-complete script − where the two remaining admits deal with the bijection property of the reindexation functions, hoping that this helps (also it seems a few lemmas, such asmem_enumT and filter_predI, might be added in MathComp, so I'll probably open a PR to propose that):

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.