问题标签 [ltac]

我想为这些简单的推理规则提供 Ltac 策略。

在 Modus Ponens 中，如果我有H:P->Q和H1:P，Ltac mp H H1将添加Q到上下文中作为H2 : Q.

在 Modus Tollens 中，如果我有H:P->Qand H1:~Q，那么Ltac mt H H1将添加H2:~P到上下文中。

我已经写了一个用于 ponens 的方法，但它不适用于先例也是暗示的复杂情况。

Ltac mp H0 H1 := let H := fresh "H" in apply H0 in H1 as H.

编辑：我在另一个看似不相关的问题中找到了 Modus Ponens 的答案（在 Coq 中重写假设，保持暗示），其中“简化”版本apply是用generalize.

Ltac mp H H0 := let H1 := fresh "H" in generalize (H H0); intros H1.

不过，我仍然会感谢 Modus Tollens 的回答。

我经常需要做“归纳加载”来证明 Coq 中的目标，在 Coq 中我通过归纳同时证明多个事物。

问题是，我经常得到以下形式的归纳假设：

这很好，但是像这样的战术eauto真的不知道如何处理这样的事情，所以它大部分时间都会扼杀自动化。

我想知道的是，有没有办法自动将这样的前提分解成m不同的前提，即

我遇到的主要问题是我不知道如何匹配 LTac 中任意长度的箭头链。我可以硬编码到一定长度，但我希望有更好的方法。

此外，如果可以进行对偶（即拆分 Premise1 .. Premise_k 中的所有析取组合），那也是有用的。

我想要一个 Ltac 策略来完成 Disjunction Commutavity 的工作。主要是，如果我P \/ Q在某个假设的某个地方有一个子项H，Ltac Com H则会在上下文中添加Q \/ P另一个假设。

我尝试通过一个公理和apply它来提供交换规则；但它只适用于简单的假设，例如失败R -> (P \/ Q)；它应该添加到上下文中R -> (Q \/ P)。

有没有办法在 Ltac 程序的中间打印变量的值（无论是假设、策略、术语）吗？

我想系统地删除所有可能出现在我的假设和目标中的双重否定。我知道这~~A -> A不是直觉主义逻辑的一部分，但我所学的课程是经典的，所以我不介意。

我知道可以访问提到的公理，Coq.Logic.Classical_Prop.NNPP但是这个公理无助于从更复杂的句子中消除双重否定，例如说

H : ~ ~ A \/ (B /\ ~ C)

最好我希望能够应用 Ltac 策略，H这样它就会变成

H1 : A \/ (B /\ ~C).

非常感谢编写此类策略的任何帮助或任何其他建议。

我有两个假设，我想使用前向推理来应用一个同时使用它们的定理。

我的具体我有假设

我想应用标准库中的定理：

现在我知道我可以手动给出 x1、y1、x2、y2 的值​​，但我希望 Coq 在与H0和统一时自动确定这些值H1。我发现我可以让它像这样工作：

但这感觉就像一个 hack，对称性被破坏，try. 我真的很想能够说apply f_equals2_mult in H0, H1清楚或类似的东西。有没有这样的方法？

考虑以下示例：

apply H失败与

所以我知道我可以使用这种策略exists 1+2+3来申请在这里工作，或者，基于这个其他 stackoverflow 问题，有一种更复杂的方式来使用前向推理H将其变成存在形式。

但我希望有一些聪明的策略可以在统一时实例化存在变量，而不必明确？

如何rewrite ->仅应用定位子表达式？例如，考虑这个定理：

直观地说，它只需要交换一个(add a b)子表达式，但如果我这样做 rewrite -> (comm a b)，它会重写所有出现的情况。如何定位特定的子表达式？

match goal with当在用户定义的策略中进行模式匹配（with ）时，我们可以使用?x绑定一个 Gallina 术语，以便稍后我们可以引用它。我们可以在一个子句中使用多个这样的标识符 ( ... ?x ... ?y ...)，或者我们甚至可以使用相同的标识符 ( ... ?x ... ?x ...) 来指示为了使子句匹配，相同的 Gallina 术语必须出现在这两个位置。在某种程度上，这限制了与“相同”要求的可能匹配。这很方便，但也能够提出“不同”的要求会更方便（原文如此）。有没有办法编写一个匹配子句的形式... ?x ... ?y ...，我们要求受约束的术语?x是?y可区分的？

通过可区分我不一定意味着不相等，而只是不同（它们的名称[或表示]不重合）。例如，假设我有两个术语a,b:C。在我们可以证明命题的意义上，这两个术语可能相等a = b，但这与我的目的无关。彼此的区别和区别在于它们的名称不同a。b

那么，我可以通过提出两个元变量?x并且?y必须绑定不同的术语的要求来进行模式匹配吗？

把它放在某种上下文中，假设我们已经定义了对、投影，并且 letR是一些（适当类型的）二元关系。假设我在我的假设中以某种方式结束了以下两个。

我希望能够在我的策略中编写一个匹配子句，它只会匹配H而不匹配H'。有什么诀窍吗？

如果没有办法只匹配H，那么也许我可以匹配两者，我绑定a到?x和c（或再次a）到?y。但是，在匹配子句的右侧，我想执行一些“它们不同吗？ ”检查xandy并做idtac，以防两者在字面上绑定相同的术语。

Coq 有战术语言 Ltac 和匹配设施等等。Isabelle/HOL 是否有一些用于策略的编程语言以及解析、模式匹配等服务？我浏览了 Isabelle 的 Isar 参考手册和旧的 Pawlson 教程，但我找到了线索。