IsarMathLib 1.27.0: Spectrum of a quotient ring, Finite State Machines

March 18, 2023

This release is again mostly based on contributions by Daniel de la Concepción Sáez in algebraic topology (or is it algebraic geometry? I am not sure), automata theory and formal languages.

The content in ring theory provides results on the spectrum of a quotient ring and reaches the result that the spectrum of a quotient ring is homeomorphic to a closed subspace of the spectrum of the original ring (in Zariski topology).

I have to say Daniel’s new theory on Finite State Machines was quite a surprise for me as the subject is quite far away from what I associate with mathematics that is easy to formalize is set theory. The material reaches the proof that non-deterministic finite state automata determine the same languages as deterministic finite state automata.

Advertisement

IsarMathLib 1.26.0: Ring ideals and Zariski topology

January 30, 2023

This is a relatively large release with new material on algebra and algebraic topology contributed by Daniel de la Concepción Sáez. The full list of topics covered and not covered (yet) is in this GitHub issue. It will take some time before the new theory files are presented on the isarmathlib.org site, in the meantime they can be viewed in the standard Isabelle generated HTML presentation, the outline (definitions and assertions only) or the full proof document with proofs.

What is Zariski topology?

Let \mathcal{I} be the set of ideals of some commutative ring and \mathcal{S} be the set of prime ideals (i.e. the spectrum) of that ring. As it turns out the collection \tau_Z = \{\{P \in \mathcal{S}: \neg (I \subseteq P)\}:I \in  \mathcal{I} \} is then a topology, called Zariski topology. The carrier of this topology is \bigcup \tau_Z =  \mathcal{S} and the closed sets are of the form \{ P \in \mathcal{S} : I \subseteq P\} for I\in  \mathcal{I}. So this notion belongs to algebraic topology but unlike for the topological groups or rings the topological structure is completely derived from the algebraic structure. Each ring has its Zariski topology.

IsarMathLib 1.25.0: Comparison with Metamath

December 28, 2022

Around 2007 at the beginning of the project I got an idea to speed up the development of the IsarMathLib library by importing theorems from Metamath’s set.mm. The theorems and proofs translated then are still a part of IsarMathLib and a small sample is presented at the isarmathlib.org site. After translating about 2000 proofs I decided to stop doing that as the work was repetitive and boring and the resulting proofs were not readable.

Metamath is considered a “low level” language and proof assistant, so I recently got curious how the Metamath proofs would compare with similar proofs written in the Isar dialect used in IsarMathLib. In this release I manually translated the Metamath’s utopreg theorem together with a couple of dependencies, taking advantage of Isabelle automation features to the extend I usually do in IsarMathlib. The following table compares verbosity of the original and translated proofs for the theorems whose proofs expressed similar ideas:

TheoremSteps MetamathLines IsarMathLibFactor
utopreg95521.8
utopsnneip15141.1
ustex3sym25112.3
imasncls64282.3
utop3cls103273.8

On average IsarMathLib proofs were about 2.3 times shorter. I have to say I expected that factor to be somewhere between 3 and 4.

The original Metamath utopreg theorem states that all Hausdorff uniform spaces are regular. After I translated the proof I was surprised to notice that the IsarMathLib’s version does not reference the hypothesis that the uniform space is Hausdorff. So, the IsarMathLib version shows that all uniform spaces are regular. I am not sure how it happened. To be honest I was not able to follow the Metamath proof exactly – it’s just too many small steps for me to put in my head at the same time. I was translating the proofs by first showing the steps marked green in Metamath Proof Explorer (I understand this indicates that the theorem referenced in the step is recent and hence close to the one being shown). Then I looked at facts made available this way and tried to figure out how one can get to the thesis of the theorem from them. It is possible that the Metamath proof does not make real use of this hypothesis as well, it’s just easier to spot in Isar.

IPC with F# and Fable.Remoting

December 11, 2022

Consider the following programming exercise:
We have a server and some unknown number of clients, possibly on different hosts. The clients send messages to the server, some of them only to say “Hi”. The server responds with a message containing an integer which says how many times the server received the “Hi” message so far. What is the minimal amount of F# code one can write to implement this (i.e. both server and client)?

There are a couple of ways to do IPC (Inter Process Communication) in F# (or C#). One can use named pipes or gRPC, but in this post I want to present Fable.Remoting.

Read the rest of this entry »

IsarMathLib 1.24.0: Update to Isabelle2022

October 29, 2022

A new version of Isabelle got released a couple of days ago and this version updates IsarMathLib to Isabelle2022. The Isabelle/ZF logic that IsarMathLib is based on is not actively developed, which has a good side that there are no changes and upgrades like this are easy and problem-free.

There is a little bit of formalized mathematics added in this IsarMathLib release as well. I added a couple of results from general topology that I always considered neat and elegant: a characterization of Hausdorff spaces as those for which the diagonal \{\langle x,x\rangle : x\in X\} is closed in the product topology on X\times X, the fact that the graph of a function into a Hausdorff space is closed in X\times X and that two continuous functions into a Hausdorff space are equal on a closed set.

Another theorem added is related to abstract neighborhood systems. IsarMathLib had had a formalization of the fact that if one has a neighborhood system on X one can construct a topology on X and vice versa: starting from a topology we can define a natural neighborhood system. In this release I added a theorem asserting that if we start from a neighborhood system, create a topology from it, then create it’s natural neighborhood system, we get back the original neighborhood system.

IsarMathLib 1.23.0: Rewrite of the presentation layer in F#

September 5, 2022

I wrote the original isar2html tool 13 years ago in Haskell as a way to learn the language. Since then I was extending it and fixing bugs. Coming back once or twice a year to a language that I was not using professionally had quite a bit of overhead just to recall how the things worked and reconstruct the development environment. As it happened I changed jobs in April this year and the new job required F#, so I decided to rewrite isar2html in F#, again as a way to learn the language. Of course as usual with that type of “big rewrite” (well, not that big here really) projects I underestimated the effort needed so I finished only about a week ago. Now I have exactly the same application implemented the same way in Haskell i F#.

HaskellF#
lines20261692
words103349239
characters7200679320
Basic verbosity statistics

The F# syntax is not as clean as Haskell’s so it was a surprise for me that the number of lines required was about 16% less in F# than in Haskell. Still, I would say that F# is slightly more verbose as the total number of characters was 10% higher in F#. Translating the parser of the subset of the Isar formal proof language that is used in IsarMathLib was almost mechanical and boring thanks to FParsec, which is the F# clone of Haskell’s Parsec parser library. I am especially happy with the result of that part of the project – the parsing errors were difficult to debug in Haskell. FParsec has better diagnostics built in – in case of failure it shows the backtracking information which helps a lot to pinpoint the problem in the text being parsed.

On the mathematics side in this release I have added a theorem stating that an ordered loop valued metric space is T2.

Read the rest of this entry »

Summing up in Kaitai Struct

January 8, 2022

I recently wanted to understand the Parquet binary format so I attempted to write a specification for it in Kaitai Struct. Kaitai Struct is a declarative binary format specification language, embedded in YAML. After writing such specification for a format one can generate parsers for it in several supported languages. Another thing that one can use such specification for is to visualize various elements of the format in the Kaitai Web IDE, which shows output somewhat similar to what Wireshark shows for network protocols. That’s what I want to use (if I ever finish the spec).

One stumbling block that I encountered was related to the way a SchemaElement is encoded in Parquet. A SchemaElement is a struct with a couple of fields selected from a fixed collection. The fields have numerical identifiers which are not provided directly but through deltas between their values. To obtain actual field id one has to compute the sum of the deltas provided (as 4-bit integers) in the file. For a while it was unclear if there is a way to encode such sum in Kaitai Struct and there was an issue about it on Kaitai GitHub repository opened more that four years ago. However, some three weeks ago cher-nov came up with a solution to this problem and posted it to the issue linked above. In this post I want to present an application of this solution to a toy format as another example that one can look at.

Read the rest of this entry »

IsarMathLib 1.22.1: Update to Isabelle2021-1

December 25, 2021

This release updates IsarMathLib to Isabelle2021-1. There was actually not much to update – only a couple of places in the informal text that referenced Isabelle2021 now reference Isabelle2021-1. The main difference is in the HTML presentation that Isabelle generates from IsarMathLib sources. This presentation improved somewhat and now has links to referenced theorems in proofs. In one respect it is even better than the presentation at the isarmathlib.org site – the locale names in the statements of theorems are linked to the definitions, which is a feature missing on isarmathlib.org. I remember some statements by Makarius Wentzel on the Isabelle mailing list that the goal is the “publication quality” of officially generated HTML presentation. I hope that this includes what I think is needed the most – folding of structured proofs, support for mathematical notation with custom symbols and options for reduction of syntactic noise so that characters like the question mark or the quotes separating the object logic statements are omitted. When this happens I would be happy to retire the tool that generates isarmathlib.org HTML files. I wrote that tool 14 years ago with only a scant knowledge of HTML, CSS or Java Script and the web pages it generates are probably hopelessly old-style.

In other news, Pedro Sánchez Terraf announced that his team has completed a formalization of the independence of CH in Isabelle/ZF. This is a good news for IsarMathLib as well. Isabelle/ZF is used by very few people and I worry that at some point the Isabelle team stops supporting it, which would be the end of IsarMathLib. Every application like this makes it less likely.

IsarMathLib 1.22.0: Uniform covers part II

October 5, 2021

The material added in this release is again about uniform spaces, more specifically about the equivalence of defining uniform space through (diagonal) uniformities and through uniform covers. The previous release concluded with the theorem stating that if \Theta is a family of uniform covers of X then the following collection \Phi of subsets of X\times X is a (diagonal) uniformity:

\Phi = \{A\in Pow(X\times X): \exists_{P\in \Theta} \bigcup\{U\times U: U\in P\} \subseteq A\}.

This shows that if we define a uniform space through a family of uniform covers then we can always get the usual definition by transforming that family into a uniformity.

The current release adds the dual fact (unicov_from_uniformity): if \Phi is a uniformity on X then the following collection of covers of X is a family of uniform covers:

\{P\in \text{Covers}(X). \exists_{A\in \Phi} \forall_{x\in X} \exists_{U\in P} A\{x \} \subseteq U\}.

The next two theorems show that these two transformations are inverses of each other.

I should probably quote sources for my formalization so that not to create an impression that I claim I am inventing some new stuff here. However the truth is that I found the Willard’s “General Topology” book that I bought for this nearly useless. So I ended up mostly getting definitions and facts from the “Uniform cover definition” section on the Wikipedia page on uniform spaces, and figuring out the proofs by myself. The only exception was a nice (even if not completely correct) proof that barycentric refinement of a barycentric refinement is a star refinement by Henno Brandsma that I found on Stack Exchange and converted to the bary_bary_star lemma.

Other news

Read the rest of this entry »

IsarMathLib 1.21.0: Uniform covers

August 22, 2021

There are three approaches to defining uniform spaces. The first one, through diagonal uniformities is presented in IsarMathLib in the UniformSpace_ZF theory. This release adds a theory about defining uniform spaces through uniform covers.

Consider a set X with its powerset (the set of subsets) \text{Pow}(X). A collection P of subsets of X whose union is equal to X is called a cover of X. So, we can define the set \text{Covers}(X) = \{ P\in  \text{Pow}( \text{Pow} (X)): \bigcup P =X \} .

For a set U\subseteq X and a collection of \mathcal{U} of subsets of X we can define the star of U in \mathcal{U} as \text{st}(U,\mathcal{U}) = \bigcup\{ W\in  \mathcal{U} : W\cap U\ne \emptyset \}.

For two covers \mathcal{R},\mathcal{C} \in \text{Covers}(X) we say that the cover \mathcal{R} is a star-refinement of the cover \mathcal{C} and write \mathcal{R} <^*  \mathcal{C} if for every R\in  \mathcal{R} we can find a C\in  \mathcal{C} such that \text{st}(R, \mathcal{R}) is contained in C.

Finally we are able to define uniform covers. This notion is a bit tricky as there is really no separate notion of a uniform cover. If we look at cover of X we cannot say if this is a uniform cover or not. What actually is defined is a family of uniform covers. A member of such family can only be called a uniform cover if it is clear from the context what family of uniform covers it belongs to.

A nonempty collection of covers \Theta of X is called a family of uniform covers iff the following two conditions hold:

a) If \mathcal{R} \in  \Theta, \mathcal{C} \in  \text{Covers}(X) and \mathcal{R} <^*  \mathcal{C}, then \mathcal{C} \in  \Theta

b) For every two covers \mathcal{R},  \mathcal{C}\in  \Theta we can find a cover \mathcal{D}\in  \Theta that is a star-refinement of both \mathcal{R} and \mathcal{C}

This definition is slightly different that the one on the Wikipedia page on uniform spaces, which specifically requires that the trivial cover \{ X\} is a member of \Theta. However, since every cover is a star-refinement of the trivial cover \{ X\} and \Theta is not empty, condition a) implies that \{ X\}\in \Theta.

The key fact here is that if \Theta is a family of uniform covers of X then the following collection \Phi of subsets of X\times X is a (diagonal) uniformity:

\Phi = \{A\in Pow(X\times X): \exists_{P\in \Theta} \bigcup\{U\times U: U\in P\} \subseteq A\}

In words, \Phi is the collection of supersets of sets of the form \bigcup\{U\times U: U\in P\} as P ranges over \Theta.

In Willard’s “General Topology” book the proof that \Phi is a uniformity is left as a “straightforward exercise” for the reader. Typically that means that the proof is long and tedious and the author does not feel like typing all that down. In this case the proof is indeed of mostly straightforward “follow your nose” kind right up to the moment when given a set A\in \Phi one needs to find a set B\in \Phi such that B\circ B \subseteq A (here B\circ B is the composition of relation B with itself). For that, I found the following identity useful:

(  \bigcup\{U\times U: U\in P\} ) \circ (  \bigcup\{U\times U: U\in P\} ) = \bigcup\{U\times \text{st}(U,P): U\in P\}

It took me some effort to figure out this identity and I was ready to type the proof of that in Isabelle, split into two inclusions etc. To my amazement though Isabelle accepted this fact without an explicit proof, only with the reference to the definition of star. This was probably the most unclear to me fact that was obvious to Isabelle that I have seen writing proofs for IsarMathLib so far. I left the proof of this identity as an exercise for the reader. This time the straightforwardness of this fact got certified by Isabelle.

Which brings us to the subject of

Automation in proof assistants

Read the rest of this entry »