在试图证明引理时，我到了一个只有一个子目标的情况，即 nat：
1 subgoal
...
______________________________________(1/1)
nat
我对那意味着什么感到困惑。我实际上需要证明什么？是否有有关该主题的文档(COQ问题对于Google来说非常困难(？
我不想分享实际的引理，因为这是一项任务。基本上，我正在尝试证明归纳定义，这就是这样：
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定义，但我怀疑问题与indef的定义中未明确说明x的类型有关。这可能是我看到nat subgoal`？
这是一个示例，但我认为它不适合您的用例。我的功能可以产生逻辑语句的证明，但是此功能需要整数。该整数实际上是没有用的，但是出于打字原因，此功能的任何使用都需要此整数。
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目标的外观并清理该定理以删除实际未使用的普遍量化变量的定理。
只要您的引理结果类型是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
我认为，当我为有充分的递归功能的证据写出证据时，我曾经遇到过类似的情况，并且我以某种方式应用了错误的假设(即定义的功能，这不是真正的假设(。但是我仍然可以完成证明，并且定义的功能按预期工作。