In this mini-tutorial we walk over some details of developing a short proof concerning Fibonacci numbers.

The Fibonacci sequence has been previously defined in Mizar
article `PRE_FF` as follows:

definition let n be Nat; func Fib (n) -> Element of 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 holds fib.(n+1) = [(fib.n)`2, (fib.n)`1 + (fib.n)`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 such functions). A theorem that follows, recasts the usual recursive property of the functor

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 text is put into a

environ :: mt1 begin for n being Nat holds Fib n >= n; ::> *143 *398 ::> 143: No implicit qualification ::> 398: Type expectedThe mysterious error

It is a reasonable practice for beginners to try to correct only the first parsing error, and, in general, it is advisable to deal with one error at a time.

`Nat` - the type of natural numbers is introduced in article `NAT_1`. New users find the
task of searching the Mizar library for needed definitions a big
challenge. A long lasting solution to the problem consists in getting
familiar with the library. For the beginners, the best starting
tactic is to ask someone who is more experienced. One can search the
libraries using `grep`, but the beginners have difficulty in
formulating search patterns as newcomers typically have trouble naming what
they are looking for.

In order to import the needed meaning of `Nat` we import
vocabulary `NAT_1` (for the mode symbol `Nat`),
notations from `NAT_1` (for parsing formats) and
constructors from `NAT_1` (for semantics, i.e. internal representation
of the notion). We are now left with two parsing errors.

environ :: mt2 vocabularies NAT_1; notations 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" expectedMizar processes the input text and inserts error messages into the presented file in lines starting with

Error `*143` indicates that
`Fib` is treated as an identifier of a variable and in the
above context such an identifier needs to have its type (qualification)
announced earlier. However, our intention was that `Fib`
denotes the functor for the Fibonacci sequence as defined in
`PRE_FF`. That `Fib` is indeed a functor symbol is
declared in vocabulary `PRE_FF`. We learned this by using the
`findvoc` utility which we called as

findvoc -w FibWe add vocabulary

environ :: mt3 vocabularies NAT_1, PRE_FF; notations NAT_1; constructors NAT_1; begin for n being Nat holds Fib n >= n; ::> *165*203 ::> 165: Unknown functor format ::> 203: Unknown token, maybe an illegal character used in an identifier

environ :: mt4 vocabularies NAT_1, PRE_FF; notations NAT_1, PRE_FF; constructors NAT_1, PRE_FF; begin for n being Nat holds Fib n >= n; ::> *203 ::> 203: Unknown token, maybe an illegal character used in an identifierThe term

definition let x,y be ext-real number; pred x <= y means :: XXREAL_0:def 5 ... definiens omitted ... reflexivity; connectedness; end; reserve a,b,c,d for ext-real number; notation let a,b; synonym b >= a for a <= b; antonym b < a for a <= b; antonym a > b for a <= b; end;

We need to import notations and constructors from `XXREAL_0`.
But this will not suffice to make the `>=` predicate
understood. The predicate as defined in `XXREAL_0` takes arguments of
type `ext-real number` which are real numbers extended with
positive and negative infinity. To use the `>=` predicate
in our text we need to import information that the types of terms we use as
arguments of `>=` widen to extended real numbers. This is
achieved through importing `registrations`.

- Importing registrations from
`XXREAL_0`imports (among others)registration cluster natural -> ext-real number; end;

which states that every natural number is also an extended real number. - Importing registrations from
`ORDINAL1`imports (among others)registration cluster -> natural Element of omega; end;

We need this registration because the type returned by`Fib`is`Element of NAT`. (`NAT`is a synonym for`omega`, see`NUMBERS`.) The above registration states that every`Element of NAT`has also the attribute`natural`. With this information, the type of`Fib n`widens also to an extended real due to the previous registration imported from`XXREAL_0`.The last paragraph may seem mysterious but explaining more details right now would complicate the story even more.

environ :: mt5 vocabularies XXREAL_0, NAT_1, PRE_FF; notations NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; begin for n being Nat holds Fib n >= n; ::> *4 ::> 4: This inference is not acceptedIt seems that we have built the right conceptual environment to formulate our goal as we are left with one purely logical message. We can now focus on proving.

The proof is to be done by induction for which we employ
scheme `NAT_1:sch 2` (`NatInd`) defined in article
`NAT_1` as follows.

scheme :: NAT_1:sch 2 NatInd { P[Nat] } : for k being Nat holds P[k] provided P[0] and for k be Nat st P[k] holds P[k + 1];A scheme provides a pattern for obtaining theorems. From the above scheme, we get a theorem for each actual predicate used in the place of the formal predicate named

In order to get access to the scheme we use the `schemes`
directive in the environment. We also try to formulate the premises for the
application of the scheme.

environ :: mt6 vocabularies XXREAL_0, NAT_1, PRE_FF; notations NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; schemes NAT_1; begin P1: Fib 0 >= 0; ::> *143 P2: for n being Nat st Fib n >= n holds Fib (n+1) >= n+1; ::> *203 for n being Nat holds Fib n >= n from NAT_1:sch 2(P1, P2); ::> 143: No implicit qualification ::> 203: Unknown token, maybe an illegal character used in an identifierIn the current version of Mizar, the symbol for 0 (zero) is introduced in vocabulary

environ :: mt6a vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; schemes NAT_1; begin P1: Fib 0 >= 0; ::> *4 P2: for n being Nat st Fib n >= n holds Fib (n+1) >= n+1; ::> *203 for n being Nat holds Fib n >= n from NAT_1:sch 2(P1, P2); ::> 4: This inference is not accepted ::> 203: Unknown token, maybe an illegal character used in an identifierNote that we did not add

We postpone dealing with the not accepted inference and first resolve
the notational error with the symbol `+` for addition. First we
find the vocabulary which declares `+` and it is `ARYTM_3`.

environ :: mt6b vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; schemes NAT_1; begin P1: Fib 0 >= 0; ::> *4 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 NAT_1:sch 2(P1, P2); ::> 4: This inference is not accepted ::> 103: Unknown functorSmall constants like

The documentation of available requirement packages is very sparse; some information is contained in.absfiles with the base name of the requirement package. For the list of these names seemml.txtin thedocdirectory of your Mizar installation.

After adding the requirements directive, we have a situation where
numeral 1 is understood as a natural number and the symbol + for
addition is understood as (re)defined in `NAT_1`. The term
`(n+1)` is typed `Element of NAT`, has the attribute
`natural` and can be used as an argument of `Fib`.

environ :: mt7 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; requirements SUBSET, NUMERALS; 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 NAT_1:sch 2(P1, P2); ::> *23 ::> 4: This inference is not accepted ::> 23: Invalid order of arguments in the instantiated predicateNote how the propositions labeled

Error `*23` relates to the formal parameter of induction, the
predicate `P`. The actual formula corresponding to this
formal predicate must be explicitly stated using the `defpred`
macro facility.
We could have used a different name than P in `defpred`
but by some coincidence we have not.

environ :: mt7a vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; requirements SUBSET, NUMERALS; 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 NAT_1:sch 2(P1, P2); ::> 4: This inference is not acceptedThis instance of

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.

`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 prove (induction loading) and making it
a conjunction of inequalities about two subsequent terms of the
Fibonacci sequence. After making appropriate adjustments we are
faced by the following text.

environ :: mt8 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; requirements SUBSET, NUMERALS; 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 for n being Nat holds P[n] from NAT_1:sch 2(P1, P2); ::> 4: This inference is not acceptedThe first premise of the induction scheme should easily follow from the theorem

environ :: mt9 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; requirements SUBSET, NUMERALS; schemes NAT_1; begin defpred P[Nat] means Fib $1 >= $1 & Fib ($1+1) >= $1+1; P1: P[0] by PRE_FF:1; ::> *144,203 P2: for n being Nat st P[n] holds P[n+1]; ::> *4 for n being Nat holds P[n] from NAT_1:sch 2(P1, P2); ::> 4: This inference is not accepted ::> 144: Unknown label ::> 203: Unknown token, maybe an illegal character used in an identifierWhenever we make a library reference, in this case to

environ :: mt10 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; requirements SUBSET, NUMERALS; 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 NAT_1:sch 2(P1, P2); ::> 4: This inference is not acceptedThe first error is due to the fact that Mizar does not see that 0+1 = 1. Mizar is able to automatically process arithmetic expressions involving equalities, but this ability becomes available when we import requirements

environ :: mt10a vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; requirements SUBSET, NUMERALS, BOOLE, ARITHM; 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 NAT_1:sch 2(P1, P2); ::> 4: This inference is not accepted

In order to justify the second premise of the induction scheme, we
write a proof whose structure is dictated by the proposition that we
are proving. The proof starts with a `let` since we are
proving a universally quantified formula.

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 formula labeled

Note that in the term `n+1+1` we did not insert parentheses as
Mizar binary infix operators associate to the left.

In order to prove the yet unjustified conclusion, we consider two
cases: either `n` is zero or it is bigger than zero. For this
we employ the `per cases` 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 end; suppose S1: n > 0; thus Fib (n+1+1) >= n+1+1; ::> *4 end; end;The

per cases by NAT_1:3; suppose S1: n = 0; thus Fib (n+1+1) >= n+1+1; ::> *4 end; suppose S1: n > 0; thus Fib (n+1+1) >= n+1+1; ::> *4 end;The theorem

theorem :: NAT_1:3 0 <> i implies 0 < i;We add

Unfortunately, the conclusion in the first case (when `n = 0`) is
false as `Fib 2` is 1. The formula that we tried to prove was
simply false and realizing this fact so late is a bit embarrassing.
However, it shows that mechanical proof-checking systems may have some
future ;-)

The simple remedy in our case is to upgrade the claim 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 get.

environ :: mt14 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1; requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL; 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:3; suppose S1: n = 0; thus Fib (n+1+1+1) >= n+1+1; ::> *4 end; suppose S1: n > 0; thus Fib (n+1+1+1) >= n+1+1; ::> *4 end; end; for n being Nat holds P[n] from NAT_1:sch 2(P1, P2); ::> 4: This inference is not acceptedPlease note that we added requirements

The proof of the first case is immediate from `PRE_FF:1` with the
use 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; end;In the proof of the second case we first use

theorem :: XREAL_1:9 a <= b & c <= d implies a+c <= b+d;and thus we add

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, XREAL_1:9; ::> *190 thus Fib (n+1+1+1) >= n+1+1; ::> *4 end; end; for n being Nat holds P[n] from NAT_1:sch 2(P1, P2); ::> 4: This inference is not accepted ::> 190: Inaccessible theorem

Theorem `XREAL_1:9` is about real numbers while our current
environment does not import all information necessary to access the
theorem. There is a utility named `constr` which assists us in
such situations. Calling

constr -f text/mt15a.miz XREAL_1:9informs us that we need to import constructors from

Unfortunately, there is no utility, probably there can not be one, that can tell which registrations are needed in a particular context to proceed as we plan. One needs to know parts of the Mizar library.

The new environment section is now:

environ :: mt16 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, XREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1, XREAL_0; requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL; theorems PRE_FF, NAT_1, XREAL_1; schemes NAT_1; begin

We continue proving the second case.
First, we state that `n` is at least `1`
in order to get that `n+(n+1)` is at least `n+1+1`.

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, XREAL_1:9; n >= 1 by S1, NAT_1:14; then n+(n+1) >= n+1+1 by XREAL_1:9; thus Fib (n+1+1+1) >= n+1+1; ::> *4 end;Here is the new theorem that we referred to.

theorem :: NAT_1:14 j < 1 implies j = 0;This theorem works as

At this moment, it is enough to use transitivity of `>=`
to complete the proof.
The transitivity of less than or equal appears as a theorem in article
`XXREAL_0`.

theorem :: XXREAL_0:2 a <= b & b <= c implies a <= c;Note that

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, XREAL_1:9; n >= 1 by S1, NAT_1:14; then n+(n+1) >= n+1+1 by XREAL_1:9; hence Fib (n+1+1+1) >= n+1+1 by A, B, XXREAL_0:2; end;Here is the complete text of our development.

environ :: mt18 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, XREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1, XREAL_0; requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL; theorems PRE_FF, NAT_1, XREAL_1, XXREAL_0; 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:3; 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; end; 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, XREAL_1:9; n >= 1 by S1, NAT_1:14; then n+(n+1) >= n+1+1 by XREAL_1:9; hence Fib (n+1+1+1) >= n+1+1 by A, B, XXREAL_0:2; end; end; for n being Nat holds P[n] from NAT_1:sch 2(P1, P2);From the last proposition we can infer a simpler statement in which we skip the second conjunct behind

then for n being Nat holds Fib (n+1) >= n;

Look at a proof of the same theorem using complete (course of values) induction.

environ :: mt_cov999 vocabularies XXREAL_0, NAT_1, PRE_FF, CARD_1, ARYTM_3; notations NUMBERS, NAT_1, XXREAL_0, PRE_FF; constructors NAT_1, XXREAL_0, XREAL_0, PRE_FF; registrations XXREAL_0, ORDINAL1, XREAL_0; requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL; theorems PRE_FF, NAT_1, XREAL_1, XXREAL_0; 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 NAT_1:26; hence Fib (k+1) >= k by PRE_FF:1; end; suppose 1 < k; then 1+1 <= k by NAT_1:13; then consider m being Nat such that A: k = 1+1+m by NAT_1:10; thus Fib (k+1) >= k proof per cases by NAT_1:3; 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; end; suppose m > 0; then m >= 1 by NAT_1:14; then B: m+(m+1) >= m+1+1 by XREAL_1:9; m < m+1 & m+1 < m+1+1 by XREAL_1:31; then m < k & m+1 < k by A, XXREAL_0:2; then C: 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 C, XREAL_1:9; hence Fib (k+1) >= k by A, B, XXREAL_0:2; end; end; end; end; for n being Nat holds P[n] from NAT_1:sch 4(P); then for n being Nat holds Fib(n+1) >= n;