1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
Require Import ZArith_base.
Require Import Coq.micromega.Lia.
Open Scope Z_scope.
Fixpoint fib (n: nat) : Z :=
match n with
| O => 1
| S O => 1
| S (S n as p) => fib p + fib n
end.
Axiom fib_47_computed: fib 47 = 2971215073.
Lemma fib_bound:
fib 47 < 2 ^ 32.
Proof.
pose proof fib_47_computed.
lia.
Qed.
Require Import Reals.
Require Import Coq.micromega.Lra.
Open Scope R_scope.
Fixpoint fibr (n: nat) : R :=
match n with
| O => 1
| S O => 1
| S (S n as p) => fibr p + fibr n
end.
Axiom fibr_47_computed: fibr 47 = 2971215073.
Lemma fibr_bound:
fibr 47 < 2 ^ 32.
Proof.
pose proof fibr_47_computed.
lra.
Qed.
Lemma fibr_bound':
fibr 47 < IZR (Z.pow_pos 2 32).
Proof.
pose proof fibr_47_computed.
lra.
Qed.
|
