Library hydras.solutions_exercises.FibonacciPR
The famous Fibonacci function
Fixpoint fib (n:nat) : nat :=
match n with
| 0 ⇒ 1
| 1 ⇒ 1
| S ((S p) as q) ⇒ fib q + fib p
end.
Section Proof_of_FibIsPR.
To do : Some parts of this proof may be made more generic
let us consider another definition of fib, as an application of
nat_rec
Let fib_step (p: nat × nat) := (fst p + snd p, fst p).
Let fib_iter n p:= (nat_rec (fun _ ⇒ (nat×nat)%type)
p
(fun _ p ⇒ fib_step p)
n).
Definition fib_alt n := snd (fib_iter n (1,1)).
The theory of primitive functions deals only with functions
of type naryFunc n.
So, let us define a variant of fib_alt
Import LispAbbreviations.
Check cPair.
Print car.
Check car.
Check cdr.
Search cPair isPR.
Search car isPR.
Search car cdr cPair.
Let fib_step_cPair p := cPair (car p + cdr p)
(car p).
Let fib_iter_cPair n p := nat_rec (fun _ ⇒ nat)
p
(fun _ p ⇒ fib_step_cPair p)
n.
Definition fibPR n := cdr (fib_iter_cPair n (cPair 1 1)).
Let us prove that fibPR is PR
Ok, but we must prove that fibPR is extensionaly equal to fib
let us consider the following relation
Definition inv (p: nat×nat) (c: nat) := c = cPair (fst p) (snd p).
Lemma inv_Pi : ∀ p c, inv p c → snd p = cPairPi2 c.
Lemma L0: inv (1,1) (cPair 1 1).
Lemma LS : ∀ p c, inv p c → inv (fib_step p) (fib_step_cPair c).
Lemma L1 : ∀ p c,
inv p c → ∀ n,
inv (fib_iter n p)
(fib_iter_cPair n c).
Lemma L2 : extEqual 1 fib_alt fibPR.
#[export] Instance fib_altIsPR : isPR 1 fib_alt.
It remains to prove that fib_alt is equivalent to the "classical" fib
Lemma fib_OK0 : ∀ n,
fib_iter n (1,1) = (fib (S n), fib n).
Lemma fib_alt_Ok : extEqual 1 fib fib_alt.
#[export] Instance fibIsPR : isPR 1 fib.
End Proof_of_FibIsPR.
Too long !
Time Compute fibPR 3.