Coq auto tacitc 失败

Question

我有以下 Coq 程序试图用自动证明 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 要么成功，要么在尝试中受阻。但它立即 returns。我做错了什么？

编辑我添加了 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.

Answer 1

来自documentation：

This tactic implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the assumption tactic, then it reduces the goal to an atomic one using intros and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals.

此外，请参阅此处的警告：

auto uses a weaker version of apply that is closer to simple apply so it is expected that sometimes auto will fail even if applying manually one of the hints would succeed.

最后，搜索深度默认限制为5；你可以使用 auto num.

来控制它

因此，如果在任何时候，当前目标的 "tactics associated to the head symbol" 的 none 取得任何进展，auto 将失败。如果 auto 达到最大深度，它将失败。

请注意 auto 它不会自动应用 unfold 策略。没有进一步的假设，当 f 不透明时，无法解决 a <= f(a)。如果需要，可以使用 Hint Unfold f or Hint Transparent f.

Answer 2

您执行的手动证明解释了为什么 auto 不能这样做。您通过归纳法进行了证明，然后进行了一些重写。 auto 策略本身不允许这种步骤。

如果手动证明仅使用 apply 和有限的定理集，策略 auto 旨在找到证明。这里的定理限制集取自 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 失败。

我再说一遍：当给定一个目标时，auto首先只看目标的头符号，然后从它的数据库中选择证明这个头符号的定理。在您的示例中，头部符号是 _ <= _。然后它只查看这些定理的结论，并检查结论在句法上是否与手头的目标相匹配。如果它确实匹配，那么这应该为定理的普遍量化变量提供值，并且定理的前提是应该在较低深度解决的新目标。正如@Elazar 所提到的，深度默认限制为 5。

仅当您定义了以下形状时，Hint unfold 指令才有用：

Definition myle (x y : nat) := x <= y.

然后 Hint Unfold myle : core. 将有助于确保 _ <= _ 的数据库定理也用于证明 myle 的实例，如下例所示（如果我们失败由于深度限制，出现 4 次 S。

Lemma myle3 (x : nat) : myle x (S (S (S x))).
Proof. auto with core.  Qed.

请注意下面的陈述在逻辑上是等价的（根据加法的定义）但不能被auto证明。即使您添加 Hint unfold plus : core. 作为指令，这也无济于事，因为 plus 不是目标的头部符号。

Lemma myleplus3 (x : nat) : myle x (3 + x).
Proof.
auto. (* the goal is unchanged. *)
simpl. auto.
Qed.

我经常使用 Coq 的自动策略，例如 lia，但我总是这样做，因为我可以预测目标是否在策略的预期范围内。

Coq auto tacitc 失败

Coq auto tacitc fails

coq

coq-tactic