HOL CASE STUDY

The Binomial Theorem proven in HOL.

Author

Andrew Gordon Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG, UK. Telephone: +44 223 334650

Email: Andrew.Gordon@cl.cam.ac.uk

Concepts illustrated

A simple way to define algebraic structures in HOL. Translation of mathematical definitions such as sums of series and binomial coefficients into HOL. Division of a medium sized proof into manageable lemmas.

Prerequisites

At least as much knowledge of HOL as is given in Getting started with HOL. Basic understanding of how to use the goal stack to do forward proof, but not necessarily possession of a large vocabulary of tactics.

Supporting files

In the directory Training/studies/binomial.

Abstract

The Binomial Theorem in HOL is a medium sized worked example whose subject matter is more widely known than any specific piece of hardware or software. This article introduces the small amount of algebra and mathematical notation needed to state and prove the Binomial Theorem, shows how this is rendered in HOL, and outlines the structure of the proof.

Contents

1 Pascal’s Triangle and the Binomial Theorem 2

2 The Binomial Coefficients 4

3 Monoids, Groups and Commutative Rings 5 3.1 Associativity and Commutativity . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 Groups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.4 Rings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

4 Powers, Reductions, Ranges and Sums 12 4.1 Scalar powers in a monoid . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.2 Reduction in a monoid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.3 Subranges of the natural numbers . . . . . . . . . . . . . . . . . . . . . . . 14 4.4 Σ-notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

5 The Binomial Theorem for a Commutative Ring 15

6 The Binomial Theorem for Integers 16

7 References 17

A Principal lemmas 17

The Binomial Theorem proven in HOL.

1 Pascal’s Triangle and the Binomial Theorem

Pascal’s Triangle^{1} is the infinite triangle of numbers which starts like this:

1

1 1
1 2 1
1 3 3 1
1 4 6 4 1
1 5 10 10 5 1
· · · · · · ·

The construction is as follows. The numbers at the edges are 1s. Each number in the interior is the sum of the number immediately above it and the number to its left in the previous row.

The numbers in Pascal’s Triangle are called Binomial Coefficients. The number in the nth row and kth column (where 0 ≤ k ≤ n, and the topmost row and the leftmost column are numbered 0) is written \binom{n}{k} and pronounced “n choose k”. The coefficients are

pronounced this way because \binom{n}{k} turns out to be the number of ways to choose k things out of n things, but that is another story (see for instance Knuth’s book [1]).

A simple form of the Binomial Theorem [2] [3] is the following equation, where a and b are integers and n is any natural number,

(a + b)^{n} = ∑_{k=0}^{n} \binom{n}{k}a^{k}b^{n−k}

The rest of this article describes how the Binomial Theorem can be proven in HOL. In fact, a more general theorem is proven, where a and b are elements of an arbitrary commutative ring, but the form displayed here can be derived from the general result.

The motivation for the proof of the Binomial Theorem in HOL is tutorial—to be a medium sized worked example whose subject matter is more widely known than any specific piece of hardware or software. The proof illustrates specific ways in HOL to represent mathematical notations and manage theorems proven about general structures such as monoids, groups and rings. The following files accompany this article in directory

Training/studies/binomial:

mk BINOMIAL.ml The ML program containing the definitions, lemmas and theorems needed to prove the Binomial Theorem in HOL.

1According to Knuth [1], the triangle gets its name from its appearance in Blaise Pascal’s Traité du triangle arithmétique in 1653, although the binomial coefficients were known long before then. The earliest surviving description is from the tenth century, in Halāyudha’s commentary on the Hindu classic, the Chandah-Sûtra. The Binomial Theorem itself was first reported in 1676 by Isaac Newton.

BINOMIAL.th The theory file which is generated by mk_BINOMIAL.ml.

BINOMIAL.ml An ML program which loads the theory BINOMIAL and declares a few derived rules and one tactic used in the proof. The Binomial Theorem is bound to the ML identifier BINOMIAL.

The aim of this article is to introduce the small amount of algebra and mathematical notation needed to state and prove the Binomial Theorem, show how this is rendered in HOL, and outline the structure of the proof contained in mk_BINOMIAL.ml. The article is meant to be intelligible without examination of any of the accompanying files, but to avoid clutter not every detail is spelt out. Often definitions and theorems are indicated in the form displayed by HOL, rather than as ML source text. Specific details of the ML definitions or tactics can be found in the file mk_BINOMIAL.ml.

The way to work with this case study is first to study this article to see the structure of the proof, and then to work interactively with HOL. Start HOL and say:

1

 #loadt `BINOMIAL`;;
 ...
 File BINOMIAL loaded
 () : void
 #BINOMIAL;;
 |- !plus times.
     RING(plus,times) ==>
     (!a b n.
       POWER times n(plus a b) =
       SIGMA(plus,0,SUC n)(BINTERM plus times a b n))

(This is the first display of an interaction with HOL. The difference between lines input to and lines output from HOL is that only the former are preceded by the HOL prompt “#”. A line of ellipsis “...” stands for output from HOL which has been omitted from the display.)

The first input line in the display above loads in all the definitions, theorems, derived rules and the tactic defined for the proof. The second input line asks HOL to print theorem BINOMIAL. The constants used in BINOMIAL are explained later in the article. The HOL session is now set up either to make use of BINOMIAL by specialising it to a specific ring, or to study mk_BINOMIAL.ml by using the subgoal package to work through proofs contained in it.

The remainder of the article follows the plan:

Section 2 shows how to define the number \binom{n}{k} in HOL as the term CHOOSE n k, where CHOOSE is a function defined by primitive recursion.

Section 3 shows how to define elementary algebraic concepts like associativity, commutativity, monoid, group and ring in HOL, and how to apply theorems proved in the general case to particular situations.

Section 4 shows how to define the iterated operations of raising a term to a power and reducing (summing) a list of terms. These operations are part of the everyday mathematical language used to state the Binomial Theorem, but they are not builtin to HOL and so need to be defined. This section and the previous two together describe enough definitions in HOL to state the Binomial Theorem.

Section 5 shows how the Binomial Theorem is proven in HOL. The proof is by induction, and depends on three main lemmas.

Section 6 outlines how to apply the general theorem to a particular case: the ring of integers.

Appendix A states the principal lemmas used to prove the theorem. Some of these are ad hoc but others could be reused elsewhere.

2 The Binomial Coefficients

The definition of the binomial coefficients as the numbers in Pascal’s Triangle is formalised in three equations:

\binom{n}{0} = 1
\binom{0}{k + 1} = 0
\binom{n + 1}{k + 1} = \binom{n}{k + 1} + \binom{n}{k}

(These actually define \binom{n}{k} to be 0 if k > n, but this is consistent with Pascal’s Triangle: think of the spaces to the right of the triangle as filled with 0’s.) The desire is to define a constant CHOOSE in HOL such that for all numbers n, k in the type num, CHOOSE n k denotes the number \binom{n}{k}. Unfortunately these three equations cannot be used directly as the definition of CHOOSE in HOL because they are not in the form of a base case (when n = 0) together with an inductive case (when n > 0).

To work towards the definition, consider a term that specifies a base case and an inductive case intended to be equivalent to the three equations above:

2

 let base_and_inductive: term =
     "(CHOOSE 0 k = ((0 = k) => 1 | 0)) /\
      (CHOOSE (SUC n) k =
          ((0 = k) => 1 | (CHOOSE n (k-1)) + (CHOOSE n k)))";;

The theory prim_rec contains a primitive recursion theorem which says that any base case and inductive case identifies a unique function, fn:

3

 #num_Axiom;;
 |- !e f. ?! fn.
     (fn 0 = e) /\
     (!n. fn (SUC n) = f (fn n) n)

Given the theorem prim_rec, the builtin function prove_rec_fn_exists can prove that there is a function that satisfies the property specified by the term base_and_inductive:

4

 #let RAW_CHOOSE_DEF = prove_rec_fn_exists num_Axiom base_and_inductive;;
 RAW_CHOOSE_DEF =
 |- ?CHOOSE.
     (!k. CHOOSE 0 k = ((0 = k) => 1 | 0)) /\
     (!n k.
       CHOOSE(SUC n)k = ((0 = k) => 1 | (CHOOSE n(k - 1)) + (CHOOSE n k)))

These equations would not do as the only definition of CHOOSE due to the presence of the conditional operator, which makes rewriting difficult. But having obtained the theorem RAW_CHOOSE_DEF it is easy to prove there is a function which satisfies the original three equations:

5

 CHOOSE_DEF_LEMMA =
 |- ?CHOOSE.
     (!n. CHOOSE n 0 = 1) /\
     (!k. CHOOSE 0(SUC k) = 0) /\
     (!n k. CHOOSE(SUC n)(SUC k) = (CHOOSE n(SUC k)) + (CHOOSE n k))

Now the constant CHOOSE can be specified as originally desired:

6

 #let CHOOSE_DEF =
 #    new_specification `CHOOSE_DEF` [`constant`,`CHOOSE`] CHOOSE_DEF_LEMMA;;
 CHOOSE_DEF =
 |- (!n. CHOOSE n 0 = 1) /\
    (!k. CHOOSE 0(SUC k) = 0) /\
    (!n k. CHOOSE(SUC n)(SUC k) = (CHOOSE n(SUC k)) + (CHOOSE n k))

Two elementary properties of the binomial coefficients can now be proven by induction:

7

 CHOOSE_LESS = |- !n k. n < k ==> (CHOOSE n k = 0)
 CHOOSE_SAME = |- !n. CHOOSE n n = 1

3 Monoids, Groups and Commutative Rings

3.1 Associativity and Commutativity

An algebraic structure is a set equipped with some operators that obey some laws. An elementary example of such a structure is the pair (A, +), where A is a set and + is a binary operator on A that obeys the laws of associativity,

a + (b + c) = (a + b) + c and commutativity,

a + b = b + a

How might these laws be represented in HOL? The simplest scheme is to deal with structures of the form (σ, +), where σ is a type of the HOL logic, and + is a HOL term of type σ → σ → σ. Notice that the set in the structure is represented as a HOL type: see the theory group presented in Elsa Gunter’s case study of Modular Arithmetic for a more sophisticated approach where the set in a structure can be a subset of a HOL type.

The two laws can be defined as two constants in HOL:

8

 #let ASSOCIATIVE =
 #    new_definition (`ASSOCIATIVE`,
 #      "!plus: *->*->*. ASSOCIATIVE plus =
 #          (!a b c. plus a (plus b c) = plus (plus a b) c)");;
 ...
 #let COMMUTATIVE =
 #    new_definition (`COMMUTATIVE`,
 #      "!plus: *->*->*. COMMUTATIVE plus =
 #          (!a b. plus a b = plus b a)");;

By instantiating the type variable * and specialising the variable plus these constants are applicable to any particular structure of the form (σ, + : σ → σ → σ).

A simple example to illustrate this methodology is a permutation theorem about an arbitrary associative commutative operator (which is called PERM in file mk_BINOMIAL.ml). It is worthwhile going through the proof in detail because it illustrates how a difficulty in making use of assumptions like ASSOCIATIVE plus and COMMUTATIVE plus can be solved.

9

 #g "!plus: *->*->*.
 #       ASSOCIATIVE plus /\ COMMUTATIVE plus ==>
 #           !a b c. plus (plus a b) c = plus b (plus a c)";;

The first step is to strip off the quantifiers, and break up the implication:

10

 #e (REPEAT STRIP_TAC);;
 OK..
 "plus(plus a b)c = plus b(plus a c)"
     [ "ASSOCIATIVE plus" ]
     [ "COMMUTATIVE plus" ]

The next step is to rewrite plus a b to plus b a on the left-hand side, from the assumption COMMUTATIVE plus. If the theorem was about a specific operator, such as $+: num->num->num from the theory of numbers in HOL, the rewriting could be done with REWRITE_TAC and the specific commutativity theorem, such as ADD_SYM:

 |- !m n. m + n = n + m.

But in the general case all that is available is the definition of COMMUTATIVE plus which cannot be used directly with REWRITE_TAC to swap the terms a and b. One approach is first to prove the following equation from the definition COMMUTATIVE plus,

 COMMUTATIVE plus |- !a b. plus a b = plus b a,

and then to use the equation with REWRITE_TAC in the same way as one might use ADD_SYM. This is a valid tactic because the assumption COMMUTATIVE plus is already present in the assumption list. A little forward proof achieves the first step, the derivation of the equation:

11

 #top_print print_all_thm;;
 - : (thm -> void)
 #let forwards = fst(EQ_IMP_RULE (SPEC "plus: *->*->*" COMMUTATIVE));;
 forwards = |- COMMUTATIVE plus ==> (!a b. plus a b = plus b a)
 #let eqn = UNDISCH forwards;;
 eqn = COMMUTATIVE plus |- !a b. plus a b = plus b a

This forward proof is a special case of a derived rule of the logic,

\frac{Γ ⊢ ∀x. t_{1} = t_{2}}{Γ, t_{1}[t′/x] ⊢ t_{2}[t′/x]}

which can be coded as the ML function SPEC_EQ:

12

 #let SPEC_EQ v th = UNDISCH(fst(EQ_IMP_RULE (SPEC v th)));;
 SPEC_EQ = - : (term -> thm -> thm)

Now the equation eqn can be used to prove swap terms a and b:

13

 #e(SUBST1_TAC (SPECL ["a:*";"b:*"] eqn));;
 OK..
 "plus(plus b a)c = plus b(plus a c)"
     [ "ASSOCIATIVE plus" ]
     [ "COMMUTATIVE plus" ]

Now that the terms appear in both sides in the same order but with different grouping, associativity can be used to make the grouping on both sides the same. Again the definition of ASSOCIATIVE cannot be used directly, but the derived rule SPEC_EQ obtains from the definition an equation analogous to eqn which can be used:

14

 #e(REWRITE_TAC [SPEC_EQ "plus: *->*->*" ASSOCIATIVE]);;
 OK..
 goal proved
 ...
 |- !plus.
     ASSOCIATIVE plus /\ COMMUTATIVE plus ==>
     (!a b c. plus(plus a b)c = plus b(plus a c))

The point of this example was to illustrate how to prove theorems about an arbitrary operator whose behaviour is specified by general predicates like ASSOCIATIVE and COMMUTATIVE. The main difficulty is in deriving equations for use with rewriting or substitution. The solution used in the example and extensively in the proof of the Binomial Theorem is to derive equations using the derived rule SPEC_EQ. Another derived rule, SPEC_IMP, is used extensively and is a variant of SPEC_EQ:

\frac{Γ ⊢ ∀x. t_{1} ⇒ t_{2}}{Γ, t_{1}[t′/x] ⊢ t_{2}[t′/x]}

15

 #let SPEC_IMP v th = UNDISCH(SPEC v th);;
 SPEC_IMP = - : (term -> thm -> thm)

Two following two rules are versions of SPEC_EQ and SPEC_IMP generalised to take lists of variables rather than just one:

16

 SPECL_EQ = - : (term list -> thm -> thm)
 SPECL_IMP = - : (term list -> thm -> thm)

The final new derived rule used in the proof of the Binomial Theorem is STRIP_SPEC_IMP, a variant of SPEC_IMP, which splits up a conjunction in the antecedent into separate assumptions:

\frac{Γ ⊢ ∀x. (t_{1} ∧ ⋯ ∧ t_{n}) ⇒ t_{n+1}}{Γ, t_{1}[t′/x], …, t_{n}[t′/x] ⊢ t_{n+1}[t′/x]}

17

 #let STRIP_SPEC_IMP v th =
 #    UNDISCH_ALL(SPEC v (CONV_RULE (ONCE_DEPTH_CONV ANTE_CONJ_CONV) th));;
 STRIP_SPEC_IMP = - : (term -> thm -> thm)

There are other methods for proving theorems which are conditional on predicates such as ASSOCIATIVE and COMMUTATIVE. One is to rewrite with the definition before assuming the predicate (see, for instance, the proof of RIGHT_CANCELLATION in mk_BINOMIAL.ml). This method is fine for small proofs, but in larger proofs it presents the problem of how to specify a particular assumption on the assumption list. Another method is to put the predicates on the assumption list, and use resolution to extract the body of the definition (see the proof of UNIQUE_LEFT_INV). When the assumption list is not short this is rather a blunt instrument, in the sense that resolution can find many more theorems than the one desired, and is also rather computationally costly when compared to carefully constructing a theorem with SPEC_EQ and its variants.

3.2 Monoids

A monoid is a structure (M, +) where M is a set, + is an associative binary operator on M, such that there is an identity element, u ∈ M, which is a left and right identity of +, that is, it satisfies u + a = a + u = a for all a ∈ M. When the operator is written as +, the structure (M, +) is called an additive monoid and the identity element is written as 0; otherwise if the operator is written as ×, the structure (M, ×) is called a multiplicative monoid and the identity element is written as 1.

18

 #let RAW_MONOID =
 #    new_definition (`RAW_MONOID`,
 #      "!plus: *->*->*. MONOID plus =
 #          ASSOCIATIVE plus /\
 #          (?u. (!a. plus a u = a) /\ (!a. plus u a = a))");;

This definition is inconvenient to manipulate as it stands, because of the presence of the existential quantifier. However it is possible via Hilbert’s ϵ-operator to specify a function Id such that Id plus stands for an identity element of plus, if such exists. In fact it is easy to prove that the identity element in a monoid is unique. The first step is to prove that there exists a function Id with the property just described:

19

 ID_LEMMA =
 |- ?Id.
     !plus.
      (?u. (!a. plus u a = a) /\ (!a. plus a u = a)) ==>
      (!a. plus(Id plus)a = a) /\ (!a. plus a(Id plus) = a)

The proof of ID_LEMMA uses Hilbert’s ϵ-operator to construct a witness for the outer existential quantifier,

    \plus.@u:*.(!a:*. (plus u a = a)) /\ (!a. (plus a u = a))

Given ID_LEMMA, the constant Id is specified as follows:

20

 #let ID = new_specification `Id` [`constant`, `Id`] ID_LEMMA;;
 ID =
 |- !plus.
     (?u. (!a. plus u a = a) /\ (!a. plus a u = a)) ==>
     (!a. plus(Id plus)a = a) /\ (!a. plus a(Id plus) = a)

The condition that Id plus is a left and right identity is expressed by the predicates LEFT_ID and RIGHT_ID, respectively:

21

 LEFT_ID = |- !plus. LEFT_ID plus = (!a. plus(Id plus)a = a)
 RIGHT_ID = |- !plus. RIGHT_ID plus = (!a. plus a(Id plus) = a)

Given these abbreviations it is easy to prove in HOL that if a left and right identity element exists, then it is unique:

22

 UNIQUE_LEFT_ID =
 |- !plus.
     LEFT_ID plus /\ RIGHT_ID plus ==>
     (!l. (!a. plus l a = a) ==> (Id plus = l))
 UNIQUE_RIGHT_ID =
 |- !plus.
     LEFT_ID plus /\ RIGHT_ID plus ==>
     (!r. (!a. plus a r = a) ==> (Id plus = r))

The use of these last two theorems is to help identify the element Id plus for some specific plus, such as $+ from the theory of arithmetic. The abbreviations LEFT_ID and RIGHT_ID admit a new characterisation of the predicate MONOID, which is easier to manipulate in HOL than RAW_MONOID:

23

 MONOID =
 |- !plus. MONOID plus = LEFT_ID plus /\ RIGHT_ID plus /\ ASSOCIATIVE plus

3.3 Groups

A group is a monoid in which every element is invertible.

24

 RAW_GROUP =
 |- !plus.
     Group plus =
     MONOID plus /\
     (!a. ?b. (plus b a = Id plus) /\ (plus a b = Id plus))

An alternative characterisation of Group^{2} which makes the existential quantification implicit can be had by specifying a function Inv so that, if Group plus holds, then the element Inv plus a is an inverse of a. The function Inv is specified in a way analogous to the specification of Id. First a lemma is proven which says there does exist a function Inv with the property desired:

25

 INV_LEMMA =
 |- ?Inv.
     !plus.
      (!a. ?b. (plus b a = Id plus) /\ (plus a b = Id plus)) ==>
      (!a.
        (plus(Inv plus a)a = Id plus) /\ (plus a(Inv plus a) = Id plus))

Given this lemma, which is proven by an easy tactic almost the same as the one for ID_LEMMA, the constant Inv can be specified:

26

 #let INV =
 #    new_specification `Inv` [`constant`, `Inv`] INV_LEMMA;;

The predicates which say that Inv produces left and right inverses are defined as new constants:

27

 LEFT_INV =
 |- !plus. LEFT_INV plus = (!a. plus(Inv plus a)a = Id plus)
 RIGHT_INV =
 |- !plus. RIGHT_INV plus = (!a. plus a(Inv plus a) = Id plus)

Finally, the alternative characterisation of Group can be proven:

2The mixed case identifier Group is used rather than GROUP, because the latter is already defined in Elsa Gunter’s theory group, a parent of her theory integer, which needs to coexist with the present theory so that integers can be used as an example ring (Section 6).

28

 GROUP = |- Group plus = MONOID plus /\ LEFT_INV plus /\ RIGHT_INV plus

The theory of groups has been developed only as far as needed to prove the Binomial Theorem; Appendix A shows the one lemma, RIGHT_CANCELLATION, specifically about groups.

3.4 Rings

A ring is a structure (R, +, ×) such that structure (R, +) is a group, structure (R, ×) is a monoid, addition, +, is commutative, and multiplication, ×, distributes (on both sides) over addition. A commutative ring is a ring in which multiplication is commutative. The word ring is used in the remainder of this article and in the HOL code to mean a commutative ring:

29

 RING =
 |- !plus times.
     RING(plus,times) =
     Group plus /\
     COMMUTATIVE plus /\
     MONOID times /\
     COMMUTATIVE times /\
     LEFT_DISTRIB(plus,times) /\
     RIGHT_DISTRIB(plus,times)

LEFT_DISTRIB and RIGHT_DISTRIB are new constants defined by the theorems:

30

 LEFT_DISTRIB =
 |- !plus times.
     LEFT_DISTRIB(plus,times) =
     (!a b c. times a(plus b c) = plus(times a b)(times a c))
 RIGHT_DISTRIB =
 |- !plus times.
     RIGHT_DISTRIB(plus,times) =
     (!a b c. times(plus a b)c = plus(times a c)(times b c))

Notice that the definition of RING abbreviates a conjunction of predicates, some of which are atomic, in the sense that they are some basic property of plus or times or both, and some are compound, in the sense that they abbreviate a further conjunction of properties. The definition is a tree of predicates with atomic ones like LEFT_DISTRIB and ASSOCIATIVE, at the leaves, and compound ones like Group and MONOID, at the branches. Many theorems conditional on RING(plus,times) need to make use of both atomic and compound predicates contained in the tree. To make access to all these predicates easy, the following lemma is proven, which makes explicit all the predicates in the tree:

31

 RING_LEMMA =
 |- RING(plus,times) ==>
    RING(plus,times) /\
    Group plus /\
    MONOID plus /\
    LEFT_ID plus /\
    RIGHT_ID plus /\
    ASSOCIATIVE plus /\
    LEFT_INV plus /\
    RIGHT_INV plus /\
    COMMUTATIVE plus /\
    MONOID times /\
    LEFT_ID times /\
    RIGHT_ID times /\
    ASSOCIATIVE times /\
    COMMUTATIVE times /\
    LEFT_DISTRIB(plus,times) /\
    RIGHT_DISTRIB(plus,times)

Goals of the form,

 !plus times. RING(plus,times) ==> ...

are consistently tackled with the following tactic, which uses RING_LEMMA to add all the atomic and compound predicates in the tree to the assumption list:

32

 #let RING_TAC =
 #    GEN_TAC THEN GEN_TAC THEN
 #    DISCH_THEN (\th. STRIP_ASSUME_TAC (MP RING_LEMMA th));;

The one lemma about rings needed here, RING_0, is stated in Appendix A.

4 Powers, Reductions, Ranges and Sums

The aim of this section is to explain how the mathematical notation ∑_{k=0}^{n} \binom{n}{k}a^{k}b^{n−k} can be rendered in HOL. If this is written out more explicitly than necessary for human consumption it looks like this:

∑_{k=0}^{n} \binom{n}{k} · (a^{k} × b^{n−k})

where × is multiplication in the ring, and where exponentiation and · stand for the scalar powers of multiplication and addition, respectively. Since binomial coefficients were treated in Section 2, what remain to be defined in this section are scalar powers and the Σ-notation. The latter is tackled in three steps: reduction of a list of monoid elements; generation of lists comprising subranges of natural numbers, [n, n + 1, …, n + k − 1]; and finally the reduction of a list of ring elements indexed by a subrange of the natural numbers.

4.1 Scalar powers in a monoid

If (M, +) and (M, ×) are additive and multiplicative monoids respectively, the scalar powers of addition and multiplication are defined informally by the following equations, where n > 0:

n · a = \overbrace{a + ⋯ + a}^{n}
a^{n} = \overbrace{a × ⋯ × a}^{n}

When n = 0, n · a = 0 and a^{n} = 1.

Scalar power is defined in HOL via the constant POWER which is defined by primitive recursion:

33

 POWER =
 |- (!plus a. POWER plus 0 a = Id plus) /\
    (!plus n a. POWER plus(SUC n)a = plus a(POWER plus n a))

Three lemmas about POWER are stated in Appendix A.

4.2 Reduction in a monoid

This section makes use of the standard HOL theory of lists, in particular the constants NIL, CONS, APPEND and MAP, definition by primitive recursion and proof by induction. The theory of lists is described in DESCRIPTION.

If (M, +) is a monoid, then the reduction of a list [a_{1}, …, a_{n}], where each a_{i} is an element of M, is the sum,

a_{1} + ⋯ + a_{n},

or the monoid’s identity element if n = 0.

Reduction is represented in HOL by the constant REDUCE, with type,

REDUCE : (*->*->*) -> (*)list -> *

and which is defined by primitive recursion on lists on its second argument:

34

 #let REDUCE =
 #  new_list_rec_definition (`REDUCE`,
 #    "(!plus. (REDUCE plus NIL) = (Id plus):*) /\
 #     (!plus (a:*) as. REDUCE plus (CONS a as) = plus a (REDUCE plus as))");;
 REDUCE =
 |- (!plus. REDUCE plus[] = Id plus) /\
    (!plus a as. REDUCE plus(CONS a as) = plus a(REDUCE plus as))

Three lemmas about REDUCE are stated in Appendix A.

4.3 Subranges of the natural numbers

The constant RANGE, which is a curried function of two numbers, is defined by primitive recursion so that,

RANGE m n = [m, m + 1, …, m + n − 1]

This definition means that the subrange is the first n numbers starting at m. In particular, when n = 0 the list is empty. Appendix A states two simple properties of RANGE

RANGE generates a subrange given its least element and length; an alternative method is to generate the subrange given its two endpoints, via a constant INTERVAL which satisfies the equation:

INT ERV AL m n = \{ \begin{matrix}[m, m + 1, …, n] & if m ≤ n \\ [] & otherwise \end{matrix}

For comparison, the two methods are definable in HOL as follows:

35

 #let RANGE =
 #    new_recursive_definition false num_Axiom `RANGE`
 #      "(RANGE m 0 = NIL) /\
 #       (RANGE m (SUC n) = CONS m (RANGE (SUC m) n))";;
 #
 #let INTERVAL =
 #    new_recursive_definition false num_Axiom `INTERVAL`
 #      "(INTERVAL m 0 =
 #          (m > 0) => NIL | [0]) /\
 #      (INTERVAL m (SUC n) =
 #          (m > (SUC n)) => NIL | APPEND (INTERVAL m n) ([SUC n]))";;

4.4 Σ-notation

The standard Σ-notation is defined informally by the equation,

∑_{i=m}^{n} a_{i} = \{ \begin{matrix}a_{m} + a_{m+1} + ⋯ + a_{n} & if m ≤ n \\ 0 & otherwise \end{matrix}

Therefore the standard Σ-notation is naturally definable via a subrange generated by

INTERVAL.

An alternative notation, naturally definable via RANGE, can be defined informally as follows:

∑_{i=m}^{(n)} a_{i} = \{ \begin{matrix}a_{m} + a_{m+1} + ⋯ + a_{m+n−1} & if n > 0 \\ 0 & otherwise \end{matrix}

The brackets around the n above the Σ distinguish this notation from the standard one.

This second notation is used in the HOL proof of the Binomial Theorem. The difference between the two is just that the standard notation is definable via INTERVAL, and the second via RANGE. The second notation was chosen entirely because the constant RANGE is easier to manipulate in HOL than INTERVAL, which is because the latter has a more complex definition. The disadvantage of this choice is that the proof of the theorem uses a non-standard notation, but that’s all the difference is: notation. If desired, the Binomial Theorem stated in the standard notation could be trivially deduced from its non-standard statement.

The non-standard Σ-notation is defined in HOL as the following abbreviation:

36

 #let SIGMA =
 #    new_definition (`SIGMA`,
 #      "SIGMA (plus,m,n) f = REDUCE plus (MAP f (RANGE m n)): *");;

Note that an indexed term a_{i} is represented in HOL as a function f of type num -> *.

Appendix A states several properties of SIGMA; their proofs make use of properties of MAP from the theory list, and also the lemmas about REDUCE and RANGE.

The functions REDUCE and RANGE are needed here only to define SIGMA, and in fact could be omitted if SIGMA were to be defined directly using primitive recursion. It is worth going to the trouble of defining REDUCE and RANGE, however, because they are likely to be useful in other situations.

5 The Binomial Theorem for a Commutative Ring

This section outlines the proof. For full details see the tactics in mk_BINOMIAL.ml.

The statement and proof of the Binomial Theorem use a new HOL constant, BINTERM, to abbreviate indexed terms of the form λk. \binom{n}{k}·a^{n−k} ×b^{k}. BINTERM is defined as a curried function as follows:

37

 #let BINTERM_DEF =
 #    new_definition (`BINTERM_DEF`,
 #      "BINTERM (plus: *->*->*) (times: *->*->*) a b n k =
 #          POWER plus (CHOOSE n k)
 #              (times (POWER times (n-k) a) (POWER times k b))");;

This abbreviation lets the Binomial Theorem be stated and proven in HOL as follows:

38

 BINOMIAL =
 |- !plus times.
     RING(plus,times) ==>
     (!a b n.
       POWER times n(plus a b) =
       SIGMA(plus,0,SUC n)(BINTERM plus times a b n))

In outline, the proof proceeds as follows. The following equation is proven by induction on n:

(a + b)^{n} = ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k}

When n = 0 both sides reduce to the multiplicative identity element, 1, of the ring. For the inductive step, the equation is assumed for n, and the following goal must be proven:

(a + b)^{n+1} = ∑_{k=0}^{(n+2)} \binom{n + 1}{k}a^{n+1−k}b^{k}

Three lemmas are used in the inductive step:

∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} = a × ∑_{k=1}^{(n)} \binom{n}{k}a^{n+1−k}b^{k} + b × ∑_{k=0}^{(n)} \binom{n}{k}a^{n+1−k}b^{k} (LEMMA 1)
a × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k} = a^{n+1} + a × ∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k}  (LEMMA 2)
b × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k} = b × ∑_{k=0}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b^{n+1}  (LEMMA 3)

LEMMA_1 is the key to the inductive step. The three stages of the inductive step are indicated (a), (b) and (c) in ML comments. Step (a) expands the right-hand side of the goal with LEMMA_1:

rhs = a^{n+1} + a × ∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b × ∑_{k=0}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b^{n+1}

Step (b) expands the left-hand side with the induction hypothesis:

lhs = (a + b) ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k}

Finally, in step (c) the expansions of the two sides are shown to be the same, using distributivity of × over +, associativity of +, and LEMMA_2 and LEMMA_3:

lhs = a × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k} + b × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k}

= a^{n+1} + a × ∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b × ∑_{k=0}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b^{n+1}
= rhs

6 The Binomial Theorem for Integers

The previous sections have dealt with the material in theory BINOMIAL, concerning how to prove the Binomial Theorem for an arbitrary ring. A natural next step is to produce some specific commutative ring, and prove a Binomial Theorem for it, as an instance of the general case.

To see how to do so for Elsa Gunter’s theory of integers, take a look at the file

mk BINOMIAL integer.ml, contained in directory Training/studies/binomial. When

loaded into HOL, this ML file proves that the integers are a ring—by quoting laws contained in the theory integer—and then derives a Binomial Theorem for the integers—by Modus Ponens from the general theorem BINOMIAL.

7 References

[1] Donald. E. Knuth. The Art of Computer Programming. Volume 1/Fundamental Algorithms. Addison-Wesley, second edition, 1973.

[2] Saunders Mac Lane and Garrett Birkhoff. Algebra. Collier-MacMillan Limited, London, 1967.

[3] George D. Mostow, Joseph H. Sampson, and Jean-Pierre Meyer. Fundamental Structures of Algebra. McGraw-Hill Book Company, 1963.

A Principal lemmas

Binomial coefficients, CHOOSE:

39

CHOOSE_LESS = |- !n k. n < k ==> (CHOOSE n k = 0)
CHOOSE_SAME = |- !n. CHOOSE n n = 1

Algebraic laws:

40

RIGHT_CANCELLATION =
|- !plus. Group plus ==> (!a b c. (plus b a = plus c a) ==> (b = c))
RING_0 =
|- !plus times.
    RING(plus,times) ==>
    (!a. times(Id plus)a = Id plus) /\ (!a. times a(Id plus) = Id plus)

Scalar powers:

41

POWER_1 = |- !plus. MONOID plus ==> (POWER plus 1 a = a)
POWER_DISTRIB =
|- !plus times.
    RING(plus,times) ==>
    (!a b n. times a(POWER plus n b) = POWER plus n(times a b))
POWER_ADD =
|- !plus.
    MONOID plus ==>
    (!m n a. POWER plus(m + n)a = plus(POWER plus m a)(POWER plus n a))

Reduction of lists:

42

REDUCE_APPEND =
|- !plus.
    MONOID plus ==>
    (!as bs.
      REDUCE plus(APPEND as bs) = plus(REDUCE plus as)(REDUCE plus bs))
REDUCE_MAP_MULT =
|- !plus times.
    RING(plus,times) ==>
    (!a bs. REDUCE plus(MAP(times a)bs) = times a(REDUCE plus bs))
REDUCE_MAP =
|- !plus.
    MONOID plus /\ COMMUTATIVE plus ==>
    (!f g as.
      REDUCE plus(MAP(\k. plus(f k)(g k))as) =
      plus(REDUCE plus(MAP f as))(REDUCE plus(MAP g as)))

Subranges of the natural numbers:

43

RANGE_TOP = |- !n m. RANGE m(SUC n) = APPEND(RANGE m n)[m + n]
RANGE_SHIFT = |- !n m. RANGE(SUC m)n = MAP SUC(RANGE m n)

Σ-notation:

44

SIGMA_ID = |- !plus m f. SIGMA(plus,m,0)f = Id plus
SIGMA_LEFT_SPLIT =
|- !plus m n f. SIGMA(plus,m,SUC n)f = plus(f m)(SIGMA(plus,SUC m,n)f)
SIGMA_RIGHT_SPLIT =
|- !plus.
    MONOID plus ==>
    (!m n f. SIGMA(plus,m,SUC n)f = plus(SIGMA(plus,m,n)f)(f(m + n)))
SIGMA_SHIFT =
|- !plus m n f. SIGMA(plus,SUC m,n)f = SIGMA(plus,m,n)(f o SUC)
SIGMA_MULT_COMM =
|- !plus times.
    RING(plus,times) ==>
    (!m n a f.
      times a(SIGMA(plus,m,n)f) = SIGMA(plus,m,n)((times a) o f))
SIGMA_PLUS_COMM =
|- !plus.
    MONOID plus /\ COMMUTATIVE plus ==>
    (!f g m n.
      plus(SIGMA(plus,m,n)f)(SIGMA(plus,m,n)g) =
      SIGMA(plus,m,n)(\k. plus(f k)(g k)))
SIGMA_EXT =
|- !plus.
    MONOID plus ==>
    (!f g m n.
      (!k. k < n ==> (f(m + k) = g(m + k))) ==>
      (SIGMA(plus,m,n)f = SIGMA(plus,m,n)g))

Terms from the Binomial Theorem:

45

BINTERM_0 =
|- !plus times.
    RING(plus,times) ==>
    (!a b n. BINTERM plus times a b n 0 = POWER times n a)
BINTERM_n =
|- !plus times.
    RING(plus,times) ==>
    (!a b n. BINTERM plus times a b n n = POWER times n b)