证明 a_j ? b_j？总和 (a_j) ? 总和 (b_j)

Question

我对所有人j都有{1, 2, .. N}这样 的看法，j \xe2\x89\xa0 i它持有这样的观点a_j \xe2\x89\xa4 b_j。我想在 Coq 中证明

\n

我该如何做到这一点以及哪些模块最适合此类操作？

\n

Answer 1

数学组件库有一个带有大量引理的“大”运算理论。以下是证明你的结果的方法：

From mathcomp Require Import all_ssreflect.

Lemma test N (f g : nat -> nat) (i : 'I_N) :
  (forall j, j != i -> f i <= g i) ->
  \sum_(j < N | j != i) f i <= \sum_(j < N | j != i) g i.
Proof. move=> f_leq_g; exact: leq_sum. Qed.

编辑

如果您想对实数进行运算推理，您还需要安装数学组件分析库。以下是如何调整这个证明来处理实数：

(* Bring real numbers into scope, as well as
   the theory of algebraic and numeric structures *) 
Require Import Coq.Reals.Reals.
From mathcomp Require Import all_ssreflect ssralg ssrnum Rstruct reals.

(* Change summation and other notations to work over rings
   rather than the naturals *) 
Local Open Scope ring_scope.

Lemma test N (f g : nat -> R) (i : 'I_N) :
  (forall j, j != i -> f i <= g i) ->
  \sum_(j < N | j != i) f i <= \sum_(j < N | j != i) g i.
Proof. move=> f_leq_g; exact: Num.Theory.ler_sum. Qed.