Software Foundations Reading Note 2: Proof by Induction

Yuchong Pan edited this page Sep 3, 2018 · 41 revisions

Overview

This module mainly introduces proof by induction in Coq. In addition to that, it talks about Coq's syntax for proofs within proofs, and about formal vs. informal proofs.

Proof by Induction

Proof by induction is an important proof technique that is commonly used in mathematics. It is used to prove that a property holds for every natural number . It follows from the principle of mathematical induction, which states:

If

  • holds, and
  • holds assuming that holds for some natural number ,

then holds for every natural number .

Hence, proof by induction consists of two steps:

  1. The base case: prove that holds for the first natural number. Usually, or . More generally, the first natural number can be taken as any arbitrary integer.
  2. The induction step (or inductive step): assume that holds for some natural number that is greater than or equal to the first natural number, and then prove that holds.

Here, the hypothesis that holds for some natural number in the induction step is called the inductive hypothesis.

As we may notice, recursion in mathematics / computer science has base cases and reductions, which are similar to base cases and induction steps in induction. As we will see, there are deep connections between recursion and induction.

Proof by Induction in Coq

In Coq, natural numbers are defined in the unary representation; i.e., a natural number is either zero (O), or the successor of a natural number (S n'). Hence, if we would like to prove in Coq that a property P(n) holds for every natural number n, we can state the proof as follows:

  • Prove that P(O) holds.
  • Prove that for any natural number n, if P(n) holds, then P(S n) also holds.

This exactly follows from the principle of mathematical induction. Coq provides a tactic induction for proof by induction. Consider the following theorem:

Theorem plus_n_O : ∀ n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

Like destruct, induction splits the argument n into two subgoals, as nat is defined by two cases, O and S n'. induction also takes an as ... clause separated by | to specify the names of introduced variables. Unlike destruct only introducing constructor parameters as variables, induction introduces both constructor parameters and inductive hypotheses.

In the above example, the first subgoal corresponds to the base case of the proof by induction, where we need to prove that the theorem holds for n = 0 (i.e. 0 + 0 = 0). This can be directly proved by simplification. No new variables are introduced, as the constructor O does not take any parameters.

The second subgoal of the above example corresponds to the induction step of the proof, where n's are replaced with S n'; i.e., we need to prove that S n' = (S n') + 0. We also add the inductive hypothesis n' = n' + 0 to the context and name it IHn'. To prove the subgoal, we first simplify the subgoal to S n' = S (n' + 0) by the definition of +. Then, the inductive hypothesis n' + 0 = n' is applied to the subgoal, rewriting n' + 0 to n' and yielding S n' = S n'. This directly follows by reflexivity.

As an aside, intros in the above example is actually redundant, because the induction tactic automatically moves the next variable from the goal to the context.

Proofs Within Proofs

The rewrite tactic in Coq is sometimes painful. From Coq's documentation, rewrite matches the first subterm in the goal, and replaces every recurrence of the matching subterm in the goal. However, sometimes we would like to rewrite a certain part in the goal with a theorem and a hypothesis.

Coq provides a convenient syntax (the assert tactic) to state and prove some miscellaneous results within a proof without giving it a top-level name. This can also be used to rewrite some certain parts in the goal. Consider the following theorem:

Theorem plus_rearrange_firsttry : ∀ n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).

An initial thought would be to rewrite the goal with the commutativity property of addition, which has been proved before. However, there are multiple occurrences of + in the goal, and Coq will first apply commutativity to the outer +, which yields (p + q) + (n + m) = (m + n) + (p + q). This is not what we want, as we only need to rewrite n + m to m + n. In this case, we can use assert to rewrite a certain part in the goal. Consider the following proof.

Theorem plus_rearrange : ∀ 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 → plus_comm. reflexivity. }
  rewrite → H. reflexivity. Qed.

Here, assert introduces two subgoals: the first is the assertion n + m = m + n, and the second is the original goal. We then prove the assertion in the curly braces; this directly follows from commutativity. As we name the assertion H, we can then rewrite the remaining goal by H. This converts (n + m) + (p + q) = (m + n) + (p + q) to (m + n) + (p + q) = (m + n) + (p + q), which directly follows from reflexivity.

Formal vs. Informal Proofs

I like the quote at the beginning of this section:

Informal proofs are algorithms; formal proofs are code.

It reminds me of a paper I read last year: Propositions as Types by Philip Wadler, who added generic types to Java. In the paper, the author connects proofs and programs by stating three claims: "propositions as types", "proofs as programs", and "simplification of proofs as evaluation of programs." I suggest anyone interested in programming languages and formal proofs read this paper.

Let's come back to the text. This section starts with a rough definition of proofs:

A proof of a mathematical proposition is a written (or spoken) text that instills in the reader or hearer the certainty that is true — an unassailable argument for the truth of .

This means that the essence of proofs is explanation, or communication, or convincing "readers" that the claim is valid. Here, the "reader" can be a computer, or a software program like Coq. In this case, the computer or Coq will only "believe" a claim if it can be derived from a collection of logical rules, and the proof "guides" the computer or Coq in checking if the claim is valid. Such proofs are called formal proofs. In other words, formal proofs derive claims from explicitly stated logical rules, but not from previous knowledge or intuition. Computers don't understand mathematical languages used by human beings; they only understand non-ambiguous programs ("recipes") written in certain programming languages like Coq.

On the other hand, the reader can be a human being, so proofs can be written in natural languages. Such proofs are called informal proofs. In contrast to formal proofs, informal proofs may contain previous knowledge that is not explicitly proved. The degree of details in an informal proof depends on the familiarity with the topic of the reader.

Exercises

basic_induction (2 stars)

This exercise asks readers to prove several theorems by induction.

The first theorem states that any natural number times 0 equals 0. The base case is to prove that 0 * 0 = 0, which directly follows from the definition of *. For the induction step, we assume that n' * 0 = 0. To prove (S n') * 0 = 0, we first simplify the goal by the definition of *, which yields 0 + n' * 0 = 0. The inductive hypothesis rewrites the goal to 0 + 0 = 0, which can be proved by simplification.

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

The second theorem states that S (n + m) = n + (S m). We prove this by induction on n. The base case is S (0 + m) = 0 + (S m). This can be proved directly by simplification. For the induction step, the inductive hypothesis is S (n' + m) = n' + (S m), and we need to prove that S ((S n') + m) = (S n') + (S m). We first simplify the goal and have S (S (n' + m)) = S (n' + (S m)). This can then be proved by rewriting with the inductive hypothesis and reflexivity.

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  induction n as [| n' IHn'].
  - reflexivity.
  - intros m. simpl. rewrite -> IHn'. reflexivity. Qed.

The third theorem asks for a proof of the commutative property of addition. As n and m are symmetric, we prove this by induction on n. The base case is 0 + m = m + 0, where the left-hand side can be simplified by the definition of +, and the right-hand can be rewritten by the plus_n_O theorem (i.e. n + 0 = 0 for all natural numbers). Then this can be proved by reflexivity. The induction step is to prove (S n') + m = m + (S n'). The left-hand side can be simplified to S (n' + m) with the definition of +, and the right-hand side can be rewritten to S (n' + m) by the plus_n_Sm theorem. The theorem then follows from reflexivity.

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  induction n as [| n' IHn'].
  - intros m. rewrite <- plus_n_O. reflexivity.
  - intros m. simpl. rewrite <- plus_n_Sm. rewrite -> IHn'. reflexivity. Qed.

The fourth theorem asks for a proof of the associative property of addition. I first tried to prove this by induction on m, but induction on m is tricky. In contrast, induction on n is much simpler. For the base case, we need to prove that 0 + (m + p) = (0 + m) + p, which can be directly simplified to m + p = m + p by the definition of +. For the induction step, we assume that n' + (m + p) = (n' + m) + p, and need to prove that (S n') + (m + p) = ((S n') + m) + p. Again, we simplify this by the definition of +, and get S (n' + (m + p)) = (S (n' + m)) + p. This can be further simplified by S (n' + (m + p)) = S ((n' + m) + p). The two parameters are equal due to the inductive hypothesis, which completes the proof.

Theorem plus_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p. induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite -> IHn'. reflexivity. Qed.

double_plus (2 stars)

This exercise asks for a proof of the theorem that double n = n + n for every natural number n. Again, we prove this by induction on n. The base case is to prove that double 0 = 0 + 0, which can be directly prove by simplification using the definition of double and of +. For the induction step, we assume that double n' = n' + n', and then need to prove that double (S n') = (S n') + (S n'). The left-hand side can be simplified using the definition of double, which yields S (S (double n')). The right-hand side can be simplified to S (n' + (S n')), which can be further simplified to S (S (n' + n')) by the plus_n_Sm theorem proved before. The remaining proof is then obvious.

Lemma double_plus : forall n, double n = n + n .
Proof.
  induction n as [| n' IHn'].
  - reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite -> IHn'. reflexivity. Qed.

evenb_S (2 stars)

This exercise asks for a proof by induction of the theorem that the parity of S n is the negation of the parity of n. The base case is evenb (S O) = negb (evenb O), which can be directly proved by simplification. For the induction step, we assume that evenb (S n') = negb (evenb n'), and need to prove that evenb (S (S n')) = negb (evenb (S n')). Rewriting with the inductive hypothesis and simplification with the definition of evenbyieldsevenb n' = negb (negb (even b')). The remaining goal directly follows from the theorem negation_fn_applied_twice`, which we proved last time.

Theorem evenb_S : forall n : nat,
  evenb (S n) = negb (evenb n).
Proof.
  induction n as [| n' IHn'].
  - reflexivity.
  - rewrite -> IHn'. simpl. rewrite -> negation_fn_applied_twice.
    + reflexivity. 
    + intros x. reflexivity. Qed.

destruct_induction (1 star)

This exercise asks the difference between destruct and induction.

This has been discussed in this blog article. The tactic [destruct] moves only variables from the hypothesis of the goal to the context. The tactic [induction] moves not only variables but also the induction hypothesis from the hypothesis of the goal to the context.

plus_comm_informal (2 stars)

This exercise asks for an informal proof for the commutative property of addition. The idea of the proof is stated above. Hence, an informal proof is as follows.

Proof: We need to show that for every natural number n and m, n + m = m + n.

By induction on n.

  • First, suppose n = 0. We must show

    0 + m = m + 0.

    We have proved that for every natural number m,

    m + 0 = m.

    Thus, 0 + m = m follows directly from the definition of +.

  • Second, suppose n = S n', where

    n' + m = m + n'.

    We must show

    (S n') + m = m + (S n').

    We have proved that for every natural number n and m,

    S (n + m) = n + (S m).

    Thus,

    m + (S n') = S (m + n'),

    and we need to show

    S (n' + m) = S (m + n').

    This is immediately from the induction hypothesis. Qed.

beq_nat_refl_informal (2 stars)

This exercise asks for an informal proof of the theorem that true = beq_nat n n for every natural number n. An informal proof is given as follows, and the idea of the proof is explained in the proof.

Proof: By induction on n.

  • First, suppose n = 0. We must show

    true = beq_nat 0 0.

    This follows directly from the definition of beq_nat.

  • Second, suppose n = S n', where

    true = beq_nat n' n'.

    We must show

    true = beq_nat (S n') (S n').

    By the definition of beq_nat, we get

    beq_nat (S n') (S n') = beq_nat n' n'.

    From the induction hypothesis,

    beq_nat n' n' = true. Qed.

mult_comm (3 stars)

This exercise asks readers to prove the plus_swap theorem that n + (m + p) = m + (n + p) without induction, and then to prove the commutative property of multiplication.

For plus_swap, we can use the associative property of addition twice to convert the initial goal to (n + m) + p = (m + n) + p, which directly follows from the commutative property of addition which gives n + m = m + n.

Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  intros n m p.
  rewrite -> plus_assoc.
  rewrite -> plus_assoc.
  assert (H: n + m = m + n). { rewrite -> plus_comm. reflexivity. }
  rewrite -> H.
  reflexivity. Qed.

Similar to the proof of the commutative property of addition, we first prove a theorem that n * (S m) = n + n * m by induction on n. The base case 0 * (S m) = 0 + 0 * m can be directly proved by simplification. For the induction step, we assume that n' * (S m) = n' + n' * m, and need to prove that (S n') * (S m) = (S n') + (S n') * m. Simplification by the definition of * gives (S m) + n' * (S m) = (S n') + (m + n' * m), and further simplification by the definition of + yields S (m + n' * (S m)) = S (n' + (m + n' * m)). From the inductive hypothesis, the left-hand side equals S (m + (n' + n' * m)). The two parameters under S are equal due to the plus_swap theorem. The remaining proof is then obvious.

Theorem mult_n_Sm : forall m n : nat,
  n * S m = n + n * m.
Proof.
  intros m n. induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite -> IHn'. rewrite -> plus_swap. reflexivity. Qed.

We then prove the commutative property of multiplication by induction on m. The base case 0 * n = n * 0 follows directly from the definition of * and the mult_0_r theorem. For the induction step, we assume that m' * n = n * m' and need to prove that (S m') * n = n * (S m'). Simplification by the definition of * yields n + m' * n = n * (S m'), and rewriting by the mult_n_Sm theorem gives n + m' * n = n + n * m'. This can be proved by rewriting with the inductive hypothesis.

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
  intros m n. induction m as [| m' IHm'].
  - simpl. rewrite -> mult_0_r. reflexivity.
  - simpl. rewrite -> mult_n_Sm. rewrite -> IHm'. reflexivity. Qed.

more_exercises (3 stars)

This exercise asks readers to think about whether each theorem can be proved (a) by simplification, (b) by case analysis, or (c) by induction. We notice that recursion and induction follow similar ideas. Hence, to determine which proof technique should be used, we can see if the given theorem can be directly derived from the function definitions without recursion. If so, then (c) is excluded, and we can further see if the function definitions perform pattern matching. If pattern matching is used, then we need to prove the theorem by case analysis; otherwise we use proof by simplification. Note that this is a rough idea, and we need to analyze each theorem case by case.

leb_refl

Since leb requires recursion for an arbitrary natural number n, we prove this theorem by induction on n.

Theorem leb_refl : forall n:nat,
  true = leb n n.
Proof.
  induction n as [| n' IHn'].
  - reflexivity.
  - simpl. rewrite <- IHn'. reflexivity. Qed.

zero_nbeq_S

We notice that the case where the first parameter is zero is one of the base cases of beq_nat. Hence, this can be directly proved by simplification.

Theorem zero_nbeq_S : forall n:nat,
  beq_nat 0 (S n) = false.
Proof.
  reflexivity. Qed.

and_false_r

The definition of andb performs case analysis on the first parameter, but the evaluation does not require recursion. Hence, we prove this theorem by case analysis.

Theorem andb_false_r : forall b : bool,
  andb b false = false.
Proof.
  intros [].
  - reflexivity.
  - reflexivity. Qed.

plus_ble_compat_l

For arbitrary natural numbers n and m, the evaluation of leb n m requires recursion when n and m are both greater than zero. Hence, we prove this theorem by induction on p.

Theorem plus_ble_compat_l : forall n m p : nat,
  leb n m = true -> leb (p + n) (p + m) = true.
Proof.
  intros n m p. intros H. induction p as [| p' IHp'].
  - simpl. rewrite -> H. reflexivity.
  - simpl. rewrite -> IHp'. reflexivity. Qed.

S_nbeq_0

The case where the second parameter is zero is also a base case of beq_nat. Hence, we can directly prove this theorem by simplification.

Theorem S_nbeq_0 : forall n:nat,
  beq_nat (S n) 0 = false.
Proof.
  reflexivity. Qed.

mult_1_l

Since the first parameter in 1 * n is a specified natural number, the evaluation of 1 * n only calls mult twice. Hence, we can prove this theorem by simplification twice.

Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
  intros n. simpl. rewrite <- plus_n_O. reflexivity. Qed.

all3_spec

Notice that only orb, andb and negb are involved in this theorem. All of these three functions does not require recursion. Hence, we perform case analysis on both parameters to prove this theorem.

Theorem all3_spec : forall b c : bool,
    orb
      (andb b c)
      (orb (negb b)
               (negb c))
  = true.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity. Qed.

mult_plus_distr_r

The definition of * requires recursion, so we should prove this theorem by induction. I initially tried induction on p; however proof by induction of p is tricky. Induction on n is much simpler.

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
  intros n m p. induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite -> IHn'. rewrite -> plus_assoc. reflexivity. Qed.

mult_assoc

Again, we use proof by induction because the definition of * requires recursion. Note that induction on n is much simpler than induction on m.

Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Proof.
  intros n m p. induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite -> mult_plus_distr_r. rewrite -> IHn'. reflexivity. Qed.

beq_nat_refl (2 stars)

This exercise asks for a proof of the theorem that beq_nat n n = true. We have given an informal proof for this theorem above, and the idea of a formal proof is the same.

Theorem beq_nat_refl : forall n : nat,
  true = beq_nat n n.
Proof.
  induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite <- IHn'. reflexivity. Qed.

plus_swap' (2 stars)

This exercise asks for a proof of the plus_swap theorem using the replace tactic. We have proved the same theorem above. Here, the idea is the same: we first apply the associative property of addition to rewrite the goal to (n + m) + p = (m + n) + p, and then replace n + m with m + n. The additional subgoal n + m = m + n is directly from the commutative property of addition.

Theorem plus_swap' : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  intros n m p.
  rewrite -> plus_assoc.
  rewrite -> plus_assoc.
  replace (n + m) with (m + n).
  - reflexivity.
  - rewrite -> plus_comm. reflexivity. Qed.

binary_commute (3 stars)

This exercise asks readers to prove that incrementing a binary number and then converting it to a (unary) natural number yields the same result as first converting it to a natural number and the incrementing, i.e. that bin_to_nat preserves incr.

We first write the theorem in Coq.

Theorem bin_to_nat_pres_incr : forall n : bin,
  bin_to_nat (incr n) = S (bin_to_nat n).

Since both bin_to_nat and incr both execute recursively, we consider induction for the proof. The base case is to prove that bin_to_nat (incr Zero) = S (bin_to_nat Zero). Since both functions has Zero as their base cases, the goal can be proved by simplification.

Second, we need to prove that bin_to_nat (incr (Twice n')) = S (bin_to_nat (Twice n')). The left-hand side can be simplified using the definition of incr, which yields bin_to_nat (TwicePlusOne n'), and further simplification using the definition of bin_to_nat yields S ((bin_to_nat n') + (bin_to_nat n')). The right-hand side can be simplified by the definition of bin_to_nat, which yields S ((bin_to_nat n') + (bin_to_nat n')). Hence, the equality of both sides can be proved by simplification.

Third, we assume that bin_to_nat (incr n') = S (bin_to_nat n'), and need to prove that bin_to_nat (incr (TwicePlusOne n')) = S (bin_to_nat (TwicePlusOne n')). We first simplify the left-hand side using the definition of incr, which yields bin_to_nat (Twice (incr n')), and simplification using the definition of bin_to_nat gives (bin_to_nat (Twice (incr n'))) + (bin_to_nat (Twice (incr n'))). The right-hand side can be simplified by the definition of bin_to_nat, which yields S (S ((bin_to_nat n') + (bin_to_nat n'))).

Now, the goal becomes (bin_to_nat (Twice (incr n'))) + (bin_to_nat (Twice (incr n'))) = S (S ((bin_to_nat n') + (bin_to_nat n'))). Rewriting the left-hand side by the inductive hypothesis gives (S (bin_to_nat n')) + (S (bin_to_nat n')). Simplification using the definition of + yields S ((bin_to_nat n') + (S (bin_to_nat n'))), and then the plus_n_Sm theorem rewrites it to S (S ((bin_to_nat n') + (bin_to_nat n'))). This completes the proof.

Theorem bin_to_nat_pres_incr : forall n : bin,
  bin_to_nat (incr n) = S (bin_to_nat n).
Proof.
  induction n as [| n' IHn' | n'' IHn''].
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. rewrite -> IHn''. simpl. rewrite <- plus_n_Sm. reflexivity. Qed.

binary_inverse (5 stars)

Part (a)

This part first asks for a function that converts (unary) natural numbers to binary numbers. This is obvious: O in nat corresponds to Zero in bin, and S n' can be converted recursively by first converting n' and then incrementing the result.

Fixpoint nat_to_bin (n : nat) : bin :=
  match n with
  | O => Zero
  | S n' => incr (nat_to_bin n')
  end.

Then, it asks readers to prove that converting any natural number to binary and then converting back yields the same natural natural that we start with. As we use recursion in the function definitions of nat_to_bin and bin_to_nat, we prove this theorem by induction.

Theorem nat_to_bin_then_back : forall n : nat,
  bin_to_nat (nat_to_bin n) = n.
Proof.
  induction n as [| n' IHn'].
  - simpl. reflexivity.
  - simpl. rewrite -> bin_to_nat_pres_incr. rewrite -> IHn'. reflexivity. Qed.

Part (b)

It is natural to think that converting any binary number to unary and then converting back also yields the same binary number. However, it is not true, and this part asks why.

We notice that the binary representation of a natural number is not unique; i.e. one natural number may have multiple binary representations. Why? A binary number may contain an arbitrary number of leading zeros. For instance, the binary numbers 10110 and 00010110 represent the same natural number 22. In our definition of binary numbers in Coq, this means that the Twice constructor may be applied on Zero multiple times before the first application of TwicePlusOne; e.g. TwicePlusOne (TwicePlusOne Zero) and TwicePlusOne (TwicePlusOne (Twice Zero)) both represent the natural number 3.

Part (c)

The last part of this exercise asks readers to define a normalization function normalize such that converting a binary number b to a natural and then converting back yields (normalize b). Although there is a warning saying that "this part is tricky!", it is not hard if we understand why converting back doesn't yield the original binary. Here, the normalize function just removes leading zeros from a binary representation, so we pattern-match the parameter, say b.

  • If b is Zero, then the result of normalization is still Zero, which is obvious.
  • If b is an application of Twice, namely Twice b', then we check if b' is zero. If yes, then this is the application of Twice here yields a leading zero, so the result should be only Zero. Otherwise, we just append the application of Twice to the normalization of b'.
  • If b is an application of TwicePlusOne, namely TwicePlusOne b', we just append it to the normalization of b'.
Fixpoint normalize (b : bin) : bin :=
  match b with
  | Zero => Zero
  | Twice b' =>
      let normalized_b' := normalize b'
      in match normalized_b' with
      | Zero => Zero
      | _ => Twice normalized_b'
      end
  | TwicePlusOne b' => TwicePlusOne (normalize b')
  end.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.