Library FunG: Hofstadter's G function and tree

Require Import Arith Omega Wf_nat List NPeano.
Require Import DeltaList Fib.
Set Implicit Arguments.

Study of the functional equation:

G (S n) + G (G n) = S n
G 0 = 0

and its relationship with the Fibonacci sequence.

References:

Hofstadter's book: Goedel, Escher, Bach, page 137.
Sequence A005206 on the Online Encyclopedia of Integer Sequences http://oeis.org/A005206

Statement of the G equations as an inductive relation.

Inductive G : nat → nat → Prop :=
| G0 : G 0 0
| GS n a b c : G n a → G a b → S n = c +b → G (S n) c.
Hint Constructors G.

Lemma G1 : G 1 1.
Hint Resolve G1.

Lemma GS_inv n a : G (S n) a →
∃ b c, G n b ∧ G b c ∧ S n = a + c.

A first upper bound on G. It is used for proving that G is a total function.

Lemma G_le n a : G n a → a ≤ n.
Hint Resolve G_le.

Lemma G_rec (P:nat→Set) :
P 0 →
(∀ n, P n → (∀ a, G n a → P a) → P (S n)) →
∀ n, P n.

The G relation is indeed functional:

Lemma G_fun n a a´ : G n a → G n a´ → a = a´.

The g function, implementing the G relation.

Definition g_spec n : { a : nat | G n a }.

Definition g n := let (a,_) := (g_spec n) in a.

Lemma g_correct n : G n (g n).
Hint Resolve g_correct.

Lemma g_complete n p : G n p ↔ p = g n.

The initial equations, formulated for g

Lemma g_0 : g 0 = 0.

Lemma g_eqn n : g (S n) + g (g n) = S n.

Same, with subtraction

Lemma g_S n : g (S n) = S n - g (g n).

Properties of g

Lemma g_unique f :
  f 0 = 0 →
  (∀ n, S n = f (S n)+f(f n)) →
  ∀ n, f n = g n.

Lemma g_step n : g (S n) = g n ∨ g (S n) = S (g n).

Lemma g_mono_S n : g n ≤ g (S n).

Lemma g_mono n m : n ≤ m → g n ≤ g m.

NB : in Coq, for natural numbers, 3-5 = 0 (truncated subtraction)

Lemma g_lipschitz n m : g m - g n ≤ m - n.

Lemma g_nonzero n : 0 < n → 0 < g n.

Lemma g_0_inv n : g n = 0 → n = 0.

Lemma g_nz n : n ≠ 0 → g n ≠ 0.

Lemma g_fix n : g n = n ↔ n ≤ 1.

Lemma g_le n : g n ≤ n.

Lemma g_lt n : 1<n → g n < n.
Hint Resolve g_lt.

Two special formulations for g_step

Lemma g_next n a : g n = a → (g (S n) ≠ a ↔ g (S n) = S a).

Lemma g_prev n a : n ≠ 0 → g n = a →
(g (n -1) ≠ a ↔ g (n -1) = a - 1).

g cannot stay flat very long

Lemma g_nonflat n : g (S n) = g n → g (S (S n)) = S (g n).

Lemma g_nonflat´ n : g (S n) = g n → g (n -1) = g n - 1.

Lemma g_SS n : S (g n) ≤ g (S (S n)).

Lemma g_double_le n : n ≤ g (2×n).

Lemma g_div2_le n : n /2 ≤ g n.

Antecedents by g

Study of the reverse problem g(x) = a for some a.

Lemma g_max_two_antecedents a n m :
g n = a → g m = a → n <m → m = S n.

Another formulation of the same fact

Lemma g_inv n m :
g n = g m → (n = m ∨ n = S m ∨ m = S n).

g is an onto map

Lemma g_onto a : ∃ n, g n = a.

The G tree

g can be related to a infinite tree where:

nodes are labeled via a breadth-first traversal
from the label of a child node, g give the label of the father node.

9 10 11 12 13
 \/   |  \ /
  6   7   8
   \ /   /
    4   5
     \ /
      3
      |
      2
      |
      1

We already proved that g is onto, hence each node has at least one child. A node is said to be unary if the node label has exactly one antecedent, and the node is said multary otherwise. We first prove that a multary node is actually binary.

Definition Unary (g:nat→nat) a :=
∀ n m, g n = a → g m = a → n = m.

Definition Multary g a := ¬ Unary g a.

Definition Binary (g:nat→nat) a :=
∃ n m,
g n = a ∧ g m = a ∧ n ≠ m ∧
∀ k, g k = a → k = n ∨ k = m.

Lemma multary_binary a : Multary g a ↔ Binary g a.

We could even exhibit at least one child for each node

Definition rchild n := n + g n.

rightmost son, always there

Definition lchild n := n + g n - 1.

left son, if there's one

Lemma rightmost_child_carac a n : g n = a →
(g (S n) = S a ↔ n = rchild a).

Lemma g_onto_eqn a : g (rchild a) = a.

This provides easily a first relationship between g and Fibonacci numbers

Lemma g_fib n : n ≠ 0 → g (fib (S n)) = fib n.

Lemma g_fib´ n : 1 < n → g (fib n) = fib (n -1).

Lemma g_Sfib n : 1 < n → g (S (fib (S n))) = S (fib n).

Lemma g_Sfib´ n : 2 < n → g (S (fib n)) = S (fib (n -1)).

Shape of the G tree

Let's study now the shape of the G tree. First, we prove various characterisation of Unary and Binary

Lemma g_children a n : g n = a →
n = rchild a ∨ n = lchild a.

Lemma g_lchild a :
g (lchild a) = a - 1 ∨ g (lchild a) = a.

Lemma unary_carac1 a :
Unary g a ↔ ∀ n, g n = a → n = rchild a.

Lemma unary_carac2 a :
Unary g a ↔ g (lchild a) = a - 1.

Lemma binary_carac1 a :
Multary g a ↔ a ≠ 0 ∧ ∀ n, (g n = a ↔ n = rchild a ∨ n = lchild a).

Lemma binary_carac2 a :
Multary g a ↔ (a ≠ 0 ∧ g (lchild a) = a ).

Lemma unary_or_multary n : Unary g n ∨ Multary g n.

Lemma unary_xor_multary n : Unary g n → Multary g n → False.

Now we state the arity of node children

Lemma leftmost_son_is_binary n p :
  g p = n → g (p -1) ≠ n → Multary g p.

Lemma unary_rchild_is_binary n : n ≠ 0 →
  Unary g n → Multary g (rchild n).

Lemma binary_lchild_is_binary n :
  Multary g n → Multary g (lchild n).

Lemma binary_rchild_is_unary n :
  Multary g n → Unary g (rchild n).

Hence the shape of the G tree is a repetition of this pattern:

where n and p and r=n+q are binary nodes and q=p+1=n+g(n) is unary.

Fractal aspect : each binary nodes (e.g. n, p and r above) have the same infinite shape of tree above them (which is the shape of G apart from special initial nodes 1 2):

     A           A
     |           |
     .       A   .
     |        \ /
 G = .     A = .

Another equation about g

This one will be used later when flipping G left/right.

Lemma g_alt_eqn n : g n + g (g (S n) - 1) = n.

Depth in the G tree

The depth of a node in the G tree is the number of iteration of g needed before reaching node 1

Notation "f ^^ n" := (nat_iter n f) (at level 30, right associativity).

Lemma iter_S (f:nat→nat) n p : (f ^^(S n )) p = (f ^^n) (f p).

Require Import Program Program.Wf.

Program Fixpoint depth (n:nat) { measure n } : nat :=
match n with
| 0 ⇒ 0
| 1 ⇒ 0
| _ ⇒ S (depth (g n))
end.

Lemma depth_SS n : depth (S (S n)) = S (depth (g (S (S n)))).

Lemma depth_eqn n : 1<n → depth n = S (depth (g n)).

Lemma g_depth n : depth (g n) = depth n - 1.

Lemma depth_correct n : n ≠ 0 → (g ^^(depth n )) n = 1.

Lemma depth_minimal n : 1<n → 1 < ((g ^^(depth n - 1)) n ).

Lemma depth_mono n m : n ≤ m → depth n ≤ depth m.

Lemma depth_fib k : depth (fib k) = k -2.

Lemma depth_Sfib k : 1 < k → depth (S (fib k)) = k -1.

Lemma depth_0 n : depth n = 0 ↔ n ≤ 1.

Lemma depth_carac k n : k ≠ 0 →
(depth n = k ↔ S (fib (S k)) ≤ n ≤ fib (S (S k))).

Conclusion: for k>0,

1+fib (k+1) is the leftmost node at depth k
fib (k+2) is the rightmost node at depth k
hence we have fib (k+2) - fib (k+1) = fib k nodes at depth k.

Alternatively, we could also have considered

U(k) : number of unary nodes at depth k
B(k) : number binary nodes at depth k

and their recursive equations:

U(k+1) = B(k)
B(k+1) = U(k)+B(k)

These numbers are also Fibonacci numbers (except when k=0), along with the number of nodes at depth k which is U(k)+B(k).

Lemma map_S_pred l : ¬In 0 l → map S (map pred l) = l.

g and Fibonacci decomposition.

We now prove that g is simply "shifting" the Fibonacci decomposition of a number, i.e. removing 1 at all the ranks in this decomposition.

For proving this result, we need to consider relaxed decompositions where consecutive fibonacci terms may occur (but still no fib 0 nor fib 1 in the decomposition). These decompositions aren't unique. We consider here these decomposition with the lowest terms first, to ease the following proof.

Lemma g_sumfib l :
Delta 1 (0::l) → g (sumfib (List.map S l)) = sumfib l.

Lemma g_sumfib´ l : Delta 1 (1::l) →
g (sumfib l) = sumfib (map pred l).

same result, for canonical decomposition expressed in rev order

Lemma g_sumfib_rev l : ¬In 0 l → ¬In 1 l → DeltaRev 2 l →
g (sumfib l) = sumfib (map pred l).

Beware! In the previous statements, map pred l might not be a canonical decomposition anymore, since 1 could appear. In this case, 1 could be turned into a 2 (since fib 1 = fib 2), and then we should saturate with Fibonacci equations (fib 2 + fib 3 = fib 4, etc) to regain a canonical decomposition (with no consecutive fib terms), see Fib.norm.

g and classification of Fibonacci decompositions.

Most of these results will be used in next file about the flipped G tree.

Lemma g_Low n k : 2<k → Fib.Low 2 n k → Fib.Low 2 (g n) (k -1).

Lemma g_Low´ n k : 2<k → Fib.Low 1 n k → Fib.Low 1 (g n) (k -1).

Lemma g_Two n : Fib.Two 2 n → g (S n) = g n.

Lemma g_Two_iff n : Fib.Two 2 n ↔ g (S n) = g n.

Lemma g_not_Two n : ¬Fib.Two 2 n → g (S n) = S (g n).

Lemma Two_g n : Fib.Two 2 n → Fib.Even 2 (g n).

Lemma Three_g n : Fib.Three 2 n → Fib.Two 2 (g n).

Lemma ThreeOdd_Sg n : Fib.ThreeOdd 2 n → Fib.ThreeEven 1 (S (g n)).

Lemma ThreeEven_Sg n : Fib.ThreeEven 2 n → Fib.ThreeOdd 2 (S (g n)).

Lemma High_g n : Fib.High 2 n → ¬Fib.Two 2 (g n).

Lemma High_Sg n : Fib.High 2 n → Fib.Even 2 (S (g n)).

Lemma Odd_g n : Fib.Odd 2 n → Fib.Even 2 (g n).

Lemma Even_g n : Fib.Even 2 n → ¬Fib.Two 2 n → Fib.Odd 2 (g n).

Lemma Odd_gP n : Fib.Odd 2 n → g (n -1) = g n.

Lemma Even_gP n : Fib.Even 2 n → g (n -1) = (g n ) - 1.

Lemma g_pred_fib_odd k : g (pred (fib (2×k +1))) = fib (2×k).

Lemma g_pred_fib_even k : g (pred (fib (2×k))) = fib (2×k -1) - 1.

Lemma g_pred_pred_fib k : g (fib k - 2) = fib (k -1) - 1.

Fibonacci decomposition and G node arity

Lemma decomp_rchild l : Delta 1 (1::l) →
rchild (sumfib l) = sumfib (map S l).

Lemma decomp_unary n : Fib.Odd 2 n → Unary g n.

Lemma decomp_binary n : Fib.Even 2 n → Binary g n.

Lemma decomp_unary_iff n : Fib.Odd 2 n ↔ (n ≠0 ∧ Unary g n ).

Lemma decomp_binary_iff n : Fib.Even 2 n ↔ Binary g n.

g and "delta" equations

We can characterize g via its "delta" (a.k.a increments). Let d(n) = g(n+1)-g(n). For all n:

a) if d(n) = 0 then d(n+1) = 1
b) if d(n) ≠ 0 then d(n+1) = 1 - d(g(n))

In fact these deltas are always 0 or 1.

Definition d n := g (S n) - g n.

Lemma delta_0_1 n : d n = 0 ∨ d n = 1.

Lemma delta_a n : d n = 0 → d (S n) = 1.

Lemma delta_b n :
d n = 1 → d (S n) + d (g n) = 1.

A short formula giving delta: This could be used to define g.

Lemma delta_eqn n :
d (S n) = 1 - d n × d (g n).

Lemma g_alt_def n :
g (S (S n)) = S (g (S n)) - (g (S n) - g n ) × (g (S (g n)) - g (g n)).

GD is a relational presentation of G via these "delta" equations.

Inductive GD : nat → nat → Prop :=
| GD_0 : GD 0 0
| GD_1 : GD 1 1
| GD_a n x : GD n x → GD (S n) x → GD (2+n) (S x)
| GD_b n x y z : GD n x → GD (S n) y → x ≠ y →
GD x z → GD (S x) z → GD (2+n) (S y)
| GD_b´ n x y z t : GD n x → GD (S n) y → x ≠ y →
GD x z → GD (S x) t → z ≠ t → GD (2+n) y.
Hint Constructors GD.

There is only one implementation of GD

Lemma GD_unique n k k´ : GD n k → GD n k´ → k = k´.

g is an implementation of GD (hence the only one).

Lemma g_implements_GD n : GD n (g n).