Induction.v

In this chapter we quickly go over proofs by induction. We introduce the induction and assert tactics. Finally, having now been familiar with Coq proofs, we reflect on the differences between formal and informal mathematical proofs.

So far, we’ve done proof by simplification, rewriting, case analysis – done using several tactics: reflexivity, simpl, intro, rewrite, destruct.

We have learnt how to close goals by reflexivity, introduce variables and hypotheses, use previous theorems and assumptions, advance the proof by simplifying (computation), and break down goals into subgoals by casing on type constructors.

We have also briefly learned how to unfold, and how to deal with contradictions.

In this chapter, we will learn a classic proof technique: induction.

From the chapter:

Recall (from a discrete math course, probably) the principle of induction over natural numbers: If P(n) is some proposition involving a natural number n and we want to show that P holds for all numbers n, we can reason like this:

• show that P(O) holds;
• show that, for any n', if P(n') holds, then so does P(S n');
• conclude that P(n) holds for all n.

In Coq, the steps are the same: we begin with the goal of proving P(n) for all n and break it down (by applying the induction tactic) into two separate subgoals: one where we must show P(O) and another where we must show P(n') -> P(S n').

The induction tactic is quite straightforward. It also takes an as annotation - setting the variable names for the “next element” in the inductive step and the induction hypothesis.

Theorem minus_n_n : forall n,
  minus n n = 0.
Proof.
    intros n. induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite -> IHn'. reflexivity.
Qed.

Note that intros n is redundant here - induction n ... already introduces n to the context.

We can use the assert tactic in order to create an anonymous “sub-theorem” within a proof.

This mimics “informal” mathematics, where large proofs are broken into a sequence of theorems – and some of these theorems will be too trivial or of little general interest to bother giving it a name.

Theorem mult_0_plus' : forall n m : nat,
  (n + 0 + 0) * m = n * m.
Proof.
  intros n m.
  assert (H: n + 0 + 0 = n).
    { rewrite add_comm. simpl. rewrite add_comm. reflexivity. }4
  rewrite -> H.
  reflexivity.  Qed.

Too often, rewrite applies rewrites in unintended places.

Here, we want to prove that (n + m) + (p + q) = (m + n) + (p + q). The only difference between the two sides of the = is n + m vs. m + n – it would be enough to use commutativity of addition: add_comm. But there are three uses of + here, and it turns out that rewrite -> add_comm will target the outer + and not what we wanted: (n + m).

To get through this, we use assert to create a local lemma stating that n + m = m + n, and then rewrite the original equation with the lemma.

Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  assert (H: n + m = m + n).
  { rewrite add_comm. reflexivity. }
  rewrite H. reflexivity.  Qed.

An alternative to assert is replace.

The replace tactic allows you to specify a particular subterm to rewrite and what you want it rewritten to: replace (t) with (u) replaces (all copies of) expression t in the goal by expression u, and generates t = u as an additional subgoal. This is often useful when a plain rewrite acts on the wrong part of the goal.

Informal proofs are algorithms; formal proofs are code.

What counts as a proof of a mathematical claim? This has been a question philosophers have been debating - the authors argue that a proof is an act of communication (to instill in the audience the certainty that P is true).

The authors continue the communication analogy:

Authors communicate to their readers. The reader can be a human person, or it could be a program like Coq.

Proofs for humans will be written in natural language, and is therefore informal. Even though such mathematical proofs may be considered “rigorous”, the fact that they are in natural language, which has a lot of ambiguityl, means that such proofs are informal by nature. A formal proof uses formal language, and sticks closely to a well-established syntax and semantics.

There are also different kinds of math readers depending on their expertise. As proofs are an act of communication, and communication depends on context, (informal) proofs can be written in different styles or phrasings to accomodate their audience.

An excerpt for the different kinds of audiences:

(…) A “valid” proof is one that makes the reader believe P. But the same proof may be read by many different readers, some of whom may be convinced by a particular way of phrasing the argument, while others may not be. Some readers may be particularly pedantic, inexperienced, or just plain thick-headed; the only way to convince them will be to make the argument in painstaking detail. But other readers, more familiar in the area, may find all this detail so overwhelming that they lose the overall thread; all they want is to be told the main ideas, since it is easier for them to fill in the details for themselves than to wade through a written presentation of them.

The following is the most important point about informal proofs.

Ultimately, there is no universal standard, because there is no single way of writing an informal proof that is guaranteed to convince every conceivable reader.

Proofs written for “machines” like Coq, i.e. formal proofs, are mechanically derived from a certain set of formal logical rules (which?), and the proof is a recipe that guides the program in checking this fact.

A formal proof carries in it a mechanical way of verifying that the proof holds.

Formal proofs are useful in many ways, but they tend to not be very efficient ways of communicating ideas between human beings.

From https://en.wikipedia.org/wiki/Proof_theory#Formal_and_informal_proof:

Formal proofs are constructed with the help of computers in interactive theorem proving. Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, whereas finding proofs (automated theorem proving) is generally hard. An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain errors.

• Total Points: 27/39

The chapter was pretty straightforward. I like the section on formal versus informal proofs. I like reading about metamathematics.

This book, and the course infrastructure, is excellent. There’s a pretty book online, but the better way to learn is by going through the Coq files - the book is derived from the Coq files which have comments.

The exercise notes were created by LLM this time, and so were the exercise scores. I don’t think I lose much by doing so – because if there was something particularly note-worthy about the exercise, I would write it down myself.

The generated notes are still useful for reference.

The discussion on formal vs informal proofs reminds me of de Bruijn’s vision for the Automath project, which I have written about before. Well, it reminds me of the linguistic turn and analytic philosophy and so on. The Logicomix story.