您如何查找CoQ证明策略的定义或实施？ [英] How do you lookup the definition or implementation of Coq proof tactics?

问题描述

我正在查看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教程或简介中的一个，如软件基础。

• 有实际的Coq实现，但除非您是Coq实现者，否则帮助不大。

这篇关于您如何查找CoQ证明策略的定义或实施？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！