如何使 Coq 中的代数运算更容易？

Question

我正在试验 Coq 的整数和有理数标准库。到目前为止，我的证明非常耗时而且看起来很糟糕。我想我错过了一些重要的证明技术。这样简单的引理不应该证明这么久。有什么提示吗？

这是一个例子：

Require Import ZArith.
Require Import QArith.
Open Scope Q_scope.

Theorem q_less: forall x y z, (0 <= x <= y)%Z -> x # z <= y # z.
Proof. intros. destruct H as [Hl Hr]. rewrite (Zle_Qle x y) in Hr.
       rewrite <- (Qmult_le_l (inject_Z x) (inject_Z y) (/ inject_Z (Zpos z))) in Hr. simpl in Hr.
       - rewrite Qmult_comm in Hr. rewrite Qmult_comm with (x := / inject_Z (Z.pos z)) in Hr.
         unfold inject_Z in Hr. unfold Qinv in Hr. destruct (Qnum (Z.pos z # 1)) eqn:ZV.
         + simpl in ZV. discriminate.
         + simpl in Hr. simpl in ZV. injection ZV. intro ZP. unfold Qmult in Hr. simpl in Hr.
           rewrite <- ZP in Hr. rewrite Z.mul_1_r in Hr. rewrite Z.mul_1_r in Hr. exact Hr.
         + simpl in ZV. discriminate.
       - unfold Qinv. simpl. apply Z.lt_0_1.
Qed.

Answer 1

我没有勇气分析你冗长的证明，但我看到你选择使用 forward 证明风格。警示标志是您的脚本中有多个 rewrite ... in ...。大多数定理库都设计为以向后证明方式工作。

将此与我对相同证明的建议进行对比：

Theorem q_less: forall x y z, (0 <= x <= y)%Z -> x # z <= y # z.
Proof.
intros x y z cmp; rewrite !Qmake_Qdiv.
apply Qmult_le_compat_r.
  rewrite <- Zle_Qle; tauto.
apply Qinv_le_0_compat; replace 0 with (inject_Z 0) by easy.
now rewrite <- Zle_Qle; apply Zle_0_pos.
Qed.

以下是我的处理方式。首先，x # z 是一种非常特殊的除法形式的符号：出现在基本分数中的除法。图书馆中的定理很可能没有很好地涵盖这种特定形式的除法，因此我选择用有理数之间的常规除法代替它。为了找到定理，我只使用 Search 查询和模式 (_ # _) (_ / _)。这给了我 Qmake_Qdiv.

那我就单纯的期望在合适的条件下有一个定理表达a <= b -> a / c <= b / c。我用Search (_ / _ <= _ / _).来求这样一个定理。唉，找到了none。所以我记得除法通常被描述为乘以倒数，所以我寻找另一种可能性 Search (_ * _ <= _ * _). 这给了我 Qmult_le_compat_r。我尝试应用它并且有效。

这就是我所说的向后证明方式的意思：我看着结论，我想 什么定理可以帮助我得出这个结论？然后我会尽量满足它的条件。

有两个条件。第一个是 (inject_Z x <= inject_Z y)。所以现在我需要一个定理，该定理通过函数 inject_Z 将 Z 中的比较和 Q 中的比较相关联。为了找到它，我输入 Search inject_Z (_ <= _). 这给了我 Qmult_le_compat_r。请注意，您的假设太强了：您不需要 x 为正。自动策略 tauto 从你的假设（我命名为 cmp）中获得正确的条件。

最后一个条件是(0 <= inject_Z (Z.pos z))。我可以重复使用与上面相同的定理，因为肯定 0 必须与 inject_Z 0.

相同

综上所述，我不建议使用 QArith 进行数学推理（您在此处展示的那种代数推理），因为它的数量不如其他库。如果您想使用数字并对其进行推理，您应该使用 math-comp 或 Reals：您会发现更多已经为您证明的定理。

如何使 Coq 中的代数运算更容易？

How to make algebraic manipulations in Coq easier?

rational-number

proof

coq