Library Phi: Hofstadter G function and the golden ratio
We consider again the function g defined by
g 0 = 0 and g (S n) = S n - g (g n),
and we prove that it can also be directly defined
via primitives using reals numbers:
g(n) = floor((n+1)/phi) = floor(tau*(n+1))
where:
In Coq, we'll use here by default operations on reals numbers,
and also:
- INR : the injection from nat to R
- IZR : the injection from Z to R
- Int_part : the integer part of a real, used as a floor function. It produces a Z integer, that we can convert to nat via Z.to_nat when necessary.
- frac_part : the faction part of a real, producing a R
Phi and tau
Definition phi := (sqrt 5 + 1)/2.
Definition tau := (sqrt 5 - 1)/2.
Lemma tau_1 : tau + 1 = phi.
Lemma tau_phi : tau × phi = 1.
Lemma tau_tau : tau × tau = 1 - tau.
Lemma tau_nz : tau ≠ 0.
Lemma phi_nz : phi ≠ 0.
Lemma tau_inv : tau = 1/phi.
Lemma tau_bound : 6/10 < tau < 7/10.
Lemma prime_5 : prime 5.
Lemma prime_irr (r:R) :
(∀ (p q:Z), Z.gcd p q = 1%Z → r × IZR q ≠ IZR p) →
(∀ (p q:Z), r × IZR q = IZR p → q=0%Z).
Lemma sqrt5_irr (p q:Z) : sqrt 5 × IZR q = IZR p → q = 0%Z.
Lemma tau_irr (p q:Z) : tau × IZR q = IZR p → q = 0%Z.