1

我正在尝试使用 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.
4

1 回答 1

2

我没有勇气分析你冗长的证明，但我看到你选择使用前向证明风格。明显的迹象是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带有 patterns 的查询(_ # _) (_ / _)。这给了我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-compor Reals：您会发现更多已经为您证明的定理。

于 2019-03-29T16:01:08.940 回答