(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(*  ---                        two_power.v                             ---  *)
(*                                                                          *)
(* Author: Pierre Casteran.                                                 *)
(*    LABRI, URA CNRS 1304,                                                 *)
(*    Departement d'Informatique, Universite Bordeaux I,                    *)
(*    33405 Talence CEDEX,                                                  *)
(*    e-mail:  casteran@labri.u-bordeaux.fr                                 *)



(* 
   The integer powers of 2 are fundamental in computer science;
   so we wrote this module, the results of which are used mainly
   in the "log2_spec" module.
*)



Require Import Arith.
Require Import Peano_dec.
Require Import Constants.
Require Import Mult_compl.
Require Import Le_lt_compl.


(* 2 at the n *)
(**************)

Fixpoint two_power (m : nat) : nat :=
  match m with
  | O => 1
  | S n => two * two_power n
  end.

Lemma zero_lt_pow : forall a : nat, 0 < two_power a.
(********************************************)
Proof.
(* Goal: forall a : nat, lt O (two_power a) *)
 simple induction a; simpl in |- *.
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: forall (n p z : nat) (_ : lt (two_power n) z) (_ : lt z (two_power (S n))) (_ : lt (two_power p) z) (_ : lt z (two_power (S p))), @eq nat n p *)
 intros.
(* Goal: lt (two_power n) z *)
 apply lt_plus_trans; auto with arith.
Qed.
Hint Resolve zero_lt_pow: arith.


Lemma two_power_S : forall n : nat, two_power (S n) = two_power n * two.
(**************************************************)
Proof.
(* Goal: lt (two_power n) z *)
 intros; unfold two_power at 1 in |- *; rewrite mult_comm; auto with arith.
Qed.


Lemma two_power_S_lt : forall n : nat, two_power n < two_power (S n).
(***************************************************************)
Proof.
(* Goal: forall n : nat, lt (two_power n) (two_power (S n)) *)
 intro; rewrite two_power_S.
(* Goal: lt (two_power n) z *)
 rewrite mult_comm; apply mult_p_lt_qp; auto with arith.
Qed.


Lemma two_power_mono : forall n p : nat, n < p -> two_power n < two_power p.
(*************************************************************)
Proof.
(* Goal: forall (n p : nat) (_ : lt n p), lt (two_power n) (two_power p) *)
 simple induction 1.
(* Goal: lt (two_power n) z *)
 intros; apply two_power_S_lt; auto with arith.
(* Goal: forall (n p z : nat) (_ : lt (two_power n) z) (_ : lt z (two_power (S n))) (_ : lt (two_power p) z) (_ : lt z (two_power (S p))), @eq nat n p *)
 intros.
(* Goal: lt (two_power n) z *)
 apply lt_trans with (two_power m); auto with arith.
(* Goal: lt (two_power n) z *)
 apply two_power_S_lt; auto with arith.
Qed.


Lemma two_power_le : forall n p : nat, n <= p -> two_power n <= two_power p.
(**************************************************************)
Proof.
(* Goal: forall (n p : nat) (_ : le n p), le (two_power n) (two_power p) *)
 intros n p H; case (le_lt_or_eq _ _ H); intro H1.
(* Goal: lt (two_power n) z *)
 apply lt_le_weak; apply two_power_mono; auto with arith.
(* Goal: lt (two_power n) z *)
 rewrite H1; auto with arith.
Qed.

Lemma two_power_monoR : forall n p : nat, two_power n < two_power p -> n < p.
(****************************************************************)
Proof.
(* Goal: forall (n p z : nat) (_ : lt (two_power n) z) (_ : lt z (two_power (S n))) (_ : lt (two_power p) z) (_ : lt z (two_power (S p))), @eq nat n p *)
 intros.
(* Goal: lt n p *)
 apply not_le_lt.
(* Goal: not (le p n) *)
 unfold not in |- *; intro.
(* Goal: False *)
 elim (lt_not_le (two_power n) (two_power p) H).
(* Goal: le (two_power p) (two_power n) *)
 case (le_lt_or_eq p n H0); intro.
(* Goal: le (two_power p) (two_power n) *)
(* Goal: le (two_power p) (two_power n) *)
 apply lt_le_weak.
(* Goal: lt (two_power n) z *)
 apply two_power_mono; auto with arith.
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: lt (two_power n) z *)
 rewrite H1; auto with arith.
Qed.


(* if 2^n < z <2^(n+1), then z cannot be a power of 2 ! *)
(*********************************************************)

Lemma holes_in_powers :
 forall n z : nat,
 two_power n < z -> z < two_power (S n) -> forall p : nat, z <> two_power p.
(**************************************************************)
Proof.
(* Goal: forall (n p z : nat) (_ : lt (two_power n) z) (_ : lt z (two_power (S n))) (_ : lt (two_power p) z) (_ : lt z (two_power (S p))), @eq nat n p *)
 unfold not in |- *; intros.
(* Goal: False *)
 cut (n < p).
(* Goal: forall _ : lt p (S n), False *)
(* Goal: lt p (S n) *)
(* Goal: lt n p *)
 intro.
(* Goal: False *)
(* Goal: lt n p *)
 cut (p < S n).
(* Goal: forall _ : lt p (S n), False *)
(* Goal: lt p (S n) *)
(* Goal: lt n p *)
 intro.
(* Goal: lt (two_power n) z *)
 case (lt_not_lt n p); auto with arith.
(* Goal: lt n p *)
 apply two_power_monoR.
(* Goal: lt (two_power n) z *)
 elim H1; auto with arith.
(* Goal: lt n p *)
 apply two_power_monoR.
(* Goal: lt (two_power n) z *)
 elim H1; auto with arith.
Qed.


(* the intervals ]2^n,2^(n+1)[ are pairwise disjoint *)
(*****************************************************)

Lemma log2_unicity :
 forall n p z : nat,
 two_power n < z ->
 z < two_power (S n) -> two_power p < z -> z < two_power (S p) -> n = p.
Proof.
(* Goal: forall (n p z : nat) (_ : lt (two_power n) z) (_ : lt z (two_power (S n))) (_ : lt (two_power p) z) (_ : lt z (two_power (S p))), @eq nat n p *)
 intros.
(* Goal: forall (n p z : nat) (_ : lt (two_power n) z) (_ : lt z (two_power (S n))) (_ : lt (two_power p) z) (_ : lt z (two_power (S p))), @eq nat n p *)
 case (le_or_lt n p); intros.		                     
(* Goal: forall (n p z : nat) (_ : lt (two_power n) z) (_ : lt z (two_power (S n))) (_ : lt (two_power p) z) (_ : lt z (two_power (S p))), @eq nat n p *)
 case (le_lt_or_eq n p H3); intros.
(* Goal: @eq nat n p *)
 absurd (z < z).
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: lt z z *)
(* Goal: @eq nat n p *)
(* Goal: @eq nat n p *)
 apply lt_trans with (two_power (S n)).
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: lt (two_power (S n)) z *)
(* Goal: @eq nat n p *)
(* Goal: @eq nat n p *)
 apply le_lt_trans with (two_power p).
(* Goal: lt (two_power n) z *)
 apply two_power_le; auto with arith.
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: @eq nat n p *)
 absurd (z < z).
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: lt z z *)
 apply lt_trans with (two_power (S p)).
(* Goal: lt (two_power n) z *)
 auto with arith.
(* Goal: lt (two_power (S p)) z *)
 apply le_lt_trans with (two_power n).
(* Goal: lt (two_power n) z *)
 apply two_power_le; auto with arith.
(* Goal: lt (two_power n) z *)
 auto with arith.
Qed.