Require Import Constants.
Require Import generation.
Require Import monoid.
Require Import machine.
Require Import strategies.
Require Import spec.
Require Import log2_spec.
Require Import log2_implementation.
Require Import Compare_dec.

Require Import while.
Require Import imperative.
Require Import develop.
Require Import dicho_strat.
Require Import binary_strat.
Require Import trivial.
Require Import standard.
Require Import monofun.
Require Import matrix.
Require Import ZArith.

Definition code_gen (s : strategy) := chain_algo s log2_impl.
Definition power_algo_r (s : strategy) := power_algo s log2_impl.

Theorem addchains :
 ∀ (gamma : strategy) (n : nat) (M : Set) (MO : monoid M) (a : M),
 {b : M | b = power M MO a n}.
Proof.
 intros gamma n M MO a; elim (zerop n); intro H;
  [ ∃ (u M MO)
  | ∃
     (config_X M
        (Exec M MO
           match power_algo gamma log2_impl n H with
           | addchain_spec_intro gc ⇒
               match gc with
               | gencode_intro co _ ⇒ co
               end
           end (config M a (emptystack M)))) ].
 rewrite H; auto with arith.
 elim (power_algo gamma log2_impl n H); intro g; elim g; intros co s.
 inversion_clear s.
 rewrite H0; simpl in |- *; auto with arith.
Qed.

Definition dic := dicho log2_impl.

Opaque matrix.


Lemma fibonacci : ∀ n : nat, {q : Z | q = Z_of_nat (Fib n)}.

refine
 (fun n ⇒
  match zerop n with
  | left _ ⇒ exist _ 1%Z _
  | right _ ⇒
      match addchains dic n Mat2 matrix fib_mat with
      | exist m _ ⇒ exist _ (M11 m) _
      end
  end).

rewrite e; rewrite Unfold_FibO; auto with arith.
rewrite fib_computation.
 rewrite e; auto with arith.
auto with arith.
Qed.

Transparent matrix.