Theory MuchAdoAboutTwo
section ‹Much Ado about Two›
theory MuchAdoAboutTwo
imports "HOL-Combinatorics.Permutations"
begin
text ‹
Due to Donald E. Knuth, it is known for some time that certain sorting
functions for lists of arbitrary types can be proved correct by only showing
that they are correct for boolean lists (\<^cite>‹"KnuthSortingAndSearching"›,
see also \<^cite>‹"LogicalAbstractionsInHaskell"›).
This reduction idea, i.e. reducing a proof for an arbitrary type to a proof for a fixed type with a fixed number of values, has also instances in other
fields.
Recently, in \<^cite>‹"MuchAdoAboutTwo"›, a similar result as Knuth's 0-1-principle
is explained for the problem of parallel prefix computation
\<^cite>‹"PrefixSumsAndTheirApplications"›.
That is the task to compute, for given $x_1, \ldots, x_n$ and an associative
operation $\oplus$, the values $x_1$, $x_1 \oplus x_2$, $\ldots$,
$x_1 \oplus x_2 \oplus \cdots \oplus x_n$.
There are several solutions which optimise this computation, and an
obvious question is to ask whether these solutions are correct.
One way to answer this question is given in \<^cite>‹"MuchAdoAboutTwo"›.
There, a ``0-1-2-principle'' is proved which relates an unspecified solution
of the parallel prefix computation, expressed as a function ‹candidate›,
with ‹scanl1›, a functional representation of the parallel prefix
computation. The essence proved in the mentioned paper is as follows:
If ‹candidate› and ‹scanl1› behave identical on all lists over
a type which has three elements, then ‹candidate› is semantically
equivalent to ‹scanl1›, that is, ‹candidate› is a correct solution
of the parallel prefix computation.
Although it seems that nearly nothing is known about the function
‹candidate›, it turns out that the type of ‹candidate› already
suffices for the proof of the paper's result. The key is relational
parametricity \<^cite>‹"TypesAbstractionsAndParametricPolymorphism"› in the form of
a free theorem \<^cite>‹"TheoremsForFree"›. This, some rewriting and a few
properties about list-processing functions thrown in allow to proof the
``0-1-2-principle''.
The paper first shows some simple properties and derives a specialisation of
the free theorem. The proof of the main theorem itself is split up in two
parts. The first, and considerably more complicated part relates lists over a
type with three values to lists of integer lists. Here, the paper uses
several figures to demonstrate and shorten several proofs. The second part then
relates lists of integer list with lists over arbitrary types, and consists of
applying the free theorem and some rewriting. The combination of these two
parts then yields the theorem.
Th article at hand formalises the proofs given in \<^cite>‹"MuchAdoAboutTwo"›,
which is called here ``the original paper''. Compared to that paper, there are
several differences in this article. The major differences are listed below.
A more detailed collection follows thereafter.
\begin{itemize}
\item The original paper requires lists to be non-empty. Eventhough lists in
Isabelle may also be empty, we stick to Isabelle's list datatype instead of
declaring a new datatype, due to the huge, already existing theory about
lists in Isabelle. As a consequence, however, several modifications become
necessary.
\item The figure-based proofs of the original paper are replaced by formal
proofs. This forms a major part of this article (see Section 6).
\item Instead of integers, we restrict ourselves to natural numbers. Thus,
several conditions can be simplified since every natural number is greater
than or equal to ‹0›. This decision has no further influence on the
proofs because they never consider negative integers.
\item Mainly due to differences between Haskell and Isabelle, certain notations
are different here compared to the original paper. List concatenation is
denoted by ‹@› instead of $++$, and in writing down intervals, we use
‹[0..<k + 1]› instead of ‹[0..k]›. Moreover, we write ‹f›
instead of $\oplus$ and ‹g› instead of $\otimes$. Functions mapping
an element of the three-valued type to an arbitrary type are denoted by
‹h›.
\end{itemize}
Whenever we use lemmas from already existing Isabelle theories, we qualify
them by their theory name. For example, instead of ‹map_map›, we
write ‹List.map_map› to point out that this lemma is taken from
Isabelle's list theory.
The following comparison shows all differences of this article compared to the
original paper. The items below follow the structure of the original paper
(and also this article's structure). They also highlight the challenges which
needed to be solved in formalising the original paper.
\begin{itemize}
\item Introductions of several list functions (e.g. ‹length›,
‹map›, ‹take›) are dropped. They exist already in Isabelle's list
theory and are be considered familiar to the reader.
\item The free theorem given in Lemma 1 of the original paper is not sufficient
for later proofs, because the assumption is not appropriate in the context
of Isabelle's lists, which may also be empty. Thus, here, Lemma 1 is a
derived version of the free theorem given as Lemma 1 in the original paper,
and some additional proof-work is done.
\item Before proceeding in the original paper's way, we state and proof
additional lemmas, which are not part of Isabelle's libraries. These lemmas
are not specific to this article and may also be used in other theories.
\item Laws 1 to 8 and Lemma 2 of the original paper are explicitly proved.
Most of the proofs follow directly from existing results of Isabelle's list
theory. To proof Law 7, Law 8 and Lemma 2, more work was necessary, especially
for Law 8.
\item Lemma 3 and its proof are nearly the same here as in the original paper.
Only the additional assumptions of Lemma 1, due to Isabelle's list datatype,
have to be shown.
\item Lemma 4 is split up in several smaller lemmas, and the order of them
tries to follow the structure of the original paper's Lemma 4.
For every figure of the original paper, there is now one separate proof.
These proofs constitute the major difference in the structure of this article
compared to the original paper.
The proof of Lemma 4 in the original paper concludes by combining the results
of the figure-based proofs to a non-trivial permutation property. These three
sentences given in the original paper are split up in five separate lemmas
and according proofs, and therefore, they as well form a major difference to
the original paper.
\item Lemma 5 is mostly identical to the version in the original paper. It has
one additional assumption required by Lemma 4. Moreover, the proof is slightly
more structured, and some steps needed a bit more argumentation than in the
original paper.
\item In principle, Proposition 1 is identical to the according proposition in
the original paper. However, to fulfill the additional requirement of Lemma 5,
an additional lemma was proved. This, however, is only necessary, because we
use Isabelle's list type which allows lists to be empty.
\item Proposition 2 contains one non-trivial step, which is proved as a
seperate lemma. Note that this is not due to any decisions of using special
datatypes, but inherent in the proof itself. Apart from that, the proof is
identical to the original paper's proof of Proposition 2.
\item The final theorem is, as in the original paper, just a combination of
Proposition 1 and Proposition 2. Only the assumptions are extended due to
Isabelle's list datatype.
\end{itemize}
›
section ‹Basic definitions›
fun foldl1 :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a list ⇒ 'a"
where
"foldl1 f (x # xs) = foldl f x xs"
fun scanl1 :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a list ⇒ 'a list"
where
"scanl1 f xs = map (λk. foldl1 f (take k xs))
[1..<length xs + 1]"
text ‹
The original paper further relies on associative functions. Thus, we define
another predicate to be able to express this condition:
›
definition
"associative f ≡ (∀x y z. f x (f y z) = f (f x y) z)"
text ‹
The following constant symbols represents our unspecified function. We want to
show that this function is semantically equivalent to ‹scanl1›, provided
that the first argument is an associative function.
›
consts
candidate :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a list ⇒ 'a list"
text ‹
With the final theorem, it suffices to show that ‹candidate› behaves like
‹scanl1› on all lists of the following type, to conclude that
‹canditate› is semantically equivalent to ‹scanl1›.
›