什么是子目标“nat”

Question

在尝试证明引理时，我遇到了只剩下一个子目标的情况，即nat：

1 subgoal
...
______________________________________(1/1)
nat

我对这意味着什么感到困惑。 我实际上需要证明什么？是否有任何关于该主题的文档（coq 问题很难用谷歌搜索）？

我不想分享实际的引理，因为这是一个作业。基本上我试图证明一个类似的归纳定义：

Inductive indef : deftype -> Prop :=
| foo x : indef (construct_0 x)
| bar a : (forall x, some_predicate x a) -> indef (construct_1 a).

在证明中我可以证明(forall x : nat, some_predicate x a)。虽然谓词some_predicate 仅针对nat 定义，但我怀疑问题与x 的类型未在indef 的定义中明确说明这一事实有关。 这可能是我看到nat 子目标的原因吗？

Answer 1

这是一个示例，但我认为它不适合您的用例。我有一个生成逻辑语句证明的函数，但是这个函数需要一个整数。这个整数实际上对证明没有用，但是出于打字的原因，任何使用这个函数都需要这个整数。

Definition my_fun (n : nat) : True := I.

Lemma dummy_setup : True.
Proof. apply my_fun.

所以此时，函数 my_fun 需要一个 nat 类型的参数，它不会在其他任何地方使用，但它需要存在。 Coq 系统处理这个参数就好像它是一个逻辑目的所需的证明，所以它要求你给定一个这种类型的元素。通常，这表明您以糟糕的方式设计了您的函数，并且他们接受了他们不使用的参数。避免这种情况的方法是回到你的引理，并确保它们没有无用的参数。

这是另一个例子。 my_trans 引理接受了一个无用的论点。

Require Import Arith.
Lemma my_trans : forall x y z t, x <= y -> y <= z -> x <= z.
Proof.  intros x y z; apply (le_trans x y z). Qed.

当使用这个引理时，需要额外的参数。证明机制只希望我证明存在某个自然数来填补那个位置。

Lemma toto x y z : y <= z -> x <= y -> x <= z.
intros h1 h2; revert h2 h1; apply my_trans.

您的问题的解决方案是查看其应用程序触发此nat 目标出现的定理，并清理此定理以删除实际未使用的普遍量化变量。

Answer 2

只要你的引理的结果类型是Prop，Coq 并不真正关心你在证明过程中如何填充子目标。 通过填充子目标，您实际上是在提供该目标类型的值。

考虑一下：

如果遇到目标True，可以通过提供True 类型的值，即I 来显式填充目标。在战术语言中，你可以这样写：

1 subgoal
______________________________________(1/1)
True

exact I.     (* explicit way, or  *)
constructor. (* less explicit way *)

No more subgoals.

拥有nat 类型的目标也是一样的。显然，O 是 nat 类型的值（任何自然数如12432523547835 也是如此），所以你可以用它填充目标：

1 subgoal
______________________________________(1/1)
nat

exact O.              (* this obviously works *)
exact 12432523547835. (* this does work too   *)

No more subgoals.

---

可能不相关，但目标或类型 nat 或任何其他类型在“以证明模式编写定义”的上下文中完全有意义。比如一个函数

Definition double (x : nat) : nat := x + x.

可以这样定义（但不要这样做，除非目标类型是复杂的依赖类型并且结果不能以经典方式轻松表述）：

Definition double (x : nat) : nat.

1 subgoal
x : nat
______________________________________(1/1)
nat

exact (x + x).  (* Fill the goal with desired value *)

No more subgoals.

Defined.      (* Use this instead of Qed to allow Coq to unfold the definition *)
Print double. (* Checking that the function body is correct *)

double = fun x : nat => x + x
     : nat -> nat

---

我想我曾经在为有充分根据的递归函数编写证明时遇到过类似的情况，并且我以某种方式将错误的假设（即，正在定义的函数，这不是真正的假设）应用于目标.但是我仍然可以完成证明，并且定义的函数按预期工作。