有这个引理
Lemma my_lemma n : n %/ 4 * 4 + n %% 4 * 5 - n %% 4 * 4 = n.
Proof.
(* ? *)
(* n %/ 4 * 4 + n %% 4 = n. *)
symmetry. apply: divn_eq n 4.
Qed.
我怎样才能转换n %% 4 * 5 - n %% 4 * 4为n %% 4？然后将是小菜一碟。
问问题
78 次
1 回答
4
为了解决这个问题，ssreflect 中的惯用方法是使用所有关于算术的定理进行重写。这需要一点搜索。我建议您Search广泛使用该命令。
第一个障碍是您的公式包含(A + B - C)与 不同的东西(A + (B - C))，因为截断减法的特殊行为。要在两者之间进行转换，您可以寻找一个定理。我输入了以下Search命令。
Search (_ + _ - _).
在列出的定理中我很满意addnBA（加减法之间的关联性），但是这个引理有一个附带条件，我想首先证明它。所以我使用下面的重写命令。
rewrite -addnBA; last first.
在这里，我想在比较中排除乘法。Search我使用以下命令查找包含此模式的定理。
搜索 _ (_ * _ <= _ * _)。
请注意_该命令中的第一个模式Search，很重要，如果不包含它，只会列出一些有趣的定理，而我们想要的不会出现。我想要的是leq_mul2l
我以以下方式执行此证明：
by rewrite leq_mul2l orbC.
在rewrite leq_mul2l语句是_ || _语句（布尔析取）之后，右边显然是真正的模计算（in ssreflect），通过对换这个布尔析取，我使得目标可以直接解决，无需多言。
现在，我们来讨论乘法对减法的分布。在这里，搜索命令使用起来更加棘手，因为分配律是用关键字处理的。
Search (_ * (_ - _)).
没有给出任何有用的结果，但有ssrnat关于命名模式的有用文档。它告诉我们，当减法是二次运算时，那么B很可能出现在定理名称中。这里我们想要一个关于自然数的定理，所以它应该在 中ssrnat，所以我尝试以下。
Search "B" in ssrnat.
这告诉我，有些定理的陈述依赖于 和 之类的left_distributive概念right_distributive。您可以通过打印这些概念来理解这些概念。
Print right_distributive.
从长远来看，你往往会记住你经常使用的定理的名称，所以在我的例子中，我知道我会使用mulnBr，因为减法在乘法的右边，我们正在使用自然数。math-comp 库的设计非常注重命名的规律性。
所以我们现在可以通过以下方式完成修改：
rewrite -mulnBr muln1.
你终于可以应用你想要应用的引理。
完整的脚本如下：
Lemma my_lemma n : n %/ 4 * 4 + n %% 4 * 5 - n %% 4 * 4 = n.
Proof.
symmetry.
rewrite -addnBA; last first.
by rewrite leq_mul2l orbC.
rewrite -mulnBr muln1.
apply: divn_eq n 4.
Qed.
于 2019-12-12T08:25:33.163 回答