Library additions.Fib2

From Coq Require Import NArith Ring.

From additions Require Import Monoid_instances Euclidean_Chains Pow
        Strategies Dichotomy BinaryStrat.
Import Addition_Chains.
Open Scope N_scope.

Fixpoint fib (n:nat) : N :=
  match n with
    0%nat | 1%nat ⇒ 1
  | (S ((S p) as q)) ⇒ fib p + fib q
  end.


Lemma fib_ind (P:nat→Prop) :
  P 0%nat → P 1%nat → (∀ n, P n → P (S n) → P(S (S n))) →
  ∀ n, P n.

Lemma fib_SSn : ∀ (n:nat) , fib (S (S n)) = (fib n + fib (S n)).

Definition mul2 (p q : N × N) :=
  match p, q with
    (a, b),(c,d) ⇒ (a×c + a×d + b×c, a×c + b×d)
  end.

Lemma neutral_l p : mul2 (0,1) p = p.

Lemma neutral_r p : mul2 p (0,1) = p.

#[ global ] Instance Mul2 : Monoid mul2 (0,1).


Lemma next_fib (n:nat) : mul2 (1,0) (fib (S n), fib n) =
                         (fib (S (S n)), fib (S n)).

Definition fib_mul2 n := let (a,b) := power (M:=Mul2) (1,0) n
                         in (a+b).


Lemma fib_mul2_OK_0 (n:nat) :
  power (M:=Mul2) (1,0) (S (S n)) =
  (fib (S n), fib n).

Lemma fib_mul2_OK n : fib n = fib_mul2 n.


Definition fib_pos n :=
  let (a,b) := Pos_bpow (M:= Mul2) (1,0) n in
  (a+b).



Locate chain_apply.
About chain_apply.

Definition fib_eucl gamma `{Hgamma: Strategy gamma} n :=
  let c := make_chain gamma n
  in let r := chain_apply c (M:=Mul2) (1,0) in
       fst r + snd r.



From additions Require Import AM.

Definition fib_with_chain c :=
  match chain_apply c Mul2 (1,0) with
    Some ((a,b), nil) ⇒ Some (a+b) | _ ⇒ None end.

Definition c153 := chain_gen dicho (gen_F 153%positive).