Archive of Formal Proofs

An Isabelle/HOL formalisation of Green's Theorem

Mohammad Abdulaziz, Lawrence C. Paulson — 11 Jan 2018 00:00:00 +0000

We formalise a statement of Green’s theorem—the first formalisation to our knowledge—in Isabelle/HOL. The theorem statement that we formalise is enough for most applications, especially in physics and engineering. Our formalisation is made possible by a novel proof that avoids the ubiquitous line integral cancellation argument. This eliminates the need to formalise orientations and region boundaries explicitly with respect to the outwards-pointing normal vector. Instead we appeal to a homological argument about equivalences between paths.

Taylor Models

Christoph Traut, Fabian Immler — 08 Jan 2018 00:00:00 +0000

We present a formally verified implementation of multivariate Taylor models. Taylor models are a form of rigorous polynomial approximation, consisting of an approximation polynomial based on Taylor expansions, combined with a rigorous bound on the approximation error. Taylor models were introduced as a tool to mitigate the dependency problem of interval arithmetic. Our implementation automatically computes Taylor models for the class of elementary functions, expressed by composition of arithmetic operations and basic functions like exp, sin, or square root.

The Falling Factorial of a Sum

Lukas Bulwahn — 22 Dec 2017 00:00:00 +0000

This entry shows that the falling factorial of a sum can be computed with an expression using binomial coefficients and the falling factorial of its summands. The entry provides three different proofs: a combinatorial proof, an induction proof and an algebraic proof using the Vandermonde identity. The three formalizations try to follow their informal presentations from a Mathematics Stack Exchange page as close as possible. The induction and algebraic formalization end up to be very close to their informal presentation, whereas the combinatorial proof first requires the introduction of list interleavings, and significant more detail than its informal presentation.

The Median-of-Medians Selection Algorithm

Manuel Eberl — 21 Dec 2017 00:00:00 +0000

This entry provides an executable functional implementation of the Median-of-Medians algorithm for selecting the k-th smallest element of an unsorted list deterministically in linear time. The size bounds for the recursive call that lead to the linear upper bound on the run-time of the algorithm are also proven.

The Mason–Stother's Theorem

Manuel Eberl — 21 Dec 2017 00:00:00 +0000

This article provides a formalisation of Snyder’s simple and elegant proof of the Mason–Stothers theorem, which is the polynomial analogue of the famous abc Conjecture for integers. Remarkably, Snyder found this very elegant proof when he was still a high-school student.

In short, the statement of the theorem is that three non-zero coprime polynomials A, B, C over a field which sum to 0 and do not all have vanishing derivatives fulfil max{deg(A), deg(B), deg(C)} < deg(rad(ABC)) where the rad(P) denotes the radical of P, i. e. the product of all unique irreducible factors of P.

This theorem also implies a kind of polynomial analogue of Fermat’s Last Theorem for polynomials: except for trivial cases, Aⁿ + Bⁿ + Cⁿ = 0 implies n ≤ 2 for coprime polynomials A, B, C over a field.

Dirichlet L-Functions and Dirichlet's Theorem

Manuel Eberl — 21 Dec 2017 00:00:00 +0000

This article provides a formalisation of Dirichlet characters and Dirichlet L-functions including proofs of their basic properties – most notably their analyticity, their areas of convergence, and their non-vanishing for ℜ(s) ≥ 1. All of this is built in a very high-level style using Dirichlet series. The proof of the non-vanishing follows a very short and elegant proof by Newman, which we attempt to reproduce faithfully in a similar level of abstraction in Isabelle.

This also leads to a relatively short proof of Dirichlet’s Theorem, which states that, if h and n are coprime, there are infinitely many primes p with p ≡ h (mod n).

The string search algorithm by Knuth, Morris and Pratt

Fabian Hellauer, Peter Lammich — 18 Dec 2017 00:00:00 +0000

The Knuth-Morris-Pratt algorithm is often used to show that the problem of finding a string s in a text t can be solved deterministically in O(|s| + |t|) time. We use the Isabelle Refinement Framework to formulate and verify the algorithm. Via refinement, we apply some optimisations and finally use the Sepref tool to obtain executable code in Imperative/HOL.

Stochastic Matrices and the Perron-Frobenius Theorem

René Thiemann — 22 Nov 2017 00:00:00 +0000

Stochastic matrices are a convenient way to model discrete-time and finite state Markov chains. The Perron–Frobenius theorem tells us something about the existence and uniqueness of non-negative eigenvectors of a stochastic matrix. In this entry, we formalize stochastic matrices, link the formalization to the existing AFP-entry on Markov chains, and apply the Perron–Frobenius theorem to prove that stationary distributions always exist, and they are unique if the stochastic matrix is irreducible.

The IMAP CmRDT

Tim Jungnickel, Lennart Oldenburg, Matthias Loibl — 09 Nov 2017 00:00:00 +0000

We provide our Isabelle/HOL formalization of a Conflict-free Replicated Datatype for Internet Message Access Protocol commands. We show that Strong Eventual Consistency (SEC) is guaranteed by proving the commutativity of concurrent operations. We base our formalization on the recently proposed "framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes" (AFP.CRDT) from Gomes et al. Hence, we provide an additional example of how the recently proposed framework can be used to design and prove CRDTs.

Hybrid Multi-Lane Spatial Logic

Sven Linker — 06 Nov 2017 00:00:00 +0000

We present a semantic embedding of a spatio-temporal multi-modal logic, specifically defined to reason about motorway traffic, into Isabelle/HOL. The semantic model is an abstraction of a motorway, emphasising local spatial properties, and parameterised by the types of sensors deployed in the vehicles. We use the logic to define controller constraints to ensure safety, i.e., the absence of collisions on the motorway. After proving safety with a restrictive definition of sensors, we relax these assumptions and show how to amend the controller constraints to still guarantee safety.

The Kuratowski Closure-Complement Theorem

Peter Gammie, Gianpaolo Gioiosa — 26 Oct 2017 00:00:00 +0000

We discuss a topological curiosity discovered by Kuratowski (1922): the fact that the number of distinct operators on a topological space generated by compositions of closure and complement never exceeds 14, and is exactly 14 in the case of R. In addition, we prove a theorem due to Chagrov (1982) that classifies topological spaces according to the number of such operators they support.

Transition Systems and Automata

Julian Brunner — 19 Oct 2017 00:00:00 +0000

This entry provides a very abstract theory of transition systems that can be instantiated to express various types of automata. A transition system is typically instantiated by providing a set of initial states, a predicate for enabled transitions, and a transition execution function. From this, it defines the concepts of finite and infinite paths as well as the set of reachable states, among other things. Many useful theorems, from basic path manipulation rules to coinduction and run construction rules, are proven in this abstract transition system context. The library comes with instantiations for DFAs, NFAs, and Büchi automata.

Büchi Complementation

Julian Brunner — 19 Oct 2017 00:00:00 +0000

This entry provides a verified implementation of rank-based Büchi Complementation. The verification is done in three steps:

Definition of odd rankings and proof that an automaton rejects a word iff there exists an odd ranking for it.
Definition of the complement automaton and proof that it accepts exactly those words for which there is an odd ranking.
Verified implementation of the complement automaton using the Isabelle Collections Framework.

Evaluate winding numbers through Cauchy indices

Wenda Li — 17 Oct 2017 00:00:00 +0000

In complex analysis, the winding number measures the number of times a path (counterclockwise) winds around a point, while the Cauchy index can approximate how the path winds. This entry provides a formalisation of the Cauchy index, which is then shown to be related to the winding number. In addition, this entry also offers a tactic that enables users to evaluate the winding number by calculating Cauchy indices.

Count the Number of Complex Roots

Wenda Li — 17 Oct 2017 00:00:00 +0000

Based on evaluating Cauchy indices through remainder sequences, this entry provides an effective procedure to count the number of complex roots (with multiplicity) of a polynomial within a rectangle box or a half-plane. Potential applications of this entry include certified complex root isolation (of a polynomial) and testing the Routh-Hurwitz stability criterion (i.e., to check whether all the roots of some characteristic polynomial have negative real parts).

Homogeneous Linear Diophantine Equations

Florian Messner, Julian Parsert, Jonas Schöpf, Christian Sternagel — 14 Oct 2017 00:00:00 +0000

We formalize the theory of homogeneous linear diophantine equations, focusing on two main results: (1) an abstract characterization of minimal complete sets of solutions, and (2) an algorithm computing them. Both, the characterization and the algorithm are based on previous work by Huet. Our starting point is a simple but inefficient variant of Huet's lexicographic algorithm incorporating improved bounds due to Clausen and Fortenbacher. We proceed by proving its soundness and completeness. Finally, we employ code equations to obtain a reasonably efficient implementation. Thus, we provide a formally verified solver for homogeneous linear diophantine equations.

The Hurwitz and Riemann ζ Functions

Manuel Eberl — 12 Oct 2017 00:00:00 +0000

This entry builds upon the results about formal and analytic Dirichlet series to define the Hurwitz ζ function and, based on that, the Riemann ζ function. This is done by first defining them for ℜ(z) > 1 and then successively extending the domain to the left using the Euler–MacLaurin formula.

Some basic results about these functions are also shown, such as their analyticity on ℂ∖{1}, that they have a simple pole with residue 1 at 1, their relation to the Γ function, and the special values at negative integers and positive even integers – including the famous ζ(-1) = -1/12 and ζ(2) = π²/6.

Lastly, the entry also contains Euler's analytic proof of the infinitude of primes, based on the fact that ζ(s) has a pole at s = 1.

Linear Recurrences

Manuel Eberl — 12 Oct 2017 00:00:00 +0000

Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n-1) + f(n - 2) and the quite non-obvious closed form (φⁿ - (-φ)^-n) / √5 where φ is the golden ratio.

In this work, I build on existing tools in Isabelle – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell.

Dirichlet Series

Manuel Eberl — 12 Oct 2017 00:00:00 +0000

This entry is a formalisation of much of Chapters 2, 3, and 11 of Apostol's “Introduction to Analytic Number Theory”. This includes:

Definitions and basic properties for several number-theoretic functions (Euler's φ, Möbius μ, Liouville's λ, the divisor function σ, von Mangoldt's Λ)
Executable code for most of these functions, the most efficient implementations using the factoring algorithm by Thiemann et al.
Dirichlet products and formal Dirichlet series
Analytic results connecting convergent formal Dirichlet series to complex functions
Euler product expansions
Asymptotic estimates of number-theoretic functions including the density of squarefree integers and the average number of divisors of a natural number

These results are useful as a basis for developing more number-theoretic results, such as the Prime Number Theorem.

Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument

David Fuenmayor, Christoph Benzmüller — 21 Sep 2017 00:00:00 +0000

Computers may help us to understand --not just verify-- philosophical arguments. By utilizing modern proof assistants in an iterative interpretive process, we can reconstruct and assess an argument by fully formal means. Through the mechanization of a variant of St. Anselm's ontological argument by E. J. Lowe, which is a paradigmatic example of a natural-language argument with strong ties to metaphysics and religion, we offer an ideal showcase for our computer-assisted interpretive method.

Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL

Daniel Kirchner — 17 Sep 2017 00:00:00 +0000

We present an embedding of the second-order fragment of the Theory of Abstract Objects as described in Edward Zalta's upcoming work Principia Logico-Metaphysica (PLM) in the automated reasoning framework Isabelle/HOL. The Theory of Abstract Objects is a metaphysical theory that reifies property patterns, as they for example occur in the abstract reasoning of mathematics, as abstract objects and provides an axiomatic framework that allows to reason about these objects. It thereby serves as a fundamental metaphysical theory that can be used to axiomatize and describe a wide range of philosophical objects, such as Platonic forms or Leibniz' concepts, and has the ambition to function as a foundational theory of mathematics. The target theory of our embedding as described in chapters 7-9 of PLM employs a modal relational type theory as logical foundation for which a representation in functional type theory is known to be challenging.

Nevertheless we arrive at a functioning representation of the theory in the functional logic of Isabelle/HOL based on a semantical representation of an Aczel-model of the theory. Based on this representation we construct an implementation of the deductive system of PLM which allows to automatically and interactively find and verify theorems of PLM.

Our work thereby supports the concept of shallow semantical embeddings of logical systems in HOL as a universal tool for logical reasoning as promoted by Christoph Benzmüller.

The most notable result of the presented work is the discovery of a previously unknown paradox in the formulation of the Theory of Abstract Objects. The embedding of the theory in Isabelle/HOL played a vital part in this discovery. Furthermore it was possible to immediately offer several options to modify the theory to guarantee its consistency. Thereby our work could provide a significant contribution to the development of a proper grounding for object theory.

Anselm's God in Isabelle/HOL

Ben Blumson — 06 Sep 2017 00:00:00 +0000

Paul Oppenheimer and Edward Zalta's formalisation of Anselm's ontological argument for the existence of God is automated by embedding a free logic for definite descriptions within Isabelle/HOL.

Microeconomics and the First Welfare Theorem

Julian Parsert, Cezary Kaliszyk — 01 Sep 2017 00:00:00 +0000

Economic activity has always been a fundamental part of society. Due to modern day politics, economic theory has gained even more influence on our lives. Thus we want models and theories to be as precise as possible. This can be achieved using certification with the help of formal proof technology. Hence we will use Isabelle/HOL to construct two economic models, that of the the pure exchange economy and a version of the Arrow-Debreu Model. We will prove that the First Theorem of Welfare Economics holds within both. The theorem is the mathematical formulation of Adam Smith's famous invisible hand and states that a group of self-interested and rational actors will eventually achieve an efficient allocation of goods and services.

Root-Balanced Tree

Tobias Nipkow — 20 Aug 2017 00:00:00 +0000

Andersson introduced general balanced trees, search trees based on the design principle of partial rebuilding: perform update operations naively until the tree becomes too unbalanced, at which point a whole subtree is rebalanced. This article defines and analyzes a functional version of general balanced trees, which we call root-balanced trees. Using a lightweight model of execution time, amortized logarithmic complexity is verified in the theorem prover Isabelle.

This is the Isabelle formalization of the material decribed in the APLAS 2017 article Verified Root-Balanced Trees by the same author, which also presents experimental results that show competitiveness of root-balanced with AVL and red-black trees.

Orbit-Stabiliser Theorem with Application to Rotational Symmetries

Jonas Rädle — 20 Aug 2017 00:00:00 +0000

The Orbit-Stabiliser theorem is a basic result in the algebra of groups that factors the order of a group into the sizes of its orbits and stabilisers. We formalize the notion of a group action and the related concepts of orbits and stabilisers. This allows us to prove the orbit-stabiliser theorem. In the second part of this work, we formalize the tetrahedral group and use the orbit-stabiliser theorem to prove that there are twelve (orientation-preserving) rotations of the tetrahedron.

The LambdaMu-calculus

Cristina Matache, Victor B. F. Gomes, Dominic P. Mulligan — 16 Aug 2017 00:00:00 +0000

The propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed λ-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. This observation set off a flurry of further research, leading to the development of Parigots λμ-calculus. In this work, we formalise λμ- calculus in Isabelle/HOL and prove several metatheoretical properties such as type preservation and progress.

Stewart's Theorem and Apollonius' Theorem

Lukas Bulwahn — 31 Jul 2017 00:00:00 +0000

This entry formalizes the two geometric theorems, Stewart's and Apollonius' theorem. Stewart's Theorem relates the length of a triangle's cevian to the lengths of the triangle's two sides. Apollonius' Theorem is a specialisation of Stewart's theorem, restricting the cevian to be the median. The proof applies the law of cosines, some basic geometric facts about triangles and then simply transforms the terms algebraically to yield the conjectured relation. The formalization in Isabelle can closely follow the informal proofs described in the Wikipedia articles of those two theorems.

Dynamic Architectures

Diego Marmsoler — 28 Jul 2017 00:00:00 +0000

The architecture of a system describes the system's overall organization into components and connections between those components. With the emergence of mobile computing, dynamic architectures have become increasingly important. In such architectures, components may appear or disappear, and connections may change over time. In the following we mechanize a theory of dynamic architectures and verify the soundness of a corresponding calculus. Therefore, we first formalize the notion of configuration traces as a model for dynamic architectures. Then, the behavior of single components is formalized in terms of behavior traces and an operator is introduced and studied to extract the behavior of a single component out of a given configuration trace. Then, behavior trace assertions are introduced as a temporal specification technique to specify behavior of components. Reasoning about component behavior in a dynamic context is formalized in terms of a calculus for dynamic architectures. Finally, the soundness of the calculus is verified by introducing an alternative interpretation for behavior trace assertions over configuration traces and proving the rules of the calculus. Since projection may lead to finite as well as infinite behavior traces, they are formalized in terms of coinductive lists. Thus, our theory is based on Lochbihler's formalization of coinductive lists. The theory may be applied to verify properties for dynamic architectures.

Declarative Semantics for Functional Languages

Jeremy Siek — 21 Jul 2017 00:00:00 +0000

We present a semantics for an applied call-by-value lambda-calculus that is compositional, extensional, and elementary. We present four different views of the semantics: 1) as a relational (big-step) semantics that is not operational but instead declarative, 2) as a denotational semantics that does not use domain theory, 3) as a non-deterministic interpreter, and 4) as a variant of the intersection type systems of the Torino group. We prove that the semantics is correct by showing that it is sound and complete with respect to operational semantics on programs and that is sound with respect to contextual equivalence. We have not yet investigated whether it is fully abstract. We demonstrate that this approach to semantics is useful with three case studies. First, we use the semantics to prove correctness of a compiler optimization that inlines function application. Second, we adapt the semantics to the polymorphic lambda-calculus extended with general recursion and prove semantic type soundness. Third, we adapt the semantics to the call-by-value lambda-calculus with mutable references.
The paper that accompanies these Isabelle theories is available on arXiv.

HOLCF-Prelude

Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel — 15 Jul 2017 00:00:00 +0000

The Isabelle/HOLCF-Prelude is a formalization of a large part of Haskell's standard prelude in Isabelle/HOLCF. We use it to prove the correctness of the Eratosthenes' Sieve, in its self-referential implementation commonly used to showcase Haskell's laziness; prove correctness of GHC's "fold/build" rule and related rewrite rules; and certify a number of hints suggested by HLint.