我正在看this https://github.com/coq/coq/blob/cdfe69d6da6b32338ba74c9f599c74389089c9dd/theories/Numbers/Natural/Abstract/NAdd.v#L49-L57:
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 or destruct mean exactly，比如查找实现（或者如果不可能，则查找定义）？有什么方法可以有效地做到这一点？
对于原始策略和用户定义的策略，答案是不同的。但是，您显示的证明脚本几乎没有使用用户定义的策略，除了now，这是一个符号easy tactic.
如果您不确定某种策略是否原始，请同时尝试两种策略；检查手册可能是最简单的第一步。
用于用户定义的策略。
对于定义为的策略Ltac foo args := body.您可以使用Print Ltac foo (e.g. Print Ltac easy.）。 AFAIK，这不适用于由Tactic Notation.在这两种情况下，我更喜欢查看来源（我通过grep).
对于原始战术
-
有 Coq 参考手册（https://coq.inria.fr/distrib/current/refman/coq-tacindex.html https://coq.inria.fr/distrib/current/refman/coq-tacindex.html），它没有完整的规范，但通常是最接近的近似值。它不是很容易理解，因此您应该首先参考众多 Coq 教程或介绍之一，例如 Software Foundations。
-
有实际的 Coq 实现，但除非您是 Coq 实现者，否则这不是很有帮助。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
