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. Note that the B proof rules for invariant preservation are an induction proof in disguise, i.e, the induction is provided by the POG (Proof Obligation Generator) and not the prover itself. They require coding your problem and induction steps as B operations. Here, I am interested in proving properties in B directly using induction without the help of an external POG.

It is well known that predicate logic is too weak to axiomatize exactly the natural numbers or concepts such as the transitive closure. So, can this be done at all, without resorting to provers such as Isabelle? The answer is, maybe surprisingly, 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, more precisely with the well-founded nature of the natural number and the concept of the minimum of a set.

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

A finite instance for ProB

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?

A generic induction proof

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".

The trick is as follows:

• 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

The proof above is very similar to, e.g., the proof of Theorem 1.7.1 on page 17 of the book "The Joy of Sets" by Keith Devlin or the proof in https://proofwiki.org for well-ordered sets: there a proof by contradiction is conducted, using the fact that

the complement NAT1 \ P  is non-empty and choosing the minimal element of the complement to arrive at a contradiction.

The full model with the inductive proof

We integrate this idea with the sum property into a single model as follows:

context InductiveSum_Prop
constants sum P Q
axioms
 @axm2 sum∈ ℕ1 → ℕ
 @axm3 sum(1)=1
 @axm4 ∀i·(i>1 ⇒ sum(i)=sum(i−1)+i)

 @axm5 P ⊆ ℕ1
 @axm6 P = {i∣i∈ℕ1 ∧ sum(i) = (i∗(i+1))÷2}

 theorem @base 1∈P
 theorem @induct ∀i·(i>1 ∧  i−1∈P ⇒ i∈P)

 @axmq1 Q ⊆ ℕ1
 @axmq2 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 @concl P=ℕ1

 theorem @thm1 ∀i·(i∈ℕ1 ⇒ sum(i) = (i∗(i+1))÷2)
end

You can notice that this time the induction base and step are not axioms but are theorems which thus need to be proven. They need to be proven from the definition of the property P in @axm6 and the definition of sum in @axm3 and @axm4 The induction step is slightly tedious, as the provers are not very powerful concerning integer division. However, it can be done. The proof of the theorems @concl1 is as describe above. The theorems @concl2 and also @thm1 can be discharged automatically by Rodin.

In the end the proofs are all discharged without the help of a inductive prover, just using the standard provers of Rodin (I used the Atelier-B provers and the SMT plugin):

This example can also be conducted within Atelier-B. In fact, Dominique Cansell showed me the "trick" at the time within AtelierB (within the B4Free version).

Encoding as B Operation

Here is how we can encode our property about the consecutive sums using a B operation to perform the computation of the sum values. The property we wish to prove by induction is @inv3:

machine SumAsOperation
variables i sum
invariants
 @inv1 i∈ℕ1
 @inv2 sum ∈ ℕ
 @inv3 sum = ( i∗ (i+1) ) ÷ 2
events
  event INITIALISATION begin
     @ini i,sum ≔ 1,1
  end
  event compute_next_sum begin
    @inci i≔i+1
    @sum sum ≔ sum+i+1
  end
end

Here is the machine when animated by ProB:

The Rodin POG generates the proof obligations for the induction:

• INITIALISATION/inv3/INV: 1=(1+1)/2
• compute_next_sum/inv3/INV: sum+i+1=(i+1)∗((i+1)+1) ÷ 2

The induction principle itself is here outside of the B provers: the provers are used to discharge the above proof obligations, not to prove that they entail that the invariant is true in all reachable states.