如何使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

我没有勇气分析你冗长的证据，但我看到你选择使用正向证明风格。告诉标志是你的脚本中有几个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 (_ / _ <= _ / _).找到这样一个定理。唉，没有找到。所以我记得，除法通常被描述为乘法逆，所以我搜索另一种可能性Search (_ * _ <= _ * _).这给了我Qmult_le_compat_r。我尝试应用它，它的工作原理。

这就是我所说的落后证明的意思：我看结论，我认为什么定理可以帮助我得出这个结论？然后我会尝试满足它的条件。

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

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

所有这些都说，我不建议使用QArith进行数学推理（这里显示的代数推理类型），因为它的填充性不如其他库。如果你想使用它们的数字和理由，你应该使用math-comp或Reals：你会发现已经为你证明的更多定理。