证明a_j b_j→sum (a_j)≤sum (b_j)

Question

我对{1, 2, .. N}中的所有j都有，这样，j ≠ i，它就包含了那个a_j ≤ b_j。我想在Coq中证明

​

我如何才能做到这一点，哪些模块最适合这些类型的操作？

Answer 1

mathematical components library有一个包含大量引理的“大”运算理论。下面是如何证明你的结果的：

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.

编辑

如果你想推断实数上的运算，你还需要安装mathematical components analysis library。下面是如何使这个证明适用于实数：

(* 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.