如何在Coq中证明指定不等式？omega与lia战术失效

你的问题出在omega和lia无法处理整数除法与二次式绝对值的组合逻辑。我们可以通过手动化简条件、转化不等式，结合反证法完成证明：

证明步骤解析 #

1. 转化除法不等式：将k < b/2转化为2k < b（利用正整数的除法性质，调用Z.lt_div2_pos定理）。
2. 推导关键下界：由2k < b可得b - 2k ≥ 1（整数差的基本性质）。
3. 反证法核心：假设绝对值等于0（即表达式为0），代入化简后推出矛盾——该方程无正整数解，因此绝对值必然≥1。

完整Coq代码 #

Require Import ZArith.
Require Import Psatz.
Open Scope Z.

Lemma ge1:
forall b k: Z,
b>=1 -> k>=1 -> k < b/2 -> Zabs (b*b-2*b*k-k*k) >=1.
Proof.
intros b k H1 H2 H3.
(* 将k < b/2转化为2k < b（正整数除法性质） *)
assert (H4: 2*k < b).
{ apply Z.lt_div2_pos; [exact H1 | exact H3]. }
(* 推导b-2k的下界 *)
assert (H5: b - 2*k >= 1) by (apply Z.le_sub_lt; [exact H4 | reflexivity]).

(* 反证法：假设绝对值小于1，即表达式为0 *)
destruct (Zabs_eq_zero (b*b-2*b*k-k*k)) as [H_zero _].
intro H_contr; apply H_zero in H_contr.

(* 代入表达式为0的条件，用变量替换化简 *)
set (m := b - 2*k) in *.
replace b with (2*k + m) in H_contr by lia.
ring_simplify in H_contr.

(* 化简得到(k - m)^2 = 2*m²，推出矛盾：2不是整数平方 *)
assert (H_square: (k - m)^2 = 2 * m * m) by ring_simplify H_contr; lia.
set (x := k - m) in H_square.

(* 证明2不是整数平方 *)
assert (H_no_square: forall z: Z, z*z <> 2).
{ intros z; destruct z; try lia; try lia; try lia; try lia. }

(* 推导x必为m的倍数，进而得到y²=2的矛盾 *)
assert (H_div: m divides x).
{ apply Z.divide_of_square_divides_square_times_two; exact H_square. }
destruct H_div as [y H_x_eq].
rewrite H_x_eq in H_square.
ring_simplify in H_square.
assert (m <> 0) by lia.
apply Z.mul_cancel_l in H_square; [exact (Z.mul_neq_0_l m H_no_square)| exact H_square].
lia.
Qed.

关键技巧说明 #

• 用Z.lt_div2_pos将除法不等式转化为整数乘法不等式，让自动化战术能处理更基础的逻辑。
• 通过变量替换m = b - 2k简化二次式，把问题转化为证明“2不是整数平方”的经典结论。
• 反证法避开直接估计绝对值下界，转而证明表达式不可能为0，从而满足绝对值≥1的要求。

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