Require Import Arith.
Require Import Peano_dec.
Require Import Constants.
Require Import Mult_compl.
Require Import Wf_nat.
Require Import euclid.
Require Import Le_lt_compl.
Require Import Euclid.
Require Import shift.
Require Import Compare_dec.
Require Import imperative.
Require Import while.
Require Import two_power.
Require Import log2_spec.

Section log2_computation.
 Variable n0 : nat.
 Hypothesis pos_n0 : 0 < n0.
 Hint Resolve pos_n0: arith.






  Record state : Set := mkstate
    {state_n : nat; state_p : nat; state_b : bool}.

  Inductive ok : state → Prop :=
    | oktrue : ∀ p : nat, n0 = two_power p → ok (mkstate one p true)
    | okfalse :
        ∀ p : nat,
        two_power p < n0 → n0 < two_power (S p) → ok (mkstate one p false).

  Let init (s : state) := state_n s = n0 ∧ state_p s = 0 ∧ state_b s = true.


  Inductive final : state → Prop :=
      mkfinal : ∀ (p : nat) (b : bool), final (mkstate one p b).


  Inductive invar : state → Prop :=
    | exact :
        ∀ n p : nat,
        n0 = two_power p × n → 0 < n → invar (mkstate n p true)
    | inexact :
        ∀ n p : nat,
        two_power p × n < n0 →
        n0 < two_power p × S n → 0 < n → invar (mkstate n p false).



  Definition stat_order := ltof state state_n.




Lemma decomp :
              ∀ s : state,
              s = mkstate (state_n s) (state_p s) (state_b s).
 Proof.
   simple induction s; simpl in |- *; auto with arith.
 Qed.


Lemma invar_inv1 :
               ∀ n p : nat,
               invar (mkstate n p true) → n0 = two_power p × n.
 Proof.
  intros; inversion_clear H; auto with arith.
 Qed.

Lemma invar_inv2 :
               ∀ n p : nat,
               invar (mkstate n p false) →
               two_power p × n < n0 ∧ n0 < two_power p × S n.
 Proof.
  intros.
  inversion_clear H; split; auto with arith.
 Qed.

Lemma invar_inv3 :
               ∀ (n p : nat) (b : bool), invar (mkstate n p b) → 0 < n.
 Proof.
  intros.
  inversion_clear H; auto with arith.
 Qed.


Lemma final_inv :
               ∀ (n p : nat) (b : bool),
               final (mkstate n p b) → n = one.
 Proof.
  intros.
  inversion_clear H; auto with arith.
 Qed.

Lemma not_final :
               ∀ (n p : nat) (b : bool),
               invar (mkstate n p b) → ¬ final (mkstate n p b) → one < n.
 Proof.
  intros.
  case (le_or_lt n one); [ intro | auto with arith ].
  cut (0 < n); [ intro | apply invar_inv3 with p b; auto with arith ].
  case (enum1 n).
  unfold two in |- *; auto with arith.
  intro; absurd (0 < n); auto with arith.
  rewrite H3; auto with arith.
  intro; absurd (final (mkstate n p b)); [ auto with arith | idtac ].
  rewrite H3; split; auto with arith.
 Qed.


Lemma wf_stat_order : well_founded stat_order.
 Proof.
  unfold stat_order in |- *; apply well_founded_ltof.
 Qed.
 Hint Resolve wf_stat_order: arith.

 Lemma log2_impl : log2_spec n0.
 Proof.
  apply Imperative with state init ok;
   [
   
   ∃ (mkstate n0 0 true)
   |
      
      intros a pre; apply while_not with init invar stat_order final a;
      [
         
         simple induction s; intros state_n0 state_p0 state_b0 i;
         elim (le_lt_eq_dec 1 state_n0); [ right | left | idtac ]
      |
         
         simple induction s; intros state_n0 state_p0 state_b0;
         elim state_b0; intros h i; elim (Unshift state_n0);
         intros m b';
         [ elim b';
            [ ∃ (mkstate m (S state_p0) true)
            | ∃ (mkstate m (S state_p0) false) ]
         | ∃ (mkstate m (S state_p0) false) ]
      | idtac
      | idtac
      | idtac
      | idtac ]
   |
      
      simple induction a; intros state_n0 state_p0 state_b0;
      elim state_b0; intro h; ∃ state_p0 ].

Hint Unfold init: arith.

split; auto; split; auto.

red in |- *; intros f; inversion f; auto.
rewrite <- H0 in a0; simpl in a0.
absurd (1 < 1); auto with arith.
rewrite <- b; constructor 1.
inversion i; auto.


  cut (one < state_n0).
  intro n_ge_1.
  2: apply not_final with state_p0 true; auto with arith.


  inversion i.


  split.
  left.
  rewrite two_power_S.
  rewrite <- mult_assoc; auto with arith.
  unfold shift in a0.
  rewrite <- a0; auto.
  unfold shift in a0.
  apply quotient_positive with state_n0 two; auto.
  rewrite mult_comm; exact a0.
  unfold stat_order, ltof in |- ×.
  apply half_lt.
  apply lt_trans with one; auto with arith.
  auto with arith.


  cut (one < state_n0).
  intro n_ge_1.
  2: apply not_final with state_p0 true; auto with arith.
  inversion i.

  split.
  right.
  rewrite two_power_S.
  rewrite <- mult_assoc; auto with arith.
  rewrite (invar_inv1 state_n0 state_p0); auto.
  rewrite b.
  unfold shift in |- ×.
  auto with arith.
  rewrite two_power_S.
  rewrite <- mult_assoc.
  rewrite (invar_inv1 state_n0 state_p0); auto.
  rewrite b.
  unfold shift in |- ×.
  apply mult_lt_l.
  auto with arith.
  simpl in |- *; auto with arith.
  case (lt_or_Zero m); auto with arith.
  intro.
  absurd (one < state_n0); auto with arith.
  rewrite b.
  rewrite H3; simpl in |- *; auto with arith.
  unfold stat_order, ltof in |- *; apply half_lt.
  simpl in |- ×.
  apply lt_trans with one; auto with arith.
  auto with arith.


  cut (one < state_n0).
  intro n_ge_1.
  2: apply not_final with state_p0 false; auto with arith.
  inversion i.

  cut (two_power (S state_p0) × m < n0).
  intro n0_left'.

  cut (n0 < two_power (S state_p0) × S m).
  intro n0_right'.

  cut (m < state_n0).
  intro m_little.

  split.
  right; auto with arith.
  case (lt_or_Zero m); auto with arith.
  intro.
  absurd (one < state_n0); auto with arith.
  simpl in b'; elim b'; intros eg; rewrite eg.
  rewrite H4; simpl in |- *; auto with arith.
  rewrite H4; simpl in |- *; auto with arith.
  unfold stat_order, ltof in |- ×.
  simpl in |- ×.
  exact m_little.


  apply half_lt.
  apply lt_trans with one; auto with arith.
  simpl in b'; elim b'; auto with arith.


  simpl in b'; elim b'; intros eg.
  apply lt_trans with (two_power state_p0 × S state_n0); auto with arith.
  rewrite two_power_S.
  rewrite <- mult_assoc; auto with arith.
  apply mult_lt_l.
  auto with arith.
  rewrite eg.
  unfold shift in |- *; simpl in |- *; auto with arith.
  replace (two_power (S state_p0) × S m) with
   (two_power state_p0 × S state_n0).
  elim (invar_inv2 state_n0 state_p0); auto with arith.
  elim H0; auto with arith.
  rewrite two_power_S.
  rewrite <- mult_assoc.
  simpl in |- ×.
  unfold shift in |- *; simpl in |- ×.
  rewrite <- plus_n_Sm.
  rewrite eg; auto with arith.


  apply le_lt_trans with (two_power state_p0 × state_n0); auto with arith.
  simpl in b'; elim b'; intro eg.
  rewrite eg.
  rewrite two_power_S.
  rewrite <- mult_assoc; auto with arith.
  rewrite eg.
  rewrite two_power_S.
  rewrite <- mult_assoc; auto with arith.

  simple induction s.
  simple induction state_b0.
  intros.
  rewrite (final_inv state_n0 state_p0 true).

  left.
  rewrite (invar_inv1 _ _ H0).
  rewrite (final_inv _ _ _ H).
  auto with arith.
  auto with arith.

  intros.
  rewrite (final_inv state_n0 state_p0 false).
  right.
  elim (invar_inv2 _ _ H0).
  rewrite (final_inv _ _ _ H).
  intros.
  rewrite <- (mult_1_r (two_power state_p0)); auto with arith.

  elim (invar_inv2 _ _ H0).
  rewrite (final_inv _ _ _ H).
  intros.
  rewrite two_power_S.
  exact H2.
  auto with arith.

  simple induction s.
  simple induction state_b0.
  intro.
  inversion_clear H.
  elim H1.
  simpl in |- *; intros.
  left.
  rewrite H; simpl in |- ×.
  rewrite <- H0; auto with arith.
  simpl in H0; rewrite H0; auto with arith.

  intro.
  inversion_clear H.
  elim H1.
  intros.
  simpl in H2.
  discriminate H2.


  auto with arith.
  auto with arith.

  left.
  inversion h; auto.

  right.
  inversion h; split; auto.

Qed.

End log2_computation.