1 Proving Termination of Functions and Properties of the Results of those Functions

In most cases we use the typewriter font accepted by HOL. For example, ∀xy. A, ∃xy. A and λxy. A are written as !x y. A, ?x y. A and x y. A. The logical connectives ¬, ∧,k ∨ and ⇒ are written as ~, /\, \/ and ==>.

1.1 MERGE
val MERGE_DEF = Define `
    (MERGE R []      right   = right)
 /\ (MERGE R left    []      = left)
 /\ (MERGE R (l::ls) (r::rs) = if R l r
                               then l::(MERGE R ls (r::rs))
                               else r::(MERGE R (l::ls) rs))`;

(this is part of defining MERGE SORT, see later)

HOL accepts this function, and can see for itself that it terminates (because one list argument gets smaller while the other remains the same, in successive recursive calls).

HOL generates an induction function for use to prove properties of the result of the MERGE function, called MERGE ind:

   |- !P.
     (!R right. P R [] right) /\ (!R v4 v5. P R (v4::v5) []) /\
     (!R l ls r rs.
        (~ R l r ==> P R (l::ls) rs) /\ (R l r ==> P R ls (r::rs)) ==>
        P R (l::ls) (r::rs)) ==>
     !v v1 v2. P v v1 v2

which says that, assuming

– P R ls rs holds whenever ls or rs is empty

– P R (l::ls) (r::rs) holds provided that

– P R ls (r::rs) and P R (l::ls) rs hold

then P v ls rs holds in all cases

HOL proves this to show that the function MERGE terminates. Note that if you instantiate P to “the definition of MERGE, above, terminates with these arguments” then the theorem MERGE ind says that the definition of MERGE terminates in all cases.

And HOL requires function definitions to terminate, because the HOL logic requires that all functions be total.

Now we want to prove that

set (MERGE c l r) = set l UNION set r

So we instantiate P of the theorem MERGE ind to

\c l r. set (MERGE c l r) = set l UNION set r

which gives that

!v v1 v2. set (MERGE v v1 v2) = set v1 UNION set v2

provided several conditions hold, which are

 (!R right. set (MERGE R [] right) = set right) /\
   (!R v4 v5. set (MERGE R (v4::v5) []) = v4 INSERT set v5) /\
   (!R l ls r rs.
      (~ R l r ==>
       (set (MERGE R (l::ls) rs) = (l INSERT set ls) UNION set rs)) /\
      (R l r ==>
       (set (MERGE R ls (r::rs)) = set ls UNION (r INSERT set rs))) ==>
      (set (MERGE R (l::ls) (r::rs)) =
       (l INSERT set ls) UNION (r INSERT set rs)))

Since these conditions match the definition of MERGE, (essentially they say that each step in the definition of MERGE preserves the property

 set (MERGE v v1 v2) = set v1 UNION set v2)

they are quite easily proved.

Thus we get the theorem

!v v1 v2. set (MERGE v v1 v2) = set v1 UNION set v2
1.2 MERGE SORT

The definition of MERGE SORT is

(MERGE_SORT R []     = [])
     /\ (MERGE_SORT R [h]    = [h])
     /\ (MERGE_SORT R (h::t) =
    let middle = (LENGTH (h::t)) DIV 2 in
    let left = MERGE_SORT R (TAKE (middle) (h::t)) in
    let right = MERGE_SORT R (DROP (middle) (h::t)) in
    MERGE R left right)

TAKE n list returns a list consisting of the first n members of list.

DROP n list returns a list consisting of all but the first n members

of list.

This function terminates because any recursive call is applied to a shorter list, though to prove this fact requires some tedious numerical work (to show that middle is shorter than the length of the original list, in cases where middle is used).

HOL does not prove this automatically.

Therefore HOL presents a condition which the user must prove, which is that there exists a well-founded relation ¡ such that where calling MERGE SORT R L generates a call of MERGE SORT R' L', then (R′, L′) < (R, L).

HOL uses R’ for the well-founded relation, and uses MERGE SORT tupled aux (R, L) = MERGE SORT R L. So the goal for the user to prove is

     ?R'.
       WF R' /\
       (!R v5 v4 h middle left.
          (middle = LENGTH (h::v4::v5) DIV 2) /\
          (left =
           MERGE_SORT_tupled_aux R' (R,TAKE middle (h::v4::v5))) ==>
          R' (R,DROP middle (h::v4::v5)) (R,h::v4::v5)) /\
       !R v5 v4 h middle.
         (middle = LENGTH (h::v4::v5) DIV 2) ==>
         R' (R,TAKE middle (h::v4::v5)) (R,h::v4::v5)

and once that is proved, the resulting theorem MERGE SORT ind is

   |- !P.
     (!R. P R []) /\ (!R h. P R [h]) /\
     (!R h v4 v5.
        (!middle left.
           (middle = LENGTH (h::v4::v5) DIV 2) /\
           (left = MERGE_SORT R (TAKE middle (h::v4::v5))) ==>
           P R (DROP middle (h::v4::v5))) /\
        (!middle.
           (middle = LENGTH (h::v4::v5) DIV 2) ==>
           P R (TAKE middle (h::v4::v5))) ==>
        P R (h::v4::v5)) ==>
     !v v1. P v v1

Again, if you instantiate P to “the definition of MERGE SORT above, terminates with these arguments” then the theorem MERGE SORT ind says that the definition of MERGE SORT terminates in all cases.

We want to prove that

!v v1. set (MERGE_SORT v v1) = set v1

so we instantiate P in MERGE SORT ind to

\c l. set (MERGE_SORT c l) = set l

to get a lemma whose conclusion is

!v v1. set (MERGE_SORT v v1) = set v1

and whose assumptions essentially say that each step in the definition of

MERGE SORT preserves the property set (MERGE SORT v v1) = set v1.

1.3 Future states

The program involves a counting “state”, which records, in particular, the candidates who are already elected or excluded, or otherwise “remaining”; for these last, the parcels of votes which are (currently) to their credit are recorded. The state also contains the parcels of votes, either arising from the surplus for an elected candidate, or from an excluded candidate, which are yet to be distributed.

The function NEXT1 STAGE returns the next state (1 step) from a given state.

Then we defined FINAL STAGE in terms of NEXT1 STAGE

   |- !state.
     FINAL_STAGE state =
     case STAGE_RESULT state of
       NONE => FINAL_STAGE (NEXT1_STAGE state)
     | SOME result => result

STAGE RESULT state = NONE means that state does not give the (finished) election result.

We haven’t yet proved the termination of this definition: we used mk thm, which creates a ”fake” theorem, without proving it.

This gives an induction theorem:

FINAL_STAGE_ind;
   |- !P.
     (!state.
        ((STAGE_RESULT state = NONE) ==> P (NEXT1_STAGE state)) ==>
        P state) ==>
     !v. P v

This theorem is clearly true if and only if repeated calls applying NEXT1 STAGE to a state eventually reaches a state where STAGE RESULT

state is not NONE.

As an alternative approach we defined, as an inductively defined relation, the concept of one state being a future state of another one.

val (IS_FUTURE_rule, IS_FUTURE_ind, IS_FUTURE_cases) = Hol_reln
  `(!state. IS_FUTURE init state /\ (STAGE_RESULT state = NONE) ==>
      IS_FUTURE init (NEXT1_STAGE state)) /\
    (IS_FUTURE init init)` ;

Here, IS FUTURE init state holds whenever repeated application of instances of the clauses given show it to be so, and not otherwise.

HOL automatically generates a theorem IS FUTURE ind

    |- !init IS_FUTURE'.
     (!state.
        IS_FUTURE' state /\ (STAGE_RESULT state = NONE) ==>
        IS_FUTURE' (NEXT1_STAGE state)) /\ IS_FUTURE' init ==>
     !a0. IS_FUTURE init a0 ==> IS_FUTURE' a0

This says that if any property is preserved from one state to the next (NEXT1 STAGE state), provided the first state does not have the finalised election result (STAGE RESULT state = NONE), and the property holds of the initial state then the property holds of all states in the future of the initial state. (note that IS FUTURE' is a variable)

This should enable us to deal with sanity checks of properties (like the distinctness of the remaining candidates) which are preserved from one state to the next.

The definition of IS FUTURE, above, derives new cases of init and state, such that IS FUTURE init state holds, by working forwards from state. Equally you can work backwards from init, as in the following definition:

val (IS_FUTURE_alt_rule, IS_FUTURE_alt_ind, IS_FUTURE_alt_cases) = Hol_reln
  `(IS_FUTURE_alt (NEXT1_STAGE init) final /\

 (STAGE_RESULT init = NONE) ==> IS_FUTURE_alt init final) /\
 (IS_FUTURE_alt final final)` ;

This gives a different definition, and, importantly, a different induction theorem, which may be easier to use.

First we need to prove the equivalence of these two definitions. IS FUTURE from alt';

|- IS_FUTURE (NEXT1_STAGE s') fst ==>
(STAGE_RESULT s' = NONE) ==>
IS_FUTURE s' fst

This says that IS FUTURE obeys the introduction rule of IS FUTURE alt, and is proved by induction on IS FUTURE.

Then we use this to show IS FUTURE from alt

|- IS_FUTURE_alt init state ==> IS_FUTURE init state

which is proved by induction on IS FUTURE alt. In the same way we prove IS FUTURE to alt

|- IS_FUTURE init state ==> IS_FUTURE_alt init state

so as to show that the two are equivalent, ie IS FUTURE eqv

|- IS_FUTURE = IS_FUTURE_alt : thm

We had also defined ALL STAGES, which gives the set of successive states in the counting process. It is defined as ALL STAGES def;

|- !states' state.
  ALL_STAGES (state::states') =
  case STAGE_RESULT state of
    NONE => ALL_STAGES (NEXT1_STAGE state::state::states')
  | SOME v => state::states'

The argument is a list of states, which should be the list of states reached so far, and returns the list of these and all subssequent states. It will be called with a singleton argument [init], the initial state.

Its definition generates an induction principle ALL STAGES ind

|- !P.
  (!state states'.
     ((STAGE_RESULT state = NONE) ==>
      P (NEXT1_STAGE state::state::states')) ==>
     P (state::states')) /\ P [] ==>
  !v. P v

So we should be able to show

IS\_FUTURE init state = MEM state (ALL\_STAGES [init])

We can prove MEM AS IF

   |- MEM fst (ALL_STAGES (s::ss)) ==> IS_FUTURE_alt s fst  MEM fst ss

using ALL STAGES ind, where the condition P on v is that if v is nonempty say v = s::ss, then this equality holds. Note that this is straightforward using the introduction clauses of IS FUTURE alt, not those of

IS FUTURE.

Then setting ss to be [], we get MEM AS1 IF

   |- MEM state (ALL_STAGES [init]) ==> IS_FUTURE_alt init state

(but note that we cannot prove MEM AS1 IF by induction directly, the inductive step needs to use, and can prove, the stronger result MEM AS IF.

   Then we prove IS FUTURE alt in AS
   |- IS_FUTURE_alt init state ==> !ss. MEM state (ALL_STAGES (init::ss))

by induction on IS FUTURE alt Again, we only want the case where ss = [], but the inductive step needs to use, and can prove, the stronger result

This actually requires another lemma, sub ALL STAGES

   |- set (s::ss) SUBSET set (ALL_STAGES (s::ss))

which we also proved using ALL STAGES ind These give us the result IS FUTURE ALL STAGES

   |- IS_FUTURE init state = MEM state (ALL_STAGES [init])
which we get from IS FUTURE alt in AS and IS FUTURE eqv

2 Some Sanity Check Conditions

2.1 That the list of candidates remains unchanged

We showed that the list of elected, excluded and remaining candidates is unchanged.

This needs to be formulated precisely, since these lists are changed by moving candidates from one list to another, and by re-ordering the remaining candidate list according to the number of votes each candidate has.

One possible way is to turn each list into a set, and to take the union of the sets, which literally should remain unchanged. But this only shows the desired property if the lists contain members which are all distinct.

In fact we want to show that these lists (jointly) contain all distinct members, as another useful sanity check condition. However if we use the built-in function PERM, which means that one list is a permutation of the other, we can achieve both results at once, because

|- !l1 l2. PERM l1 l2 ==> (set l1 = set l2)
|- !l1 l2. PERM l1 l2 ==> (ALL_DISTINCT l1 = ALL_DISTINCT l2)

The definition of PERM is provided by HOL, along with these and numerous other useful lemmas.

So we want to show that at each iteration, the concatenation of these lists is permuted. We defined ALL CANDS state to be the concatenation of these lists:

ALL_CANDS (time,seats,quota,elected,excluded,rem,surps,groups) =
     elected ++ excluded ++ MAP FST rem

Then the required result is

   PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)

However we need the condition rem3ne rem (where rem is the remaining candidates component of state. This means that for each remaining candidate the entry in rem has at least one group of votes. This is required by the code for EXTRACT SURPS which gets the surplus votes for an elected candidate, since the surplus votes are (at a reduced value) the last parcel of votes credited to that candidate. That this propoerty holds is clear enough since each candidate gets an initial parcel of votes, and then can only accumulate more (until elected or excluded).

state_rem3ne ;
   |- !seats cands ballots state.
        IS_FUTURE (INIT_STATE seats cands ballots) state ==>
     rem3ne (REM_CANDS_VAR state)

The following lemma, PERM elected rem, handles the phase of a counting step where the list of remaining candidates is divided into those elected with a surplus, those elected with exactly the right number of votes, and those continuing as “remaining candidates”.

This phase is handled by the three functions EXTRACT SURPS which returns a pair, of which the first (FST) component

is the remaining candidates after deleting those elected with a surplus DROP EXACT which returns the remaining candidates after deleting those

elected with just enough votes (no surplus) EXTRACT ELECTED which returns the candidates elected (its argument acc

just accumulates previous results)

These functions rely on their input list rem being sorted by number of votes, so their code need only look along the list from the start until reaching the first candidate not satisfying the relevant criterion.

Note that entries for remaining candidates consist of the candidate, total votes, and groups of votes, whereas EXTRACT ELECTED returns a list of just candidates. Hence the occurrences of MAP FST in the code below.

   |- !rem acc.
     rem3ne rem ==>
     SORTED (COMBINE TOTAL_COUNT $>=) rem ==>
     PERM
       (EXTRACT_ELECTED quota rem acc ++
        MAP FST (DROP_EXACT quota (FST (EXTRACT_SURPS quota rem []))))
       (acc ++ MAP FST rem)

Other parts of a counting step have relevant lemmas: for example, since the remaining candidates are sorted by total votes, we need MERGE SORT PERM

   |- !v v1. PERM (MERGE_SORT v v1) v1

At several stages in the proof, to cope with the rearrangement of candidates in the code (especially as some functions were written to be tail-recursive), we needed lemmas such as:

   |- PERM (ee ++ el ++ nl::ex ++ mfde) (el ++ ex ++ mfr)
      PERM (ee ++ nl::mfde) mfr

Finally this gave us the theorem PERM NEXT1 CANDS, that candidates are preserved:

   |- rem3ne rem ==>
   (state = (time,seats,quota,elected,excluded,rem,surps,groups)) ==>
   PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)

3 Difficulties in the proofs

3.1 Conditions which need to be proved

These are examples of conditions which seem obvious, and are assumed by the code (and, indeed, by the legislation), but proving that they hold requires several steps of reasoning and tracing through the code.

Termination of the main algorithm This relies on the fact that in each iteration of the algorithm (ie, in each call to NEXT1 STAGE), the state gets closer to the termination condition, which is that the number of elected and remaining candidates is less than or equal to the number of candidates to be elected. This relies on the fact that, at each iteration

– group of votes is distributed, or

– a remaining candidate is excluded

So we need to look at when new groups of votes are created, ready to be distributed. This occurs when

– a remaining candidate is elected

– a remaining candidate is excluded

So this requires constructing a measure on the state, involving

– the number of elected or “remaining” candidates

– the number of remaining candidates

– the number of groups of votes remaining to be distributed

and showing that this measure decreases at each iteration.

The condition that there be “remaining” candidates Since the counting program chooses the lowest ranking candidate to be eliminated, this code depends on the fact that the list of “remaining” candidates be non-empty.

Since the code finishes the count whenever the number of elected and remaining candidates is less than or equal to the number of candidates to be elected, the problem can arise only when too many candidates get elected. The mathematics defining the quota for election makes this impossible, but to prove it requires that the total number of votes represented by the state does not increase.

That transfer values do not have denominator zero The code relies on the fact that the denominator of a transfer value (which is a fraction) is not zero. This in turn relies on the fact that the final parcel of votes which elects a candidate is non-empty and that a candidate can get only one new parcel of votes in each iteration of the algorithm (ie, in each call

to NEXT1 STAGE).

3.2 Errors discovered

We found errors where conditions (expressed in HOL), which we set out to prove, were in fact not provable.

We have not yet found cases where this was due to errors in the code (that is, the specification, in HOL, of the program’s behaviour). Rather, the errors were all in the expression of conditions which were to be checked.

We surmise that this is because the “program” specification, in HOL, was translated into Standard ML, and tested. No doubt there were errors which were found in the course of this testing. On the other hand, the correctness conditions were not tested in this way.

The errors found were as follows.

taking the n’th member of a shorter list The condition that the list of remaining candidates are distinct:

    !entry1 entry2 x y. (EL x (REM_CANDS_VAR state) = entry1)
              /\ (EL y (REM_CANDS_VAR state) = entry2)
          ==> ((FST entry1 = FST entry2) ==> (x = y))

REM CANDS VAR gives the list of entries for the remaining candidates, where an entry consists of, firstly, the candidate name, and then the votes currently credited to that candidate. We want all the candidate names to be distinct.

This condition is erroneous in that EL n list is undefined for a list which is too short to have an n’th member.

In fact we reformulated the condition to use the predicate ALL DISTINCT, provided in HOL, which has the supplied theorem EL ALL DISTINCT EL EQ, which illustrates the need for a condition that the index is within the length of the list.

    |- !l.  ALL_DISTINCT l =
      !n1 n2.  n1 < LENGTH l /\ n2 < LENGTH l ==>
        ((EL n1 l = EL n2 l) =(n1 = n2))

need to assume candidates distinct initially To proving that the list of remaining candidates are distinct at any stage, it is necessary to assume that the list of candidates provided initially is distinct. This assumption was omitted.

characterization of states of the count Although we describe the functions ALL STAGES and IS FUTURE above, the specification of the program does not use these. They are used only to prove things about the program.

Initially the notion of a state which occurs during the count was given by

   (COUNT HCT seats cands ballots = FINAL STAGE state)

where COUNT HCT expresses the entire process: it calculates the initial state, and then applies FINAL STAGE, described above.

A state satisfies this condition if, by starting at that state, and completing the count, you reach the same final state as the actual count. While this condition is clearly satisfied by states in the actual count, it is not clear that it cannot be satisfied by states which are not states of the actual count.

So we replaced this condition by

   IS FUTURE (INIT STATE seats cands ballots) state

4 Overcoming some difficulties in the proofs

This section of this document was written some time after the preceding. Possibly some of the material in it could be incorporated in the earlier sections in due course.

4.1 Termination of the main routine

We added to the termination condition

– if there are no remaining candidates (other than those elected or eliminated) then the counting terminates

– if the list of remaining candidates does not satisfy rem3ne then the counting terminates

We aim to prove that neither of these conditions ever is needed. However having them there helps in the structure of the proof because it makes it possible to use the fact that the steps of the algorithm are welldefined in proving termination. Without doing this, we have to prove simultaneously that the algorithm is well-defined at each step and to prove termination, which is much more complicated.

So the termination measure is a lexicographic combination of

– the number of remaining candidates

– the number of groups of surplus votes waiting to be distributed

– the number of groups of votes waiting to be distributed from excluded candidates

It is easy to see that this reduces at each stage of the count, theorem FINAL STAGE term, where R is instantiated to the ordering mentioned just above.

?R. WF R /\
  !state. (STAGE_RESULT state = NONE) ==> R (NEXT1_STAGE state) state

From this we can define FINAL STAGE, using the HOL code, which uses the fact that we have a well-founded measure on the state which reduces at each counting step.

val FINAL_STAGE_def = tDefine "FINAL_STAGE" `FINAL_STAGE state =
  case STAGE_RESULT state of NONE => FINAL_STAGE (NEXT1_STAGE state)
        | SOME result => result` (ACCEPT_TAC FINAL_STAGE_term) ;

As noted above, we have proved, as state rem3ne, that at each stage rem3ne holds of the list of remaining candidates, which is easy enough since each candidate starts with a parcel of votes (which may be empty

— that’s fine, we need only that the candidate’s list of parcels of votes is not empty), and can only accumulate more.

4.2 Proving that the rem never becomes empty

To prove that REM CANDS VAR state, the list of remaining candidates, which we will call rem, is not empty, is more difficult.

This relies on the fact that if rem is [] but the first condition in

STAGE RESULT def, namely LENGTH elected + LENGTH rem <= seats is

not already satisfied, then we must have LENGTH elected > seats, ie too many people have been elected.

This is impossible in a system using the Droop quota, but to prove it we need a preservation of vote numbers argument, where an elected candidate is represented by quota votes, and we could fractional votes according to the transfer value. Even so we lose votes because an elected canddiate may have a fractional number of votes, but we only transfer (count - quota), a whole number.

However we need to take account of fractional numbers of votes, because parcels of transferred votes can get collected together if they have the same transfer value (see code of COALESCE and GROUP), and this can result in the integer vote numbers increasing (eg, two parcels of 2/3 vote each).

In proving the first lemma regarding preservation of vote numbers, we discovered that we need to use the fact that transfer values have non-zero denominator (simply because the value of a group of votes is the transfer value multiplied by the number of votes).

4.3 Proving that transfer values do not have denominator zero

The denominator of a transfer value is the size of the parcel of votes when the transfer value is calculated (the numerator being the number of surplus votes, above the quote, of a candidate). Note that such a parcel can subsequently be divided up, including into empty parts, but when the transfer value is calculated we need it to be non-empty.

To show that no transfer value has zero denominator we need to check where such transfer values originate — it is in EXTRACT SURPS which should take the last parcel of votes for each newly elected candidate.

The argument is:

– if a candidate gets enough to be elected in one count, he is removed (by EXTRACT ELECTED) and his surplus transferred (by EXTRACT SURPS) at the start of the next count

– a candidate only gets one parcel of votes per count

– therefore once a candidate reaches the quota he doesn’t get any more votes

– therefore a successful candidate’s last parcel of votes must be nonempty

Definition 1 (LPNE def). A candidate satisfies LPNE iff: if he has at least a quota of votes then his latest parcel of votes is non-empty.

LPNE quota (name, count, (tv, bs, cl) :: gl) =
  count >= quota ==> ~ (bs = [])

Lemma 1 (REM TOT NEXT). A candidate’s total vote count, minus the value of his latest parcel of votes, is less than a quota

rem3ne (REM_CANDS_VAR state) ==>
    MEM (name, tot, g :: gl) (REM_CANDS_VAR (NEXT1_STAGE state)) ==>
        tot - GROUP_VAL (FIRST_TWO g) < QUOTA_VAR state

Thus, if he has at least a quota, then his latest parcel is non-empty.

Lemma 2 (REM NZD LPNE). given the sanity conditions rem3ne (already proved) and R TVnzd (which says that transfer values already calculated have non-zero denominator), a candidate satisfies LPNE,

rem3ne (REM_CANDS_VAR state) ==>
    MEM rc (REM_CANDS_VAR (NEXT1_STAGE state)) ==>
        R_TVnzd rc ==> LPNE (QUOTA_VAR state) rc

So the transfer value when his own surplus is transferred will have non-zero denominator.

From these we get the theorem:

Theorem 1 (all S TVnzd). all transfer values involved in all states have non-zero denominator.

!seats cands ballots state.
     IS_FUTURE (INIT_STATE seats cands ballots) state ==> S_TVnzd state