Unable to unify "n * 0" with "0"

Question

I'm in the first chapter of Software Foundation. In my attempt to write a simple theorem as follows (It is just an implementation of the built-in theorem mult_n_O):

Theorem mult_n_O' : forall n : nat, 0 = n * 0.
Proof. intros n. reflexivity. Qed.

I got the error: Unable to unify "n * 0" with "0" At the reflexivity step. Can someone please explain the error and why I get this error when it is the exact same theorem as mult_n_O?

Answer 1

For Coq, n * 0 and 0 are different terms, which cannot be made equal by (syntactic) unification, hence the error message.

You can, however, prove this theorem by using induction on n, which is going to create two new goals, one for n = 0, and the other for "n + 1", i.e., S n or n.+1, assuming that the theorem holds for n(the induction hypothesis).

EDITED (answering comments)

A simple step-by-step solution can be as follows (I'm using ssreflect, where induction is performed via the elim tactic, but you should get the idea).

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Theorem mult_n_O' : forall n : nat, 0 = n * 0.
Proof. 
elim.
- by [].
- move=> n IH.
  by rewrite mulSnr -IH.
Qed.

Note the use of IH to rewrite n * 0 as 0.

Since ssreflect offers quite a bit of automation, this can be simplified to

Theorem mult_n_O'' : forall n : nat, 0 = n * 0.
Proof. by elim. Qed.

Answer 2

The fact that mult_n_O exists makes that your theorem is provable. But there are several ways to prove different statements. The tactic reflexivity can only be used when the two members of an equality are the same modulo the intrinsic computation rules. In the case of your statement, no computation rule makes it work, so reflexivity fails.

What are the intrinsic computation rules? They trace back to how multiplication was defined, and I don't wish to dwell on this here. You should read the software foundations further.

But now, there is this theorem mult_n_O, how do we use it? It is shown in the software foundations book. The method to use it is rewrite (in you case you could also use apply).

The takeaway lesson: the point is not only to know what facts are true, but understand how these facts are provable from the basic definitions, or from other theorems that have already been proven. This "how" relies on several techniques, each of these techniques is embodied in one of these commands, named reflexivity or rewrite. It is better to understand what each of them does. The Software Foundations book does a good job of illustrating their use progressively.

There are also more powerful commands, that will try several methods to solve the problem. But the pedagogical process used in the book prefers to let you learn the basic tools first before getting acquainted with the powerful ones later. This pedagogical process makes you discover elementary ideas about what is a proof that will be useful in the long run.

Answer 3

reflexivity can prove things like 5 = 5 or a + b = a + b, that is, where both sides of the equal sign are syntactically equal.

Coq also allows eta expansion, i.e. unfolding of defintion, and beta reduction i.e. applying a lambda expression to an argument, when comparing if two terms are equal. This is called that the terms are convertible in the Coq world.

Now, back to your question, n * 0 and 0 are not convertible, so you need to prove that they are equal, which is called being propositionally equal.

Why are they not convertible? Well, if you expand * to mult to get mult n 0 and replace mult with its definition, which is

Definition mult := fix mul n m := match n with 0 => 0 | S n' => m + mul n' m end.

you have

(fix mul n m := match n with 0 => 0 | S n' => m + mul n' m end) n 0

and next do beta reduction (applying the lambda on its args), you (kind of) get the term

match n with 0 => 0 | S n' => 0 + mul n' 0 end

which is not syntactically equal to 0.

And here the builtin equivalence check ("convertibility") stops. It does not have any way of simplifying the match n with ... any more. (The only way to do that is if the thing that was being matched on was an expression that reduced to something that starts with a constructor, not a function or a variable)

Since the convertibility check doesn't solve it, you have to come up with another way to prove the equivalence.

To do that, you have more powerful tools at your hands than plain convertibility. You can apply theorems (induction, or mult_n_0), fold expressions, etc. But that power means that it is hard to search for the proof automatically, and some ingenuity is needed.

There are of course some who have made tactics ("coq commands") with useful heuristics, that try a number of useful tricks that "often work", but reflexivity is not one of them. It just looks for convertibility (and a little more, which is besides the point here).

I hope this explains "why it doesn't work".