We present two formalizations with the natural proof assistant Naproche which explore the notational and typographical potential of the new LATEX input format. The first formalization leads up to Yoneda's Lemma in category theory. Commutative diagrams are defined and printed using the L ATEX package tikz-cd. A specific Naproche module translates a commutative diagram defined by tikz-cd commands into equalities of functional compositions which are proved by the Naproche reasoner. The second formalization is an abstract version of Euclid's proof of the infinitude of primes, using general algebraic concepts. It uses LATEX commands to follow the common mathematical practice of making some obvious symbols implicit and hide them from the typeset output. The hidden information can be revealed by hovering over the PDF output.
are interpreted logically and typographically. Other LATEX commands are ignored by the logical processing. One can also arrange that parts of the logical content are not printed out to reduce typographical complexity and to enhance understanding. This interplay is a topic of ongoing development and research.
Our first formalization explores the treatment of commutative diagrams in category theory. Diagrams are input linearly by tikz-cd commands. These can be printed in two dimensions using tikz-cd. To extract the logical content of a diagram, a new (sub-)parser for tikz-cd commands was written which finds all paths through a finite diagram and then generates function identities for distinct paths whose sources and targets agree. The use and treatment of diagrams is demonstrated in the axiomatic setup of categories and in the proof of the Yoneda lemma.
The second formalization presents an “algebraic” approach to arithmetic and primes. In ForTheL, the distributivity of a ring can be expressed by: \begin{Axiom}[DistribI] Let $x,y,z \in \sR{R}$. $x \tR{R} (y \pR{R} z) = (x \tR{R} y) \pR{R} (x \tR{R} z)$.
\end{Axiom}
where \sR{R}, \sR{R}, and \sR{R} stand for the underlying set, the multiplication, and the
addition of resp. Often a structure is identified with its underlying set, and it is clear from the
context which multiplication and addition are to be used. Such simplifications facilitate reading
and understanding of texts and can be implemented by “forgetful” LATEX functions:
\newcommand{\sR}[
Axiom. (DistribI) Let , , ∈ . · ( + ) = ( · ) + ( · ). without extra indices like · or · etc. Note that we output the formal parts of ForTheL texts on a light-gray background throughout this paper.
Such “hacks” lead to a conveniently readable Euclid formalization and motivate further
systematic work on presenting or hiding information in the LATEX projection. This is also related
to elaboration mechanisms like in Lean, where implicit variables can be hidden since their
values can be derived automatically [
The apparent loss of information in the PDF output can be counteracted by dynamic features of electronic documents. In our formalization we employ a hovering mechanism to display extra information in a balloon, which is, e.g., available for Adobe Reader and some other PDF viewers. Augmenting the definitions of the L ATEX commands \sR{R}, \tR{R}, and \pR{R} we can arrange that complete terms and possibly other information are displayed on “mouse-over”. 1. Commutative Diagrams and the Yoneda Lemma in Category
Commutative diagrams are essential in category theory. Natural formalizations require
prettyprinting of diagrams by some LATEX package and the logical checking of their mathematical
content. For this purpose, we have added an experimental module to Naproche which reads
out functional equalities from commutative diagrams defined in the tikz-cd environment. We
have used this in a Naproche formalization of the beginnings of category theory up to the
Yoneda-Lemma. The complete formalization is available at [
As an example, we give the definition of the one-sorted notion of a category as we use it in
our formalization. Standard categories can be viewed as one-sorted by identifying every object
with the identity function on that object itself (see [
Definition. (Category) A category is a collection of arrows such that (for every arrow such that we have [ ] and [ ] and [[ ]] = [ ] and [[ ]] = [ ] and .... .... and (for each arrow , such that , we have ([ ] = [] =⇒ (there is an arrow ℎ such that ℎ and
We briefly describe the implementation of the diagram parser and its use. For a more detailed
description see [
Our new Haskell module provides a translation from tikz-cd code to a conjunction of equations which is then translated to FOL by the ForTheL parser for further checking. tikzcdP :: String -> String tikzcdP a = maybe " Error: No proper diagram found."
(printEq . mkEqtClasses . arrows . mkPaths . snd) (runParser diagramP a) If no error is thrown, this function and for every arrow such that and ∘ = we have ℎ = ))) and for all arrows , , ℎ such that , , ℎ and [ ] = [] and [] = [ℎ] [ ] [ ] (∘ ) [] ℎ ℎ [ ]
[] [ ] [ℎ] (ℎ∘ ) . 1. identifies the arrows of a diagram through diagramP 2. lists all possible paths with mkPaths 3. finds paths that are meant to be equal by mkEqtClasses 4. conjuncts these equations via printEq The input is parsed into a Diagram type, which is a list of Arrow. An Arrow is a triple consisting of a name, source and target. A position is a tuple of integers as we view diagrams as two dimensional objects on a grid. We start in the upper left corner on initpos = (0,0) and count down each row in the left entry and up each column on the right. Since we want to identify paths with the same source and target, we define a corresponding equality on Arrow and obtain an instance of Eq. data Arrow = Arrow { name :: String , source :: Position , target :: Position } deriving Show instance Eq Arrow where
(==) a b = source a == source b && target a == target b data Diagram = Diagram { arrows :: [Arrow] } deriving Show diagramP :: Parser Diagram diagramP = Diagram <$> many arP arP :: Parser Arrow arP = Parser $ \input -> do let pos = pstn input (input1, rest) <- runParser (spanP (/= '{')) input let newpos = src rest pos (input2, _) <- runParser (charP '{') input1 (input3, dr) <- runParser (spanP (/= '}')) input2 (input4, _) <- runParser (spanP (/= '{')) input3 (input5, _) <- runParser (charP '{') input4 (input6, name) <- runParser (spanP (/= '}')) input5 (input7, _) <- runParser (charP '}') input6 case name /= " " of
True -> Just (show newpos ++ input7, Arrow name newpos (trgt dr newpos)) _ -> Nothing The diagram parser repeats arP as often as possible. The arrow parser waits for braces to get the direction and name of the current arrow. The current position is added to the beginning of the unparsed input at show newpos ++ input8 to keep track of it. When the next arrow is parsed, we get this position by pstn input.
All possible paths are built by: mkPaths1 :: Arrow -> Arrow -> [Arrow] mkPaths1 a x | source x == target a =
[Arrow ((name x) ++ " \\mcirc " ++ (name a)) (source a) (target x)] | source a == target x =
[Arrow ((name a) ++ " \\mcirc " ++ (name x)) (source x) (target a)] | otherwise = [] mkPaths2 :: Arrow -> Diagram -> Diagram mkPaths2 x d = case arrows d of [] -> Diagram [] (y:ys) -> Diagram $ mkPaths1 x y
++ arrows (mkPaths2 x (Diagram ys)) mkPaths :: Diagram -> Diagram mkPaths d = case arrows d of [] -> Diagram [] x : xs -> Diagram $ x : arrows (mkPaths (Diagram (xs ++ newA))) where
newA = arrows $ mkPaths2 x $ Diagram xs
The thesis [
Now the path complete diagram has to be partitioned by our predefined equality relation for Arrow. For an arrow x and a list of arrows xs, mkEqtClass2 compares any arrow of xs with x and creates a list of arrows equal to x. Finally, x itself is added. mkEqtClass1 :: (Eq a) => a -> a -> [a] mkEqtClass1 x y | x == y = [y] | otherwise = [] mkEqtClass2 :: (Eq a) => a -> [a] -> [a] mkEqtClass2 x xs = case xs of [] -> [x] y : ys -> mkEqtClass2 x ys ++ mkEqtClass1 x y Then mkEqtClasses creates a class z by taking the first arrow y from a list of arrows xs and comparing it to the rest ys. The recursive call of this function is restricted to the original list minus the generated class. (This behaves well since partitions are disjunct.) mkEqtClasses :: (Eq a) => [a] -> [[a]] mkEqtClasses xs = case xs of [] -> [] y : ys -> z : mkEqtClasses (ys \\ z)
where z = (mkEqtClass2 y ys) Finally, the classes are printed out by connecting class members with \= and classes with and. printEq1 :: [Arrow] -> String printEq1 l = case l of [] -> " " [x] -> name x x : xs -> name x ++ " = " ++ printEq1 xs printEq :: [[Arrow]] -> String printEq a = case filter (\l -> length l >= 2) a of [] -> " " [l] -> printEq1 l -- ++ " ." l : ls -> printEq1 l ++ " and " ++ printEq ls To test the parser consider the following diagram:
Φ ℎ
Just ( " (-2,1) & F" , Diagram { arrows = [ Arrow {name = " f", source = (0,0), target = (0,1)} , Arrow {name = " h", source = (0,0), target = (-2,0)} , Arrow {name = " \\Phi", source = (0,0), target = (-2,1)} , Arrow {name = " j", source = (0,0), target = (0,2)} , Arrow {name = " g", source = (0,1), target = (-2,1)} , Arrow {name = " k", source = (0,2), target = (-2,2)} , Arrow {name = " i", source = (-2,1), target = (-2,2)}]}) The final output is \Phi = g \mcirc f and i \mcirc \Phi = i \mcirc g \mcirc f = k \mcirc j where \mcirc is the composition function of arrows in our formalization of categories.
We want to demonstrate the usage of commutative diagrams within our formalized proof of the Yoneda-Lemma. Note that Nat[, , , ] is the class of all natural transformations : → where , : ⇒ . Such a natural transformation has its -component [, , , , , ] for every .
Axiom. (PhiDef) Let be a functor from to . Let . Let [, , [, ], ]. ∈ Φ( ) = [, , [, ], , , []]([]).
Lemma. (Yoneda) Let C be a locally small category. Let be a functor from to . Let and [] = .
Φ is a bijection between [, , [, ], ] and [].
For comparison we give a textbook version as it can be found in [
Lemma. (Yoneda) For any functor : → , whose domain is locally small, and any object ∈ , there is a bijection Nat((, − ), ) ∼= that associates a natural transformation : (, − ) ⇒ to the element (1) ∈ .
Let us compare the diagrams of a standard proof of the Yoneda-Lemma with the diagrams in our single-sorted Naproche formalization. In the second diagram we have [] and [] corresponding to the objects and on the left as source and target of .
Proof. The association Φ( ) := (1) is clearly well defined. We need to verify for any element ∈ (), that Ψ( ), defined componentwise by Ψ( )( ) := ( )() for each ∈ and : → , is the inverse of Φ . Any element : → of (, ) is sent to ( ) applied on Φ( ) = .
For all arrows , such that and [, , ] we have
[,, [,],,, ] [, , ] [] [,][]
[] [, , ] [] [,, [,],,, ].
By naturality of , (, ) * ))( ) = ( )(Φ( )) = ( )( (1)) = (* (1)) = ( ).
Φ(Ψ(
)) = (Ψ )(1) = (1)() = 1 ()() = .
To see why Ψ( ) is a natural transformation we have to show that commutes for every arrow ∈ (, ).
By definition, Ψ( ) sends : → to ( )() and Ψ( ) sends * ( ) to (* ( ))(). Therefore, the claim follows by functoriality of . □
Diagrams are an indispensable notation for equal paths in categories. They illustrate the mathematical core and make it more comprehensible for the reader. We have reproduced the proof above in Naproche using the diagram package.
Our notation of natural transformations in Naproche mentions all parameters explicitly, which makes the display somewhat bulky. The next section discusses methods to hide obvious or trivial parameters. We plan on combining those methods with the diagram parser so that that the final diagram might take the form
We present an approach to the infinitude of primes via wellfounded order relations in rings,
defined by divisibility. The complete formalization can be found in [
{ ∈ | is a minimum of } has no upper bound by .
We work in general structures like magmas, monoids or rings to exhibit the abstract arguments. Although Naproche does not yet have dedicated mechanisms for algebraic structures, we can make use of the first-order approach to typing to deal with subtyping and coercions.
We introduce a method to only display “mathematically relevant” information in the LATEXoutput to prevent losing the overview. The hidden information is not completely lost in the document, since it can be made visible by moving the mouse over the text. Thus uncertainty about meanings of terms can be resolved without inspecting the .ftl.tex file.
A magma is a set together with a binary operation on it. In principle we must distinguish between a magma and the underlying set | | since there may be two diferent magma structures on the same set. We first introduce the new word magma by the signature-command
Signature. A magma is a notion. and then we pretype some variable to be a magma:
Let denote a magma.
\begin{signature}
$\sGC{M}$ is a set.
\end{signature} The function \sGC has two faces: from the Naproche perspective the function sGC is a class function from the class of magmas to the class of sets; from the LATEX perspective, the function sGC puts absolute value bars around its argument, as it is defined by
\newcommand{\sGC}[
Let $x,y \in \sGC{M}$. $x \gdot{M} y$ is an element of $\sGC{M}$. \end{signature} Note that the operation depends on the parameter , so that \gdot really is a ternary mixfix function. The logical processing by Naproche requires all three parameters to determine the magma under consideration. But if the magma is understood from the context one usually suppresses that parameter in the printed output. This can be achieved by defining the L ATEX command \gdot as
Omitting obvious parameters of a function is not the only situation in which we may use such “hacks”. One often identifies a structure with its underlying set. So we want to print out instead of | |. This can be achieved by redefining the L ATEX command \sGC without the vertical bars.
A reader may be interested to see the full information behind the LATEX printout. This is possible without looking up the .ftl.tex-file. Some PDF viewers, such as Adobe Reader or Foxit Reader, feature so-called tooltips for editable PDF files to show alternative information in a box through a mouseover event. This allows to define a version of \sGC which normally omits the vertical bars, but shows the bars on mouseover, using the LATEX command \tooltip: For Naproche, \sG should have the same meaning as \sGC. This can be arranged by an alias command of the form
Let stand for | |.
Similarly for the operation on the magma we can define: The associative law then becomes:
Definition. is associative if (· )· = · (· ) for all , , ∈ .
Everything which is colored blue is linked to a hidden expression which gets visible if one moves the mouse over it. Note, that the color of the multiplication symbol is dificult to see.
Now we expand the magma-theory to monoids.
Definition. A monoid is an associative magma with a neutral element. For eventual study of prime numbers we define divisibility in a Monoid :
Definition. Let , ∈ . divides in if there exists ∈ such that · = . Now we already can prove the transitivity of divisibility :
Lemma. (transitiveDiv) Let , , ∈ . Suppose divides in and divides in . Then divides in .
Proof. Take an ∈ such that · = .
Take an ∈ such that · = .
Then = · = · (· ) = (· )· . Thus divides in .
Divisibility defines an order. As with magmas we introduce orders together with their underlying set || and appropriate tooltips and aliases. In Naproche, relations can be declared with the keyword “atom”.
Signature. Let , ∈ . is an atom.
Definition. Let ∈ . A predecessor of by is an element of such that ≤ .
To see the implementation of partial orders, minima and upper bounds, see [
Let M denote a monoid.
Definition. .
Lemma. | is reflexive and transitive.
Proof. | is reflexive. Indeed divides in for all ∈ . | is transitive (by transitiveDiv).
| is an order on such that for any , ∈ we have | if divides in Since our goal is to show that there are infinitely many primes, we may want to use a property of finiteness: If you have finitely many elements 1, . . . , of a monoid you can multiply them all together. This is captured order-theoretically as follows:
Axiom. (FiniteMultiplication) Let M be an abelian Monoid. Let be a finite subset of . Then has an upper bound by |.
The further formalization of groups (i.e. the definition of inverse elements in monoids) can
be found in [
Signature. Ab() is an abelian group based on .
Signature. Mu() is a Monoid based on .
Let + stand for · Ab() .
Let · stand for · Mu() .
0 and 1 can be defined as the neutral elements of Ab() and Mu() resp. Adding distributitivity axioms, we have completely formalized the algebraic structure of rings.
We now introduce an order-theoretic concept which will give strong results about minimal elements (which later will be standard prime numbers).
Definition. is wellfounded if is a partial order and for all nonempty subsets of || there exists a minimum of with .
Definition.
ℳ() = { ∈ | is a minimum of }.
To show the strength of the concept of wellfounded orders, here is one example: Lemma. Let be a wellfounded order. Let ∈ . Then there exists a predecessor of by such that is a minimum of .
Proof. Define = { ∈ | ≤ }. ⊆ . Take a minimum of with . is a minimum of .
The idea of relative primality is captured by the notion of stranger.
Definition. Let ∈ . A stranger of in is an element of such that and have no common predecessors by .
Theorem. (StrangerTheorem) Let be a wellfounded order. Assume every element of has a stranger in . Then ℳ() has no upper bound by .
Somewhat surprisingly, Naproche could find a derivation without an explicit proof given.
We now introduce Z as a commutative ring and
Signature. N>0 is a submonoid of Mu(Z).
We call the elements of N>0 positive numbers. This signature command requires, that N>0 is closed under the Z-multiplication and that 1 is a positive number.
Furthermore we require for positive number , :
Axiom. (MultEquiv) Assume divides in Z and divides in Z. Then = . Note, that we used another tooltip here. If you don’t use the long-term-expressions provided by tooltip you have to be careful, since in the PDF file a blue Z can indicate either the underlying set or the underlying monoid. It helps the reader, that the context (’∈ Z’ or ’divides . . . in Z’) already forces a disambiguation.
The key point of the last axiom is, that | is a partial order.
Axiom. + is a nontrivial positive number, where nontrivial means ̸= 1.
We denote the order |>1 for | restricted to the set of nontrivial positive numbers N>1. The reason to use this restriction of the underlying set is that prime numbers are exactly the minimal elements of |>1 (i.e. a nontrivial positive number such that the only nontrivial divisor is itself). We need one final axiom:
Axiom. Let be a nonempty subset of N>1. Then there exists a minimum of with |. Of course |>1 is a partial order, since it is the restriction of the partial order |. The axiom ensures, that |>1 is also wellfounded.
Lemma. (ExistenceOfStrangers) Every element of N>1 has a stranger in |>1.
Indeed, + 1 is a stranger of in |>1. This follows, since a nontrivial common divisor of
and + 1 would also divide the diference 1 (lemma divDif [
Letting P denote the set of prime numbers, we get Euclid’s theorem in Naproche: Theorem. (Euclid) P is not finite.
Proof. Proof by contradiction. Assume P is finite.
P = ℳ(|>1). ℳ(|>1) has no upper bound by |>1 (by ExistenceOfStrangers, StrangerTheorem). ℳ(|>1) is a finite subset of N>0. N>0 is an abelian monoid.
Take an upper bound b of ℳ(|>1) by | (by FiniteMultiplication). b = 1. ℳ(|>1) is nonempty.
Contradiction.