This is a short summary of a Mizar demo performed at the Schloss Dagstuhl Seminar "Deduction" on February 27, 1997.
New users of the Mizar system may find this mini-tutorial helpful.
Acknowledgements
I would like to thank the generous German taxpayers who make the Dagstuhl seminars possible and very enjoyable.
H. Schwichtenberg asked me for a demo of the Mizar system and suggested that we do a certain logic puzzle put forward by J. Cunningham. This puzzle needed only some simple gymnastics in propositional logic and we very quickly came to the mutual understanding that Mizar is not exactly meant for solving cute logic puzzles, although it can be used for such exercises.
The second suggestion was to prove a version of the mean value theorem but this was also rejected as it seemed a bit too much for a first encounter with Mizar, especially since we had some time constraints.
The third suggestion was to define the Fibonacci sequence. Since the Fibonacci sequence has been previously defined in Mizar (article PRE_FF) we decided to study its definition in detail and this took us about half an hour.
Here is the complete text of the definition of Fib in Mizar, together with proofs, taken verbatim from the source Mizar article. Mizar does not permit recursive definitions of functors, therefore we first define (recursively) a set theoretic function using one of the available schemes for recursive definitions of functions. Then, the theorem recasts the recursive property of the functor Fib. In the sequel, we will frequently refer to the following theorem
as PRE_FF:1. This is how the theorem appears in the Mizar abstract of the PRE_FF article, which is used to create the data base files. The definition of the Fib functor precedes the theorem in the Mizar abstract file:
At this point, we were running short on time as we wanted to go to the next seminar session. We started looking for some simple fact about the Fibonacci sequence that we could use as a small but illustrative example of developing a Mizar text.
M. Beeson, who joined us halfway through, proposed to prove that the n-th Fibonacci number is no less than n. It looked simple enough and we decided to continue the proof after the evening session. I had promised not to do any preparatory work such that the demonstration could illustrate how a beginner is fighting with the Mizar processor. (You will shortly see that I did not do any preparatory work.)
At the evening part of the Mizar demo, we were joined, for most of the time, by M. Kohlhase, T. Nipkow, and H. de Nivelle.
First we formulated the theorem that we wanted to prove:
Unfortunately, Mizar could not understand it in the empty environment and we got the following errors:
The error *151 under Nat means that Nat in this context is expected to denote a mode (a type) and the current (empty) environment does not provide such a meaning. Nat - the type of natural numbers is introduced in article ARYTM.
In order to import this meaning of Nat we imported constructors from ARYTM (for semantics) and notation from ARYTM (for parsing formats). With this correction, we are left with two parsing errors:
Mizar processes the input text and inserts error messages into the presented file in lines starting with ::>. These lines are treated as comments and are stripped off when the text is processed the next time. New error messages are usually inserted. As a result, we work with one text file which is modified during processing.
The error *143 indicates that Fib is treated as a free (actually not free but quantified by default) variable and it is required that the type of such a variable be announced earlier. We meant Fib to denote the functor for the Fibonacci sequence. That Fib is a functor symbol is declared in vocabulary SCM; we learned this by using the findvoc utility. With the vocabulary SCM added to the environment we obtained:
Now, Fib is known to be a functor but its parsing format and the information on how it is used to construct terms is still not in the environment. Fib has been defined in article PRE_FF and thus we imported constructors and notation from there.
We were left with one checker error and finally could focus on proving, as it seemed that we had built the right conceptual environment for now. The proof is to be done by induction for which we employed scheme Ind defined in article NAT_1 as follows:
In order to get access to the scheme we had to use the schemes directive in the environment. We also formulated the premises for the application of the scheme and got:
Just for illustration, we were correcting one error at a time, starting with the last one.
What caused the error *195 can be sorted out using the scconstr utility. Using the utility we learned that for the scheme Ind to be understood by Mizar, the environment must include constructors from article NAT_1. After adding the constructors and "mizaring" the text we got:
Why is Fib 0 indicated as an unknown usage of Fib while Fib n is OK?
The small constants like 0 and 1 are built into the processor but by default are typed as set. In order to use them as numerals one has to use the environment directive requirements ARYTM.
The last *103 error is announced under + because 1 is typed as a set and in the current environment in which we imported ARYTM, Mizar does not know how to add a Nat (which widens to Real) to an arbitrary set. After adding the library directive requirements ARYTM we got:
Note how the proposition labeled P1 is now understood but not accepted as the Mizar checker does not see why is this true without some justification.
The remaining parsing error *103 is puzzling at first and it took us a while to sort out why it occurred. n is a Nat and 1 is a Nat, and every Nat is Real. In the current environment, there is a functor for addition imported from ARYTM. Unfortunately, this functor results in type Real which is inappropriate as a type the Fib's argument, thus the error. The functor for addition of two Nats that results in a Nat is defined in NAT_1 and in order to be able to use it we had to add the notation from NAT_1 (the constructors from NAT_1 have been already imported) into the environment. Thus we got:
Finally, we were left only with logical errors. However, we could not proceed as the inductive step is hard to prove the way it has been stated. Fib, in its recursive properties, makes reference to two preceding values while the inductive hypothesis provides some information only about the immediate predecessor. Someone suggested that there is a simple remedy in this case by strengthening the proposition that we wanted to prove (induction loading) and making it a conjunction of inequalities about two subsequent terms of the Fibonacci sequence. After making appropriate adjustments we were faced by the following text:
Aside
At this point, M. Beeson asked why did we not do the course of values induction and I authoritatively lied that there is no course of values induction in Mizar. Certainly there is one, although it is called complete induction. For the proof using this induction see the end of this text. It puzzles me until now why I lied, but it could have been a genuine lie under pressure.
(H. Schwichtenberg told me the next day that he did not believe me anyway.)
End of aside
We guessed that the first premise to the induction easily follows from the theorem PRE_FF:1 about the Fibonacci sequence. However, we got:
Whenever we make a library reference, in this case to PRE_FF:1, the name of the article to whose theorems we want to have access must appear in the library directive theorems. After making this simple change we got:
Note that Mizar automatically processes some arithmetic expressions involving small natural constants.
In order to justify the second premise to the induction scheme, we wrote a proof whose structure is dictated by the proposition that we are proving. Thus we got:
The yet unjustified conclusion required us to consider two cases: either n is zero or it is not. For this we employed the per cases Mizar construct:
The per cases construct requires justification of the disjunction of all the suppose conditions:
The theorem NAT_1:19 is:
We also added NAT_1 to the theorems directive.
Unfortunately, the conclusion in the first case is false as Fib 2 is 1. The theorem that we tried to prove was simply false and realizing this fact so late was kind of funny, taking into account the collective brain power engaged in the exercise (M. Beeson laughed loudest). This also shows that mechanical proof-checking systems have some future.
The simple remedy in our case was to upgrade the proposition that we wanted to prove to something like: the (n+1)-th Fibonacci is not less than n. After making all the necessary changes we got:
The proof in the first case is immediate from PRE_FF:1 with the help of built-in calculations, and may look like:
In the proof of the second case we first used PRE_FF:1. Then, we added the sides of both equalities from the inductive hypothesis labeled IH. This required using the following theorem REAL_1:55:
which in turn required adding REAL_1 to the theorems directive. Then we started to show that n is at least 1 which is needed to show that n+(n+1) is at least n+1+1. We got:
The error *192 is described as Inaccessible theorem and what is needed to be done can be sorted out using the thconstr utility. The theorem REAL_1:59 is as follows:
and it uses a constructor for subtraction, which we did not need in our writings but which is needed by the processor in order to use the theorem. The constructor for subtraction is defined in article REAL_1 and thus we added it to the constructors directive. Note that we did not add REAL_1 to the notation directive as we did not need the parsing format of the subtraction constructor in what we wrote. We kept on getting:
Here are the theorems that we referred to:
At this moment, it is enough to use transitivity of greater than or equal to complete the proof. The ordering relation is defined in ARYTM as a synonym to less than or equal as follows:
The transitivity of less than or equal is assumed in AXIOMS:
The second case of our proof is completed as follows:
Here is the complete text of our development:
From the last proposition we can infer a simpler statement in which we skip the second conjunct: