如何证明不等式

Question

如何在 Coq 中证明这一点？战术“欧米茄”不起作用。 “lia”也没有。

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.
intros b k.
intros H1 H2 H3.
omega.

谢谢你。

Answer 1

由于绝对值总是正数，所以你要证明的是 Z.abs 的参数不能为零。但由于在给定的范围内它可以变得正或负，所以你需要一个数论论证。 Lia（和 nia）只能得出结论，当你可以争论不等式时，比如说你是否可以证明 Zabs 的论证总是 >=1 或 <=-1, which is not the case.

当您求解“b b - 2 b k - k k = 0”以获得 k 时，您将得到“k=(+-sqrt(2)-1)*b”。为了证明不存在满足该方程的 k 和 b，您需要 sqrt(2) 的无理数。 Lia 不知道 sqrt(2)。