您如何查找Coq证明策略的定义或实施？

问题描述

我正在看this：

Theorem eq_add_1 : forall n m,n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
Proof.
intros n m. rewrite one_succ. intro H.
assert (H1 : exists p,n + m == S p) by now exists 0.
apply eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
Qed.

我如何找到像intros或destruct这样的东西准确，就像查找实现（或者，如果不可能的话，定义）一样？有效执行此操作的方法是什么？

解决方法

对于原始和用户定义的策略，答案有所不同。但是，您显示的证明脚本几乎不使用用户定义的策略，只有now是easy策略的一种表示法。

用于用户定义的策略。

对于定义为Ltac foo args := body.的战术，您可以使用Print Ltac foo（例如Print Ltac easy.）。 AFAIK，不适用于Tactic Notation.定义的策略在这两种情况下，我都希望查看源（我是通过grep找到的）。

用于原始战术

• 有Coq参考手册（https://coq.inria.fr/distrib/current/refman/coq-tacindex.html），它没有完整的规范，但通常是最接近的近似值。它不是很容易访问，因此您应该首先参考许多Coq教程或简介之一，例如Software Foundations。

• 有实际的Coq实施，但是除非您是Coq实施者，否则不会很有用。

,

正如Blaisorblade提到的那样，可能很难准确地理解策略的作用，并且更容易阅读参考手册以了解如何使用它们。但是，从概念上讲，策略并不那么复杂。通过Curry-Howard correspondence，使用与编写常规程序相同的功能语言来表示Coq证明。 intros或destruct之类的策略只是用这种语言编写程序的元程序。

例如，假设您需要证明A -> B。这意味着您需要编写功能类型为A -> B的程序。当您编写intros H.时，Coq将构建部分证明fun (H : A) => ?，其中?表示应为B类型的孔。同样，destruct在证明中添加一个match表达式以进行案例分析，并要求您为每个match分支生成证明。随着您添加更多策略，您将不断填补这些漏洞，直到获得完整的证明。

Coq的语言非常少，因此，策略只能用来建立证明：函数应用程序和抽象，构造函数，模式匹配等。原则上，可能只有少数几个的策略，对于Coq中的每个语法构造都是一个，这将使您能够构建 any 证明！我们之所以不这样做，是因为直接使用这些核心结构太低了，而战术则使用自动证明搜索，统一和其他功能来简化编写证明的过程。