% symbols to change   ∃ ∧ ∀ ⇒ ∪ 
% :.,$s/∀/!/g
% :.,$s/∃/?/g
% :.,$s/⇒/==>/g
% :.,$s/∪/UNION/g
% :.,$s/⊆/SUBSET/g
% :.,$s/¬/\~ /g
% :.,$s/λ/\\/g
% :.,$s/⇔ /=/g
% :.,$s/∧/\/\\/g


\documentclass[a4paper,11pt]{llncs}

\begin{document}

\section{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, 
$\forall x y.\ A$, $\exists x y.\ A$ and $\lambda x y.\ A$
are written as 
\texttt{!x y.\ A}, \texttt{?x y.\ A} and \texttt{\\ x y.\ A}.
The logical connectives $\lnot$, $\land$,k $\lor$ and $\Rightarrow$ 
are written as \verb!~!, \verb!/\!, \verb!\/! and \verb!==>!.

\subsection{\texttt{MERGE}}

\begin{verbatim}
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))`;
\end{verbatim}

(this is part of defining \texttt{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 \texttt{MERGE} function, called \texttt{MERGE\_ind}:

\begin{verbatim}
   |- !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
\end{verbatim}

which says that, assuming
\begin{itemize}
  \item P R ls rs holds whenever ls or rs is empty
  \item P R (l::ls) (r::rs) holds provided that
  \item P R ls (r::rs) and P R (l::ls) rs hold
\end{itemize}
then P v ls rs holds in all cases

HOL proves this to show that the function \texttt{MERGE} terminates.
Note that if you instantiate P to
``the definition of \texttt{MERGE}, above, terminates with these arguments"
then the theorem \texttt{MERGE\_ind} says that
the definition of \texttt{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
\begin{verbatim}
set (MERGE c l r) = set l UNION set r
\end{verbatim}

So we instantiate P of the theorem \texttt{MERGE\_ind} to

\begin{verbatim}
\c l r. set (MERGE c l r) = set l UNION set r
\end{verbatim}

which gives that

\begin{verbatim}
!v v1 v2. set (MERGE v v1 v2) = set v1 UNION set v2
\end{verbatim}

provided several conditions hold, which are
\begin{verbatim}
 (!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)))
\end{verbatim}
Since these conditions match the definition of \texttt{MERGE},
(essentially they say that each step in the definition of \texttt{MERGE}
preserves the property
\begin{verbatim}
 set (MERGE v v1 v2) = set v1 UNION set v2)
\end{verbatim}
they are quite easily proved.

Thus we get the theorem
\begin{verbatim}
!v v1 v2. set (MERGE v v1 v2) = set v1 UNION set v2
\end{verbatim}

\subsection{\texttt{MERGE\_SORT}}

The definition of \texttt{MERGE\_SORT} is
\begin{verbatim}
	(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)
\end{verbatim}

\texttt{TAKE n list} returns a list consisting of the first $n$ members of 
\texttt{list}.

\texttt{DROP n list} returns a list consisting of all but the 
first $n$ members of \texttt{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 \texttt{MERGE\_SORT R L} generates a call of
 \texttt{MERGE\_SORT R' L'}, then $(R',L') < (R,L)$.

HOL uses R' for the well-founded relation,
and uses \texttt{MERGE\_SORT\_tupled\_aux (R, L) = MERGE\_SORT R L}.
So the goal for the user to prove is 

\begin{verbatim}
     ?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)
\end{verbatim}

and once that is proved, the resulting theorem \texttt{MERGE\_SORT\_ind} is 

\begin{verbatim}
   |- !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
\end{verbatim}

Again, if you instantiate P to
``the definition of \texttt{MERGE\_SORT} above, terminates with these arguments"
then the theorem \texttt{MERGE\_SORT\_ind} says that the definition of
\texttt{MERGE\_SORT}
 terminates in all cases.

We want to prove that 
\begin{verbatim}
!v v1. set (MERGE_SORT v v1) = set v1
\end{verbatim}
so we instantiate P in \texttt{MERGE\_SORT\_ind} to
\begin{verbatim}
\c l. set (MERGE_SORT c l) = set l
\end{verbatim}
to get a lemma whose conclusion is 
\begin{verbatim}
!v v1. set (MERGE_SORT v v1) = set v1
\end{verbatim}
and whose assumptions essentially say that 
each step in the definition of \texttt{MERGE\_SORT}
preserves the property \texttt{set (MERGE\_SORT v v1) = set v1}.

\subsection{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 \texttt{NEXT1\_STAGE} returns the next state (1 step)
from a given state.

Then we defined \texttt{FINAL\_STAGE} in terms of \texttt{NEXT1\_STAGE}

\begin{verbatim}
   |- !state.
     FINAL_STAGE state =
     case STAGE_RESULT state of
       NONE => FINAL_STAGE (NEXT1_STAGE state)
     | SOME result => result
\end{verbatim}

\texttt{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 \texttt{mk\_thm}, which creates a "fake" theorem, without proving it.

This gives an induction theorem:

\begin{verbatim}
FINAL_STAGE_ind;
   |- !P.
     (!state.
        ((STAGE_RESULT state = NONE) ==> P (NEXT1_STAGE state)) ==>
        P state) ==>
     !v. P v
\end{verbatim}

This theorem is clearly true if and only if repeated calls applying
 \texttt{NEXT1\_STAGE} to a state eventually reaches a state where
\texttt{STAGE\_RESULT state}
is not \texttt{NONE}.

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

\begin{verbatim}
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)` ;
\end{verbatim}

Here, \texttt{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 \texttt{IS\_FUTURE\_ind}

\begin{verbatim}
    |- !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
\end{verbatim}

This says that if any property is preserved from one state to the next
(\texttt{NEXT1\_STAGE state}),
 provided the first state does not have the finalised
election result (\texttt{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 \texttt{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 \texttt{IS\_FUTURE}, above,
 derives new cases of init and state,
such that \texttt{IS\_FUTURE init state} holds, by working forwards from state.
Equally you can work backwards from init, as in the following definition:

\begin{verbatim}
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)` ;
\end{verbatim}

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.
\texttt{IS\_FUTURE\_from\_alt'};
\begin{verbatim}
   |- IS_FUTURE (NEXT1_STAGE s') fst ==>
   (STAGE_RESULT s' = NONE) ==>
   IS_FUTURE s' fst
\end{verbatim}

This says that \texttt{IS\_FUTURE} obeys the introduction rule of
\texttt{IS\_FUTURE\_alt},
and is proved by induction on \texttt{IS\_FUTURE}.

Then we use this to show
\texttt{IS\_FUTURE\_from\_alt}
\begin{verbatim}
   |- IS_FUTURE_alt init state ==> IS_FUTURE init state
\end{verbatim}

which is proved by induction on \texttt{IS\_FUTURE\_alt}.

In the same way we prove
\texttt{IS\_FUTURE\_to\_alt}
\begin{verbatim}
   |- IS_FUTURE init state ==> IS_FUTURE_alt init state
\end{verbatim}

so as to show that the two are equivalent, ie
\texttt{IS\_FUTURE\_eqv}
\begin{verbatim}
   |- IS_FUTURE = IS_FUTURE_alt : thm
\end{verbatim}

We had also defined \texttt{ALL\_STAGES},
which gives the set of successive states in the counting process.
It is defined as
\texttt{ALL\_STAGES\_def};
\begin{verbatim}
   |- !states' state.
     ALL_STAGES (state::states') =
     case STAGE_RESULT state of
       NONE => ALL_STAGES (NEXT1_STAGE state::state::states')
     | SOME v => state::states'
\end{verbatim}

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
\texttt{ALL\_STAGES\_ind}
\begin{verbatim}
   |- !P.
     (!state states'.
        ((STAGE_RESULT state = NONE) ==>
         P (NEXT1_STAGE state::state::states')) ==>
        P (state::states')) /\ P [] ==>
     !v. P v
\end{verbatim}

So we should be able to show
\begin{verbatim}
IS\_FUTURE init state = MEM state (ALL\_STAGES [init])
\end{verbatim}

We can prove
\texttt{MEM\_AS\_IF}
\begin{verbatim}
   |- MEM fst (ALL_STAGES (s::ss)) ==> IS_FUTURE_alt s fst ∨ MEM fst ss
\end{verbatim}
using \texttt{ALL\_STAGES\_ind},
where the condition P on v is that if v is non-empty
say v = s::ss, then this equality holds.
Note that this is straightforward using the introduction clauses of
\texttt{IS\_FUTURE\_alt}, not those of \texttt{IS\_FUTURE}.

Then setting ss to be [], we get
\texttt{MEM\_AS1\_IF}
\begin{verbatim}
   |- MEM state (ALL_STAGES [init]) ==> IS_FUTURE_alt init state
\end{verbatim}
(but note that we cannot prove \texttt{MEM\_AS1\_IF} by induction directly,
the inductive step needs to use, and can prove, the stronger result
\texttt{MEM\_AS\_IF}.

Then we prove
\texttt{IS\_FUTURE\_alt\_in\_AS}
\begin{verbatim}
   |- IS_FUTURE_alt init state ==> !ss. MEM state (ALL_STAGES (init::ss))
\end{verbatim}
by induction on \texttt{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,
\texttt{sub\_ALL\_STAGES}
\begin{verbatim}
   |- set (s::ss) SUBSET set (ALL_STAGES (s::ss))
\end{verbatim}
which we also proved using \texttt{ALL\_STAGES\_ind}

These give us the result
\texttt{IS\_FUTURE\_ALL\_STAGES}
\begin{verbatim}
   |- IS_FUTURE init state = MEM state (ALL_STAGES [init])
\end{verbatim}
which we get from \texttt{IS\_FUTURE\_alt\_in\_AS} and \texttt{IS\_FUTURE\_eqv} 

\section{Some Sanity Check Conditions}

\subsection{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 \texttt{PERM},
which means that one list is a permutation of the other,
we can achieve both results at once, because

\begin{verbatim}
|- !l1 l2. PERM l1 l2 ==> (set l1 = set l2)
|- !l1 l2. PERM l1 l2 ==> (ALL_DISTINCT l1 = ALL_DISTINCT l2)
\end{verbatim}

The definition of \texttt{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 \texttt{ALL\_CANDS state} to be the concatenation of these lists:
\begin{verbatim}
ALL_CANDS (time,seats,quota,elected,excluded,rem,surps,groups) =
     elected ++ excluded ++ MAP FST rem
\end{verbatim}

Then the required result is
\begin{verbatim}
   PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)
\end{verbatim}

However we need the condition \texttt{rem3ne rem}
(where \texttt{rem} is the remaining candidates component of \texttt{state}.
This means that for each remaining candidate the entry in \texttt{rem} 
has at least one group of votes.
This is required by the code for \texttt{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).

\begin{verbatim}
state_rem3ne ;
   |- !seats cands ballots state.
        IS_FUTURE (INIT_STATE seats cands ballots) state ==>
	     rem3ne (REM_CANDS_VAR state) 
\end{verbatim}

 
The following lemma, \texttt{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
\begin{description}
\item[\texttt{EXTRACT\_SURPS}] which returns a pair, of which the first
(\texttt{FST}) component is the remaining candidates after
deleting those elected with a surplus
\item[\texttt{DROP\_EXACT}] which returns the remaining candidates after
deleting those elected with just enough votes (no surplus)
\item[\texttt{EXTRACT\_ELECTED}] which returns the candidates elected
(its argument \texttt{acc} just accumulates previous results)
\end{description}
These functions rely on their input list \texttt{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 \texttt{EXTRACT\_ELECTED} returns a list of just candidates.
% (and, in other code examples, \texttt{elected} and \texttt{excluded})
Hence the occurrences of \texttt{MAP FST} in the code below.

\begin{verbatim}
   |- !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)
\end{verbatim}

Other parts of a counting step have relevant lemmas:
for example, since the remaining candidates are sorted by total votes,
we need \texttt{MERGE\_SORT\_PERM}

\begin{verbatim}
   |- !v v1. PERM (MERGE_SORT v v1) v1
\end{verbatim}

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:
\begin{verbatim}
   |- PERM (ee ++ el ++ nl::ex ++ mfde) (el ++ ex ++ mfr) ⇔
      PERM (ee ++ nl::mfde) mfr
\end{verbatim}

Finally this gave us the theorem \texttt{PERM\_NEXT1\_CANDS},
that candidates are preserved:

\begin{verbatim}
   |- rem3ne rem ==>
   (state = (time,seats,quota,elected,excluded,rem,surps,groups)) ==>
   PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)
\end{verbatim}

\section{Difficulties in the proofs}

\subsection{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.

\subsubsection{Termination of the main algorithm}
This relies on the fact that in each iteration of the algorithm
(ie, in each call to \texttt{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
\begin{itemize}
\item group of votes is distributed, or 
\item a remaining candidate is excluded
\end{itemize}
So we need to look at when new groups of votes are created, 
ready to be distributed.
This occurs when
\begin{itemize}
\item a remaining candidate is elected
\item a remaining candidate is excluded
\end{itemize}

So this requires constructing a measure on the state, involving
\begin{itemize}
\item the number of elected or ``remaining" candidates
\item the number of remaining candidates
\item the number of groups of votes remaining to be distributed
\end{itemize}
and showing that this measure decreases at each iteration.

\subsubsection{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.

\subsubsection{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 
\texttt{NEXT1\_STAGE}).

\subsection{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.

\subsubsection{taking the $n$'th member of a shorter list}
The condition that the list of remaining candidates are distinct:

\begin{verbatim}
    !entry1 entry2 x y. (EL x (REM_CANDS_VAR state) = entry1)
              /\ (EL y (REM_CANDS_VAR state) = entry2)
          ==> ((FST entry1 = FST entry2) ==> (x = y))
\end{verbatim}

\texttt{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 \texttt{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
\texttt{ALL\_DISTINCT}, provided in HOL, which has the supplied theorem
\texttt{EL\_ALL\_DISTINCT\_EL\_EQ}, which illustrates the need for a condition
that the index is within the length of the list. 
\begin{verbatim}
    |- !l.  ALL_DISTINCT l = 
      !n1 n2.  n1 < LENGTH l /\ n2 < LENGTH l ==>
        ((EL n1 l = EL n2 l) =(n1 = n2))
\end{verbatim}

\subsubsection{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. 

\subsubsection{characterization of states of the count}
Although we describe the functions \texttt{ALL\_STAGES} and
\texttt{IS\_FUTURE} above, the specification of the program does not use these.
They are used only to prove things \emph{about} the program.

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

\texttt{(COUNT\_HCT seats cands ballots = FINAL\_STAGE state)}

where \texttt{COUNT\_HCT} expresses the entire process: it calculates the
initial state, and then applies \texttt{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 

\texttt{IS\_FUTURE (INIT\_STATE seats cands ballots) state}

\section{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.

\subsection{Termination of the main routine}

We added to the termination condition
\begin{itemize}
\item if there are no remaining candidates (other than those elected or
eliminated) then the counting terminates
\item if the list of remaining candidates does not satisfy
\texttt{rem3ne} then the counting terminates
\end{itemize}

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 well-defined
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
\begin{itemize}
\item the number of remaining candidates
\item the number of groups of surplus votes waiting to be distributed
\item the number of groups of votes waiting to be distributed from excluded
candidates
\end{itemize}

It is easy to see that this reduces at each stage of the count,
theorem \texttt{FINAL\_STAGE\_term}, where \texttt{R} is instantiated
to the ordering mentioned just above.

\begin{verbatim}
?R. WF R /\
  !state. (STAGE_RESULT state = NONE) ==> R (NEXT1_STAGE state) state
\end{verbatim}

From this we can define \texttt{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.

\begin{verbatim}
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) ;
\end{verbatim}

As noted above, we have proved, as \texttt{state\_rem3ne},
that at each stage \texttt{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.

\subsection{Proving that the \texttt{rem} never becomes empty }

To prove that \texttt{REM\_CANDS\_VAR state}, the list of remaining candidates,
which we will call \texttt{rem}, is not empty, is more difficult.

This relies on the fact that if \texttt{rem} is \texttt{[]} 
but the first condition in \texttt{STAGE\_RESULT\_def},
namely \texttt{LENGTH elected + LENGTH rem <= seats}
is not already satisfied, then we must have \texttt{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 (\texttt{count} - \texttt{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 \texttt{COALESCE} and \texttt{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).

\subsection{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 \texttt{EXTRACT\_SURPS}
which should take the last parcel of votes for each newly elected candidate.

The argument is:
\begin{itemize}
\item if a candidate gets enough to be elected in one count,
  he is removed (by \texttt{EXTRACT\_ELECTED}) and his surplus transferred
  (by \texttt{EXTRACT\_SURPS}) at the start of the next count

\item a candidate only gets one parcel of votes per count

\item therefore once a candidate reaches the quota he doesn't get any more
votes

\item therefore a successful candidate's last parcel of votes must be non-empty
\end{itemize}

\begin{definition}[\texttt{LPNE\_def}]
A candidate satisfies \texttt{LPNE} iff: if he
has at least a quota of votes then his latest parcel of votes is non-empty.
\end{definition}

\begin{verbatim}
LPNE quota (name, count, (tv, bs, cl) :: gl) =
  count >= quota ==> ~ (bs = [])
\end{verbatim}

\begin{lemma}[\texttt{REM\_TOT\_NEXT}]
A candidate's total vote count,
minus the value of his latest parcel of votes, is less than a quota
\end{lemma}

\begin{verbatim}
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
\end{verbatim}

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

\begin{lemma}[\texttt{REM\_NZD\_LPNE}] 
given the sanity conditions 
rem3ne (already proved) and \texttt{R\_TVnzd} 
(which says that transfer values already calculated have non-zero denominator),
a candidate satisfies \texttt{LPNE},
\end{lemma}

\begin{verbatim}
rem3ne (REM_CANDS_VAR state) ==>
    MEM rc (REM_CANDS_VAR (NEXT1_STAGE state)) ==>
        R_TVnzd rc ==> LPNE (QUOTA_VAR state) rc
\end{verbatim}

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

From these we get the theorem: 

\begin{theorem}[\texttt{all\_S\_TVnzd}]
all transfer values involved in
all states have non-zero denominator.
\end{theorem}

\begin{verbatim}
!seats cands ballots state.
     IS_FUTURE (INIT_STATE seats cands ballots) state ==> S_TVnzd state
\end{verbatim}






\begin{verbatim}
\end{verbatim}
\end{document}

