Coq: goal is just a type (when using theorems with unnecessary arguments)

user_5036722 0
Viewed 61

I've discovered a weird quirk in Coq. It happens when you have a theorem with unnecessary arguments, and we use rewrite with this theorem. For example, consider the following code snippet.

Theorem foo : forall (k : nat) (x : bool), k=0+k.
Proof. reflexivity. Qed.

Theorem bar : forall (k : nat), 0+k=k.
Proof.
  intros k. rewrite foo. reflexivity.
  (* At this point, the goal is just "bool"! *)
Abort.

In this example, foo has a redundant argument x. Then, when I use rewrite foo in the proof of bar, it generates a goal which just reads "bool".

My first question is: why is such a goal generated?

Second, I've discovered that this goal can be completed using the assumption tactic. But, this doesn't really show how the goal is resolved. What other tactic could be used to complete such a goal?

coq-tactic coq arguments
2 Answers

The goal bool is created when you apply the rewrite foo. tactic. At that point you are asking Coq to find expression ek : nat and ex : bool so that the left hand side of foo ek ex occur in the goal. Using unification, Coq infers that ek := k is a reasonable choice, but it does not get any information for ex since the variable x does not appear in the codomain of foo. So it creates a fresh goal so that you as as user can fill the missing argument to foo.

Now, since that argument is actually unused you have various ways to discharge that goal: you can provide a concrete boolean exact true. or exact false, leave it to automation constructor. or use any boolean you have in your context (I'm actually a bit surprised by the behaviour of assumption is your context is closed as in your example).

You could also supply the argument before Coq creates a goal using rewrite (foo k true). for instance.

user_78074380

kyo answered your questions well, but I remember being confused about this, so here is some extra context:

In Coq, saying that X holds (as in, it was a goal and now it's proved) is the same as saying that there exists a term of type X (ie, X is inhabited). When X happens to be a logical formula (ie, when X : Prop), we expect to find it as a goal and to prove it using tactics. When X happens to be anything else (eg, bool), we expect to find it as a term and use it in definitions. However, there is nothing stopping you from using logical formulas in definitions (often leading to dependent types), proving a logical formula by explicitly providing a proof instead of using tactics (eg eq_refl : 0 = 0), or from showing that bool is inhabited using tactics.

The distinction is still useful because we often don't care which proof was used to show a given theorem, but we often do care which term of type bool we have in our hands (although not in your example).

user_23054580
Related