coq - Coq - 在 Ssreflect 中证明涉及 bigops 的严格不等式

Question

我正在尝试使用数学组件库来证明以下内容：

Lemma bigsum_aux (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R):
  (forall i0, F i0 <= G i0) /\ (exists j0, F j0 < G j0) ->
  \sum_(i < q) F i < \sum_(i < q) G i.

最初，我试图在orbigsum_aux的文档中找到一些等效的引理，但我找不到；所以这就是我到目前为止所能做的：ssralgbigop

Proof.
 move => [Hall Hex]. rewrite ltr_neqAle ler_sum; last first.
 - move => ? _. exact: Hall.
 - rewrite andbT. (* A: What now? *)

欢迎任何有关相关引理的帮助或指示。

Answer 1

您想将总和拆分为“坏” (<) 部分，然后剩下的就很简单了：

From mathcomp Require Import all_ssreflect all_algebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.
Import Num.Theory.

Lemma bigsum_aux (R : numDomainType) q (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R)
      (hle : forall i0, F i0 <= G i0) z (hlt : F z < G z) :
  \sum_(i < q) F i < \sum_(i < q) G i.
Proof.
by rewrite [\sum__ F _](bigD1 z) ?[\sum__ G _](bigD1 z) ?ltr_le_add ?ler_sum.
Qed.