勒柯克 - 证明涉及bigops在Ssreflect
问题描述:
我试图证明使用数学组件库遵循严格的不等式:勒柯克 - 证明涉及bigops在Ssreflect
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.
起初,我试图找到一些引理相当于bigsum_aux
的ssralg
或文档中bigop
,但我找不到任何;所以这是我已经能够到目前为止做:
Proof.
move => [Hall Hex]. rewrite ltr_neqAle ler_sum; last first.
- move => ? _. exact: Hall.
- rewrite andbT. (* A: What now? *)
任何帮助或指针向相关引理将受到欢迎。
答
要在“坏”(<)部分分割的总和,那么剩下的就是简单:
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.
这是非常漂亮的使用重写!谢谢 :) – VHarisop