IsarMathLib 1.21.0: Uniform covers

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

Ok, it’s grandfather’s story time. Long time ago and far away, when I was studying mathematics at the University of Tennessee, Knoxville, there was a very talented student from Romania there, let’s call him Gabriel P. Once I was struggling with a proof of some theorem and I asked him if he has an idea how to prove this thing. He looked at the problem, thought for a minute, then nodded his head, smiled and said “It’s true”. And left. I was more frustrated than enlightened and since then I am of opinion that automation in proof assistants is overrated.

Sure, automation is good for the writer as it reduces their effort. However, if there is too much of automation it affects the reader as it reduces the amount of information contained in the proofs. So there is a trade off with some optimum depending on writer’s goals. If the writer goal is certification of truth only, as is usually the case with software verification, then the more automation the better. In mathematics the issue of communication comes into play and the proofs are supposed to convey information on why an assertion is true.

Of course ideally the proofs would be built by a dialogue between a researcher and a proof assistant AI. The PA would then generate readable proofs in a structured proof language that processed by the presentation layer would allow a reader to set their desired level of detail, from high level bullet points down to the Metamath-style atomic steps. A couple of days ago I considered proof assistants like this such a remote possibility that it would not be worth it to even write this paragraph. This changed after I saw the Open AI Codex demo. I think now that proof assistants that do for crafting formal proofs what Open AI Codex does for programming are a couple of years off, at most.

Tags: formalized mathematics, IsarMathLib releases, proof assistants

This entry was posted on August 22, 2021 at 4:26 pm and is filed under IsarMathLib releases. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Formalized Mathematics