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 Fib. In the sequel, we will
frequently refer to this theorem, which in other
circumstances is 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 text is put into a .miz file and checked by the
Mizar processor. Unfortunately, Mizar could not 'understand' the text
in the empty environment and we got the following errors.
environ :: mt1
begin
for n being Nat holds Fib n >= n;
::> *143 *398
::> 143: No implicit qualification
::> 398: Type expected
The mysterious error *143 under Nat means that in
this context Nat is treated as an unknown identifier. (The
"No implicit qualification" comment relates to the lack of the
reserve construct but we will not explain more here in order
to avoid discussing constructs which we will not use.)
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" 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
while new error messages are usually inserted. As a result, we work with one
text file which we edit and which is modified by Mizar during processing.
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 Fib
We add vocabulary PRE_FF to the environment and obtain
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
Fib is now 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 this article.
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 identifier
The term Fib n seems to be understood by Mizar but now we need
to import vocabulary in which the >= is defined.
The greater than or equal relation
that we want to use is defined in article
XXREAL_0 as a synonym for
less than or equal with swapped arguments.
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.
registration
cluster natural -> ext-real number;
end;
which states that every natural number is also an extended real number.
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 accepted
It 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 P in the scheme. This formal predicate
takes one natural number argument. Each application of this scheme depends
on two premises corresponding to the formulas listed after
provided in the scheme declaration.
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 identifier
In the current version of Mizar, the symbol for 0 (zero) is introduced
in vocabulary CARD_1 as a functor symbol. A functor using
this symbol is defined as a synonym for empty set in article NUMBERS (also in CARD_1) and then redefined in
NUMBERS such that 0 is
typed as Element of NAT. We add vocabulary CARD_1 to
the vocabularies directive and NUMBERS to notations and
obtain.
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 identifier
Note that we did not add NUMBERS to constructors. We did not
have to do this as importing constructors for NAT_1 brought the
constructors from NUMBERS to our environment. However, listing
NUMBERS on the constructors' list would not cause any problems.
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 functor
Small constants
like 1, 2 and so on up to 16 bit unsigned integers
are built-in but by default are typed as set. In order to
use them as natural numbers one has to use the environment directive
requirements. This directive enables default processing of
certain objects; we will not comment more on this feature at this
point. In our case, we need requirement package named NUMERALS which
provides the needed properties of small numerals. We also
need requirements SUBSET on which NUMERALS depend.
The documentation of available requirement packages is very sparse; some information is contained in .abs files with the base name of the requirement package. For the list of these names see mml.txt in the doc directory 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 predicate
Note how the propositions labeled P1 and P2, which
form the premises of induction, are now
understood but not accepted as the Mizar checker does not see why
they are true without some justification.
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 accepted
This instance of defpred defines a one place predicate
P such that later occurrences like P[n] are
understood as Fib n >= n. In
defpred, the symbol $1 refers to the first parameter
of the defined predicate; $2 would refer to the second parameter
if there was one, and so on.
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 accepted
The first premise of the induction scheme should easily follow from
the theorem PRE_FF:1 about the Fibonacci sequence. However, we get:
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 identifier
Whenever we make a library reference, in this case to PRE_FF:1, the
name of the article whose theorems we want to access must appear
in the library directive theorems.
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 accepted
The 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 ARITHM (which depend also on
requirements BOOLE) and thus we obtain:
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 IH (for Induction Hypothesis) is really
P[n] expanded as defined by defpred. After making the
assumption we are to prove P[n+1] which when expanded is
a conjunction. We conclude each conjunct in a separate thus.
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 construct requires justification of the disjunction
of all the suppose conditions.
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 NAT_1:3 states that for natural numbers we have:
theorem :: NAT_1:3 0 <> i implies 0 < i;We add NAT_1 to the theorems directive in order to be able to refer to this theorem.
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 accepted
Please note that we added requirements REAL. In order to justify
the claim labeled P1 we need the fact that 1 >= 0.
This fact becomes obvious with requirements REAL. By now, we have
imported all requirements available in the current version of Mizar.
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 PRE_FF:1. Then,
we add the sides of inequalities from the inductive hypothesis labeled
IH. To justify this step, we refer to theorem
XREAL_1:9.
theorem :: XREAL_1:9 a <= b & c <= d implies a+c <= b+d;and thus we add XREAL_1 to the theorems directive. Even with this addition we run into a new problem.
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:9
informs us that we need to import constructors from XREAL_0
in order to access theorem XREAL_1:9 in our file named
text/mt15a.miz. (Constructors from XREAL_0 provide
internal information about attribute real.) We also import
registrations from XREAL_0
which are needed to
establish the relationship between real numbers and other numbers, in
particular that a natural number is a real number.
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 n >= 1 is an antonym of n < 1 and the > predicate is irreflexive (as an antonym to a reflexive predicate).
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 n >= 1 is a synonym for 1 <= n. The second case of our proof is completed as follows:
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 P[n].
then for n being Nat holds Fib (n+1) >= n;
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;