What is subgoal "nat"

Question

While trying to prove a lemma, I get to a situation where there is only one subgoal left, which is nat:

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

I'm confused as to what that means. What do I actually need to prove? Is there any documentation on the subject available (coq questions are incredibly hard to google)?

I don't want to share the actual lemma, because it's an assignment. Basically I'm trying to prove an inductive definition which is something like that:

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

In the proof I'm able to show that (forall x : nat, some_predicate x a). While the predicate some_predicate is only defined for nat, I suspect that the problem has something to do with the fact that the type of x is not explicitly stated in the definition of indef. Could this be the reason I'm seeing the nat subgoal`?

Answer 1

Here is an example, but I don't think it fits your use case. I have a function that produces a proof of a logical statement, but this function requires an integer. This integer is actually useless for the proof, but for typing reason, any use of this function will require this integer.

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

Lemma dummy_setup : True.
Proof. apply my_fun.

So at this point, the function my_fun requires an argument of type nat, which is not used anywhere else, but it needs to exist. The Coq system handles this argument as if it was a proof that is needed for logical purposes, so it requires that you given an element of this type. Often, this shows that you designed your functions in a poor way, and that they take arguments that they don't use. The way to avoid this is to go back to your lemmas, and make sure they don't have useless arguments.

Here is another example. The my_trans lemma takes a useless argument.

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.

When using this lemma, the need for the extra argument pops up. The proof machinery only expects me to show that there exists some natural number to fill in that spot.

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

The solution to your problem is to go and look at the theorem whose application triggered the appearance of this nat goal and to cleanup this theorem to remove the universally quantified variables that are actually not used.

Answer 2

As long as your lemma's result type is a Prop, Coq doesn't really care how you fill subgoals during its proof. By filling subgoals, you're essentially providing a value of that goal type.

Consider this:

If you encounter a goal True, you can explicitly fill the goal by providing a value of type True, namely I. In the tactic language, you could write:

1 subgoal
______________________________________(1/1)
True

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

No more subgoals.

Having a goal of type nat is just the same thing. Obviously, O is a value of type nat (and so is any natural number like 12432523547835), so you can fill the goal with it:

1 subgoal
______________________________________(1/1)
nat

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

No more subgoals.

---

Probably unrelated, but a goal or type nat or any other type totally makes sense in the context of "writing a definition in proof mode". For example, a function

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

can be defined this way (don't do this though, unless the target type is a complex dependent type and the result can't be easily stated in a classical way):

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

---

I think I once encountered the similar case when I was writing a proof for a well-founded recursive function and I somehow applied a wrong hypothesis (that is, the function being defined, which is not really a hypothesis) to the goal. But I could still complete the proof, and the defined function worked as expected.