查找重写规则

如何解决查找重写规则

我很难找到适合我的情况的可用重写规则。由于我不想为每个重写问题打扰您，我想知道您是否有一些寻找合适的重写规则的技巧？

您是否有任何关于如何解决和/或搜索重写以下示例的提示：

1 subgoal
H: P
H0: Q
__________
R

说我有Lemma Join: P /\ Q = R 为了进行这种重写，我想我需要先将 H 和 H0 重写为 P /\ Q。 那么对于这种情况，您将如何解决或找到重写规则？

另一个例子

H: a <= b
____________
b < a

我相信应该存在一些交换性重写规则，但我怎样才能最好地找到这个规则？

非常感谢！

解决方法

首先是一个提示，这样您以后就不会遇到这个问题：不要将类型的相等性与逻辑等价性混淆。在上面的第一个示例中，您通常指的是 P/\Q <-> R，而不是类型 P/\Q 在定义上与 R 相同。

关于您关于在图书馆中寻找引理的问题；是的，能够在那里找到东西非常重要。 Coq 的 Search 命令可让您找到所有 (Required) 引理，其中包含某个特定模式或某个特定字符串。后者很有用，因为库往往有一个有点可预测的命名方案，例如关于可判定性的引理的名称通常包含字符串“dec”，交换性引理通常被称为带有“comm”等的东西。

例如，尝试搜索有关整数的可判定性引理，即在其中某处具有术语 Z 且名称包含字符串“dec”的引理。

Require Import ZArith.
Search "dec" Z.

回到你的问题；在你的情况下，你想找到一个以“something and something”结尾的引理，所以你可以使用模式 ( _ /\ _ )

Search ( _ /\ _ ).

然而，你得到了非常多的点击，因为许多引理以“something and something”结尾。

在您的特定情况下，您可能希望将搜索范围缩小到

Search (?a -> ?b -> ?a /\ ?b).

但是当你使用模式变量时要小心，因为也许你正在寻找的引理有其他顺序的参数。

在这种特殊情况下，您找到了引理

conj: forall [A B : Prop],A -> B -> A /\ B

这不是真正的引理，而是归纳类型的实际构造函数。它只是一个函数。请记住，类型论中的每个定理/引理等都是“只是一个函数”。甚至重写也只是函数应用。

无论如何，认真对待学习寻找引理和阅读 Search 输出的任务。它会对你有很大帮助。

顺便说一句，模式匹配语法类似于术语语法，但带有漏洞或变量，您在编写 Ltac 策略时也会使用它们，因此出于多种原因了解它很有用。