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.