How does one know what statements in Coq require Induction?

Question

I was trying to learn Coq using the famous book Software Foundations. In it I found the following:

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  induction n as [| n IHn].
  - simpl. reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

which I understand perfectly but find rather unintuitive. I understand perfectly how each step works but it would have never occurred to me to use induction to prove such a trivial fact. In fact in the mathematical proof I had in mind that would have been a fact/property (or I guess an axiom) of 0. i.e. $\forall n \in N, n \cdot 0 = 0$ is true by definition. I guess in Coq (or the way we set up numbers? thats not true).

My biggest complaint or worry is that if such a trivial thing requires induction I feel now I am unable to recognize what needs induction (at least in Coq). I know it needs it here because I am in the induction chapter. But in normal maths its usually quite obvious because the problem is obviously recursive. But I wouldn't have really thought of that proposition as recursive. For example it goes on to prove more things as exercises:

Theorem plus_n_Sm : ∀n m : nat,
  S (n + m) = n + (S m).
Proof.
  (* FILL IN HERE *) Admitted.
Theorem plus_comm : ∀n m : nat,
  n + m = m + n.
Proof.
  (* FILL IN HERE *) Admitted.
Theorem plus_assoc : ∀n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  (* FILL IN HERE *) Admitted. 

which I am sure are not too difficult, but my worry is that in isolation I would have never thought such trivial statements required something as sophisticated as induction. I didn't even learn induction until last 2 years of highschool and didn't really do it seriously until college. So now I see trivial statements requiring what seems to me, sophisticated mathematics.

I just feel my intuition got really lost. When I do Coq proofs (in isolation), how do I know when to use induction and on what? I doubt there is a general procedure (of course) but proofs do exist. So there must be something guiding us to use induction in Coq.

Answer 1

Coq allows one to prove mathematical theorems in a completely formal way. At first, this copes with our experience of doing maths, which is far more informal.

Most of the time, people doing maths are not exposed to mathematical logic. They do not know, for instance, how to define the set of real numbers. Or even the set of natural numbers. Numeric sets are simply taken for granted, together with their operations and related properties. On top of these "basic facts" people build more complex theorems. Essentially, the "basic facts" are used as if they were axioms.

Note that one could work at a similar level in Coq, if one wishes. One can import the Arith Coq library, which provides the basic facts of arithmetics, and exploit those.

However, the underlying logic of Coq does not take those properties for granted. The type of natural numbers, for instance, is not a primitive concept in the logic, but rather something which is defined using induction. Since that makes nat an inductive type, virtually every proof about naturals will require induction. (This also holds in set theory, e.g. Zermelo-Fraenkel, where naturals are also defined in a sort-of inductive way.)

Arithmetical operators are also defined using induction. Using a simplified syntax, one could define multiplication as

x * 0     = 0
x * (S y) = x + (x * y)

or, alternatively,

0 * x     = 0
(S y) * x = x + (y * x)

Both definitions are equivalent. However, using the first one will result in us being able to prove x * 0 = 0 "without induction" -- it follows by definition. In Coq, we can simply write reflexivity and let the system expand the definition for us.

By comparison, 0 * x = 0 is not a trivial equation which follows from the definition: to expand the definition we need to know what is the second argument of the multiplication, but here it's merely an unknown x. Hence, for this we do need induction over x. There's no way around that.

Note that, if we used the second definition instead, we would prove 0 * x = 0 immediately, and instead require induction for x * 0 = 0. So, no definition is strictly better than the other one.

Answer 2

As the others have mentioned, in Coq's standard library (or typical presentations of naturals in Coq), naturals are defined inductively, usually a la Peano. We could make other choices, e.g. one could imagine defining naturals as the free semiring on one generator which would give you many of the "axiomatic" facts for "free". (Well, you'd have to prove them about general rings...)

For any inductively defined type, T, whenever you want to prove a statement of the form forall x:T, P(x) you will need to use induction on T unless the proof doesn't actually depend on T, i.e. it is parametric, e.g. forall x:T, x = x. In fact, all proofs of this form can be written as an induction, they may just be a trivial induction. Often the induction will be hidden away in some lemma.

However, the key concept it seems you are unfamiliar/uncomfortable with is the notion of definitional equality in intensional dependent type theories like Coq. Let's say you state that $2$ means $1+1$. If you then ask whether $2=1+1$ there are no steps of proof required. You simply substituted the meaning of $2$ and see that $1+1=1+1$ which is true by reflexivity. More generally, (closed) terms in Coq have normal forms, and Coq treats any two terms with the same normal form as identical. This is definitional equality. Reducing to that normal form may involve large amounts of computation, but there is no proof rule that to tell Coq to reduce a term to normal form. It just does it in the background as necessary to perform type checking. Definitions, such as the one for multiplication reproduced below:

Fixpoint mul n m :=
  match n with
  | 0 => 0
  | S p => m + p * m
  end
where "n * m" := (mul n m) : nat_scope.

introduce new (non-normal) terms and new computational rules for normalizing them. In this case, it adds a rule that says 0 * x = 0. These follow from the generic rules for Fixpoint and match for the Coq type theory. If you were to ask whether forall x:nat, 0 * x = 0, Coq sees forall x:nat, 0 = 0 since 0 is the normal form of 0 * x. There is no computational rule saying how x * 0 should be reduced when x is a variable, so the "normal" form of x * 0 is x * 0. With this understanding, it is much easier to see why and how induction helps in this particular case. When we do induction, we get two new problems: 0 * 0 = 0 and (S p) * 0 = 0 which allows steps of computation to be performed. In the latter case, we get 0 + p * 0 which then leans on the computation rules induced by the definition of natural number addition, but also leaves us with n * 0 which requires the induction hypothesis to resolve.

At more advanced levels of proof engineering, it is common to try to set up definitions so that a decent amount of work can be done by this implicit computation mechanism. Extreme forms of this are reflection principles where we prove an implementation of a decision procedure correct after which we can simply run it and appeal to this result to prove other results. Techniques like this are behind things like the ring solver and ssreflect.

Answer 3

To see how you can prove something about natural numbers, you must know what you know about natural numbers. Usually, we learn all sorts of 'basic facts' about numbers in high school that are pretty much given without further proof, which we can use later to prove more interesting statements about numbers.

In most mathematical disciplines, this 'naive' approach to numbers is fine. However, when we care about the formalization of numbers, we want a 'minimal definition' of what a number (and related concepts such as successors, predecessors and arithmetic) is and prove all 'basic facts' from them.

So, in the book you're reading, all we know about numbers is the following definition:

   Inductive nat : Type :=
     | O
     | S (n : nat).

That is, natural numbers are an inductive type, defined as either the natural number O or the successor of a natural number. This is the reason why we do proofs by induction: it is all we know about the natural numbers in this setting.

---

So, where did your intuition let you get lost? When learning mathematics, you get taught that 'basic facts' about numbers early on, which therefore seem easy and get taught induction fairly late (and when you actually have to prove things!) which makes it seem hard.

What is actually the case is that, from a viewpoint of formalisation, induction is the one fundamental property of natural numbers! The best way to see this is that, in fact, all other properties of natural numbers follow from it.

My final advice is not to worry. The fact that all 'basic facts' are suddenly not as basic as they may have seemed so far can be intimidating, but this is simply what formalisation is about: having rigid constructions for 'basic facts'. Once you have these in place, you can prove more complicated statements as usual, by relying on the 'basic facts' just proven.

Answer 4

I want to share my own experience of learning Coq and theorem proving in general.

Most of the time, the proof of a statement largely depends on the recursive structure of the function or operation at hand. IMHO it is even more important than the recursive structure of data types.

Again, let's look at multiplication of natural numbers.

Fixpoint mul n m :=
  match n with
  | 0 => 0
  | S p => m + p * m
  end
where "n * m" := (mul n m) : nat_scope.

Theorem mult_0_r : forall n, mul n 0 = 0.

(Before you write a proof, just focus on the definition of the function, and ignore what it means as a number operation.)

The definition of mul matches on the structure of n, then, if n = S p, recursively calls itself with p. The structure is the strong sign that you'll need induction on the first argument of mul. On the other hand, you won't need to do induction on the second argument, or even destruct, simply because it's not pattern-matched inside mul.

This applies to more complex statements as well. Say we were to prove distributivity of multiplication over addition:

Theorem mult_distr_plus_r : forall n m p, (n + m) * p = n * p + m * p.

And suppose that we know both plus and mult are recursive on the first argument. In this case, the natural choice to do induction on is n because, by its positions, destructing n gives the largest amount of expansion (three times in total):

(S n + m) * p = S (n + m) * p = p + (n + m) * p
S n * p + m * p = (p + n * p) + m * p

It's easy to see that you can complete this proof by IH and plus_assoc.

In contrast, destructing m gives just one, and p gives none, so you'll need more lemmas to complete the proof (e.g. plus_n_Sm, plus_comm if you destruct m, mult_n_Sm in addition if you destruct p).

(n + S m) * p = ?
n * p + S m * p = n * p + (p + m * p)

(n + m) * S p = ?
n * S p + m * S p = ?

---

Here's another example to show that proof by induction depends on the function structure. Suppose we have the Fibonacci function:

Fixpoint fib n :=
  match n with
  | 0 => 0
  | 1 => 1
  | S (S p) => fib p + fib (S p)
  end.

Then we want to prove some property on it, say it gives the same result as another definition of Fibonacci.

Theorem fib_is_fib' : forall n, fib n = fib' n.

Now, the recursive structure of fib is more complicated than mul above. It has two base cases, and the result of fib (S (S p)) depends on both fib p and fib (S p). If you try good ol' induction (with tactic induction n.) on it, you immediately fail.

In order to prove a property of fib, you actually need a stronger induction principle:

• Given a property P on natural numbers, if all of the following holds:
  • P holds for 0.
  • P holds for 1.
  • If P holds on n and S n, it holds on S (S n).
• Then P holds on all natural numbers.

In Coq:

Theorem nat_ind_fib :
  forall P : nat -> Prop, (* For a given property P, *)
  P 0 ->                  (* if P holds for 0 *)
  P 1 ->                  (* and 1, *)
  (forall n : nat, P n -> P (S n) -> P (S (S n))) ->
                          (* and `P n` and `P (S n)` implies `P (S (S n))` *)
  forall n : nat, P n.    (* then P holds for all n. *)

Now we can prove a property on fib by induction using tactic induction n using nat_ind_fib.