Coq中证明a_j ≤ b_j对应序列和不等式的方法及适用模块问询

适用的Coq模块 #

处理这类有限序列求和、数值不等式推导的问题，常用的模块分为原生标准库和第三方库两类：

• 原生标准库：
  • 整数运算和线性不等式：Arith、ZArith、Lia（整数线性不等式自动证明策略，替代旧版Omega）
  • 实数运算和线性不等式：Reals、Lra（实数线性不等式自动证明策略）
  • 有限序列和操作：List模块自带的sum函数可直接对列表类型的序列求和
• 第三方数学组件库（MathComp）：
  是处理这类代数问题的首选，推荐搭配ssreflect、ssrnat、ssrnum、BigOp模块使用，内置了大量求和拆分、集合操作的预制引理，代码简洁度远高于原生标准库。

证明思路 #

你要证的命题核心逻辑非常直观：

把全量求和拆分为「下标不等于i的项的和」+「第i项」两部分，由于所有j≠i的项都满足a_j ≤ b_j，因此所有j≠i的a求和必然小于等于b的对应求和，这部分可以作为公共项从不等式两边消去，最终就能得到全量求和不等式和a_i ≤ b_i的等价性。

示例证明代码（基于原生标准库，整数场景） #

Require Import List Arith Lia.

(* 用List存储序列，nth j l 0表示取序列l的第j项，默认缺省值为0 *)
Lemma sum_ineq_equiv (N : nat) (a b : list nat) (i : nat) :
  length a = N -> 
  length b = N -> 
  i < N ->
  (forall j, j < N -> j <> i -> nth j a 0 <= nth j b 0) ->
  (sum a <= sum b <-> nth i a 0 <= nth i b 0).
Proof.
  (* 输入前提引入 *)
  intros Hla Hlb Hi Hcond.
  (* 把序列拆分为前i项、第i项、i之后的项，分别求和 *)
  rewrite <- (firstn_skipn i a) at 1.
  rewrite <- (firstn_skipn i b) at 1.
  simpl sum.
  (* 取出第i项的值 *)
  destruct (skipn i a) as [|a_i tl_a] eqn:Ea; lia.
  destruct (skipn i b) as [|b_i tl_b] eqn:Eb; lia.
  simpl sum.
  (* 剩余线性不等式用lia自动证明 *)
  split; intros H; lia.
Qed.

如果是实数场景，只需要把nat类型替换为R，导入Reals和Lra模块，最后一步用lra替代lia即可。
如果用MathComp的BigOp处理求和，不需要手动拆分列表，直接调用内置引理bigD1即可完成「去掉第i项的求和拆分」，后续同样可以用自动策略消解剩余不等式，代码量会减少一半左右。

内容的提问来源于stack exchange，提问作者dkutlesic