在 Coq 中证明涉及有理数的非线性方程和不等式

Question

我正在尝试使用 Coq 交互式定理证明器来形式化稳定币协议。我的证明涉及大量涉及有理数的线性和非线性方程的操作。目前，我正在使用标准 Coq 有理数库，但它涉及大量的证明编写。我尝试使用“nra”和“lra”等策略来自动查找证据，但它给了我一个错误，提示“策略失败：无法找到证人”。 作为一个例子，我试图使用下面给出的证明来证明这个简单的引理。

Lemma test (qs : Q) (n : Q) (nu : Q) (ex : Q) :
  qs > 0 /\ n > 0 /\ nu > 0 /\ ex > 0 -> 
  qs <= ex -> qs / ex <= 1.
Proof.
    intros. lra.
Qed.

但它给了我一个错误，说“战术失败：找不到证人”。我尝试破坏有理数但无法完成证明。

我的问题是：

1. 如何用最简单的方式解决上述证明？
2. 是否有任何其他库可以帮助我编写不等式和方程有理数的简单证明，并自动查找上面给出的简单引理的证明？
3. 有处理涉及有理数/实数的代数运算的论文/代码示例吗？

任何形式的帮助将不胜感激。

希望大家度过愉快的一天！

Answer 1

我知道您正在寻找一种我不知道的自动化策略，但是库中有引理，了解如何使用“搜索”命令查找它们非常重要。您可以查询其中出现的模式、名称的一部分等。非常方便。我搜索了与

Search (_ %Q <= _ -> _).

和

Search (1 %Q * _).

相关的定理（

%Q

将其标记为

Q

类型），发现了两个有用的定理。删除示例中未使用的变量可以证明：

Require Import QArith.

Lemma foo (a b:Q) (H: 0 < b <= a): 1 <= a/b. 
    intros; apply Qle_shift_div_l; rewrite ?Qmult_1_l; apply H. 
Qed.