我有以下Coq程序试图用auto证明n <= 2^n：
(***********)
(* imports *)
(***********)
Require Import Nat.
(************************)
(* exponential function *)
(************************)
Definition f (a : nat) : nat := 2^a.
Hint Resolve plus_n_O.
Hint Resolve plus_n_Sm.
(**********************)
(* inequality theorem *)
(**********************)
Theorem a_leq_pow_2_a: forall a, a <= f(a).
Proof.
auto with *.
Qed.
我期望Coq成功或陷入困境。但它立即返回。我在做什么错？
编辑我添加了Hint Unfold f.，并增加到100但我看不到debug auto 100进行的任何展开：
(* debug auto: *)
* assumption. (*fail*)
* intro. (*success*)
* assumption. (*fail*)
* intro. (*fail*)
* simple apply le_n (in core). (*fail*)
* simple apply le_S (in core). (*fail*)
编辑2我要添加手动证明以证明其复杂性：
(**********************)
(* inequality theorem *)
(**********************)
Theorem a_leq_pow_2_a: forall a, a <= f(a).
Proof.
induction a as[|a' IHa].
- apply le_0_n.
- unfold f.
rewrite Nat.pow_succ_r.
* rewrite Nat.mul_comm.
rewrite Nat.mul_succ_r.
rewrite Nat.mul_1_r.
unfold f in IHa.
rewrite Nat.add_le_mono with (n:=1) (m:=2^a') (p:=a') (q:=2^a').
-- reflexivity.
-- apply Nat.pow_le_mono_r with (a:=2) (b:=0) (c:=a').
auto. apply le_0_n.
-- apply IHa.
* apply le_0_n.
Qed.
此策略实施类似于Prolog的解决程序来解决当前目标。它首先尝试使用假设策略解决目标，然后使用简介将目标简化为基本目标，并引入新生成的假设作为提示。然后，它查看与目标的开头符号关联的策略列表，并尝试应用其中的一种（从成本较低的策略开始）。此过程将递归应用于生成的子目标。
也请参阅警告：
[
auto使用较弱版本的Apply，它更接近简单Apply，因此，即使手动应用其中一个提示会成功，预计有时auto也会失败。
最后，搜索深度默认限制为5；您可以使用auto num进行控制。
因此，在任何时候，当前目标的“与头部符号关联的策略”均未取得任何进展，auto将失败。如果auto达到最大深度，它将失败。
请注意，auto不会自动应用unfold战术。如果a <= f(a)不透明，就无法解决f，没有进一步的假设。如果需要，可以使用Hint Unfold f或Hint Unfold f。
您执行的手动打样说明了为什么Hint Transparent f无法做到。您通过归纳做了证明，然后进行了一些重写。 Hint Transparent f策略不允许自己采取这种步骤。
战术auto用于在手动证明仅使用带有受限定理的auto的情况下寻找证明。在这里，定理的限制集取自auto提示数据库。为了简洁起见，假设此数据库仅包含apply，core，le_S和le_n。
为简单起见，假设我们使用目标plus_n_O。该语句的主要谓词为plus_n_Sm，因此该策略将仅查看其主要语句由a <= 2 ^ a表示的定理。这排除在外_ <= _和_ <= _。您添加这些内容的主动性无济于事。
[如果我们查看plus_n_O，则语句为plus_n_Sm。如果我们用模式变量代替通用量化，则该模式为le_n。这与forall n : nat, n <= n统一吗？答案是不。因此，?1 < ?1不会使用该定理。现在，如果我们查看a <= 2 ^ a，则主体语句的模式为auto。用le_S统一此模式，这将需要?1 <= S ?2为a <= 2 ^ a。现在?1的值是多少？我们需要在符号上比较表达式a和?2。在左侧，根据您希望如何看待它，功能符号为2 ^ a或S ?2，但无论如何不是_ ^ _。因此，2 ^ _认识到这些功能不相同，引理不能适用。 S失败。
[我重复：给定目标时，auto首先仅查看目标的头部符号，然后从其数据库中选择实现该头部符号的证明的定理。在您的示例中，标题符号为auto。然后，仅查看这些定理的结论，并检查结论是否在语法上与当前目标相匹配。如果匹配，则应该为定理的普遍量化变量提供值，而定理的前提是应在较低深度处解决的新目标。正如@Elazar所提到的，默认情况下，深度限制为5。
auto指令仅在定义以下形状后才有用：
_ <= _然后，Hint unfold将有助于确保Definition myle (x y : nat) := x <= y.
的数据库定理也用于证明Hint Unfold myle : core.的实例，如以下示例所示（如果我们出现4次_ <= _，则会失败，因为深度限制）。
myle[请注意，以下语句在逻辑上是等效的（根据加法的定义），但不能由S证明。即使将Lemma myle3 (x : nat) : myle x (S (S (S x))).
Proof. auto with core. Qed.
添加为指令，这也无济于事，因为auto不是目标的开头符号。
Hint unfold plus : core.[我经常使用Coq的自动战术，例如plus，但我总是这样做，因为我可以预测目标是否属于该战术的预期范围。