Induction Proofs in B: Difference between revisions

The classical B and Event-B method are both rooted in classical predicate logic and do not have an explicit inference rule for induction. The B proof rules for invariant preservation are an induction proof in disguise, but that is another story. They require coding your problem and induction steps as B operations. Here, I am interested in proving properties in B directly using induction. Can this be done at all, without resorting to provers such as Isabelle? The answer is, yes. The reason is that B is not just rooted in predicate logic, but has access to arithmetic and set theory. As such, induction comes ``bundled with the arithmetic operators and data types.

Let us look at one of the classic examples used to illustrate induction proofs, proving the formula for the consecutive sum of natural numbers (see Wikipedia):

• the sum of the numbers from 1 to n is equal to (n*(n+1)) / 2

We can write a small Event-B model in Rodin (using Camille syntax) like this. Note, as in Rodin the Sigma operator for summing is not pre-defined, I axiomatise the summing up using the constant sum This model computes the sum until a given limit lim It is made finite to be able to be validated using ProB.

context InductiveSum
constants sum lim
axioms
 @axm1 lim∈ℕ1
 @axm2 sum∈ 1‥lim → ℕ
 @axm3 sum(1)=1
 @axm4 ∀i·(i∈2‥lim ⇒ sum(i)=sum(i−1)+i)
 theorem @thm1 ∀i·(i∈1‥lim ⇒ sum(i) = (i∗(i+1))÷2)
 @prob lim=100
 end

We can load this model with ProB, and check that the property holds for all numbers until 100:

The theorem is the property we wish to prove by induction for any number i>0. How can this be done? I describe here a "trick" that was shown to me by Dominique Cansell many years ago. It relies on specifying your property as a set of natural numbers. Let us first write a small generic Rodin context, which just describes the ideas of the induction proof:

context InductiveProp
constants P Q
axioms
 @axm1 P ⊆ ℕ1
 @axm2 Q ⊆ ℕ1
 @base 1∈P // the base case of the induction
 @induct ∀i·(i>1 ∧ i−1∈P ⇒ i∈P) // the induction step
 @axmq Q = ℕ1 ∖ P // define the elements not satisfying the inductive property
 theorem @concl1 Q=∅ // proof by contradiction using min(Q) in induct for i
 theorem @concl2 P=ℕ1
end

Here P is the property we wish to hold for all natural numbers ≥ 1. We stipulate the base of the induction proof as an axiom here:

we assume we have prove that 1 is an element of P in the axiom @base

We also assume that we have proven the induction step in the axiom @induct, namely that i-1 in P implies that i is in the property P. Our proof target ins the theorem @concl2: that P must hold for all natural numbers ≥ 1.

One crucial idea is to introduce the set Q of properties for which the property does not hold and prove that it is empty. Rodin can automatically discharge @concl2 from @concl1. However, to discharge @concl1 we need to apply the crucial "trick":

• do a proof by contradiction
• this implies that Q is not empty is in the hypotheses
• this implies that min(Q) is well-defined
• this implies that we can instantiate the induction quantifier for i = min(Q)
• this allows us to find a contradiction in the hypothesis, given that min(Q)-1 is in P