Archive of Formal Proofs

Syntax-Independent Logic Infrastructure

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We formalize a notion of logic whose terms and formulas are kept abstract. In particular, logical connectives, substitution, free variables, and provability are not defined, but characterized by their general properties as locale assumptions. Based on this abstract characterization, we develop further reusable reasoning infrastructure. For example, we define parallel substitution (along with proving its characterizing theorems) from single-point substitution. Similarly, we develop a natural deduction style proof system starting from the abstract Hilbert-style one. These one-time efforts benefit different concrete logics satisfying our locales' assumptions. We instantiate the syntax-independent logic infrastructure to Robinson arithmetic (also known as Q) in the AFP entry Robinson_Arithmetic and to hereditarily finite set theory in the AFP entries Goedel_HFSet_Semantic and Goedel_HFSet_Semanticless, which are part of our formalization of Gödel's Incompleteness Theorems described in our CADE-27 paper A Formally Verified Abstract Account of Gödel's Incompleteness Theorems.

Robinson Arithmetic

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We instantiate our syntax-independent logic infrastructure developed in a separate AFP entry to the FOL theory of Robinson arithmetic (also known as Q). The latter was formalised using Nominal Isabelle by adapting Larry Paulson’s formalization of the Hereditarily Finite Set theory.

An Abstract Formalization of Gödel's Incompleteness Theorems

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We present an abstract formalization of Gödel's incompleteness theorems. We analyze sufficient conditions for the theorems' applicability to a partially specified logic. Our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser's variation of the first theorem, Jeroslow's variation of the second theorem, and the Swierczkowski–Paulson semantics-based approach. This AFP entry is the main entry point to the results described in our CADE-27 paper A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. As part of our abstract formalization's validation, we instantiate our locales twice in the separate AFP entries Goedel_HFSet_Semantic and Goedel_HFSet_Semanticless.

From Abstract to Concrete Gödel's Incompleteness Theorems—Part II

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We validate an abstract formulation of Gödel's Second Incompleteness Theorem from a separate AFP entry by instantiating it to the case of finite consistent extensions of the Hereditarily Finite (HF) Set theory, i.e., consistent FOL theories extending the HF Set theory with a finite set of axioms. The instantiation draws heavily on infrastructure previously developed by Larry Paulson in his direct formalisation of the concrete result. It strengthens Paulson's formalization of Gödel's Second from that entry by not assuming soundness, and in fact not relying on any notion of model or semantic interpretation. The strengthening was obtained by first replacing some of Paulson’s semantic arguments with proofs within his HF calculus, and then plugging in some of Paulson's (modified) lemmas to instantiate our soundness-free Gödel's Second locale.

From Abstract to Concrete Gödel's Incompleteness Theorems—Part I

Andrei Popescu, Dmitriy Traytel — 16 Sep 2020 00:00:00 +0000

We validate an abstract formulation of Gödel's First and Second Incompleteness Theorems from a separate AFP entry by instantiating them to the case of finite sound extensions of the Hereditarily Finite (HF) Set theory, i.e., FOL theories extending the HF Set theory with a finite set of axioms that are sound in the standard model. The concrete results had been previously formalised in an AFP entry by Larry Paulson; our instantiation reuses the infrastructure developed in that entry.

A Formal Model of Extended Finite State Machines

Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick — 07 Sep 2020 00:00:00 +0000

In this AFP entry, we provide a formalisation of extended finite state machines (EFSMs) where models are represented as finite sets of transitions between states. EFSMs execute traces to produce observable outputs. We also define various simulation and equality metrics for EFSMs in terms of traces and prove their strengths in relation to each other. Another key contribution is a framework of function definitions such that LTL properties can be phrased over EFSMs. Finally, we provide a simple example case study in the form of a drinks machine.

Inference of Extended Finite State Machines

Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick — 07 Sep 2020 00:00:00 +0000

In this AFP entry, we provide a formal implementation of a state-merging technique to infer extended finite state machines (EFSMs), complete with output and update functions, from black-box traces. In particular, we define the subsumption in context relation as a means of determining whether one transition is able to account for the behaviour of another. Building on this, we define the direct subsumption relation, which lifts the subsumption in context relation to EFSM level such that we can use it to determine whether it is safe to merge a given pair of transitions. Key proofs include the conditions necessary for subsumption to occur and that subsumption and direct subsumption are preorder relations. We also provide a number of different heuristics which can be used to abstract away concrete values into registers so that more states and transitions can be merged and provide proofs of the various conditions which must hold for these abstractions to subsume their ungeneralised counterparts. A Code Generator setup to create executable Scala code is also defined.

Practical Algebraic Calculus Checker

Mathias Fleury, Daniela Kaufmann — 31 Aug 2020 00:00:00 +0000

Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus (PAC). In this development, we present the verified checker Pastèque that is obtained by synthesis via the Refinement Framework. This is the formalization going with our FMCAD'20 tool presentation.

Some classical results in inductive inference of recursive functions

Frank J. Balbach — 31 Aug 2020 00:00:00 +0000

This entry formalizes some classical concepts and results from inductive inference of recursive functions. In the basic setting a partial recursive function ("strategy") must identify ("learn") all functions from a set ("class") of recursive functions. To that end the strategy receives more and more values $f(0), f(1), f(2), \ldots$ of some function $f$ from the given class and in turn outputs descriptions of partial recursive functions, for example, Gödel numbers. The strategy is considered successful if the sequence of outputs ("hypotheses") converges to a description of $f$. A class of functions learnable in this sense is called "learnable in the limit". The set of all these classes is denoted by LIM.

Other types of inference considered are finite learning (FIN), behaviorally correct learning in the limit (BC), and some variants of LIM with restrictions on the hypotheses: total learning (TOTAL), consistent learning (CONS), and class-preserving learning (CP). The main results formalized are the proper inclusions $\mathrm{FIN} \subset \mathrm{CP} \subset \mathrm{TOTAL} \subset \mathrm{CONS} \subset \mathrm{LIM} \subset \mathrm{BC} \subset 2^{\mathcal{R}}$, where $\mathcal{R}$ is the set of all total recursive functions. Further results show that for all these inference types except CONS, strategies can be assumed to be total recursive functions; that all inference types but CP are closed under the subset relation between classes; and that no inference type is closed under the union of classes.

The above is based on a formalization of recursive functions heavily inspired by the Universal Turing Machine entry by Xu et al., but different in that it models partial functions with codomain nat option. The formalization contains a construction of a universal partial recursive function, without resorting to Turing machines, introduces decidability and recursive enumerability, and proves some standard results: existence of a Kleene normal form, the s-m-n theorem, Rice's theorem, and assorted fixed-point theorems (recursion theorems) by Kleene, Rogers, and Smullyan.

Relational Disjoint-Set Forests

Walter Guttmann — 26 Aug 2020 00:00:00 +0000

We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in the Hoare-logic library. Using relation algebras and Kleene algebras we verify the correctness of an array-based implementation of disjoint-set forests with a naive union operation and a find operation with path compression.

Extensions to the Comprehensive Framework for Saturation Theorem Proving

Jasmin Blanchette, Sophie Tourret — 25 Aug 2020 00:00:00 +0000

This Isabelle/HOL formalization extends the AFP entry Saturation_Framework with the following contributions:

an application of the framework to prove Bachmair and Ganzinger's resolution prover RP refutationally complete, which was formalized in a more ad hoc fashion by Schlichtkrull et al. in the AFP entry Ordered_Resultion_Prover;
generalizations of various basic concepts formalized by Schlichtkrull et al., which were needed to verify RP and could be useful to formalize other calculi, such as superposition;
alternative proofs of fairness (and hence saturation and ultimately refutational completeness) for the given clause procedures GC and LGC, based on invariance.

Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching

Peter Gammie — 25 Aug 2020 00:00:00 +0000

Richard Bird and collaborators have proposed a derivation of an intricate cyclic program that implements the Morris-Pratt string matching algorithm. Here we provide a proof of total correctness for Bird's derivation and complete it by adding Knuth's optimisation.

Amicable Numbers

Angeliki Koutsoukou-Argyraki — 04 Aug 2020 00:00:00 +0000

This is a formalisation of Amicable Numbers, involving some relevant material including Euler's sigma function, some relevant definitions, results and examples as well as rules such as Thābit ibn Qurra's Rule, Euler's Rule, te Riele's Rule and Borho's Rule with breeders.

Ordinal Partitions

Lawrence C. Paulson — 03 Aug 2020 00:00:00 +0000

The theory of partition relations concerns generalisations of Ramsey's theorem. For any ordinal $\alpha$, write $\alpha \to (\alpha, m)^2$ if for each function $f$ from unordered pairs of elements of $\alpha$ into $\{0,1\}$, either there is a subset $X\subseteq \alpha$ order-isomorphic to $\alpha$ such that $f\{x,y\}=0$ for all $\{x,y\}\subseteq X$, or there is an $m$ element set $Y\subseteq \alpha$ such that $f\{x,y\}=1$ for all $\{x,y\}\subseteq Y$. (In both cases, with $\{x,y\}$ we require $x\not=y$.) In particular, the infinite Ramsey theorem can be written in this notation as $\omega \to (\omega, \omega)^2$, or if we restrict $m$ to the positive integers as above, then $\omega \to (\omega, m)^2$ for all $m$. This entry formalises Larson's proof of $\omega^\omega \to (\omega^\omega, m)^2$ along with a similar proof of a result due to Specker: $\omega^2 \to (\omega^2, m)^2$. Also proved is a necessary result by Erdős and Milner: $\omega^{1+\alpha\cdot n} \to (\omega^{1+\alpha}, 2^n)^2$.

A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm

Ben Fiedler, Dmitriy Traytel — 21 Jul 2020 00:00:00 +0000

We provide a suitable distributed system model and implementation of the Chandy--Lamport distributed snapshot algorithm [ACM Transactions on Computer Systems, 3, 63-75, 1985]. Our main result is a formal termination and correctness proof of the Chandy--Lamport algorithm and its use in stable property detection.

Relational Characterisations of Paths

Walter Guttmann, Peter Höfner — 13 Jul 2020 00:00:00 +0000

Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in Kleene relation algebras, which are relation algebras equipped with an operation for reflexive transitive closure. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms.

A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

Albert Rizaldi, Fabian Immler — 01 Jun 2020 00:00:00 +0000

The Vienna Convention on Road Traffic defines the safe distance traffic rules informally. This could make autonomous vehicle liable for safe-distance-related accidents because there is no clear definition of how large a safe distance is. We provide a formally proven prescriptive definition of a safe distance, and checkers which can decide whether an autonomous vehicle is obeying the safe distance rule. Not only does our work apply to the domain of law, but it also serves as a specification for autonomous vehicle manufacturers and for online verification of path planners.

A verified algorithm for computing the Smith normal form of a matrix

Jose Divasón — 23 May 2020 00:00:00 +0000

This work presents a formal proof in Isabelle/HOL of an algorithm to transform a matrix into its Smith normal form, a canonical matrix form, in a general setting: the algorithm is parameterized by operations to prove its existence over elementary divisor rings, while execution is guaranteed over Euclidean domains. We also provide a formal proof on some results about the generality of this algorithm as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out switching conveniently between two different existing libraries: the Hermite normal form (based on HOL Analysis) and the Jordan normal form AFP entries. This permits to reuse results from both developments and it is done by means of the lifting and transfer package together with the use of local type definitions.

The Nash-Williams Partition Theorem

Lawrence C. Paulson — 16 May 2020 00:00:00 +0000

In 1965, Nash-Williams discovered a generalisation of the infinite form of Ramsey's theorem. Where the latter concerns infinite sets of n-element sets for some fixed n, the Nash-Williams theorem concerns infinite sets of finite sets (or lists) subject to a “no initial segment” condition. The present formalisation follows a monograph on Ramsey Spaces by Todorčević.

A Formalization of Knuth–Bendix Orders

Christian Sternagel, René Thiemann — 13 May 2020 00:00:00 +0000

We define a generalized version of Knuth–Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.

Irrationality Criteria for Series by Erdős and Straus

Angeliki Koutsoukou-Argyraki, Wenda Li — 12 May 2020 00:00:00 +0000

We formalise certain irrationality criteria for infinite series of the form: \[\sum_{n=1}^\infty \frac{b_n}{\prod_{i=1}^n a_i} \] where $\{b_n\}$ is a sequence of integers and $\{a_n\}$ a sequence of positive integers with $a_n >1$ for all large n. The results are due to P. Erdős and E. G. Straus [1]. In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1. The latter is an application of Theorem 2.1 involving the prime numbers.

Recursion Theorem in ZF

Georgy Dunaev — 11 May 2020 00:00:00 +0000

This document contains a proof of the recursion theorem. This is a mechanization of the proof of the recursion theorem from the text Introduction to Set Theory, by Karel Hrbacek and Thomas Jech. This implementation may be used as the basis for a model of Peano arithmetic in ZF. While recursion and the natural numbers are already available in Isabelle/ZF, this clean development is much easier to follow.

An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation

Salomon Sickert — 08 May 2020 00:00:00 +0000

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} \varphi_i \vee \mathbf{F}\mathbf{G} \psi_i$, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present an executable formalisation of a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up.

Formalization of Forcing in Isabelle/ZF

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf — 06 May 2020 00:00:00 +0000

We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC.

Banach-Steinhaus Theorem

Dominique Unruh, Jose Manuel Rodriguez Caballero — 02 May 2020 00:00:00 +0000

We formalize in Isabelle/HOL a result due to S. Banach and H. Steinhaus known as the Banach-Steinhaus theorem or Uniform boundedness principle: a pointwise-bounded family of continuous linear operators from a Banach space to a normed space is uniformly bounded. Our approach is an adaptation to Isabelle/HOL of a proof due to A. Sokal.

Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems

Florian Kammueller — 27 Apr 2020 00:00:00 +0000

In this article, we present a proof theory for Attack Trees. Attack Trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, we develop a generic theory of Attack Trees with a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of Attack Trees and at the same time the developed proof theory enables application to case studies. A central correctness and completeness result proved in Isabelle establishes a connection between the notion of Attack Tree validity and CTL. The application is illustrated on the example of a healthcare IoT system and GDPR compliance verification.

Power Sum Polynomials

Manuel Eberl — 24 Apr 2020 00:00:00 +0000

This article provides a formalisation of the symmetric multivariate polynomials known as power sum polynomials. These are of the form p_n(X₁,…, X_k) = X₁ⁿ + … + X_kⁿ. A formal proof of the Girard–Newton Theorem is also given. This theorem relates the power sum polynomials to the elementary symmetric polynomials s_k in the form of a recurrence relation (-1)^k k s_k = ∑_i∈[0,k) (-1)ⁱ s_i p_k-i .

As an application, this is then used to solve a generalised form of a puzzle given as an exercise in Dummit and Foote's Abstract Algebra: For k complex unknowns x₁, …, x_k, define p_j := x₁^j + … + x_k^j. Then for each vector a ∈ ℂ^k, show that there is exactly one solution to the system p₁ = a₁, …, p_k = a_k up to permutation of the x_i and determine the value of p_i for i>k.

The Lambert W Function on the Reals

Manuel Eberl — 24 Apr 2020 00:00:00 +0000

The Lambert W function is a multi-valued function defined as the inverse function of x ↦ x e^x. Besides numerous applications in combinatorics, physics, and engineering, it also frequently occurs when solving equations containing both e^x and x, or both x and log x.

This article provides a definition of the two real-valued branches W₀(x) and W_-1(x) and proves various properties such as basic identities and inequalities, monotonicity, differentiability, asymptotic expansions, and the MacLaurin series of W₀(x) at x = 0.

Gaussian Integers

Manuel Eberl — 24 Apr 2020 00:00:00 +0000

The Gaussian integers are the subring ℤ[i] of the complex numbers, i. e. the ring of all complex numbers with integral real and imaginary part. This article provides a definition of this ring as well as proofs of various basic properties, such as that they form a Euclidean ring and a full classification of their primes. An executable (albeit not very efficient) factorisation algorithm is also provided.

Lastly, this Gaussian integer formalisation is used in two short applications:

The characterisation of all positive integers that can be written as sums of two squares
Euclid's formula for primitive Pythagorean triples

While elementary proofs for both of these are already available in the AFP, the theory of Gaussian integers provides more concise proofs and a more high-level view.

Matrices for ODEs

Jonathan Julian Huerta y Munive — 19 Apr 2020 00:00:00 +0000

Our theories formalise various matrix properties that serve to establish existence, uniqueness and characterisation of the solution to affine systems of ordinary differential equations (ODEs). In particular, we formalise the operator and maximum norm of matrices. Then we use them to prove that square matrices form a Banach space, and in this setting, we show an instance of Picard-Lindelöf’s theorem for affine systems of ODEs. Finally, we use this formalisation to verify three simple hybrid programs.