New users of the Mizar system may find this mini-tutorial helpful.
The Fibonacci sequence has been previously defined in Mizar article PRE_FF as follows:
definition let n;
func Fib (n) -> Nat means
:: PRE_FF:def 1
ex fib being Function of NAT, [:NAT, NAT:] st
it = (fib.n)`1 & fib.0 = [0,1] &
for n being Nat, x being Element of [: NAT, NAT :] st x = fib.n
holds fib.(n+1) = [ x`2, x`1 + x`2 ];
end;
Mizar does not permit recursive definitions of functors, therefore the
above definition depends on a recursively defined set theoretic
function (several schemes are available for recursive definitions of
functions). Then, a theorem recasts the recursive property of the
functor Fib. In the sequel, we will frequently refer to the
following theorem (which is usually understood as the definition of
the Fibonacci sequence):
theorem :: PRE_FF:1
Fib(0) = 0 &
Fib(1) = 1 &
(for n being Nat holds Fib((n+1)+1) = Fib(n) + Fib(n+1));
Let us try to prove that the n-th Fibonacci number is no less than n.
environ :: mt1
begin
for n being Nat holds Fib n >= n;
(The above is put into a .miz file). Unfortunately, Mizar
could not understand it in the empty environment and we got the
following errors:
environ :: mt1
begin
for n being Nat holds Fib n >= n;
::> *151 *143,321
::>
::> 143: No implicit qualification
::> 151: Unknown mode format
::> 321: Predicate symbol or "is" expected
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 NAT_1.
In order to import this meaning of Nat we imported constructors from NAT_1 (for semantics) and notation from NAT_1 (for parsing formats). With this correction, we are left with two parsing errors:
environ :: mt2
notation NAT_1;
constructors NAT_1;
begin
for n being Nat holds Fib n >= n;
::> *143,321
::>
::> 143: No implicit qualification
::> 321: Predicate symbol or "is" expected
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 PRE_FF; we learned this by using the findvoc utility. With the vocabulary PRE_FF added to the environment we obtained:
environ :: mt3
vocabulary PRE_FF;
notation NAT_1;
constructors NAT_1;
begin
for n being Nat holds Fib n >= n;
::> *165 *153,395
::> 153: Unknown predicate format
::> 165: Unknown functor format
::> 395: Justification expected
We will pay attention only to the first error *165. 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
current environment. Fib has been defined in article
PRE_FF and thus we import constructors and notation from
there.
environ :: mt4
vocabulary PRE_FF;
notation NAT_1, PRE_FF;
constructors NAT_1, PRE_FF;
begin
for n being Nat holds Fib n >= n;
::> *153,395
::> 153: Unknown predicate format
::> 395: Justification expected
Now, the term Fib n seems to be understood by Mizar but we
are left with two other errors. Again, we will pay attention only to
the first error *153 as the second error is its consequence.
This error says that while >= is known to be a predicate
symbol (it is introduced in vocabulary HIDDEN), the actual
format of its usage is not accessible through the current environment.
The greater than or equal relation that we want to use is defined
in article XREAL_0.
Therefore, we have to import notation and constructors from XREAL_0.
For this import to be successful, we needed to import some additional
facts through clusters which we will not discuss at this place.
environ :: mt5
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
begin
for n being Nat holds Fib n >= n;
::> *4
::> 4: This inference is not accepted
We are left with one checker error and finally can focus on proving,
as it seems that we have 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:
scheme Ind { P[Nat] } :
for k holds P[k]
provided
P[0] and
for k st P[k] holds P[k + 1];
In order to get access to the scheme we use the schemes
directive in the environment. We also formulated the premises for the
application of the scheme and got:
environ :: mt6
vocabulary PRE_FF;
notation ARYTM, NAT_1, PRE_FF;
constructors ARYTM, NAT_1, PRE_FF;
clusters ARYTM, ARYTM_3;
schemes NAT_1;
begin
P1: Fib 0 >= 0;
::> *103
P2: for n being Nat
st Fib n >= n
holds Fib (n+1) >= n+1;
::> *103 *103
for n being Nat holds Fib n >= n from Ind(P1, P2);
::> 103: Unknown functor
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 natural numbers one has to use the environment directive requirements. In our case, we need requirements named ARYTM and SUBSET. (The requirements directives enable default processing of certain objects; we will not comment more on this feature at this point.)
environ :: mt7
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements NUMERALS, SUBSET;
schemes NAT_1;
begin
P1: Fib 0 >= 0;
::> *4
P2: for n being Nat
st Fib n >= n
holds Fib (n+1) >= n+1;
::> *4
for n being Nat holds Fib n >= n from Ind(P1, P2);
::> *23
::> 4: This inference is not accepted
::> 23: Invalid order of arguments in the instantiated predicate
Note how the propositions labeled P1 and P2 are now
understood but not accepted as the Mizar checker does not see why
they are true without some justification.
Error *23 relates to a parameter of induction: the formal predicate which must be explicitely stated using defpred.
environ :: mt7a
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements NUMERALS, SUBSET;
schemes NAT_1;
begin
defpred P[Nat] means Fib $1 >= $1;
P1: P[0];
::> *4
P2: for n being Nat st P[n] holds P[n+1];
::> *4
for n being Nat holds P[n] from Ind(P1, P2);
::> 4: This inference is not accepted
We are left with logical errors only, however, we can not proceed as the inductive step is hard to prove the way it has been stated.
Namely, Fib, in its recursive properties, makes reference to two preceding values while the inductive hypothesis provides some information only about the immediate predecessor. 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:
environ :: mt8
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements NUMERALS, SUBSET;
schemes NAT_1;
begin
defpred P[Nat] means Fib $1 >= $1 & Fib ($1+1) >= $1+1;
P1: P[0];
::> *4,4
P2: for n being Nat st P[n] holds P[n+1];
::> *4,4
for n being Nat holds P[n] from Ind(P1, P2);
::> 4: This inference is not accepted
The first premise to the induction should easily follow from
the theorem PRE_FF:1 about the Fibonacci sequence. However, we get:
environ :: mt9
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements NUMERALS, SUBSET;
schemes NAT_1;
begin
defpred P[Nat] means Fib $1 >= $1 & Fib ($1+1) >= $1+1;
P1: P[0] by PRE_FF:1;
::> *144,330
P2: for n being Nat st P[n] holds P[n+1];
::> *4,4
for n being Nat holds P[n] from Ind(P1, P2);
::> 4: This inference is not accepted
::> 144: Unknown label
::> 330: Unexpected end of an item (perhaps ";" missing)
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 have:
environ :: mt10
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements NUMERALS, SUBSET;
theorems PRE_FF;
schemes NAT_1;
begin
defpred P[Nat] means Fib $1 >= $1 & Fib ($1+1) >= $1+1;
P1: P[0] by PRE_FF:1;
::> *4
P2: for n being Nat st P[n] holds P[n+1];
::> *4
for n being Nat holds P[n] from Ind(P1, P2);
::> 4: This inference is not accepted
The first error is due to the fact that Mizar does not see that 0+1 =
1. Although Mizar automatically processes some arithmetic expressions
involving small natural constants, it still has to be told to do so by
specifying appropriate requirements, ARITHM in this case.
(See file ARITHM for the list of the imported properties.)
And thus we get:
environ :: mt10a
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements ARITHM, NUMERALS, SUBSET;
theorems PRE_FF;
schemes NAT_1;
begin
defpred P[Nat] means Fib $1 >= $1 & Fib ($1+1) >= $1+1;
P1: P[0] by PRE_FF:1;
P2: for n being Nat st P[n] holds P[n+1];
::> *4
for n being Nat holds P[n] from Ind(P1, P2);
::> 4: This inference is not accepted
In order to justify the second premise to the induction scheme, we write
a proof whose structure is dictated by the proposition that we are proving.
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib n >= n & Fib (n+1) >= n+1;
thus Fib (n+1) >= n+1 by IH;
thus Fib (n+1+1) >= n+1+1;
::> *4
end;
The yet unjustified conclusion requires us to consider two cases: either
n is zero or it is not.
For this we employed the per cases Mizar construct:
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib n >= n & Fib (n+1) >= n+1;
thus Fib (n+1) >= n+1 by IH;
per cases;
::> *4
suppose S1: n = 0;
thus Fib (n+1+1) >= n+1+1;
::> *4
suppose S1: n > 0;
thus Fib (n+1+1) >= n+1+1;
::> *4
end;
The per cases construct requires justification of the disjunction
of all the suppose conditions:
per cases by NAT_1:19;
suppose S1: n = 0;
thus Fib (n+1+1) >= n+1+1;
::> *4
suppose S1: n > 0;
thus Fib (n+1+1) >= n+1+1;
::> *4
The theorem NAT_1:19 is:
theorem :: NAT_1:19 0 <> k implies 0 < k;We also added NAT_1 to the theorems directive.
Unfortunately, the conclusion in the first case (n = 0 ) is false as Fib 2 is 1. The theorem that we tried to prove was simply false and realizing this fact so late is a bit embarassing. However, it shows that mechanical proof-checking systems have some future.
The simple remedy in our case is to upgrade the proposition that we want to prove to something like: the (n+1)-th Fibonacci is not less than n. After making all the necessary changes we have:
environ :: mt14
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements REAL, ARITHM, NUMERALS, SUBSET;
theorems PRE_FF, NAT_1;
schemes NAT_1;
begin
defpred P[Nat] means Fib ($1+1) >= $1 & Fib ($1+1+1) >= $1+1;
P1: P[0] by PRE_FF:1;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib (n+1) >= n & Fib (n+1+1) >= n+1;
thus Fib (n+1+1) >= n+1 by IH;
per cases by NAT_1:19;
suppose S1: n = 0;
thus Fib (n+1+1+1) >= n+1+1;
::> *4
suppose S1: n > 0;
thus Fib (n+1+1+1) >= n+1+1;
::> *4
end;
for n being Nat holds P[n] from Ind(P1, P2);
::> 4: This inference is not accepted
Note that we added another requirements in order to have the claim
labelled P1 accepted.
The proof of the first case is immediate from PRE_FF:1 with the help of built-in calculations, and may look like:
suppose S1: n = 0;
Fib (0+1+1+1) = Fib (0+1) + Fib (0+1+1) by PRE_FF:1
.= 1+1 by PRE_FF:1;
hence Fib (n+1+1+1) >= n+1+1 by S1;
In the proof of the second case we first use PRE_FF:1.
Then, we add the sides of both inequalities from the inductive hypothesis
labeled IH. This required using the following theorem
REAL_1:55:
theorem :: REAL_1:55 (x<=y & z<=t) implies x+z<=y+t;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 get:
suppose S1: n > 0;
A: Fib (n+1+1+1) = Fib (n+1) + Fib (n+1+1) by PRE_FF:1;
B: Fib (n+1) + Fib (n+1+1) >= n+(n+1) by IH, REAL_1:55;
0+1 < n+1 by S1, REAL_1:67; then
n >= 1 by NAT_1:38; then
n+(n+1) >= n+1+1 by REAL_1:55;
thus Fib (n+1+1+1) >= n+1+1;
::> *4
Here are the theorems that we referred to:
theorem :: NAT_1:38 k < n + 1 iff k <= n; theorem :: REAL_1:55 x<=y & z<=t implies x+z<=y+t;At this moment, it is enough to use transitivity of greater than or equal to complete the proof. The ordering relation is defined in XREAL_0 as a synonym to less than or equal as follows:
definition let x,y be real number;
pred x <= y means
:: XREAL_0:def 2
... definiens omitted ...
reflexivity;
connectedness;
synonym y >= x;
antonym y < x;
antonym x > y;
end;
The transitivity of less than or equal appears as theorem in article
named (for historical reasons) AXIOMS:
theorem :: AXIOMS:22 x <= y & y <= z implies x <= z;The second case of our proof is completed as follows:
suppose S1: n > 0;
A: Fib (n+1+1+1) = Fib (n+1) + Fib (n+1+1) by PRE_FF:1;
B: Fib (n+1) + Fib (n+1+1) >= n+(n+1) by IH, REAL_1:55;
0+1 < n+1 by S1, REAL_1:67; then
n >= 1 by NAT_1:38; then
n+(n+1) >= n+1+1 by REAL_1:55;
hence Fib (n+1+1+1) >= n+1+1 by A, B, AXIOMS:22 ;
Here is the complete text of our development:
environ :: mt18
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements REAL, ARITHM, NUMERALS, SUBSET;
theorems PRE_FF, NAT_1, REAL_1, AXIOMS;
schemes NAT_1;
begin
defpred P[Nat] means Fib ($1+1) >= $1 & Fib ($1+1+1) >= $1+1;
P1: P[0] by PRE_FF:1;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat; assume
IH: Fib (n+1) >= n & Fib (n+1+1) >= n+1;
thus Fib (n+1+1) >= n+1 by IH;
per cases by NAT_1:19;
suppose S1: n = 0;
Fib (0+1+1+1) = Fib (0+1) + Fib (0+1+1) by PRE_FF:1
.= 1+1 by PRE_FF:1;
hence Fib (n+1+1+1) >= n+1+1 by S1;
suppose S1: n > 0;
A: Fib (n+1+1+1) = Fib (n+1) + Fib (n+1+1) by PRE_FF:1;
B: Fib (n+1) + Fib (n+1+1) >= n+(n+1) by IH, REAL_1:55;
0+1 < n+1 by S1, REAL_1:67; then
n >= 1 by NAT_1:38; then
n+(n+1) >= n+1+1 by REAL_1:55;
hence Fib (n+1+1+1) >= n+1+1 by A, B, AXIOMS:22;
end;
for n being Nat holds P[n] from Ind(P1, P2);
then for n being Nat holds Fib (n+1) >= n;
From the last proposition we can infer a simpler statement in which we
skip the second conjunct:
then for n being Nat holds Fib (n+1) >= n;
environ :: mt_cov
vocabulary PRE_FF;
notation XREAL_0, NAT_1, PRE_FF;
constructors ARYTM_2, XREAL_0, NAT_1, PRE_FF;
clusters XREAL_0, ARYTM_3;
requirements REAL, ARITHM, NUMERALS, SUBSET;
theorems PRE_FF, NAT_1, REAL_1, AXIOMS, CQC_THE1, XCMPLX_1;
schemes NAT_1;
begin
defpred P[Nat] means Fib ($1+1) >= $1;
P: for k being Nat
st for n being Nat st n < k holds P[n]
holds P[k]
proof let k be Nat; assume
IH: for n being Nat st n < k holds Fib (n+1) >= n;
per cases;
suppose k <= 1; then k = 0 or k = 0+1 by CQC_THE1:2;
hence Fib (k+1) >= k by PRE_FF:1;
suppose 1 < k; then
1+1 <= k by NAT_1:38; then
consider m being Nat such that
A: k = 1+1+m by NAT_1:28;
thus Fib (k+1) >= k proof
per cases by NAT_1:19;
suppose S1: m = 0;
Fib (0+1+1+1) = Fib(0+1) + Fib(0+1+1) by PRE_FF:1
.= 1 + 1 by PRE_FF:1;
hence Fib (k+1) >= k by A, S1;
suppose m > 0; then
m+1 > 0+1 by REAL_1:67; then
m >= 1 by NAT_1:38; then
B: m+(m+1) >= m+1+1 by REAL_1:55;
C: k = m+1+1 by A, XCMPLX_1:1;
m < m+1 & m+1 < m+1+1 by REAL_1:69; then
m < k & m+1 < k by C, AXIOMS:22; then
D: Fib (m+1) >= m & Fib (m+1+1) >= m+1 by IH;
Fib (m+1+1+1) = Fib (m+1) + Fib (m+1+1) by PRE_FF:1; then
Fib (m+1+1+1) >= m+(m+1) by D, REAL_1:55;
hence Fib (k+1) >= k by C, B, AXIOMS:22;
end;
end;
for n being Nat holds P[n] from Comp_Ind(P);