Если я правильно проанализирую ваш вопрос, вы сосредоточитесь на следующем равенстве:
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)
*)
и мы застряли, потому что на * 1018 нет гипотез *.
Однако лемму можно доказать, опираясь на «ручную индукцию» в сочетании со следующими леммами:
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)
однако это выглядит не так просто, как я ожидал: к вашему сведению ниже является почти полным сценарием, где два оставшихся объекта разрешений имеют дело со свойством bijection функций переиндексации, надеясь, что это поможет (также кажется, что некоторые леммы, такие как mem_enumT и filter_predI, могут быть добавлены в MathComp, так что я, вероятно, открою пиар, чтобы предложить это):
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.