Require Import strategies.
Require Import Arith.
Require Import euclid.
Require Import shift.
Require Import two_power.
Require Import log2_spec.
Require Import Euclid.
Require Import Le_lt_compl.
Require Import Mult_compl.
Require Import Constants.

Section import_log2.
Variable log2_r : n : nat, 0 < n log2_spec n.

Lemma dicho : strategy.
Proof.
split.
intros n H.
elim (ceiling_log2 log2_r n).
2: apply lt_trans with four; unfold one, four in |- *; auto with arith.
intros x y.
elim y; intros.
cut (0 < 2).
2: auto with arith.
intro H'.
elim (quotient 2 H' x); intros.
refine match quotient (two_power x0) _ n with
| exist n _exist _ n _
end.

unfold gt in |- ×.
apply lt_le_trans with 1; auto with arith.

elim p; intros.
elim e; intros.
elim H2; intros H4 H5.
elim H3; intros H6 H7.
clear y p e H2 H3 H'.
cut (0 < x0).
2: case (lt_or_Zero x0); [ auto with arith | intro ].
2: cut (x one).
2: intro.
2: absurd (n two).
2: unfold not in |- *; intro.
2: absurd (four < two).
2: apply le_not_lt; auto with arith.
2: unfold four, two in |- *; auto with arith.
2: apply lt_le_trans with n; auto with arith.
2: replace two with (two_power one).
2: apply le_trans with (two_power x).
2: auto with arith.
2: apply two_power_le; auto with arith.
2: simpl in |- *; auto with arith.
2: rewrite H4; rewrite H2; simpl in |- *; auto with arith.
intro x0_pos.
cut (1 < two_power x0).
2: replace 1 with (two_power 0).
2: apply two_power_mono; auto with arith.
2: simpl in |- *; auto with arith.
intro H8.  cut (x0 < x).
2: rewrite H4.
2: apply lt_le_trans with (x0 × 2).
2: rewrite mult_comm; apply mult_p_lt_qp; auto with arith.
2: auto with arith.
intro H9.
cut (x0 pred x).
2: apply le_S_n.
2: elim (S_pred _ _ H9).
2: auto with arith.
intro H10.
cut (0 < n0).
2: case (lt_or_Zero n0); [ auto with arith | intro ].
2: absurd (n < two_power x0).
2: apply le_not_lt.
2: apply le_trans with (two_power (pred x)).
2: apply two_power_le; auto with arith.
2: auto with arith.
2: rewrite H6; rewrite H2; simpl in |- ×.
2: auto with arith.
intro H11.  split.
apply lt_le_trans with (n0 × two_power x0).
rewrite mult_comm; apply mult_p_lt_qp; auto with arith.
rewrite H6; auto with arith.

apply not_lt_le.
unfold not in |- *; intro H12.
case (enum1 n0 H12); intro.
absurd (0 < n0); [ rewrite H2; auto with arith | auto with arith ].

cut (n < two_power (S x0)).
2: rewrite H6.
2: rewrite H2.
2: rewrite mult_1_l.
2: rewrite two_power_S.
2: rewrite mult_comm; simpl in |- ×.
2: rewrite <- plus_n_O.
2: apply plus_lt_compat_l.
2: auto with arith.
intro.
cut (two_power x0 n).
intro H13.
cut (S x0 x); [ intro H14 | auto with arith ].
case (le_lt_or_eq _ _ H14); intro.
cut (S x0 pred x); [ intro | auto with arith ].
absurd (n < n); [ auto with arith | idtac ].
apply lt_trans with (two_power (S x0)).
auto with arith.
apply le_lt_trans with (two_power (pred x)).
apply two_power_le; auto with arith.
auto with arith.

cut (x0 1).
intro H16.
absurd (n < four).
apply lt_asym.
auto with arith.

apply lt_le_trans with (two_power (S x0)).
auto with arith.
replace four with (two_power 2).
apply two_power_le; auto with arith.
unfold four in |- *; simpl in |- *; auto with arith.
apply (fun p n m : natplus_le_reg_l n m p) with x0.
replace (x0 + x0) with (x0 × 2).
rewrite plus_comm; simpl in |- ×.
apply le_trans with x.
rewrite H4; auto with arith.
elim H15; auto with arith.
rewrite mult_comm; simpl in |- *; rewrite <- plus_n_O; auto with arith.
rewrite <- (mult_1_l (two_power x0)).
elim H2; rewrite H6; auto with arith.
Qed.

End import_log2.