\documentclass{book} \usepackage{amssymb} \newtheorem{xercise}{Exercise}[section] \newenvironment{exercise}{\begin{xercise}\rm\ }{\end{xercise}} \newenvironment{answer}{}{} \def\answer#1{\paragraph{Answer to exercise \ref{#1}}} \newenvironment{example}{\paragraph{The example}}{} \newenvironment{mizar}{\begin{flushleft}}{\end{flushleft}} \def\toolong{$\hspace{-1.5cm}$} \begin{document} \raggedbottom \title{Mizar manual} \author{Andrzej Trybulec, Freek Wiedijk} \date{} \maketitle \chapter{Background} ??? \section{Mizar history} ??? \section{Mizar sites} ??? \section{Large formalization projects} ??? \part{Reference} \chapter{Vocabularies} ??? \chapter{Language} ??? \section{Lexical syntax} ??? \subsection{Identifiers} ??? \subsection{Symbols} ??? \subsection{Keywords} ??? \section{Environment} ??? \subsection{Vocabulary directive} ??? \subsection{Notation directive} ??? \subsection{Constructors directive} ??? \subsection{Clusters directive} ??? \subsection{Definitions directive} ??? \subsection{Theorems directive} ??? \subsection{Schemes directive} ??? \subsection{Requirements directive} ??? \section{Requirements} ??? \subsection{{\tt SUBSET}} ??? \subsection{{\tt BOOLE}} ??? \subsection{{\tt ARYTM}} ??? \subsection{{\tt REAL}} ??? \section{Reservations} ??? \section{References} ??? \subsection{Labels} ??? \subsection{MML theorem references} ??? \subsection{MML definition references} ??? \subsection{Cancellations} ??? \subsection{Scheme names} ??? \section{Definitions} ??? \subsection{Modes defined using {\tt means}}\label{ref:lan:mode:means} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| |[{\em assumptions\/}]\\ \verb| mode |{\em symbol\/}\verb| |[\verb|of |{\em arguments\/}]\verb| |[\verb|-> |{\em type\/}]\verb| means|\\ \verb| :|{\em label\/}\verb|: |{\em formula\/}\verb|;|\\ \verb| existence|\\ \verb| |{\em proof}\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} Section \ref{ref:lan:mode:is} (Modes defined using {\tt is}), Section \ref{ref:lan:existence} (Existence), Section \ref{ref:lan:types} (Type expressions). \subsection{Modes defined using {\tt is}}\label{ref:lan:mode:is} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| mode |{\em symbol\/}\verb| |[\verb|of |{\em arguments\/}]\verb| is |{\em type\/}\verb|;|\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} Section \ref{ref:lan:mode:means} (Modes defined using {\tt means}), Section \ref{ref:lan:structures} (Structures), Section \ref{ref:lan:types} (Type expressions). \subsection{Structures}\label{ref:lan:structures} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| struct |[\verb|(|{\em ancestors\/}\verb|)|]\verb| |{\em symbol\/}\verb| |[\verb|over |{\em arguments\/}]\\ \verb| (# |{\em field\/}${}_1$\verb| -> |{\em type\/}${}_1$\verb|,|\\ \verb| |{\em field\/}${}_2$\verb| -> |{\em type\/}${}_2$\verb|,|\\ \verb| |\dots\\ \verb| |{\em field\/}${}_n$\verb| -> |{\em type\/}${}_n$\verb| #);|\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar}\footnotesize \verb|definition let FS1,FS2 be 1-sorted;|\\ \verb| struct (VectSpStr over FS1, RightModStr over FS2) BiModStr over FS1,FS2|\\ \verb| (# carrier -> set,|\\ \verb| add -> BinOp of the carrier,|\\ \verb| compl -> UnOp of the carrier,|\\ \verb| Zero -> Element of the carrier,|\\ \verb| lmult -> Function of [:the carrier of FS1, the carrier:], the carrier,|\\ \verb| rmult -> Function of [:the carrier, the carrier of FS2:], the carrier #);|\\ \verb|end;| \end{mizar} ??? \paragraph{See also} Section \ref{ref:lan:types} (Type expressions). \subsection{Attributes} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| attr |{\em variable\/}\verb| is |{\em symbol\/}\verb| means |{\em formula\/}\verb|;|\\ \verb| |[\verb|synonym |{\em pattern\/}\verb|;|]\verb| |[\verb|antonym |{\em pattern\/}\verb|;|]\\ \verb| |[\verb|synonym |{\em variable\/}\verb| is |{\em symbol\/}\verb|;|]\verb| |[\verb|antonym |{\em variable\/}\verb| is |{\em symbol\/}\verb|;|]\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Existential clusters}\label{ref:lan:clusters:existential} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| cluster |{\em adjectives\/}\verb| |{\em type\/}\verb|;|\\ \verb| existence|\\ \verb| |{\em proof\/}\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Conditional clusters}\label{ref:lan:clusters:conditional} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| cluster |{\em adjectives\/}${}_1$\verb| -> |{\em adjectives\/}${}_2$\verb| |{\em type\/}\verb|;|\\ \verb| coherence|\\ \verb| |{\em proof\/}\\ \verb|end;| \end{mizar} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| cluster -> |{\em adjectives\/}${}_2$\verb| |{\em type\/}\verb|;|\\ \verb| coherence|\\ \verb| |{\em proof\/}\\ \verb|end;| \end{mizar} \paragraph{Description} Registering this kind of cluster causes all terms that have type {\em adjectives\/}${}_1$ {\em type\/} to also get adjectives {\em adjectives\/}${}_2$. The {\em loci\/} give the variables that occur in {\em type}, if any. If the cluster {\em adjectives\/}${}_1$ is empty, as in the second form, it means that every term of type {\em type\/} gets adjectives {\em adjectives\/}${}_2$. The \verb|coherence| statement for this kind of cluster registration is: \begin{mizar} \verb|for X being |{\em type\/}\verb| st X is |{\em adjectives\/}${}_1$\verb| holds X is |{\em adjectives\/}${}_2$ \end{mizar} \paragraph{Example} \begin{mizar} \verb| reserve X for set;|\\ \verb| reserve D for non empty set;|\\ \medskip \verb|definition let X,D;|\\ \verb| cluster quasi_total -> total PartFunc of X,D;|\\ \verb| coherence|\\ \verb| proof let f be PartFunc of X,D;|\\ \verb| assume f is quasi_total;|\\ \verb| then dom f = X by Def1;|\\ \verb| hence thesis by PARTFUN1:def 4;|\\ \verb| end;|\\ \verb|end;| \end{mizar} This cluster states that every term that has type \verb|quasi_total| \verb|PartFunc| \verb|of| \verb|X,D| will get type \verb|quasi_total| \verb|total| \verb|PartFunc| \verb|of| \verb|X,D|. \paragraph{See also} Section \ref{ref:lan:clusters:existential} (Existential clusters), Section \ref{ref:lan:clusters:functorial} (Functorial clusters), Section \ref{ref:lan:coherence} (Coherence), Section \ref{ref:lan:types} (Type expressions). \subsection{Functorial clusters}\label{ref:lan:clusters:functorial} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| cluster |{\em term\/}\verb| -> |{\em adjectives\/}\verb|;|\\ \verb| coherence|\\ \verb| |{\em proof\/}\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Predicates} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| pred |[{\em arguments\/}]\verb| |{\em symbol\/}\verb| |[{\em arguments\/}]\verb| means|\\ \verb| :|{\em label\/}\verb|: |{\em formula\/}\\ \verb| |[\verb|symmetry |{\em proof\/}]\\ \verb| |[\verb|connectedness |{\em proof\/}]\\ \verb| |[\verb|reflexivity |{\em proof\/}]\\ \verb| |[\verb|irreflexivity |{\em proof\/}]\\ \verb| |[\verb|synonym |{\em pattern\/}\verb|;|]\verb| |[\verb|antonym |{\em pattern\/}\verb|;|]\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Functors defined using {\tt means}} \paragraph{Syntax} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| |[{\em assumptions\/}]\\ \verb| func |[{\em arguments\/}]\verb| |{\em symbol\/}\verb| |[{\em arguments\/}]\verb| |[\verb|-> |{\em type\/}]\verb| means|\\ \verb| :|{\em label\/}\verb|: |{\em formula\/}\verb|;|\\ \verb| existence|\\ \verb| |{\em proof}\\ \verb| uniqueness|\\ \verb| |{\em proof}\\ \verb| |[\verb|commutativity |{\em proof\/}]\\ \verb| |[\verb|projectivity |{\em proof\/}]\\ \verb| |[\verb|involutiveness |{\em proof\/}]\\ \verb| |[\verb|synonym |{\em pattern\/}\verb|;|]\verb| |[\verb|antonym |{\em pattern\/}\verb|;|]\\ \verb|end;| \end{mizar} \begin{mizar} \verb|definition |[{\em loci\/}]\\ \verb| |[{\em assumptions\/}]\\ \verb| func |{\em symbol\/}\verb| |{\em arguments\/}\verb| |{\em symbol\/}\verb| |[\verb|-> |{\em type\/}]\verb| means|\\ \verb| :|{\em label\/}\verb|: |{\em formula\/}\verb|;|\\ \verb| existence|\\ \verb| |{\em proof}\\ \verb| uniqueness|\\ \verb| |{\em proof}\\ \verb| |[\verb|commutativity |{\em proof\/}]\\ \verb| |[\verb|projectivity |{\em proof\/}]\\ \verb| |[\verb|involutiveness |{\em proof\/}]\\ \verb| |[\verb|synonym |{\em pattern\/}\verb|;|]\verb| |[\verb|antonym |{\em pattern\/}\verb|;|]\\ \verb|end;| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Functors defined using {\tt equals}} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Definitions by cases} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Redefinitions}\label{ref:lan:redefinitions} ??? \section{Correctness conditions} ??? \subsection{Existence}\label{ref:lan:existence} ??? \subsection{Uniqueness} ??? \subsection{Coherence}\label{ref:lan:coherence} ??? \subsection{Compatibility} ??? \subsection{Consistency} ??? \section{Properties} ??? \subsection{Commutativity} ??? \subsection{Symmetry} ??? \subsection{Connectedness} ??? \subsection{Reflexivity} ??? \subsection{Irreflexivity} ??? \subsection{Synonym} ??? \subsection{Antonym} ??? \section{Theorems and schemes} ??? \subsection{Theorems} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Schemes} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \section{Reasoning Items} ??? \subsection{Compact statements} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Assume} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Thus} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Let} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Take} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Given} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Consider} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Reconsider} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Set} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Deffunc and defpred} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Per cases with {\tt case}} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Per cases with {\tt suppose}} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \subsection{Iterative equalities} \paragraph{Syntax} \begin{mizar} \verb|???| \end{mizar} \paragraph{Description} ??? \paragraph{Example} \begin{mizar} \verb|???| \end{mizar} ??? \paragraph{See also} ??? \section{Justification} ??? \subsection{Proof} ??? \subsection{{\tt @}Proof} ??? \subsection{Now} ??? \subsection{By} ??? \subsection{Then, hence, hereby} ??? \subsection{From} ??? \section{Formula expressions} ??? \subsection{Predicate logic}\label{ref:lan:predlogic} ??? \subsection{Atomic formulas} ??? \section{Type qualifications} ??? \section{Type expressions}\label{ref:lan:types} ??? \subsection{Structures}\label{ref:lan:types:structures} ??? {\tt strict} ??? \section{Term expressions} ??? \subsection{Qua} ??? \subsection{Structures} ??? \subsection{Fraenkel operator} ??? \chapter{System} ??? \section{Installing Mizar under Windows}\label{ref:sys:install} ??? \section{Installing Mizar under Linux} ??? \section{Directories and files} ??? \subsection{{\tt TEXT} directory} ??? \subsection{{\tt DICT} directory} ??? \subsection{{\tt PREL} directory} ??? \subsection{{\tt MIZ} files} ??? \subsection{{\tt ABS} files} ??? \subsection{{\tt VOC} files} ??? \subsection{Other files in {\tt TEXT}} ??? \subsection{Files in {\tt PREL}} ??? \subsection{Other files in {\tt MIZFILES}} ??? \section{Kernel programs} ??? \subsection{{\tt MIZF}} ??? \subsection{{\tt MAKEENV}} ??? \subsection{{\tt ACCOM}} ??? \subsection{{\tt VERIFIER}} ??? \subsection{{\tt ENV}} ??? \subsection{{\tt EXPORTER}} ??? \subsection{{\tt TRANSFER}} ??? \subsection{{\tt PRE}} ??? \section{Programs for optimization} ??? \subsection{{\tt RELPREM}} ??? \subsection{{\tt RELINFER}} ??? \subsection{{\tt RELITERS}} ??? \subsection{{\tt TRIVDEMO}} ??? \subsection{{\tt CHKLAB}} ??? \subsection{{\tt INACC}} ??? \subsection{{\tt IRRVOC}} ??? \subsection{{\tt IRRTHS}} ??? \section{Programs for error messages} ??? \subsection{{\tt REVF}} ??? \subsection{{\tt CHKERR}} ??? \subsection{{\tt ERRFLAG}} ??? \subsection{{\tt REMFLAGS}} ??? \subsection{{\tt ADDFMSG}} ??? \section{Programs to generate the abstract} ??? \subsection{{\tt MIZ2ABS}} ??? \subsection{{\tt ABSEDT}} ??? \subsection{{\tt EDTFILE}} ??? \section{Programs for vocabularies} ??? \subsection{{\tt CHECKVOC}} ??? \subsection{{\tt FINDVOC}} ??? \subsection{{\tt LISTVOC}} ??? \section{Other programs} ??? \subsection{{\tt CONSTR}} ??? \subsection{{\tt RATPROOF}} ??? \subsection{{\tt BIBART}} ??? \section{Obsolete programs} ??? \section{Error messages} ??? \chapter{Library} ??? \section{Getting the library} ??? \section{Submitting to the library}\label{ref:lib:submitting} ??? \section{Copyright} ??? \part{Tutorial} \chapter{Writing a Mizar article in nine easy steps} After reading this chapter and doing the exercises, you will be able to write a basic Mizar article all by yourself. The chapter presents an explanation of the nine steps needed to finish a Mizar article. For each step it also shows how this turns out for a specific example. There are exercises too, so you can test your understanding. To be able to read this chapter you should know some basic mathematics but not much. You should know a little bit about: \begin{itemize} \item first order predicate logic \item some basic set theory \end{itemize} Mizar is based on set theory on top of predicate logic, that's why. The most difficult part of writing Mizar is finding what you need in the MML which is the name of the {\em Mizar Mathematical Library}. Unfortunately that problem has no easy solution. You will discover that apart from that, writing a Mizar article is straight-forward. \section{Step 1: the mathematics} Before you start writing a Mizar article you need to decide what it should be about. It's very important not to start writing the article too soon! A proof that takes five minutes to explain -- after which people look into the air and then mumble: `hm, yes, I see' -- takes about a week to formalize. So every improvement to the mathematics that you can make {\em before} you start formalizing will pay off very much. \begin{example} As a running example in this chapter we write a small Mizar article called \verb|MY_MIZAR.MIZ|. It is about {\em Pythagorean triples}. Those are triples of natural numbers $\{ a,b,c \}$ for which holds that: $$a^2 + b^2 = c^2$$ The Pythagorean theorem tells us that these triples correspond to square angled triangles that have sides of integer length. The best known of these triples are $\{ 3,4,5 \}$ and $\{ 5,12,13 \}$ but there are an infinite number of them. The theorem that we will formalize says that all Pythagorean triples are given by the formula: $$a = n^2 - m^2 \qquad b = 2mn \qquad c = n^2 + m^2$$ or are multiples of such a triple. For instance the triple $\{ 3,4,5 \}$ is given by $n = 2$, $m = 1$, and the triple $\{ 5,12,13 \}$ is given by $n = 3$, $m = 2$. The proof of the theorem is straight-forward. You only needs to consider the case where $a$ and $b$ are relative prime. Some thought about parity gives that one of the $a$ and $b$ has to be even, and that the other and $c$ is odd. Then if $b$ is the even number of the two we get that: $$\Big({b\over 2}\Big)^2 = {c^2 - a^2\over 4} = \Big({c - a\over 2}\Big)\Big({c + a\over 2}\Big)$$ But if the product of two relative prime numbers is a square, then both of those numbers are squares. So you get: $${c - a\over 2} = m^2 \qquad {c + a\over 2} = n^2$$ which leads to the required formula. \end{example} \begin{exercise} Study the Mizar Mathematical Library and try to decide whether Mizar is equally suited to all fields of mathematics and computer science, or that Mizar is best suited to certain subjects. In the latter case, what is most easily formalized in Mizar? And what least? \end{exercise} \begin{exercise} We mentioned the {\em Pythagorean theorem\/} which says that the sides $a$, $b$ and $c$ of a square angled triangle satisfy $a^2 + b^2 = c^2$. Try to find this theorem in the MML. If it's there, in what article does it occur and what is the theorem's reference? If not, or if you don't like the version that you find (exercise for when you finished this chapter): write an article that proves it. \end{exercise} \section{Step 2: the empty Mizar article} In order to write a Mizar article you need a working Mizar system and a file to put the Mizar article in. In fact, as you will find out, you will need {\em two\/} files: a \verb|.MIZ| file for your article and a \verb|.VOC| file for its vocabulary. In this tutorial we follow the Windows conventions of naming files. For Mizar under Unix everything should be lower case instead of upper case and the backslashes should go the other way. So what is called \verb|TEXT\MY_MIZAR.MIZ| here, under Unix should be \verb|text/my_mizar.miz|. We will assume that you already have a properly installed Mizar system. For a description of how to install Mizar read Section \ref{ref:sys:install}, or see the \verb|README.TXT| file that is in the Mizar distribution. To write your article, you need to be in a directory that has two subdirectories called \verb|TEXT| and \verb|DICT|. If those directories don't exist yet, make them. Put in the \verb|TEXT| directory an empty file called \verb|MY_MIZAR.MIZ| and put in the \verb|DICT| directory an empty file called \verb|MY_MIZAR.VOC|. (Replace the \verb|MY_MIZAR| with a more appropriate name if you are writing an article of your own.) The smallest legal \verb|.VOC| file is empty but the smallest legal \verb|.MIZ| file looks like this: \begin{mizar} \verb|environ|\\ \verb|begin| \end{mizar} Use your favorite text editor to put those two lines in the \verb|TEXT\MY_MIZAR.MIZ| file. Then check it using the command: \begin{mizar} \verb|mizf text\my_mizar| \end{mizar} It will both check syntax and mathematics of your article. If everything is well this command prints something like: \begin{mizar} \verb|Make Environment, Mizar Ver. 6.1.05 (Win32/Delphi 4)|\\ \verb|Copyright (c) 1990,2001 Association of Mizar Users|\\ \verb|-Vocabularies-Constructors-Clusters-Notation| \bigskip\\ \verb|Verifier, Mizar Ver. 6.1.05 (Win32/Delphi 4)|\\ \verb|Copyright (c) 1990,2001 Association of Mizar Users|\\ \verb|Processing: text\my_mizar.miz| \medskip\\ \verb|Parser [ 2] 0:00|\\ \verb|Analyzer 0:00|\\ \verb|Checker [ 1] 0:00|\\ \verb|Time of mizaring: 0:01| \end{mizar} meaning that this `article' contains no errors. (If you use the \verb|emacs| editor with its Mizar mode you don't need to type the \verb|mizf| command. In that case all you need to do to check the file is hit \verb|C-c| \verb|RET|.) Apart from the \verb|MY_MIZAR.MIZ| file, the \verb|TEXT| directory now contains 24 other files. You never need to look inside them. They are only used internally by the Mizar system. The next step is to connect the \verb|.MIZ| file to the \verb|.VOC| vocabulary. Add a \verb|vocabulary| directive to your article: \begin{mizar} \verb|environ|\\ \verb| vocabulary MY_MIZAR;| \medskip\\ \verb|begin| \end{mizar} % Now the article is ready to be written. For the moment add some line of text at the end of the file just to find out what happens if the article contains errors: \begin{mizar} \verb|environ|\\ \verb| vocabulary MY_MIZAR;| \medskip\\ \verb|begin|\\ \verb| hello Mizar!| \end{mizar} After you ran \verb|mizf text\my_mizar.miz| command again, Mizar will insert the error messages {\em inside\/} your file. It will put a \verb|*| with a number below any error. Also there will be an explanation of those error numbers at the end of the file. So after running the \verb|mizf| command again your file looks like: \begin{mizar} \verb|environ|\\ \verb| vocabulary MY_MIZAR;| \medskip\\ \verb|begin|\\ \verb| hello Mizar!|\\ \verb|::> *143,321|\\ \verb|::>|\\ \verb|::> 143: No implicit qualification|\\ \verb|::> 321: Predicate symbol or "is" expected| \end{mizar} There is no need to try to understand those two error messages, because of course \verb|hello Mizar!| is not legal Mizar. So remove this line, now that you have seen what Mizar thinks of it. You don't need to remove the error message lines. They vanish the next time you run \verb|mizf|. The lines containing error messages can be recognized because they start with \verb|::>|. Mizar only gives you error numbers. It never prints anything about why it thinks it is wrong. Sometimes this lack of explanation is frustrating but generally Mizar errors are quite obvious. \begin{exercise} The minimal Mizar article that we showed is 2 lines long. What is the shortest article in the MML? What is the longest? What is the average number of lines in the articles in the MML? As a rule of thumb an article less than a 1000 lines is considered too short to be submitted to the MML. However several articles in the MML are less than a 1000 lines long since articles are shortened during revision of the MML. How many of the articles in the MML are currently shorter than a 1000 lines? \end{exercise} \begin{exercise} Copy an article from the MML to your private \verb|TEXT| directory. Check that the Mizar checker \verb|mizf| processes it without error messages. Experiment with making small modifications to it and see whether Mizar can detect where you tampered with it. Put one screen-full of non-Mizar text -- for instance from a Pascal or C program -- somewhere in the middle of the article. How many error messages will you get? Can Mizar sufficiently recover from those errors to check the second half of the file reasonably well? \end{exercise} \section{Step 3: the statement} To start translating your mathematics to Mizar you need to write the theorem that you want to prove in Mizar syntax. There are two things about Mizar syntax that are important for you to note: \begin{itemize} \item There are no spelling variants in Mizar. Although Mizar resembles natural language a lot, it is a formal language and there are no possibilities to choose between phrasings. For example: \begin{itemize} \item[] \verb|and| means something different from \verb|&| \item[] \verb|not| means something different from \verb|non| \item[] \verb|such that| means something different from \verb|st| \item[] \verb|assume| means something different from \verb|suppose| \item[] \verb|NAT| means something different from \verb|Nat| means something different from \verb|natural| \end{itemize} So you should really pay attention to the exact keywords in the Mizar syntax. It's not enough if it resembles it. The only exception to this rule is that \verb|be| and \verb|being| are alternative spellings. So although it's more natural to write {\tt let X be set} and {\tt for X being set holds }{\dots} you are also allowed to write {\tt let X being set} and {\tt for X be set holds }{\dots} \item There is no distinction in Mizar between `function notation' and `operator notation'. In most programming languages something like \verb|f(x,y)| and \verb|x+y| are syntactically different things. In Mizar this distinction doesn't exist. In Mizar {\em everything\/} is an operator. If you write \verb|f(x,y)| in Mizar then it really is a `operator symbol' \verb|f| with zero left arguments and two right arguments. Similarly predicate names and type names can be any string of characters that you might wish. You can mix letters, digits and any other character you might like in them. So for instance if you want to call a predicate \verb|\/-distributive| you can do so in Mizar. And it will be one `symbol'. If you are not sure what characters go together as a symbol in a Mizar formula, you can go to the web pages of the MML abstracts. In those pages the symbols are hyperlinks that point to definitions. So just click on them to find out what symbol they are. \end{itemize} \noindent To write Mizar you need to know how to write terms and how to write formulas. We tackle this in top-down fashion. First we describe how to translate formulas from predicate logic into Mizar. Then we describe how the syntax of Mizar terms works. \subsection{Formulas} Here is a table that shows all you want to know about how to write predicate logic in Mizar: \begin{center} \begin{tabular}{cl} $\bot$ & \verb|contradiction|\\ $\neg\phi$ & \verb|not |$\phi$\\ $\phi\land\psi$ & $\phi$\verb| & |$\psi$\\ $\phi\lor\psi$ & $\phi$\verb| or |$\psi$\\ $\phi\Rightarrow\psi$ & $\phi$\verb| implies |$\psi$\\ $\phi\Leftrightarrow\psi$ & $\phi$\verb| iff |$\psi$\\ $\exists\,x.\,\psi$ & \verb|ex x st |$\psi$\\ $\forall\,x.\,\psi$ & \verb|for x holds |$\psi$\\ $\forall\,x.\,(\phi\Rightarrow\psi)$ & \verb|for x st |$\phi$\verb| holds |$\psi$ \end{tabular} \end{center} There is no special way to write $\top$ in Mizar. One usually writes {\tt not} {\tt contradic\-tion} for this. Note that with the quantifiers it should be \verb|st| and not \verb|such| \verb|that|. Using this table you now can write logical formulas in Mizar. There is one more thing that you need to know to write Mizar formulas in practice. Mizar is a {\em typed\/} language. We will discuss Mizar types in detail in Section \ref{tut:stat:types} below, but the types turn up in the predicate logic formulas too. All variables that you use in formulas need to have a type. There are two ways to give a variable a type: \begin{itemize} \item Put the type in the formula using a \verb|being| type attribution. For instance you can write an existential formula about natural numbers $m$ and $n$ as: \begin{mizar} \verb|ex m,n being Nat st |\dots \end{mizar} \item Give the type for the variable with a \verb|reserve| statement. This doesn't introduce a variable, it just introduces a notation convention. If you use a \verb|reserve| statement you can leave out the type in the formula: \begin{mizar} \verb|reserve m,n for Nat;|\\ \verb|ex m,n st |\dots \end{mizar} This way of typing variables in formulas is much more convenient than explicitely typing the variables and so it is the method that is generally used. \end{itemize} \begin{exercise} Translate the following Mizar formulas into predicate logic notation: \begin{itemize} \item[] $\phi$\verb| iff not not |$\phi$ \item[] \verb|not (|$\phi$\verb| & |$\psi$\verb|) implies not |$\phi$\verb| or not |$\psi$ \item[] \verb|ex x st |$\phi$\verb| implies |$\psi$ \item[] \verb|for x st for y st |$\phi$\verb| holds |$\psi$\verb| holds |$\chi$ \end{itemize} Translate the following predicate logic formulas into Mizar syntax: \begin{itemize} \item[] $\neg\phi\Leftrightarrow\neg\neg\neg\phi$ \item[] $\neg(\phi\lor\psi)\Rightarrow(\neg\phi\land\neg\psi)$ \item[] $\exists\,x.\,(\phi\land\psi)$ \item[] $\exists\,x.\,\big(\big(\exists\,y.\,(\phi\Rightarrow\psi)\big)\Rightarrow\chi\big)$ \end{itemize} If you worry about the priorities of the Mizar logical operators add as many brackets as you need to feel sure. Alternatively look at the table in Section \ref{ref:lan:predlogic}. \end{exercise} \subsection{Relations} You still need to know how to write atomic formulas. In Mizar there are two ways to write those: \begin{itemize} \item If $R$ is a {\em predicate\/} symbol, write: \begin{center} $x_1$\verb|,|$\,x_2$\verb|,|$\,\ldots$\verb|,|$\,x_m \mathrel{R} x_{m+1}$\verb|,|$\,\ldots$\verb|,|$\,x_{m+n}$ \end{center} Both $m$ or $n$ might be $0$, in which case this becomes prefix or postfix notation. Note that postfix notation can have more than one argument, as for instance in \verb|x,y| \verb|are_relative_prime|. Please note that brackets around the arguments of the predicate are not allowed. \item If ${\cal T}$ is a {\em type}, or the adjectives part of a type, write: \begin{center} $x$\verb| is |${\cal T}$ \end{center} For instance you can write \verb|x| \verb|is| \verb|prime|. We will discuss types in Section \ref{tut:stat:types} below. \end{itemize} % To find out what relations are available to you, you will need to browse the MML. Here is a short list of some of the most frequent used relations to get you started. \begin{center} \begin{tabular}{cc} $=$ & \verb|=|\\ $\ne$ & \verb|<>|\\ $<$ & \verb|<|\\ $\le$ & \verb|<=|\\ $\in$ & \verb|in|\\ $\subseteq$ & \verb|c=| \end{tabular} \end{center} The first character in the Mizar representation of $\subseteq$ is the letter \verb|c|. \subsection{Terms} There are three ways to write Mizar terms: \begin{itemize} \item If $f$ is an operator symbol, which Mizar calls a {\em functor\/}, write: \begin{center} \verb|(|$x_1$\verb|,|$\,x_2$\verb|,|$\,\ldots$\verb|,|$\,x_m\verb|)| \mathrel{f} \verb|(|x_{m+1}$\verb|,|$\,\ldots$\verb|,|$\,x_{m+n}$\verb|)| \end{center} Again, $m$ or $n$ might be $0$, in which case this becomes prefix or postfix notation. As an example of a postfix operator there is \verb|^2| for square. The brackets around either list of arguments can be omitted if there is just one argument. \item If ${\cal L}$ and ${\cal R}$ are {\em bracket} symbols, write: \begin{center} ${\cal L}\;x_1$\verb|,|$\,x_2$\verb|,|$\,\ldots$\verb|,|$\,x_n\;{\cal R}$ \end{center} In this case brackets \verb|(| and \verb|)| around the arguments are not necessary, since the symbols themselves are already brackets. An example of this kind of term is the ordered pair \verb|[x,y]|. In that case $n = 2$, ${\cal L}$ is \verb|[| and ${\cal R}$ is \verb|]|. \item Any natural number is a Mizar term. If you write natural numbers, you should add to your \verb|environ| the line: \begin{mizar} \verb|requirements SUBSET, ARYTM;| \end{mizar} because else they won't behave like natural numbers. \end{itemize} % The word {\em functor\/} for function symbol or operator symbol is Mizar terminology. It has nothing to do with the notion of functor in category theory. It is used to distinguish a function symbol in the logic from a function object in the set theory (which is a set of pairs). Again to find out what operators are available to you, you will need to browse the MML. Here is a short list of some of the most frequent used operators to get you started. \begin{center} \begin{tabular}{cc} $\emptyset$ & \verb|{}|\\ $\{x\}$ & \verb|{|$\,x\,$\verb|}|\\ $\{x,y\}$ & \verb|{|$\,x$\verb|,|$y\,$\verb|}|\\ $X\cup Y$ & $X$\verb| U |$Y$\\ $X\cap Y$ & $X$\verb| |{\footnotesize $\cap$}\verb| |$Y$\\ ${\mathbb N}$ & \verb|NAT|\\ ${\mathbb Z}$ & \verb|INT|\\ ${\mathbb R}$ & \verb|REAL|\\ $x+y$ & $x$\verb| + |$y$\\ $x-y$ & $x$\verb| - |$y$\\ $-x$ & \verb|-|$\,x$\\ $xy$ & $x\cdot y$\\ $x/y$ & $x\,$\verb|/|$\,y$\\ $x^2$ & $x$\verb|^2|\\ $\sqrt{x}$ & \verb|sqrt |$x$\\ ${\cal P}(X)$ & \verb|bool |$X$\\ $(x,y)$ & \verb|[|$\,x$\verb|,|$y\,$\verb|]|\\ $X\times Y$ & \verb|[:|$X$\verb|,|$Y$\verb|:]|\\ $Y^X$ & \verb|Funcs(|$X$\verb|,|$Y$\verb|)|\\ $f(x)$ & $f$\verb|.|$x$\\ $\langle\rangle$ & \verb|<**>|$D$\\ $\langle x\rangle$ & \verb|<*|$\,x\,$\verb|*>|\\ $\langle x,y\rangle$ & \verb|<*|$\,x$\verb|,|$y\,$\verb|*>|\\ $p\cdot q$ & $p$\verb|^|$q$ \end{tabular} \end{center} The union operator is the capital letter \verb|U|. The digit \verb|2| is part of the symbol for the square operator. The last four operators are used to build finite sequences over the set $D$. The characters $\,\cdot\,$ and {\footnotesize $\cap$} are DOS characters with ASCII codes $\ge 128$. Mizar uses that kind of character for some of its symbols. The specific characters $\,\cdot\,$ and {\footnotesize $\cap$} have codes 249 and 239. How to type them may depend on your editor. Try holding the {\em alt\/} key and simultaneously typing the number on the numeric keypad. The \verb|.| operation is function application {\em inside the set theory}. If \verb|f| is a symbol {\em in the language} representing a functor with zero left arguments and one right argument then you write: \begin{mizar} \verb|f x| \end{mizar} or (you can always put a term in brackets): \begin{mizar} \verb|f(x)| \end{mizar} If \verb|f| is a function in the set theory -- a set of pairs -- then \begin{mizar} \verb|f.x| \end{mizar} is the image of \verb|x| under \verb|f|, in other words it is the \verb|y| such that \verb|[x,y]| \verb|in| \verb|f|. \subsection{Types: modes and attributes}\label{tut:stat:types} The one thing left for you to understand to write Mizar formulas is Mizar's types. Although Mizar is based on ZF-style set theory -- so the {\em objects\/} of Mizar are untyped -- the {\em terms\/} of Mizar are typed. An example of a Mizar type is: \begin{center} \verb|non empty finite Subset of NAT| \end{center} This type should be parsed as: \begin{center} {\tt \framebox{\tt \framebox{\tt non empty\strut} \framebox{\tt finite\strut}} \framebox{\tt \underline{\tt Subset} of NAT\strut}} \end{center} A Mizar type consists of an instance of a {\em mode} with in front a cluster of {\em adjectives}. The type without the adjectives is called the {\em radix type}. In this case the mode is \verb|Subset| and its argument is \verb|NAT|, the radix type is \verb|Subset| \verb|of| \verb|NAT|, and the two adjectives are \verb|non| \verb|empty| and \verb|finite|. To put this abstractly, a Mizar type is written: \begin{center} $\alpha_1$\verb| |$\alpha_2$\verb| |\dots\verb| |$\alpha_m$\verb| |${\cal M}$\verb| of |$x_1$\verb|,|$\,x_2$\verb|,|$\,\ldots$\verb|,|$\,x_n$ \end{center} where $\alpha_1$, {\dots} $\alpha_m$ are adjectives, ${\cal M}$ is a mode symbol and $x_1$, $x_2$, {\dots}, $x_n$ are terms. The keyword \verb|of| binds the arguments of the mode to the mode. It's like the brackets in a term. The number of arguments $n$ is part of the definition of the mode. For instance for \verb|set| it is zero. You can't write \verb|set| \verb|of| {\dots}, because there does not exist a \verb|set| mode that takes arguments. Modes are dependent types. To find out what modes are available to you, you will need to browse the MML. Here is a short list of some of the most frequent used modes to get you started. \begin{center} \begin{tabular}{c} \verb|set|\\ \verb|number|\\ \verb|Element of |$X$\\ \verb|Subset of |$X$\\ \verb|Nat|\\ \verb|Int|\\ \verb|Real|\\ \verb|Ordinal|\\ \verb|Relation|\\ \verb|Relation of |$X$\verb|,|$Y$\\ \verb|Function|\\ \verb|Function of |$X$\verb|,|$Y$\\ \verb|FinSequence of |$X$ \end{tabular} \end{center} Note that there both are modes \verb|Relation| and \verb|Function| with no arguments, and more specific modes \verb|Relation| \verb|of| \verb|X,Y| and \verb|Function| \verb|of| \verb|X,Y| with two arguments. They share the mode symbol but they are different. Also note that the modes depend on {\em terms}. So there are no types representing the functions from a type to a type. The \verb|Function| mode represents the functions from a set to a set. As an example the function space $(X\to Y)\times X\to Y$ corresponds to the Mizar type \verb|Function| \verb|of| \verb|[:Funcs(X,Y),X:],Y| Adjectives restrict a radix type to a subtype. They either are an {\em attribute\/}, or the negation of an attribute using the keyword \verb|non|. Again, to find out what attributes are available to you, you will need to browse the MML. Here is a list of a few attributes. \begin{center} \begin{tabular}{c} \verb|empty|\\ \verb|even|\\ \verb|odd|\\ \verb|prime|\\ \verb|natural|\\ \verb|integer|\\ \verb|real|\\ \verb|finite|\\ \verb|infinite|\\ \verb|countable| \end{tabular} \end{center} % Maybe you now wonder about how types are used in Mizar. To clarify this take a look at three Mizar notions -- \verb|NAT|, \verb|Nat| and \verb|natural| -- that all mean the same thing: the set of natural numbers. Here is a table that compares their uses: \begin{center} \begin{tabular}{ccc} {\em meaning\/} & {\em declaration\/} & {\em formula\/}\\ \noalign{\smallskip} $n\in{\mathbb N}$ & & \verb|n in NAT|\\ $n\mathrel{:}{\mathbb N}$ & \verb|n be Nat| & \verb|n is Nat|\\ $n\mathrel{:}{\mathbb N}$ & \verb|n be natural number| & \verb|n is natural| \end{tabular} \end{center} \verb|NAT| is a term, \verb|Nat| is a type and \verb|natural| is an adjective. \verb|be|/\verb|being| are a typing in a declaration and go between a variable and a type. \verb|in| is the $\in$ relation of the set theory and goes between two terms. \verb|is| goes between a term and a type or between a term and an adjective. Note that in Mizar you can have a `type judgement' as a formula in the logic. \begin{example} We now give the statement of the theorem for the example. The statement that we will prove in this chapter is: \begin{mizar} \verb|reserve a,b,c,m,n for Nat;| \medskip\\ \verb|a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2;| \end{mizar} So put this after the \verb|begin| line of your \verb|MY_MIZAR.MIZ| file. We also could have made the quantification of the \verb|a|, \verb|b| and \verb|c| explicit: \begin{mizar} \verb|for a,b,c st|\\ \verb| a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd holds|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2;| \end{mizar} but it is not necessary. Mizar automatically quantifies over free variables. We now analyze this statement in some detail. The formula has the structure: \begin{center} $\phi_1$\verb| & |$\phi_2$\verb| & |$\phi_3$\verb| implies ex m,n st |$\phi_4$\verb| & |$\phi_5$\verb| & |$\phi_6$\verb| & |$\phi_7$\verb|;| \end{center} The predicate logic formula that corresponds to this is: $$(\phi_1 \land \phi_2 \land \phi_3) \Rightarrow \exists\,m,n.\,(\phi_4 \land \phi_5 \land \phi_6 \land \phi_7)$$ The first three atomic formulas in this are: \begin{eqnarray*} \phi_1 &\equiv& \verb|a^2 + b^2 = c^2|\\ \phi_2 &\equiv& \verb|a,b are_relative_prime|\\ \phi_3 &\equiv& \verb|a is odd| \end{eqnarray*} They have the structure: \begin{eqnarray*} \phi_1 &\equiv& t_1\;\framebox{\tt =}\;t_2\\ \phi_2 &\equiv& t_3\verb|,|\,t_4\;\framebox{\tt are\_relative\_prime}\\ \phi_3 &\equiv& t_5\verb| is |{\cal T} \end{eqnarray*} In this \verb|=| and \verb|are_relative_prime| are predicate symbols. ${\cal T}$ is the adjective \verb|odd|. So we here see both kinds of atomic formula: twice a relation between terms and once a typing. The first term $t_1$ in $\phi_1$ is: \begin{eqnarray*} t_1 &\equiv& \verb|a^2 + b^2| \end{eqnarray*} It has the structure: \begin{eqnarray*} t_1 &\equiv& u_1\;\framebox{\tt +}\;u_2\\ u_1 &\equiv& v_1\;\framebox{\tt \^{}2}\\ u_2 &\equiv& v_2\;\framebox{\tt \^{}2}\\ v_1 &\equiv& \verb|a|\\ v_2 &\equiv& \verb|b| \end{eqnarray*} In this \verb|+| and \verb|^2| are functor symbols. \end{example} \begin{exercise} Find Mizar types for the following concepts: \begin{itemize} \item[] odd number that is not a prime number \item[] empty finite sequence of natural numbers \item[] uncountable set of reals \item[] element of the empty set \item[] non-empty subset of the empty set \end{itemize} What is the problem with the last two concepts? Do you think they should be allowed in Mizar? Study this manual to find out whether they are. \end{exercise} \begin{exercise} Write the following statements as Mizar formulas: \begin{itemize} \item[] The only even prime number is $2$. \item[] If a prime number divides a product it divides one of the factors. \item[] There is no biggest prime number. \item[] There are infinitely many prime twins. \item[] Every even number $\ge 4$ is the sum of two primes. \end{itemize} Write these statements first using \verb|reserve| statements. Then write them again but this time with the types in the formulas. \end{exercise} \section{Step 4: getting the environment right} Add the statement that you wrote to your article. Then check it. You will get error messages: \begin{mizar} \verb|environ|\\ \verb| vocabulary MY_MIZAR;| \medskip\\ \verb|begin|\\ \verb| reserve a,b,c,m,n for Nat;|\\ \verb|::> *151| \medskip\\ \verb|a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies|\\ \verb|::>,203|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2;|\\ \verb|::>|\\ \verb|::> 151: Unknown mode format|\\ \verb|::> 203: Unknown token| \end{mizar} That's because you didn't import what you used from the MML. There's nothing wrong with the statement, there's something wrong with the environment (it's empty). To correct this, you need to add {\em directives\/} to the \verb|environ| part of the article to import what you need. It is hard to get the environment of a Mizar article correct. In practice people often just copy the environment of an old article. However that doesn't help much when it doesn't work, and occasionally it doesn't work. So you still have to understand how the environment works to get it right when you get environment related errors. \subsection{Vocabulary, notation, constructors} The rule is quite simple. For everything you use -- predicate, functor, mode or attribute -- you have to add a relevant reference to three directives: \begin{itemize} \item \verb|vocabulary| \item \verb|notation| \item \verb|constructors| \end{itemize} The list of references for \verb|notation| and \verb|constructors| is generally almost identical. In fact, if you follow the algorithm from this section to get them right they {\em will\/} be identical. These directives are about: \begin{itemize} \item Lexical analysis. The tokens in a Mizar article come from lists called {\em vocabularies}. Mizar variables are identifiers with a fixed syntax, but the predicates, functors, types and attributes all are {\em symbols\/} which can contain any character. You need to indicate from what vocabularies you use symbols. \item Parsing of expressions. To have an expression you need to list the articles that you use predicates, functors, types and attributes from. The \verb|notation| directive is for the syntax of expressions. The \verb|constructors| directive is for its meaning. \end{itemize} Here is a list of what we use in our statement, what kind of thing it is, and what vocabularies and articles we need for it: \begin{center} \begin{tabular}{lccc} {\em symbol\/} & {\em kind\/} & {\em vocabulary\/} & {\em article\/}\\ \noalign{\smallskip} \verb|=| & {\em pred\/} & & \verb|HIDDEN| \\ \verb|<=| & {\em pred\/} & \verb|HIDDEN| & \verb|ARYTM| \\ \verb|+| & {\em func\/} & \verb|HIDDEN| & \verb|ARYTM| \\ $\,\cdot\,$ & {\em func\/} & \verb|HIDDEN| & \verb|ARYTM| \\ \verb|-| & {\em func\/} & \verb|REAL_1| & \verb|REAL_1| \\ \verb|Nat| & {\em mode\/} & \verb|HIDDEN| & \verb|NAT_1| \\ \verb|are_relative_prime| & {\em pred\/} & \verb|INT_2| & \verb|INT_2| \\ \verb|^2| & {\em func\/} & \verb|SQUARE| & \verb|SQUARE_1| \\ \verb|odd| & {\em attr\/} & \verb|MATRIX2| & \verb|ABIAN| \end{tabular} \end{center} You don't need to refer to the \verb|HIDDEN| vocabulary or the \verb|HIDDEN| article but you need to list the others. The vocabularies should go in the \verb|vocabulary| directive and the articles should go both in the \verb|notation| and \verb|constructors| directives. So your environment needs to be: \begin{mizar} \verb|environ|\\ \verb| vocabulary MY_MIZAR, REAL_1, INT_2, SQUARE, MATRIX2;|\\ \verb| notation ARYTM, REAL_1, NAT_1, INT_2, SQUARE_1, ABIAN;|\\ \verb| constructors ARYTM, REAL_1, NAT_1, INT_2, SQUARE_1, ABIAN;| \end{mizar} % Here is the way to find out what the vocabulary and article a given symbol are: \begin{itemize} \item To find the vocabulary use the command: \begin{mizar} \verb|findvoc -w |{\em symbol} \end{mizar} For instance the command: \begin{mizar} \verb|findvoc -w ^2| \end{mizar} gives: \begin{mizar} \verb|FindVoc, Mizar Version 6.0.04 (/TP 7.0)|\\ \verb|Copyright (c) 1990,2000 Association of Mizar Users|\\ \verb|vocabulary: SQUARE|\\ \verb|O^2 254| \end{mizar} The \verb|O| means that this is a functor symbol, and 254 is the priority. \item To find the article, the easiest way is to go to the web pages of the abstracts of the MML, find a use of the symbol somewhere, and click on it to go to the definition. \end{itemize} \subsection{Redefinitions and clusters}\label{tut:env:clusters} But now things get tough. It turns out that your environment still does not work! The problem is that the types are wrong. If we check the article with the new environment we get: \begin{mizar} \verb|a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2;|\\ \verb|::> *102 *103|\\ \verb|::>|\\ \verb|::> 102: Unknown predicate|\\ \verb|::> 103: Unknown functor| \end{mizar} To get rid of these kind of typing problems is the most difficult part of writing a Mizar article. (In practice this kind of error often is caused because a {\em cluster\/} is missing. So if you are completely mystified by a Mizar error, start thinking `cluster!') In this specific case: \begin{itemize} \item The first error is caused by the fact that \verb|m| and \verb|n| have type \verb|Nat|, but \verb|<=| wants arguments of type \verb|real| \verb|number|. \item The second error is caused by the fact that Mizar doesn't know (with this environment) that \verb|2| has type \verb|Nat|. \end{itemize} We solve the first error in this section and the second error in the next one. A Mizar expression doesn't have just one type, it has a whole set of types. There are two ways to influence the type of an expression. \begin{itemize} \item To give a specific expression a more precise radix type, you use {\em redefinitions}. A functor can have many redefinitions that cause it to have different radix types depending on the types of its arguments. Here is an example of a redefinition taken from \verb|FINSET_1|. \begin{mizar} \verb|definition let E be set, let A,B be Subset of E;|\\ \verb| redefine func A U B -> Subset of E;|\\ \verb|end;| \end{mizar} It means that if \verb|A| and \verb|B| have type \verb|Subset| \verb|of| \verb|E| then \verb|A| \verb|U| \verb|B| has type \verb|Subset| \verb|of| \verb|E| instead of \verb|set|. See Section \ref{ref:lan:redefinitions} for a full discussion of redefinitions. Since the last defined redefinition that matches the types of the arguments is the one that is used, the order of the articles in the \verb|notation| directive is important! \item To generate more adjectives for an expression, Mizar has something called {\em clusters}. The process of adding adjectives according to these cluster definitions is called the {\em rounding up\/} of clusters. Here are examples of three kinds of clusters taken from \verb|FINSET_1|. \begin{mizar} \verb|definition|\\ \verb| cluster empty -> finite set;|\\ \verb|end;| \end{mizar} This means that every \verb|set| that has adjective \verb|empty| also will get adjective \verb|finite|. \begin{mizar} \verb|definition let X,Y be finite set;|\\ \verb| cluster X U Y -> finite;|\\ \verb|end;| \end{mizar} This means that every expression of the shape \verb|X| \verb|U| \verb|Y| where \verb|X| and \verb|Y| have type \verb|finite| \verb|set| also will get adjective \verb|finite|. \begin{mizar} \verb|definition let B be finite set;|\\ \verb| cluster -> finite Subset of B;|\\ \verb|end;| \end{mizar} This means that every expression that has type \verb|Subset| \verb|of| \verb|B| where \verb|B| has type \verb|finite| \verb|set| also will get adjective \verb|finite|. See Sections \ref{ref:lan:clusters:conditional} and \ref{ref:lan:clusters:functorial} for a full discussion of clusters. \end{itemize} So to summarize: redefinitions are for narrowing the radix type and clusters are for extending the set of adjectives. (There are also redefinitions that have nothing to do with typing, and clusters that have nothing to do with adding adjectives. You should not be confused by this.) You can always test whether some type ${\cal T}$ is in the set of types of an expression $t$ by changing it to \verb|(|$\,t\,$ \verb|qua| ${\cal T}$\verb|)|. You get an error if $t$ didn't have ${\cal T}$ in its set of types. In that case you might start looking for a redefinition or cluster that changes this situation. \begin{example} Here is the solution to the first typing error. We want to accomplish that the type \verb|Nat| widens to the type \verb|real| \verb|number|. Type \verb|Nat| expands to \verb|Element| \verb|of| \verb|omega|. Furthermore \verb|number| is equivalent to \verb|set| and all types widen to \verb|set|. The cluster from \verb|ARYTM_3|: \begin{mizar} \verb|definition|\\ \verb| cluster -> natural Element of omega;|\\ \verb|end;| \end{mizar} causes all expressions that have type \verb|Element| \verb|of| \verb|omega| to also get the adjective \verb|natural|. The cluster from \verb|ARYTM|: \begin{mizar} \verb|definition|\\ \verb| cluster natural -> real number;|\\ \verb|end;| \end{mizar} causes all expressions that have type \verb|natural number| to also get the adjective \verb|real|. So adding: \begin{mizar} \verb| clusters ARYTM_3, ARYTM;| \end{mizar} to the environment causes all expressions of type \verb|Nat| to also get type \verb|real| \verb|number|. This gets rid of the first error. \end{example} \subsection{The other directives} Here is a list of the eight kinds of directives in the \verb|environ| and the kind of reference they take: \begin{center} \begin{tabular}{ll} \verb|vocabulary| & {\em vocabulary\/}\\ \verb|notation| & {\em article\/}\\ \verb|constructors| & {\em article\/}\\ \verb|clusters| & {\em article\/}\\ \verb|definitions| & {\em article\/}\\ \verb|theorems| & {\em article\/}\\ \verb|schemes| & {\em article\/}\\ \verb|requirements| & \verb|SUBSET|, \verb|BOOLE|, \verb|ARYTM|, \verb|REAL| \end{tabular} \end{center} Here is when you need the last four kinds of directive: \begin{itemize} \item The \verb|definitions| directive is {\em not\/} about being able to use the theorems that are part of the definitions (that's part of the \verb|theorems| directive.) It's about automatically unfolding predicates in the thesis that you are proving. This directive is useful but not important. You can ignore it until you get up to speed with Mizar. \item The \verb|theorems| and \verb|schemes| directives list the articles you use theorems and schemes from. So whenever you refer to a theorem in a proof, you should check whether the article is in the list of this directive. These are easy directives to get right. \item The \verb|requirements| directive makes Mizar know appropriate things automatically. For instance to give numerals type \verb|Nat| you need \begin{mizar} \verb| requirements SUBSET, ARYTM;| \end{mizar} So this is the solution to the second typing error left in our article. With \verb|ARYTM| and \verb|REAL| Mizar knows some basic equations about numbers automatically. For instance with it, Mizar accepts \verb|1+1| \verb|=| \verb|2| without proof. This is an easy directive to get right. Just put in a requirement if you think it will help, and see what happens. \end{itemize} % So now that we got the environment right the article checks like this: \begin{mizar} \verb|environ|\\ \verb| vocabulary MY_MIZAR, REAL_1, INT_2, SQUARE, MATRIX2;|\\ \verb| notation ARYTM, REAL_1, NAT_1, INT_2, SQUARE_1, ABIAN;|\\ \verb| constructors ARYTM, REAL_1, NAT_1, INT_2, SQUARE_1, ABIAN;|\\ \verb| clusters ARYTM_3, ARYTM;|\\ \verb| requirements SUBSET, ARYTM;| \medskip\\ \verb|begin|\\ \verb| reserve a,b,c,m,n for Nat;| \medskip\\ \verb|a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2;|\\ \verb|::> *4|\\ \verb|::>|\\ \verb|::> 4: This inference is not accepted| \end{mizar} The only error left is \verb|*4|. It means that Mizar is not able to prove the statement on its own. This is an important milestone. Articles with only \verb|*4| errors are `almost finished'. They just need a bit of proof. \begin{exercise} Consider the nine types: \begin{verse} \verb|Element of NAT|\\ \verb|Element of INT|\\ \verb|Element of REAL|\\ \verb|Nat|\\ \verb|Integer|\\ \verb|Real|\\ \verb|natural number|\\ \verb|integer number|\\ \verb|real number| \end{verse} There are 45 pairs of different types ${\cal T}_1$ and ${\cal T}_2$ from this list for which the formula: \begin{mizar} \verb|for x being |${\cal T}_1$\verb| holds (x qua |${\cal T}_2$\verb|) = x;| \end{mizar} should be allowed. What is an environment that gives the minimum number of error messages \verb|*116| (meaning \verb|Invalid| \verb|"qua"|)? What is used from the articles in this environment? In particular explain why Mizar will allow: \begin{mizar} \verb|for x being Nat holds (x qua Real) = x;| \end{mizar} What are the redefinitions that make this work? \end{exercise} \begin{exercise} Apart from the kinds of cluster that we showed in Section \ref{tut:env:clusters} (the ones that generate extra adjectives for terms), Mizar has something called {\em existential clusters}. These are the clusters without \verb|->|. They don't generate extra adjectives for a term. Instead they are needed to be allowed to add adjectives to a type. The reason for this is that Mizar types always have to be non-empty. So to be allowed to use a type something has to be proved. That is what an existential cluster does. For example to be allowed to use the type: \begin{mizar} \verb|non empty finite Subset of NAT| \end{mizar} you needs an existential cluster from \verb|GROUP_2|: \begin{mizar} \verb|definition let X be non empty set;|\\ \verb| cluster finite non empty Subset of X;|\\ \verb|end;| \end{mizar} If you don't have the right existential clusters in your article you will get error \verb|*136| which means \verb|Non| \verb|registered| \verb|cluster|. Which types in the following list have an existential cluster in the MML? For the ones that have one, where did you find them? For the ones that don't have one, what would be an appropriate existential cluster? \begin{itemize} \item[] \verb|empty set| \item[] \verb|odd prime Nat| \item[] \verb|infinite Subset of REAL| \item[] \verb|non empty Relation of NAT,NAT| \end{itemize} \end{exercise} \section{Step 5, maybe: definitions and lemmas} Step 5 you can skip. Then you just start working on the proof of the theorem immediately. However if you did step 1 right, you probably have some lemmas that you know you will need. Or maybe you need to define some notions before being able to state your theorem at all. So do so in this step. Add relevant definitions and lemmas to your article now. Just like the statement in step 3. Without proof. Yet. \subsection{Functors, predicates} There are two ways to define a functor in Mizar: \begin{itemize} \item As an abbreviation: \begin{mizar} \verb|definition let x be Real;|\\ \verb| func x^2 -> Real equals x|$\,\cdot\,$\verb|x;|\\ \verb| coherence;|\\ \verb|end;| \end{mizar} The \verb|coherence| correctness condition is that the expression \verb|x|$\,\cdot\,$\verb|x| really has type \verb|Real| like it was claimed. If Mizar can't figure this out by itself you will have to prove it. \item By a characterization of the result: \begin{mizar} \verb|definition let x be Real;|\\ \verb| assume 0 <= x;|\\ \verb| func sqrt x -> Real means|\\ \verb| 0 <= it & it^2 = x;|\\ \verb| existence;|\\ \verb| uniqueness;|\\ \verb|end;| \end{mizar} In the characterizing statement the variable \verb|it| is the result of the functor. The \verb|existence| and \verb|uniqueness| are again correctness conditions. They state that there always exists a value that satisfies the defining property, and that this value is unique. (In the proof of them you are allowed to use that the assumption from the definition is satisfied.) In this case \verb|existence| is the statement: \begin{mizar} \verb|ex y being Real st 0 <= y & y^2 = x| \end{mizar} and \verb|uniqueness| is the statement: \begin{mizar} \verb|for y,y' being Real st|\\ \verb| 0 <= y & y^2 = x & 0 <= y' & y'^2 = x holds y = y'| \end{mizar} \end{itemize} % And here is an example of the way to define a predicate: \begin{itemize} \item \begin{mizar} \verb|definition let m,n be Nat;|\\ \verb| pred m,n are_relative_prime means|\\ \verb| m hcf n = 1;|\\ \verb|end;| \end{mizar} The definition of a predicate doesn't have a correctness condition. (In this example \verb|hcf| is the greatest common divisor.) \end{itemize} \subsection{Modes and attributes} There are two ways to define a mode in Mizar: \begin{itemize} \item As an abbreviation: \begin{mizar} \verb|definition let X,Y be set;|\\ \verb| mode Function of X,Y is|\\ \verb| quasi_total Function-like Relation of X,Y;|\\ \verb|end;| \end{mizar} In this definition \verb|quasi_total| and \verb|Function-like| are attributes. \item By a characterization of its elements. \begin{mizar} \verb|definition|\\ \verb| let X,Y be set;|\\ \verb| mode Relation of X,Y means|\\ \verb| it c= [:X,Y:];|\\ \verb| existence;|\\ \verb|end;| \end{mizar} The \verb|existence| correctness condition states that the mode is inhabited. This has to be the case because Mizar's logic wants all Mizar types to be non-empty. In this case \verb|existence| is the statement: \begin{mizar} \verb|ex R st R c= [:X,Y:]|\\ \end{mizar} \end{itemize} % And here is an example of the way to define an attribute: \begin{itemize} \item \begin{mizar} \verb|definition let n be number;|\\ \verb| attr n is square means|\\ \verb| ex m being Nat st n = m^2;|\\ \verb|end;| \end{mizar} \end{itemize} % If your symbol is not already in one of the MML vocabularies you need to put it in your own vocabulary. It should be on a line of its own with \verb|O| in front for functors, \verb|R| in front for predicates, \verb|M| in front for modes or \verb|V| in front for attributes. For instance you might add the line: \begin{mizar} \verb|Vsquare| \end{mizar} to the \verb|MY_MIZAR.VOC| file. You can run: \begin{mizar} \verb|listvoc |{\em vocabulary} \end{mizar} to look at vocabularies from the MML. \begin{example} The essential lemma for the example is that if two numbers are relative prime and their product is a square, then they are squares themselves. In Mizar syntax this is the statement: \begin{mizar} \verb|m|$\,\cdot\,$\verb|n is square & m,n are_relative_prime implies|\\ \verb| m is square & n is square| \end{mizar} A Mizar article is a sequence of definitions and statements. Definitions are always public, but statements can only be referred to from the outside of the article when they're preceded by the keyword \verb|theorem|. So change the body of the article to: \begin{mizar} \verb|theorem Th1:|\\ \verb| m|$\,\cdot\,$\verb|n is square & m,n are_relative_prime implies|\\ \verb| m is square & n is square;|\\ \verb|::> *4,4| \medskip\\ \verb|theorem Th2:|\\ \verb| a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2;|\\ \verb|::> *4|\\ \verb|::>|\\ \verb|::> 4: This inference is not accepted| \end{mizar} \end{example} \begin{exercise} We claimed that Mizar's types are always non-empty. However you can write the type: \begin{mizar} \verb|Element of {}| \end{mizar} Explain why this is not a problem. \end{exercise} \section{Step 6: proof skeleton} Mizar is a block structured language like the Pascal programming language. Instead of \verb|begin|/\verb|end| blocks it has \verb|proof|/\verb|end| blocks. And instead of procedures it has theorems. Apart from that it is a rather similar language. We will now write the proof of the theorem. For the moment we just write the steps and not link them together. Linking the steps in the proof will be step 7 of the nine easy steps. A Mizar proof begins with the keyword \verb|proof| and ends with the keyword \verb|end|. Important! If you have a proof after a statement there should not be a semicolon after the statement. So: \begin{mizar} {\em statement\/}\verb| |\framebox{{\tt ;}}\\ \verb|proof|\\ \verb| |{\em proof steps\/}\\ \verb|end;| \end{mizar} is wrong! It should be: \begin{mizar} {\em statement\/}\\ \verb|proof|\\ \verb| |{\em proof steps\/}\\ \verb|end;| \end{mizar} This is easy to do wrong. Then you will get a \verb|*4| error at the semicolon that shouldn't be there. In this section we will discuss the following kinds of proof step. There are some more but these are the frequently used ones: \begin{center} \begin{tabular}{cc} {\em step\/} & {\em section}\\ \noalign{\smallskip} {\em compact\/} & \ref{tut:skel:other}\\ \verb|assume| & \ref{tut:skel:skel}\\ \verb|thus| & \ref{tut:skel:skel}\\ \verb|let| & \ref{tut:skel:skel}\\ \verb|take| & \ref{tut:skel:skel}\\ \verb|consider| & \ref{tut:skel:other}\\ \verb|per cases|/\verb|suppose| & \ref{tut:skel:other}\\ \verb|set| & \ref{tut:skel:abbr}\\ \verb|reconsider| & \ref{tut:skel:abbr}\\ {\em iterative equality\/} & \ref{tut:skel:iter} \end{tabular} \end{center} \subsection{Skeleton steps}\label{tut:skel:skel} During the steps of the proof the statement that needs to be proved is kept track of. This is the `goal' of the proof. It is called the {\em thesis} and can be referred to with the keyword \verb|thesis|. A Mizar proof consists of steps. Steps contain statements that you know to be true in the given context. Some of the steps reduce the thesis. At the \verb|end| of the proof the thesis should be reduced to $\top$ or else you will get error \verb|*70| meaning \verb|Something| \verb|remains| \verb|to| \verb|be| \verb|proved|. Steps that change the thesis are called {\em skeleton steps}. The four basic skeleton steps are \verb|assume|, \verb|thus|, \verb|let| and \verb|take|. They correspond to the shape of the thesis in the following way: \begin{center} \begin{tabular}{lll} {\em thesis to be proved, before\/} & {\em the step\/} & {\em thesis to be proved, after\/}\\ \noalign{\smallskip} $\phi$\verb| implies |$\psi$ & \verb|assume |$\phi$\verb|| & $\psi$\\ $\phi$\verb| & |$\psi$ & \verb|thus |$\phi$\verb|| & $\psi$\\ \verb|for x being |${\cal T}$\verb| holds |$\psi$ & \verb|let x be |${\cal T}$\verb|| & $\psi$\\ \verb|ex x being |${\cal T}$\verb| st |$\psi$ & \verb|take |$t$\verb|| & $\psi[\verb|x|:=t]$ \end{tabular} \end{center} Just like with \verb|for| the typing can be left out of the \verb|let| if the variable is in a \verb|reserve| statement. Here is an example of how these skeleton steps work in a very simple proof: \begin{mizar} \verb|for x,y st x = y holds y = x|\\ \verb|proof|\\ \verb| let x,y;|\\ \verb| assume x = y;|\\ \verb| thus y = x;|\\ \verb|end;| \end{mizar} At the start of the proof the thesis is \verb|for| \verb|x,y| \verb|st| \verb|x| \verb|=| \verb|y| \verb|holds| \verb|y| \verb|= x|. After the \verb|let| step it is reduced to \verb|x| \verb|=| \verb|y| \verb|implies| \verb|y| \verb|=| \verb|x|. After the \verb|assume| step it is reduced to \verb|y| \verb|=| \verb|x|. After the \verb|thus| step it is reduced to $\top$ and the proof is complete. The skeleton steps of the proof of the example will be: \begin{mizar} \verb|theorem Th2:|\\ \verb| a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2|\\ \verb|proof|\\ \verb| assume a^2 + b^2 = c^2;|\\ \verb| assume a,b are_relative_prime;|\\ \verb| assume a is odd;|\\ \verb| take |$m$\verb|,|$n$\verb|;|\\ \verb| thus |$m$\verb| <= |$n$\verb|;|\\ \verb| thus a = |$n$\verb|^2 - |$m$\verb|^2;|\\ \verb| thus b = 2|$\,\cdot\,m\,\cdot\,n$\verb|;|\\ \verb| thus c = |$n$\verb|^2 + |$m$\verb|^2;|\\ \verb|end;| \end{mizar} At this point we don't have anything to put in the place of the $m$ and $n$. We need another kind of step for that. \begin{exercise} Explain why you can always end a proof with a \verb|thus| \verb|thesis| step. This is the Mizar version of {\sc quod erat demonstrandum}. Count in the MML how many times this construction occurs. (Include in your count \verb|hence| \verb|thesis| which is the same thing.) Is there an occurence of \verb|thesis| in the MML which is {\em not\/} part of this construction? \end{exercise} \begin{exercise} Write the skeleton steps in the proofs for the following Mizar statements: \begin{itemize} \item[] \verb|x = 0 & y = 0 implies x + y = 0 & x|$\,\cdot\,$\verb|y = 0| \item[] \verb|ex x st x in X implies for y holds y in X| \item[] \verb|for n st not ex m st n = 2|$\,\cdot\,$\verb|m holds ex m st n = 2|$\,\cdot\,$\verb|m + 1| \item[] \verb|(ex n st n in X) implies|\hfill\break \verb| ex n st n in X & for m st m < n holds not m in X| \end{itemize} Write a fresh variable in the \verb|take| steps if there is no good choice for the term. \end{exercise} \subsection{Compact statements and elimination}\label{tut:skel:other} The simplest step is a {\em compact\/} step. This is just a statement that is true in the current context. This is the most common step in a Mizar proof. And these are the \verb|consider| and \verb|per cases|/\verb|suppose| constructions. They are both related to a statement: \begin{center} \begin{tabular}{rcl} {\em if you can prove this\/} & {\dots} & {\em you can have this as a proof step\/}\\ \noalign{\smallskip} \verb|ex x st |$\phi$ && \verb|consider x such that |$\phi$\verb|;|\\ \noalign{\smallskip} $\phi_1$\verb| or |$\phi_2$\verb| or |\dots\verb| or |$\phi_n$ && \verb|per cases;|\\ && \verb|suppose |$\phi_1$\verb|;| \\ && \verb| |{\em proof for the case $\phi_1$\/} \\ && \verb|suppose |$\phi_2$\verb|;| \\ && \verb| |{\em proof for the case $\phi_2$\/} \\ && \verb||\dots \\ && \verb|suppose |$\phi_n$\verb|;| \\ && \verb| |{\em proof for the case $\phi_n$\/} \end{tabular} \end{center} To use natural deduction terminology, these steps correspond to existential and disjuction {\em elimination}. The \verb|consider| step introduces a variable that you can refer to in your proof, just like the \verb|let| step. We can now add the following steps to the example proof to give us terms \verb|m| and \verb|n| for the \verb|take| step: \begin{mizar} \verb| |\dots\\ \verb| ((c - a)/2)|$\,\cdot\,$\verb|((c + a)/2) = (b/2)^2;|\\ \verb| ((c - a)/2)|$\,\cdot\,$\verb|((c + a)/2) is square;|\\ \verb| (c - a)/2,(c + a)/2 are_relative_prime;|\\ \verb| (c - a)/2 is square & (c + a)/2 is square;|\\ \verb| consider m such that (c - a)/2 = m^2;|\\ \verb| consider n such that (c + a)/2 = n^2;|\\ \verb| take m,n;|\\ \verb| |\dots \end{mizar} The first four steps are compact statements. The two \verb|consider| steps use the existential statement that's part of the definition of \verb|square|. \subsection{Macros and casts}\label{tut:skel:abbr} Often in proofs certain expressions occur many times. It is possible to give such expressions a name using \verb|set| commands: \begin{mizar} \verb| set h = b/2;|\\ \verb| set m2 = (c - a)/2;|\\ \verb| set n2 = (c + a)/2;| \end{mizar} A \verb|set| command is a definition of a constant that is local to the proof. It behaves very much like a {\em macro}. When writing Mizar articles, often you want to use an expression with a different type than it's got. You can change the type of an expression with the \verb|reconsider| command. This is like a \verb|set|, but also gives the type of the new variable. In the example we will need the abbreviated variables \verb|h|, \verb|m2| and \verb|n2| to have type \verb|Nat|. This can be accomplished by changing the \verb|set| lines in the previous paragraph to: \begin{mizar} \verb| reconsider h = b/2 as Nat;|\\ \verb| reconsider m2 = (c - a)/2 as Nat;|\\ \verb| reconsider n2 = (c + a)/2 as Nat;| \end{mizar} Again the new variables behave like macros, but now with a different type. So \verb|reconsider| is a way to {\em cast\/} the type of a term. \subsection{Iterative equalities}\label{tut:skel:iter} In mathematical calculations one often has a chain of equalities. Mizar has this feature too. You can write a calculation: $$ \Big({c - a\over 2}\Big)\Big({c + a\over 2}\Big) = {(c - a)(c + a)\over 4} = {c^2 - a^2\over 4} = {b^2\over 4} = \Big({b\over 2}\Big)^2$$ in Mizar as: \begin{mizar} \verb| ((c - a)/2)|$\,\cdot\,$\verb|((c + a)/2) = (c - a)|$\,\cdot\,$\verb|(c + a)/4|\\ \verb| .= (c^2 - a^2)/4|\\ \verb| .= b^2/4|\\ \verb| .= (b/2)^2;| \end{mizar} Such a chain of \verb|.=| equalities is called an {\em iterative equality}. Note that the first equality in the chain is written with the \verb|=| symbol instead of with the \verb|.=| symbol. \begin{exercise}\label{tut:skel:exercise:th2} Collect the steps for the proof of \verb|Th2| that were given in this section. Put them in the proper order in your \verb|MY_MIZAR.MIZ| file. Use the \verb|reconsider| lines (not the \verb|set| lines) and replace the abbreviated expressions everywhere by their abbreviation. Put in the iterated equality as well. Add two compact statements before the \verb|reconsider| lines stating that \verb|b| is even and that \verb|c| is odd. They will be needed to justify the \verb|reconsider| lines. Add two compact statements relating \verb|m2| and \verb|n2| to \verb|a| and \verb|c| after the \verb|reconsider| lines. Now check your file with \verb|mizf|. Update the environment if necessary until you have only \verb|*4| errors left. How many \verb|*4| errors do you get? \end{exercise} \section{Step 7: completing the proof} In this section you will add justifications to the steps of your proof. That will finish your article. \subsection{Getting rid of the {\tt *4} errors} There are three ways to justify a step in Mizar: \begin{itemize} \item By putting a semicolon \verb|;| after it: \begin{mizar} {\em statement}\verb| |\framebox{{\tt ;}} \end{mizar} This is the empty justification. It tells Mizar: {\em figure this out by yourself.} \item By putting \verb|by| after it with a list of labels of previous statements: \begin{mizar} {\em statement}\verb| |\framebox{{\tt by }{\em reference}$\,${\tt ,}$\;$\dots$\,${\tt ,}$\,${\em reference}$\,${\tt ;}} \end{mizar} In fact the previous way to justify a step is the special case of this in which the list of references is empty. \item By putting a subproof after it: \begin{mizar} {\em statement}\verb| |% \framebox{% {\tt proof} {\tt \ }{\em steps in the subproof\/}{\tt \ } {\tt end;}} \end{mizar} The subproofs are what gives Mizar proofs the block structured look. If you don't use \verb|thesis| in the subproof, the statement can be reconstructed from the steps. Therefore you might want to omit the statement. You can do this by using \verb|now|: \begin{mizar} \framebox{% {\tt now} {\tt \ }{\em steps in the subproof\/}{\tt \ } {\tt end;}} \end{mizar} This is exactly the same as the statement with the subproof, but you don't need to write the statement. \end {itemize} Here is a small example that shows how \verb|by| is used: \begin{mizar} \verb|(x in X implies x in Y) & x in X implies x in Y|\\ \verb|proof|\\ \verb| assume|\\ \verb|A1: x in X implies x in Y;|\\ \verb| assume|\\ \verb|A2: x in X;|\\ \verb| thus x in Y |\framebox{{\tt by A1,A2;}}\\ \verb|end;| \end{mizar} Of course this one is so easy that Mizar can do it on its own: \begin{mizar} \verb|(x in X implies x in Y) & x in X implies x in Y |\framebox{{\tt ;}} \end{mizar} % Often in the list of references after a \verb|by| justification, there is a reference to the previous statement. This can also be written by putting \verb|then| in front of the step. Using \verb|then| you can often avoid having to label statements. So you can replace: \begin{mizar} \verb|A1: |{\em statement\/}\verb|;|\\ \verb|A2: |{\em statement\/}\verb|;|\\ \verb| |{\em statement\/}\verb| by A1,A2:| \end{mizar} by \begin{mizar} \verb|A1: |{\em statement\/}\verb|;|\\ \verb| |{\em statement\/}\verb|;|\\ \verb| then |{\em statement\/}\verb| by A1;| \end{mizar} Some people like writing the \verb|then| on the previous line, after the statement that it refers to: \begin{mizar} \verb|A1: |{\em statement\/}\verb|;|\\ \verb| |{\em statement\/}\verb|; then|\\ \verb| |{\em statement\/}\verb| by A1;| \end{mizar} This is a matter of taste. Other people choose the position of the \verb|then| depending on whether the statement after the \verb|then| has a label or not. When you want to use \verb|then| to justify a \verb|thus| step you are not allowed to write \verb|then| \verb|thus|. You have to write \verb|hence|. In Mizar when in certain combinations of two keyword get together you have to replace the combination by something else. Here are the two relevant equations: $$ \begin{array}{ccccl} \verb|then| &+& \verb|thus| &=& \verb|hence|\\ \verb|thus| &+& \verb|now| &=& \verb|hereby| \end{array} $$ So the \verb|hence| keyword means two things: \begin{enumerate} \item This follows from the previous step. \item This is part of what was to be proved. \end{enumerate} A common Mizar idiom is \verb|hence| \verb|thesis|. You see that many times in any Mizar article. \subsection{Properties and requirements} So now you need to hunt the MML for relevant theorems. This is made difficult by three reasons: \begin{itemize} \item The MML is big. \item The MML is not ordered systematically but chronologically. It is like a mediaeval library in which the books are put on the shelf in the order that they have been acquired. \item Mizar is smart. The theorem you can use might not look very much like the theorem you are looking for. \end{itemize} As an example of the fact that theorems can be in unexpected places, the basic theorem that relates the two kinds of dividability that are in the Mizar libary: \begin{mizar} \verb|m|$\,|\,$\verb|n iff m|$\,|\,$\verb|(n qua Integer);| \end{mizar} is in an article called \verb|SCPINVAR| which is about loop invariants of a certain small computer program (SCP stands for SCMPDS program and SCMPDS stands for small computer model with push-down stack). The best way to find theorems in the MML is by using the \verb|grep| command to search all the \verb|.ABS| abstract files. Although the MML is huge it's small enough for this to be practical. For instance this is an appropriate command to search for the theorem in the \verb|SCPINVAR| article: \begin{mizar} \verb|% grep '|$\,|\,$\verb| qua ' *.ABS|\\ \verb|INT_2.ABS: a|$\,|\,$\verb|b iff (abs(a))|$\,|\,$\verb|(abs(b) qua Nat);|\\ \verb|SCPINVAR.ABS: m|$\,|\,$\verb|n iff m|$\,|\,$\verb|(n qua Integer);|\\ \verb|% | \end{mizar} % And another problem when looking for theorems is that Mizar is too smart. If you look at the definitions of \verb|+|, $\,\cdot\,$ and \verb|<=| you will find that they contain the keywords \verb|commutativity|, \verb|reflexivity|, \verb|connectedness|, \verb|synonym| and \verb|antonym|: \begin{mizar} \verb|definition let x,y be real number;|\\ \verb| func x + y means|\\ \verb|:: ARYTM:def 3|\\ \verb| |\dots\\ \verb| commutativity;| \medskip\\ \verb| func x|$\,\cdot\,$\verb|y means|\\ \verb|:: ARYTM:def 4|\\ \verb| |\dots\\ \verb| commutativity;| \medskip\\ \verb| pred x <= y means|\\ \verb|:: ARYTM:def 5|\\ \verb| |\dots\\ \verb| reflexivity;|\\ \verb| connectedness;|\\ \verb| synonym y >= x;|\\ \verb| antonym y < x;|\\ \verb| antonym x > y;|\\ \verb|end;| \end{mizar} These keywords mean two things: \begin{itemize} \item If you use a \verb|synonym| or \verb|antonym| then Mizar will internally use the real name. So if you write: \begin{mizar} \verb|a < b| \end{mizar} then internally Mizar will consider this to be an abbreviation of: \begin{mizar} \verb|not b <= a| \end{mizar} and if you write: \begin{mizar} \verb|a >= b| \end{mizar} then internally Mizar will consider this to mean: \begin{mizar} \verb|b <= a| \end{mizar} \item Mizar will always `know' when justifying a step, about the properties \verb|commutativity|, \verb|reflexivity| and \verb|connectedness|. So if you have a statement: \begin{mizar} \dots\verb| x|$\,\cdot\,$\verb|y |\dots \end{mizar} then Mizar behaves as if this statement is exactly the same as: \begin{mizar} \dots\verb| y|$\,\cdot\,$\verb|x |\dots \end{mizar} Also Mizar will use all implication of the shape: $$x = y \Rightarrow x\le y$$ and: $$x\le y \mathrel{\lor} y\le x$$ when trying to do a justification. These properties mean for the $<$ relation that: $$\neg(x < x)$$ and: $$x < y \Rightarrow x\le y$$ For instance if you have proved: \begin{mizar} \verb|a < b| \end{mizar} then you can refer to this when you only need: \begin{mizar} \verb|a <> b| \end{mizar} \end{itemize} This is all very nice but let's look at three examples of the subtlety it leads to: \begin{itemize} \item Suppose you want to justify the following step: \begin{mizar} \verb| a >= 0;|\\ \verb| then c - a <= c by |\dots\thinspace\verb|;| \end{mizar} It turns out that the theorem that you need is: \begin{mizar} \verb|theorem :: REAL_2:173|\\ \verb| (a<0 implies a+bb) & (a+bb implies a<0);| \end{mizar} It will give you: \begin{mizar} \verb|c - a > c implies a < 0| \end{mizar} but because of the \verb|antonym| definition of \verb|<| and \verb|>| this really means: \begin{mizar} \verb|not c - a <= c implies not 0 <= a| \end{mizar} which is equivalent to: \begin{mizar} \verb|0 <= a implies c - a <= c| \end{mizar} Which is what you need. \item Suppose you need to prove the equation: \begin{mizar} \verb|(c + a + c - a)/2 = (c + c + a - a)/2| \end{mizar} The \verb|+| and \verb|-| operators have the same priority and are left associative, so this has to be read as: \begin{mizar} \verb|(((c + a) + c) - a)/2 = (((c + c) + a) - a)/2| \end{mizar} Because of \verb|commutativity| of \verb|+| this really is the same as: \begin{mizar} \verb|((c + (c + a)) - a)/2 = (((c + c) + a) - a)/2| \end{mizar} So you need to show that: \verb|c + (c + a) = (c + c) + a| which is associativity of \verb|+|, a theorem from the \verb|AXIOMS| article: \begin{mizar} \verb|theorem :: AXIOMS:13|\\ \verb| x + (y + z) = (x + y) + z;| \end{mizar} Note that the original equation doesn't look very much like an instance of associativity! \item Consider the transitive law for \verb|<=|: \begin{mizar} \verb|theorem :: AXIOMS:22|\\ \verb| x <= y & y <= z implies x <= z;| \end{mizar} It's good to have this, but where is the analogous law for \verb|<|: \begin{mizar} \verb|x < y & y < z implies x < z;| \end{mizar} It turns out that this also is \verb|AXIOMS:22|! To see why this is the case, note that it is a consequence of the stronger theorem: \begin{mizar} \verb|x <= y & y < z implies x < z;| \end{mizar} and becase of the \verb|antonym| definition of \verb|<| this is the same as: \begin{mizar} \verb|x <= y & not z <= y implies not z <= x;| \end{mizar} which is equivalent to: \begin{mizar} \verb|z <= x & x <= y implies z <= y;| \end{mizar} which is indeed \verb|AXIOMS:22|. \end{itemize} (The `arithmetical lemmas' for the arithmetical operations that we have used as examples here all are in the three articles \verb|AXIOMS|, \verb|REAL_1| and \verb|REAL_2|. Unfortunately you will often have to look in all three. There is not an easy rule that will tell you what is where.) Sometimes you should not go look for a theorem. If you have \verb|requirements| \verb|ARYTM| then Mizar knows many facts about the natural numbers without help. Sometimes those facts even don't have a \verb|theorem| in the library anymore, so you search for a long time if you don't realize that you should use \verb|requirements|. For instance if you use \verb|requirements| \verb|ARYTM|: \begin{mizar} \verb|x + 0 = x;| \end{mizar} and: \begin{mizar} \verb|0|$\,\cdot\,$\verb|x = 0;| \end{mizar} and: \begin{mizar} \verb|1|$\,\cdot\,$\verb|x = x;| \end{mizar} and: \begin{mizar} \verb|0 < 1;| \end{mizar} and: \begin{mizar} \verb|0 <> 1;| \end{mizar} all don't need any justification. Suppose you want to justify: \begin{mizar} \verb| a >= 1;|\\ \verb| then a > 0 by |\dots\thinspace\verb|;| \end{mizar} If you had \verb|0| \verb|<| \verb|1| then this would just be an instance of \verb|AXIOMS:22| (as we just saw). But \verb|requirements| \verb|ARYTM| gives that to you for free! So you can just justify this step with \verb|AXIOMS:22|. \begin{exercise} We claim that the MML is big. Count how many source lines there are in the \verb|.MIZ| articles in the MML. Try to guess how many lines of Mizar a competent Mizar author writes per day and then estimate the number of man-years that are in the MML. \end{exercise} \subsection{Automation in Mizar} In Mizar it's not possible to write {\em tactics\/} to automate part of your proof effort like you can do in other proof checkers. All Mizar's automation is built into the Mizar system by its developers. Mizar has four kinds of automation: \paragraph{Semantic correlates} Internally Mizar stores its formulas in some kind of conjunctive normal form that only uses $\land$, $\neg$ and $\forall$. This means that it automatically identifies some equivalent formulas. These equivalence classes of formulas are called {\em semantic correlates}. Because of semantic correlates, the skeleton steps of a formula are more powerful than you might expect. For instance you can prove: \begin{mizar} $\phi$\\ \verb|proof|\\ \verb| assume not |$\phi$\verb|;|\\ \verb| |\dots\\ \verb| thus contradiction;|\\ \verb|end;| \end{mizar} and also you can prove: \begin{mizar} $\phi$\verb| or |$\psi$\\ \verb|proof|\\ \verb| assume not |$\phi$\verb|;|\\ \verb| |\dots\\ \verb| thus |$\psi$\verb|;|\\ \verb|end;| \end{mizar} (Mizar does not identify $\phi$ \verb|&| $\psi$ with $\psi$ \verb|&| $\phi$. You have to put the \verb|thus| steps in a proof in the same order as the conjuncts appear in the thesis.) \paragraph{Properties and requirements} Properties and requirements were discussed in the previous section. \paragraph{Clusters} Clusters automatically generate adjectives for expressions. Often theorems can be rephrased as clusters, after which they will become automatic. Consider for instance the theorem: \begin{mizar} \verb|m is odd square & n is odd square implies m + n is non square;| \end{mizar} which says that a square can never be the sum of two odd squares. (The reason for this is that odd squares are always 1 modulo 4, so the sum would be 2 modulo 4, but an even square is always 0 modulo 4.) This theorem can be rephrased as a cluster: \begin{mizar} \verb|definition let m,n be odd square Nat;|\\ \verb| cluster m + n -> non square;|\\ \verb|end;| \end{mizar} Once you have proved this cluster Mizar will apply the theorem automatically when appropriate and you don't have to give a reference to it in your proofs. \paragraph{Justification using {\tt by}} The \verb|by| justifier is a weak first order prover. It tries to deduce the statement in front of the \verb|by| from the statements that are referred to after the \verb|by|. A \verb|by| justification pretty much feels like a `natural reasoning step'. When one studies the proofs that humans write, it turns out that they tend to choose slightly smaller steps than \verb|by| can do. The way \verb|by| works is: \begin{itemize} \item It puts the implication that it has to prove in conjunctive normal form. Then it tries to do each conjunct separately. That's why you often get more than one \verb|*4| error for a failed justification. Mizar puts in an error for every conjunct that has not been justified. \item It then tries to prove the inference. In only {\em one\/} of the antecedents can a universal quantifier be instantiated. Therefore: \begin{mizar} \verb|A1: for x holds x in X;|\\ \verb|A2: for x holds not x in X;|\\ \verb| contradiction by A1,A2;| \end{mizar} won't work because it both has to instantiate the \verb|for| in \verb|A1| and \verb|A2|. You will need to split this into: \begin{mizar} \verb|A1: for x holds x in X;|\\ \verb|A2: for x holds not x in X;|\\ \verb| a in X by A1;|\\ \verb| then contradiction by A2;| \end{mizar} \item The \verb|by| prover will do congruence closure of all the equalities that it knows. It also will combine the typing information of equal terms. \item A conclusion that has an existential quantifier is equivalent to an antecedent that has a universal quantifier. Therefore \verb|by| is able to derive existential statements from instantiations of it. \end{itemize} \subsection{Unfolding of definitions} Here is a table that shows when Mizar will unfold definitions: \begin{center} \begin{tabular}{llc} \verb|func|/\verb|equals| & $-$\\ \verb|func|/\verb|means| & $-$\\ \verb|pred|/\verb|means| & $\,\diamond$\\ \verb|mode|/\verb|is| & $+$\\ \verb|mode|/\verb|means| & $\,\diamond$\\ \verb|attr|/\verb|means| & $\,\diamond$\\ \verb|set| & $+$ \end{tabular} \end{center} The items in this table that have a $+$ behave like macros. For instance the definition of \verb|Nat| is: \begin{mizar} \verb|definition|\\ \verb| mode Nat is Element of NAT;|\\ \verb|end;| \end{mizar} If you write \verb|Nat| it's exactly like writing \verb|Element| \verb|of| \verb|NAT|. So theorems about the \verb|Element| mode will automatically apply to \verb|Nat|. The items in the table that have a $-$ will never be expanded. All you get is a definitional theorem about the notion. You will need to refer to this theorem if you want to use the definition. The items in the table that have a $\,\diamond\,$ will be expanded if you use the \verb|definitions| directive. Expansion only happens in the thesis. It takes place if a skeleton step is attempted that disagrees with the shape of the thesis. For instance the definition of \verb|c=| is: \begin{mizar} \verb|definition let X,Y;|\\ \verb| pred X c= Y means|\\ \verb|:: TARSKI:def 3|\\ \verb| x in X implies x in Y;|\\ \verb| reflexivity;|\\ \verb|end;| \end{mizar} If you have \verb|TARSKI| in your \verb|definitions| you can prove set inclusion as follows: \begin{mizar} \verb|X c= Y|\\ \verb|proof|\\ \verb| let x be set;|\\ \verb| assume x in X;|\\ \verb| |\dots\\ \verb| thus x in Y;|\\ \verb|end;| \end{mizar} Similarly consider the definition of equality in \verb|BOOLE|: \begin{mizar} \verb|definition let X,Y;|\\ \verb| redefine pred X = Y means|\\ \verb|:: BOOLE:def 8|\\ \verb| X c= Y & Y c= X;|\\ \verb|end;| \end{mizar} If you add \verb|BOOLE| to your \verb|definitions| it will allow you to prove: \begin{mizar} \verb|X = Y|\\ \verb|proof|\\ \verb| |\dots\\ \verb| thus X c= Y;|\\ \verb| |\dots\\ \verb| thus Y c= X;|\\ \verb|end;| \end{mizar} or even: \begin{mizar} \verb|X = Y|\\ \verb|proof|\\ \verb| hereby|\\ \verb| let x be set;|\\ \verb| assume x in X;|\\ \verb| |\dots\\ \verb| thus x in Y;|\\ \verb| end;|\\ \verb| let x be set;|\\ \verb| assume x in Y;|\\ \verb| |\dots\\ \verb| thus x in X;|\\ \verb|end;| \end{mizar} \begin{exercise}\label{tut:just:exercise:drinker} Take the following skeleton proof of the {\em the drinker's principle}. Add labels to the statements and put in justifications for all the steps: \begin{mizar} \verb|ex x st x in X implies for y holds y in X|\\ \verb|proof|\\ \verb| per cases;|\\ \verb| suppose ex x st not x in X;|\\ \verb| consider x such that not x in X;|\\ \verb| take x;|\\ \verb| assume x in X;|\\ \verb| contradiction;|\\ \verb| let y;|\\ \verb| thus y in X;|\\ \verb| suppose not ex x st not x in X;|\\ \verb| for x holds x in X;|\\ \verb| assume x in X;|\\ \verb| thus thesis;|\\ \verb|end;| \end{mizar} Experiment with other proofs of the same statement. If you know constructive logic: write a Mizar proof of this statement that shows where the non-constructive steps in the proof are. \end{exercise} \begin{exercise} Write a proof of the following statement: \begin{mizar} \verb|(ex x st x in X implies y in Y) & (ex x st y in Y implies x in X)|\\ \verb| iff (ex x st x in X iff y in Y);| \end{mizar} Can you think of a proof that doesn't need \verb|per| \verb|cases|? \end{exercise} \begin{exercise}\label{tut:just:exercise:th2} Finish the proof of \verb|Th2|. Add as many clusters and lemmas as you need. For instance you might use: \begin{mizar} \verb|Lm1: m is odd square & n is odd square implies|\\ \verb| m + n is non square;|\\ \verb|Lm2: n is even iff n/2 is Nat;|\\ \verb|Lm3: m,n are_relative_prime iff|\\ \verb| for p being prime Nat holds not (p|$\,|\,$\verb|m & p|$\,|\,$\verb|n);|\\ \verb|Lm4: m^2 = n^2 iff m = n;| \end{mizar} but if you choose to use different lemmas that's fine too. Just put them before the theorem (you can prove them later if you like). If you don't think a lemma will be useful to others you don't have to put \verb|theorem| in front of it. Now add compact statements and justifications to the proof of \verb|Th2| until all the \verb|*4| errors are gone. \end{exercise} \section{Step 8: cleaning the proof} Now that you finished your article the fun starts! Mizar has several utilities to help you improve your article. These utilities will point out to you what is in your article that is not necessary. Those utilities don't put their error messages inside your file on their own. You need to use the program called \verb|errflag| after running them to accomplish that. \paragraph{{\tt relprem}} This program points out references in a \verb|by| justifications -- as well occurrences of \verb|then| -- that are not necessary. These references can be safely removed from your article. This program also points out the real errors in the article. Some people prefer to always use \verb|relprem| instead of \verb|mizf|. \paragraph{{\tt relinfer}} This program points out steps in the proof that are not necessary. It will indicate references to statements that can be short-circuited. You can omit such a reference and replace it with the references from the step that it referred to. As an example of {\tt relinfer} consider the following part of a proof: \begin{mizar} \verb|A1: m2|$\,\cdot\,$\verb|n2 = h^2 by |\dots\verb|;|\\ \verb|A2: m2|$\,\cdot\,$\verb|n2 is square by A1;|\\ \verb|A3: m2,n2 are_relative_prime by |\dots\verb|;|\\ \verb|A4: m2 is square & n2 is square by A2,A3,Th1;|\\ \verb| consider m such that m2 = m^2 by A4;|\\ \verb| |\dots \end{mizar} If you run: \begin{mizar} \verb|relinfer text\my_mizar|\\ \verb|errflag text\my_mizar| \end{mizar} then you will get \verb|*604| meaning \verb|Irrelevant| \verb|inference|: \begin{mizar} \verb|A1: m2|$\,\cdot\,$\verb|n2 = h^2 by |\dots\verb|;|\\ \verb|A2: m2|$\,\cdot\,$\verb|n2 is square by A1;|\\ \verb|A3: m2,n2 are_relative_prime by |\dots\verb|;|\\ \verb|A4: m2 is square & n2 is square by A2,A3,Th1;|\\ \verb|::> *604|\\ \verb| consider m such that m2 = m^2 by A4;|\\ \verb| |\dots \end{mizar} It means that you can replace the reference to \verb|A2| in step \verb|A4| with the references in the justification of \verb|A2| itself. In this case that's \verb|A1|. So the proof can be shortened to: \begin{mizar} \verb|A1: m2|$\,\cdot\,$\verb|n2 = h^2 by |\dots\verb|;|\\ \verb|A3: m2,n2 are_relative_prime by |\dots\verb|;|\\ \verb|A4: m2 is square & n2 is square by A1,A3,Th1;|\\ \verb| consider m such that m2 = m^2 by A4;|\\ \verb| |\dots \end{mizar} % Please take note that the \verb|relinfer| program is dangerous! Not because your proofs will break but because they might become ugly. \verb|relinfer| encourages you to cut steps that a human might want to see. \paragraph{{\tt reliters} {\rm (pronounced {\em rel-iters}, not {\em re-liters\/})}} This program points out steps in an interative equality that can be skipped. If you omit such a step you have to add its references to the references of the next one. As an example of {\tt reliters} consider the following iterative equality: \begin{mizar} \verb| m2|$\,\cdot\,$\verb|n2 = (c - a)|$\,\cdot\,$\verb|(c + a)/(2|$\,\cdot\,$\verb|2) by REAL_1:35|\\ \verb| .= (c - a)|$\,\cdot\,$\verb|(c + a)/4|\\ \verb| .= (c^2 - a^2)/4 by SQUARE_1:67|\\ \verb| .= b^2/4 by A1,REAL_2:17|\\ \verb| .= b^2/(2|$\,\cdot\,$\verb|2)|\\ \verb| .= b^2/2^2 by SQUARE_1:def 3|\\ \verb| .= h^2 by SQUARE_1:69;| \end{mizar} If you run: \begin{mizar} \verb|reliters text\my_mizar|\\ \verb|errflag text\my_mizar| \end{mizar} then you will get \verb|*746| meaning \verb|References| \verb|can| \verb|be| \verb|moved| \verb|to| \verb|the| \verb|next| \verb|step| \verb|of| \verb|this| \verb|iterative| \verb|equality|: \begin{mizar} \verb| m2|$\,\cdot\,$\verb|n2 = (c - a)|$\,\cdot\,$\verb|(c + a)/(2|$\,\cdot\,$\verb|2) by REAL_1:35|\\ \verb| .= (c - a)|$\,\cdot\,$\verb|(c + a)/4|\\ \verb|::> *746|\\ \verb| .= (c^2 - a^2)/4 by SQUARE_1:67|\\ \verb| .= b^2/4 by A1,REAL_2:17|\\ \verb|::> *746|\\ \verb| .= b^2/(2|$\,\cdot\,$\verb|2)|\\ \verb| .= b^2/2^2 by SQUARE_1:def 3|\\ \verb| .= h^2 by SQUARE_1:69;|\\ \end{mizar} So you can remove the terms with the \verb|*746| from the iterative equality. You then have to move the references in the justification to that of the next term in the sequence. So the iterative equality can be shortened to: \begin{mizar} \verb| m2|$\,\cdot\,$\verb|n2 = (c - a)|$\,\cdot\,$\verb|(c + a)/(2|$\,\cdot\,$\verb|2) by REAL_1:35|\\ \verb| .= (c^2 - a^2)/4 by SQUARE_1:67|\\ \verb| .= b^2/(2|$\,\cdot\,$\verb|2) by A1,REAL_2:17|\\ \verb| .= b^2/2^2 by SQUARE_1:def 3|\\ \verb| .= h^2 by SQUARE_1:69;| \end{mizar} \paragraph{{\tt trivdemo}} This program points out subproofs that are so simple that you can replace them with a single \verb|by| justification. It's surprising how often this turns out to be the case! \paragraph{{\tt chklab}} This program points out all labels that are not referred to. They can be safely removed from your article. \paragraph{{\tt inacc}} This program points out the parts of the proofs that are not referred to. They can be safely removed from your article. \paragraph{{\tt irrvoc}} This program points out all vocabularies that are not used. They can be safely removed from your article. \paragraph{{\tt irrths}} This program points out the articles in the \verb|theorem| directive that are not used for references in the proofs. They can be safely removed from your article. \bigskip\noindent Cleaning your article is fun! It really feels like polishing something after it is finished and making it beautiful. Remember to check your article once more with \verb|mizf| after you're finished optimizing it to make sure that you haven't accidentally introduced any new errors. \begin{exercise} Take the proof that you made in exercise \ref{tut:just:exercise:drinker} and run the programs that are discussed in this section on it. Which of the programs advise you to change your proof? \end{exercise} \begin{exercise} Consider the statements in a Mizar proof to be points in a graph and references to the statements to be the edges. What are the \verb|relprem| and \verb|relinfer| optimizations when you consider them as transformations of these graphs? Draw a picture! \end{exercise} \section{Step 9: submitting to the library} So now your article is finished and clean. You should consider submitting it to the MML. There are two rules that articles for the MML have to satisfy: \begin{itemize} \item It is mathematics that's not yet in the MML. There should not be alternate formalizations of the same concepts in the MML. There's too much double work in the MML already. \item It is significant. As a rule of thumb the article should be at least a 1000 lines long. If it's too short consider extending your article until it's long enough. \end{itemize} There are many reasons to submit your article to the MML: \begin{itemize} \item People will be able to use your work and build on it. \item Your definitions will be the standard for your subject in later Mizar articles. \item When the Mizar system changes your article will be kept compatible by the people of the Mizar group. \item An automatically generated {\TeX} version of your article will be published in a journal called {\em Formalized Mathematics}. \end{itemize} To find the details of how to submit an article to the MML see Section \ref{ref:lib:submitting} or go to the web page of the Mizar project and click on the appropriate link. Be aware that to submit your article to the MML you need to sign a form that gives the Mizar people the right to change it as they see fit. If your article is not suitable for submission to the MML but you still want to use it to write further articles, you can put it in a local library of your own. Currently this kind of local library will only support a few articles before it becomes rather inefficient. The MML has been optimized such that library files don't grow too much. You can't do this optimization for your local library yourself, because the tool for it is not distributed. So it's really better to submit your work to the MML if possible. If you want a local library of your own there need to be a third directory called \verb|PREL| next to the already existing \verb|TEXT| and \verb|DICT| directories. To put the files for your article in this directory you need to run the commands: \begin{mizar} \verb|env text\my_mizar|\\ \verb|pre text\my_mizar| \end{mizar} The \verb|env| command creates the necessary library files and the \verb|pre| command copies them to your private \verb|PREL| directory. After you have run \verb|env| and \verb|pre| you can use your article in further articles. \begin{exercise} How many Mizar authors are there in the MML? Shouldn't you be one? \end{exercise} \chapter{Some advanced features} Now that you know how to write a Mizar article, let's take a look at some more advanced features of Mizar that you haven't seen yet. To show these features we use a small proof by Grzegorz Bancerek from the article \verb|QUANTAL1.MIZ|. This article is about the mathematical notion of {\em quantales}. It is not important that you know what quantales are. We just use this proof to show some of Mizar's features. \begin{mizar} \verb|reserve| \verb| Q for left-distributive right-distributive complete Lattice-like|\\ \verb| (non empty QuantaleStr),|\\ \verb| a, b, c, d for Element of the carrier of Q;| \medskip\\ \verb|theorem Th5:|\\ \verb| for Q for X,Y being set holds \/(X,Q) [*] \/(Y,Q) = \/({a[*]|\\ \verb|b: a in X & b in Y}, Q)|\\ \verb| proof let Q; let X,Y be set;|\\ \verb|A1: for a holds a[*]\/(Y,Q) = \/({a[*]b: b in Y}, Q) by Def5;|\\ \verb| {c[*]\/(Y,Q): c in X} = {\/({a[*]b: b in Y},Q): a in|\\ \verb| X} from FraenkelF'(A1);|\\ \verb| hence|\\ \verb| \/(X,Q) [*] \/(Y,Q) =|\\ \verb| \/({\/({a[*]b where b is Element of the carrier of Q: b in Y}, Q)|\toolong\\ \verb| where a is Element of the carrier of Q: a in X}, Q) by Def6 .=|\toolong\\ \verb| \/({c[*]d where c is Element of the carrier of Q,|\\ \verb| d is Element of the carrier of Q: c in X & d in Y}, Q)|\toolong\\ \verb| from LUBFraenkelDistr;|\\ \verb| end;| \end{mizar} This proof is about a more abstract kind of mathematics than the example from the previous chapter. Mizar is especially good at formalizing abstract mathematics. \section{Set comprehension: the Fr\"ankel operator} The proof of theorem \verb|Th5| from \verb|QUANTAL1.MIZ| contains expressions like: \begin{mizar} \verb|{ a[*]b where b is Element of the carrier of Q: a in X & b in Y }| \end{mizar} This corresponds to: $$\{a\ast b\mathrel{:} a\in X \land b \in Y\}$$ where $a$ is a fixed parameter and $b$ is allowed to range over the elements of the carrier of $Q$. In Mizar this style of set comprehension is called the {\em Fr\"ankel operator}. It corresponds to the axiom of replacement in set theory, which was first proposed by Fr\"ankel, the F in ZF. The general form of the Fr\"ankel operator is: \begin{mizar} \verb|{ |{\em term\/}\verb| where |{\em declaration of the variables\/}\verb|: |{\em formula}\verb| }| \end{mizar} As you can see in some of the other Fr\"ankel operator terms in the proof, if all variables in the term occur in a \verb|reserve| statement their declarations can be left implicit. To be allowed to write a Fr\"ankel operator, the types of the variables involved need to {\em widen\/} to a Mizar type that has the form \verb|Element| \verb|of| $A$. Only then can Mizar know that the defined set is really a set. Because else you could write proper classes like: \begin{mizar} \verb|{ X where X is set: not X in X }| \end{mizar} But in Mizar this expression is illegal because \verb|set| doesn't widen to a type of the form \verb|Element| \verb|of|. \begin{exercise} Write in Mizar syntax the statement that the set of prime numbers is infinite. Prove it. \end{exercise} \section{Beyond first order: schemes} The proof of theorem \verb|Th5| from \verb|QUANTAL1.MIZ| uses the \verb|from| justification. Mizar is based on first order predicate logic. However first order logic is slightly too weak to do ZF-style set theory. With first order logic ZF-style set theory needs infinitely many axioms. That's because ZF set theory contains an {\em axiom scheme}, the axiom of replacement. Here is a table that shows how \verb|scheme| and \verb|from| is similar to \verb|theorem| and \verb|by|: \begin{center} \begin{tabular}{lcc} {\em order\/} & {\em item\/} & {\em used\/}\\ \noalign{\smallskip} first order & \verb|theorem| & \verb|by|\\ higher order & \verb|scheme| & \verb|from| \end{tabular} \end{center} Schemes are higher order but only in a very weak sense. It has been said that Mizar schemes are not second order but 1.001th order. Let's study the second \verb|from| in the proof. It justifies an equality: \begin{mizar} \verb|\/({\/({a[*]b where b is Element of the carrier of Q: b in Y}, Q)|\\ \verb| where a is Element of the carrier of Q: a in X}, Q) =|\\ \verb|\/({c[*]d where c is Element of the carrier of Q,|\\ \verb| d is Element of the carrier of Q: c in X & d in Y}, Q)|\toolong\\ \verb| from LUBFraenkelDistr;| \end{mizar} The scheme that is used is: \begin{mizar}\footnotesize \verb|scheme LUBFraenkelDistr|\\ \verb| {Q() -> complete Lattice-like (non empty QuantaleStr),|\\ \verb| f(set, set) -> Element of the carrier of Q(),|\\ \verb| X, Y() -> set}:|\\ \verb| \/({\/({f(a,b) where b is Element of the carrier of Q(): b in Y()},Q())|\\ \verb| where a is Element of the carrier of Q(): a in X()}, Q()) =|\\ \verb| \/({f(a,b) where a is Element of the carrier of Q(),|\\ \verb| b is Element of the carrier of Q(): a in X() & b in|\\ \verb| Y()}, Q());| \end{mizar} Clearly the statement in this scheme looks very similar to the statement that is being justified. When using a scheme you {\em don't\/} give the parameters of the scheme. Mizar figures them out by matching the statement you're justifying to the statement in the scheme. So when using a scheme you really have to make sure that the statement that you're justifying and the statement in the scheme match exactly. In this case matching the statement to the scheme leads to the following substitutions: \begin{center} \begin{tabular}{rcl} \verb|Q()| & $\to$ & \verb|Q|\\ \verb|f(|$x$\verb|,|$y$\verb|)| & $\to$ & $x$\verb|[*]|$y$\\ \verb|X()| & $\to$ & \verb|X|\\ \verb|Y()| & $\to$ & \verb|Y| \end{tabular} \end{center} Here the parameters \verb|Q()|, \verb|X()| and \verb|Y()| are very simple, but they could have been arbitrarily complicated expressions. In real higher order logic finding higher order parameters by matching expressions is very difficult. However in Mizar it's easy because Mizar is first order (it has no $\beta$ conversion so it doesn't get the difficulty). Maybe this example of a scheme is hard to relate to because you probably don't know what it is about. Let's look at the most commonly used scheme. It is the scheme called \verb|Ind| from the article \verb|NAT_1|. It is used to do induction over the natural numbers. This scheme is: \begin{mizar} \verb|scheme Ind { P[Nat] } :|\\ \verb| for k being Nat holds P[k]|\\ \verb| provided|\\ \verb| P[0] and|\\ \verb| for k being Nat st P[k] holds P[k + 1];| \end{mizar} So let's show how to use this scheme to prove some statement about the natural nummbers. For example consider the non-negativity of the natural numbers: \begin{mizar} \verb|for n being Nat holds n >= 0| \end{mizar} If you match this statement to the statement that's given by the scheme: \begin{mizar} \verb|for k being Nat holds P[k]| \end{mizar} then clearly they match with the substitution: \begin{center} \begin{tabular}{rcl} \verb|P[|$x$\verb|]| & $\to$ & $x$\verb| >= 0| \end{tabular} \end{center} Now this scheme has {\em conditions}, after the keyword \verb|provided|. When using the scheme you have to give references to statements that correspond to these conditions. (This is slightly confusing: the {\em arguments\/} of the scheme are figured out automatically by Mizar, but the {\em conditions\/} of the scheme you have to give as {\em arguments\/} in the \verb|from|.) Applying the substitution that we already found to the conditions we get: \begin{center} \begin{tabular}{rcr} \verb|P[0]| & $\to$ & \verb|0 >= 0|\\ \verb|for k being Nat st P[k] holds P[k + 1]| & $\to$ & \\ && \hbox to 0pt{\hss {\tt for k being Nat st k >= 0 holds k + 1 >= 0}} \end{tabular} \end{center} So the \verb|from| justification will be \verb|from| \verb|Ind(A1,A2)| in the following proof: \begin{mizar} \verb|A1: 0 >= 0 by |\dots\verb|;|\\ \verb|A2: for k being Nat st k >= 0 holds k + 1 >= 0|\\ \verb| proof|\\ \verb| let k be Nat;|\\ \verb| assume k >= 0;|\\ \verb| |\dots\\ \verb| thus k + 1 >= 0;|\\ \verb| end;|\\ \verb| for n being Nat holds n >= 0 from Ind(A1,A2);| \end{mizar} Of course you still will need to prove the two cases \verb|A1| and \verb|A2|. Note that \verb|A1| is the {\em base case\/} of the induction and that \verb|A2| is the {\em induction case}. Mizar has a feature that makes it easier for you to ensure that your statements will match the statements in the scheme. You can define {\em macros\/} with \verb|deffunc| and \verb|defpred|. \verb|deffunc| and \verb|defpred| are similar to \verb|set| but with parameters. Using \verb|defpred|, the proof of the non-negativity of natural numbers looks like: \begin{mizar} \verb| defpred P[Nat] means $1 >= 0;|\\ \verb|A1: P[0] by |\dots\verb|;|\\ \verb|A2: for k being Nat st P[k] holds P[k + 1]|\\ \verb| proof|\\ \verb| let k be Nat;|\\ \verb| assume k >= 0;|\\ \verb| |\dots\\ \verb| thus k + 1 >= 0;|\\ \verb| end;|\\ \verb| for n being Nat holds P[n] from Ind(A1,A2);| \end{mizar} If you write your induction in this way it is harder to see what you need to prove but it is easier to see that you are matching the statements in the scheme. \begin{exercise} Write the natural deduction rules as Mizar schemes and prove them. For instance the rule of implication elimination (`modus ponens') becomes: \begin{mizar} \verb|scheme implication_elimination { P[], Q[] } : Q[]|\\ \verb|provided|\\ \verb|A1: P[] implies Q[] and|\\ \verb|A2: P[]|\\ \verb| by A1,A2;| \end{mizar} \end{exercise} \begin{exercise} The axioms of the Mizar set theory are in the article called \verb|TARSKI|. It's called that way because it contains the axioms of a theory called Tarski-Grothendieck set theory, which is ZF set theory with an axiom about the existence of big cardinal numbers. The \verb|TARSKI| article contains one scheme: \begin{mizar} \verb|scheme Fraenkel { A()-> set, P[set, set] }:|\\ \verb| ex X st for x holds x in X iff ex y st y in A() & P[y,x]|\\ \verb| provided for x,y,z st P[x,y] & P[x,z] holds y = z;| \end{mizar} Is it possible to prove this scheme using the Fr\"ankel operator from the previous section (and without using other schemes from the MML)? Conversely, is it possible to eliminate the use of the Fr\"ankel operator from Mizar proofs by using the \verb|Fraenkel| scheme? \end{exercise} \section{Structures} The proof of theorem \verb|Th5| from \verb|QUANTAL1.MIZ| uses the exciting type: \begin{mizar} \verb|left-distributive right-distributive complete Lattice-like|\\ \verb| (non empty QuantaleStr)| \end{mizar} In this type \verb|left-distributive|, \verb|right-distributive|, \verb|complete|, \verb|Lattice-|\penalty10\verb|like| and \verb|empty| are just attributes like before, but the mode \verb|QuantaleStr| is something new. The mode \verb|QuantaleStr| is a {\em structure}. Structures are the records of Mizar. They contain {\em fields} that you can select using the construction: \begin{mizar} \verb|the |{\em field\/}\verb| of |{\em structure\/} \end{mizar} For an example, the \verb|Th5| proof contains the expression: \begin{mizar} \verb|the carrier of Q| \end{mizar} In this the structure is \verb|Q| and the field name is \verb|carrier|. Many Mizar structures have the \verb|carrier| field. The definition of the \verb|QuantaleStr| structure is: \begin{mizar} \verb|struct (LattStr, HGrStr) QuantaleStr|\\ \verb| (# carrier -> set,|\\ \verb| L_join, L_meet, mult -> BinOp of the carrier #);| \end{mizar} Apparently it has four fields: \verb|carrier|, \verb|L_join|, \verb|L_meet| and \verb|mult|. The modes \verb|LattStr| and \verb|HGrStr| are called the {\em ancestors\/} of the structure. They are structures that have a subset of the fields of the structure that is defined. Any term that has type \verb|QuantaleStr| will automatically also get the types \verb|LattStr| and \verb|HGrStr|. The definitions of the ancestors of \verb|QuantaleStr| are: \begin{mizar} \verb|struct(/\-SemiLattStr,\/-SemiLattStr) LattStr|\\ \verb| (# carrier -> set, L_join, L_meet -> BinOp of the carrier #);| \end{mizar} and: \begin{mizar} \verb|struct(1-sorted) HGrStr (# carrier -> set,|\\ \verb| mult -> BinOp of the carrier #);| \end{mizar} % Structures are a powerful concept. They give the MML its abstract flavor. \begin{exercise} Find the definition of the mode \verb|Field| in \verb|VECTSP_1|. What is the structure it is based on? Recursively trace all ancestors of that structure. Draw a graph of the widening relation between those ancestors. \end{exercise} \begin{exercise} The most basic structure in the MML is from \verb|STRUCT_0|: \begin{mizar} \verb|definition|\\ \verb| struct 1-sorted (# carrier -> set #);|\\ \verb|end;| \end{mizar} Is an object of type \verb|1-sorted| uniquely determined by its \verb|carrier|? Why or why not? And what if it has type \verb|strict| \verb|1-sorted|? (For a description of the attribute \verb|strict| see Section \ref{ref:lan:types:structures}.) \end{exercise} \begin{exercise} You can construct an object of type \verb|1-sorted| as: \begin{mizar} \verb|1-sorted (# A #)| \end{mizar} Use this notation to define functors \verb|in| and \verb|out| that map objects of type \verb|set| to their natural counterparts in \verb|1-sorted| and back. Prove in Mizar that \verb|out| is a left inverse to \verb|in|. \end{exercise} \begin{exercise} Are structures ZF sets or not? More specifically: if \verb|Q| is a structure, can there be an \verb|x| with \verb|x| \verb|in| \verb|Q|? If not, why not? If so, can you prove the following? \begin{mizar} \verb|ex Q being 1-sorted, x being set st x in Q| \end{mizar} If a structure has elements: is it uniquely determined by its elements? \end{exercise} \begin{exercise} Because of G\"odel's theorems we know that Mizar's set theory is incomplete. That is, there has to be a Mizar formula $\phi$ without free variables, for which no Mizar proof exists of $\phi$, and also no Mizar proof exists of \verb|not| $\phi$. Can you think of a non-G\"odelian $\phi$ that is provable nor disprovable in Mizar? \end{exercise} \appendix \chapter{Mizar grammar} ??? \chapter{Mizar glossary} ??? \chapter{Answers to exercises} \begin{answer}{tut:skel:exercise:th2} The proof, put together, becomes: \begin{mizar} \verb|theorem Th2:|\\ \verb| a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies|\\ \verb| ex m,n st m <= n & a = n^2 - m^2 & b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n & c = n^2 + m^2|\\ \verb|proof|\\ \verb| assume a^2 + b^2 = c^2;|\\ \verb| assume a,b are_relative_prime;|\\ \verb| assume a is odd;|\\ \verb| b is even;|\\ \verb| c is odd;|\\ \verb| reconsider h = b/2 as Nat;|\\ \verb| reconsider m2 = (c - a)/2 as Nat;|\\ \verb| reconsider n2 = (c + a)/2 as Nat;|\\ \verb| n2 - m2 = a;|\\ \verb| n2 + m2 = c;|\\ \verb| m2|$\,\cdot\,$\verb|n2 = (c - a)|$\,\cdot\,$\verb|(c + a)/4|\\ \verb| .= (c^2 - a^2)/4|\\ \verb| .= b^2/4|\\ \verb| .= h^2;|\\ \verb| m2|$\,\cdot\,$\verb|n2 is square;|\\ \verb| m2,n2 are_relative_prime;|\\ \verb| m2 is square & n2 is square;|\\ \verb| consider m such that m2 = m^2;|\\ \verb| consider n such that n2 = n^2;|\\ \verb| take m,n;|\\ \verb| thus m <= n;|\\ \verb| thus a = n^2 - m^2;|\\ \verb| thus b = 2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n;|\\ \verb| thus c = n^2 + m^2;|\\ \verb|end;| \end{mizar} No update to the environment has been necessary to check this proof. Every step in the proof that's not an \verb|assume| or \verb|take| step gives a \verb|*4| error. The step \verb|m2| \verb|is| \verb|square| \verb|&| \verb|n2| \verb|is| \verb|square| gives two \verb|*4| errors because it is a conjunction of two statements, and Mizar tries to justify the conjuncts separately. So there are twenty-one \verb|*4| errors in the proof of \verb|Th2|. Together with the two \verb|*4| errors for \verb|Th1| there are at this point twenty-three \verb|*4| errors in the article. \end{answer} \begin{answer}{tut:just:exercise:th2} Here is a possible proof. The skeleton that was the solution to exercise \ref{tut:skel:exercise:th2} has been underlined. Apart from the four lemmas, three clusters are used that tell when a term of the shape \verb|n^2| is even, odd and square. \begin{mizar} \underbar{\tt{theorem Th2:}}\\ \verb| |\underbar{\tt{a\^{}2 + b\^{}2 = c\^{}2 \& a,b are\_relative\_prime \& a is odd implies}}\\ \verb| |\underbar{\tt{ex m,n st m <= n \& a = n\^{}2 - m\^{}2 \& b = 2}$\,\cdot\,$\tt{m}$\,\cdot\,$\tt{n \& c = n\^{}2 + m\^{}2}}\\ \underbar{\tt{proof}}\\ \verb| |\underbar{\tt{assume}}\\ \verb|A1: |\underbar{\tt{a\^{}2 + b\^{}2 = c\^{}2;}}\\ \verb| |\underbar{\tt{assume}}\\ \verb|A2: |\underbar{\tt{a,b are\_relative\_prime;}}\\ \verb| |\underbar{\tt{assume a is odd;}}\\ \verb| then reconsider a' = a as odd Nat;|\\ \verb| |\underbar{\tt{b is even}}\\ \verb| proof|\\ \verb| assume b is odd;|\\ \verb| then reconsider b' = b as odd Nat;|\\ \verb| a'^2 is odd square & b'^2 is odd square;|\\ \verb| hence contradiction by A1,Lm1;|\\ \verb| end|\underbar{\tt{;}}\\ \verb| then reconsider b' = b as even Nat;|\\ \verb| |\underbar{\tt{c is odd}}\\ \verb| proof|\\ \verb| assume c is even;|\\ \verb| then reconsider c' = c as even Nat;|\\ \verb| a'^2 + b'^2 is odd & c'^2 is even;|\\ \verb| hence contradiction by A1;|\\ \verb| end|\underbar{\tt{;}}\\ \verb| then reconsider c' = c as odd Nat;|\\ \verb| |\underbar{\tt{reconsider h = b}}\verb|'|\underbar{\tt{/2 as Nat}}\verb| by Lm2|\underbar{\tt{;}}\\ \verb| b^2 >= 0 by NAT_1:18;|\\ \verb| then a^2 + b^2 >= a^2 + 0 by AXIOMS:24;|\\ \verb| then c^2 >= a^2 & c >= 0 by A1,NAT_1:18;|\\ \verb| then c >= a by SQUARE_1:78;|\\ \verb| then c - a >= 0 by REAL_2:106;|\\ \verb| then c - a is Nat by INT_1:16;|\\ \verb| then |\underbar{\tt{reconsider m2 = (c}}\verb|'|\underbar{\tt{ - a}}\verb|'|\underbar{\tt{)/2 as Nat}}\verb| by Lm2|\underbar{\tt{;}}\\ \verb| |\underbar{\tt{reconsider n2 = (c}}\verb|'|\underbar{\tt{ + a}}\verb|'|\underbar{\tt{)/2 as Nat}}\verb| by Lm2|\underbar{\tt{;}}\\ \verb|A3: |\underbar{\tt{n2 - m2 =}}\verb| ((c + a) - (c - a))/2 by REAL_1:40|\\ \verb| .= (c + a - c + a)/2 by REAL_1:28|\\ \verb| .= (a + a)/2 by REAL_2:17|\\ \verb| .= |\underbar{\tt{a}}\verb| by SQUARE_1:15|\underbar{\tt{;}}\\ \verb|A4: |\underbar{\tt{n2 + m2 =}}\verb| ((c + a) + (c - a))/2 by REAL_1:40|\\ \verb| .= (c + a + c - a)/2 by REAL_2:18|\\ \verb| .= (c + c + a - a)/2 by AXIOMS:13|\\ \verb| .= (c + c)/2 by REAL_2:17|\\ \verb| .= |\underbar{\tt{c}}\verb| by SQUARE_1:15|\underbar{\tt{;}}\\ \verb| |\underbar{\tt{m2$\,\cdot\,$n2 =}}\verb| (c - a)|$\,\cdot\,$\verb|(c + a)/(2|$\,\cdot\,$\verb|2) by REAL_1:35|\\ \verb| .= |\underbar{\tt{(c - a)$\,\cdot\,$(c + a)/4}}\\ \verb| |\underbar{\tt{.= (c\^{}2 - a\^{}2)/4}}\verb| by SQUARE_1:67|\\ \verb| |\underbar{\tt{.= b\^{}2/4}}\verb| by A1,REAL_2:17|\\ \verb| .= b^2/(2|$\,\cdot\,$\verb|2)|\\ \verb| .= b^2/2^2 by SQUARE_1:def 3|\\ \verb| |\underbar{\tt{.= h\^{}2}}\verb| by SQUARE_1:69;|\\ \verb| then|\\ \verb|A5: |\underbar{\tt{m2$\,\cdot\,$n2 is square;}}\\ \verb| now|\\ \verb| let p be prime Nat;|\\ \verb| assume|\\ \verb|A6: p|$\,|\,$\verb|m2 & p|$\,|\,$\verb|n2;|\\ \verb| then p|$\,|\,$\verb|(m2 qua Integer) & p|$\,|\,$\verb|(n2 qua Integer) by SCPINVAR:2;|\\ \verb| then p|$\,|\,$\verb|(n2 qua Integer) & p|$\,|\,$\verb|-m2 by INT_2:14;|\\ \verb| then p|$\,|\,$\verb|(n2 + -m2) by WSIERP_1:9;|\\ \verb| then p|$\,|\,$\verb|(a qua Integer) by A3,REAL_1:def 3;|\\ \verb| then|\\ \verb|A7: p|$\,|\,$\verb|a by SCPINVAR:2;|\\ \verb|A8: p|$\,|\,$\verb|c by A4,A6,NAT_1:55;|\\ \verb|A9: b|$\,\cdot\,$\verb|b = b^2 by SQUARE_1:def 3|\\ \verb| .= c^2 - a^2 by A1,REAL_2:17|\\ \verb| .= c|$\,\cdot\,$\verb|c - a^2 by SQUARE_1:def 3|\\ \verb| .= c|$\,\cdot\,$\verb|c - a|$\,\cdot\,$\verb|a by SQUARE_1:def 3|\\ \verb| .= c|$\,\cdot\,$\verb|c + -(a|$\,\cdot\,$\verb|a) by REAL_1:def 3;|\\ \verb| p|$\,|\,$\verb|c|$\,\cdot\,$\verb|c & p|$\,|\,$\verb|a|$\,\cdot\,$\verb|a by A7,A8,NAT_1:56;|\\ \verb| then p|$\,|\,$\verb|(c|$\,\cdot\,$\verb|c qua Integer) & p|$\,|\,$\verb|(a|$\,\cdot\,$\verb|a qua Integer) by SCPINVAR:2;|\\ \verb| then p|$\,|\,$\verb|(c|$\,\cdot\,$\verb|c qua Integer) & p|$\,|\,$\verb|-(a|$\,\cdot\,$\verb|a) by INT_2:14;|\\ \verb| then p|$\,|\,$\verb|(b|$\,\cdot\,$\verb|b qua Integer) by A9,WSIERP_1:9;|\\ \verb| then p|$\,|\,$\verb|b|$\,\cdot\,$\verb|b by SCPINVAR:2;|\\ \verb| then p|$\,|\,$\verb|b by NAT_LAT:95;|\\ \verb| hence contradiction by A2,A7,Lm3;|\\ \verb| end;|\\ \verb| then |\underbar{\tt{m2,n2 are\_relative\_prime}}\verb| by Lm3|\underbar{\tt{;}}\\ \verb| then|\\ \verb|A10: |\underbar{\tt{m2 is square \& n2 is square}}\verb| by A5,Th1|\underbar{\tt{;}}\\ \verb| |\underbar{\tt{consider m such that}}\\ \verb|A11: |\underbar{\tt{m2 = m\^{}2}}\verb| by A10,Def1|\underbar{\tt{;}}\\ \verb| |\underbar{\tt{consider n such that}}\\ \verb|A12: |\underbar{\tt{n2 = n\^{}2}}\verb| by A10,Def1|\underbar{\tt{;}}\\ \verb| |\underbar{\tt{take m,n;}}\\ \verb| a >= 0 by NAT_1:18;|\\ \verb| then c - a <= c & c + a >= c by REAL_2:173;|\\ \verb| then c - a <= c + a by AXIOMS:22;|\\ \verb| then m^2 <= n^2 & n >= 0 by A11,A12,REAL_1:73,NAT_1:18;|\\ \verb| |\underbar{\tt{hence m <= n}}\verb| by SQUARE_1:78|\underbar{\tt{;}}\\ \verb| |\underbar{\tt{thus a = n\^{}2 - m\^{}2}}\verb| by A3,A11,A12|\underbar{\tt{;}}\\ \verb| b^2 = c^2 - a^2 by A1,REAL_2:17|\\ \verb| .= (c - a)|$\,\cdot\,$\verb|(c + a) by SQUARE_1:67|\\ \verb| .= (2|$\,\cdot\,$\verb|((c - a)/2))|$\,\cdot\,$\verb|(c + a) by REAL_2:62|\\ \verb| .= (2|$\,\cdot\,$\verb|((c - a)/2))|$\,\cdot\,$\verb|(2|$\,\cdot\,$\verb|((c + a)/2)) by REAL_2:62|\\ \verb| .= 2|$\,\cdot\,$\verb|m2|$\,\cdot\,$\verb|2|$\,\cdot\,$\verb|n2 by AXIOMS:16|\\ \verb| .= 2|$\,\cdot\,$\verb|2|$\,\cdot\,$\verb|m2|$\,\cdot\,$\verb|n2 by AXIOMS:16|\\ \verb| .= 2^2|$\,\cdot\,$\verb|m^2|$\,\cdot\,$\verb|n^2 by A11,A12,SQUARE_1:def 3|\\ \verb| .= (2|$\,\cdot\,$\verb|m)^2|$\,\cdot\,$\verb|n^2 by SQUARE_1:68|\\ \verb| .= (2|$\,\cdot\,$\verb|m|$\,\cdot\,$\verb|n)^2 by SQUARE_1:68;|\\ \verb| |\underbar{\tt{hence b = 2$\,\cdot\,$m$\,\cdot\,$n}}\verb| by Lm4|\underbar{\tt{;}}\\ \verb| |\underbar{\tt{thus c = n\^{}2 + m\^{}2}}\verb| by A4,A11,A12|\underbar{\tt{;}}\\ \underbar{\tt{end;}} \end{mizar} \end{answer} \end{document}