Module div2


Require Export Zextensions.

Require Export pow.

 

Fixpoint ceildiv2' [n : nat] : nat :=

 Cases n of

   O => O

  | (S O) => (S O)

  | (S (S n)) => (S (ceildiv2' n))

 end.

 

Lemma two_step_ind:

 (P : nat ->  Prop)

 (P O) -> (P (S O)) -> ((n : nat) (P n) ->  (P (S (S n)))) -> (n : nat)  (P n).

 

Lemma ceildiv2_aux_lemma:

 (n : nat)

  (mult (S (S O)) (ceildiv2' n)) = n \/

  (mult (S (S O)) (ceildiv2' n)) = (plus n (S O)).

 

Definition ceildiv2:

 (n : nat)

  {p : nat | (mult (S (S O)) p) = n \/ (mult (S (S O)) p) = (plus n (S O))}.

 

Fixpoint floordiv2 [n : nat] : nat :=

 Cases n of (S (S n)) => (S (floordiv2 n)) | _ => O end.

 

Lemma floordiv2_ge: (n : nat)  (le (mult (S (S O)) (floordiv2 n)) n).

 

Lemma ceildiv2_eq: (n : nat)  (plus (ceildiv2' n) (floordiv2 n)) = n.

 

Lemma hdiv_decrease:

 (h, h' : nat)

 (lt (S O) h) ->

 (mult (S (S O)) h') = h \/ (mult (S (S O)) h') = (plus h (S O)) ->  (lt h' h).

 

Lemma pow_decompose:

 (b : Z)

 (h : nat)  (pow b h) = (Zmult (pow b (ceildiv2' h)) (pow b (floordiv2 h))).

 

Lemma ceildiv2_characteristic:

 (h, h' : nat)

 <nat> (mult (S (S O)) h') = h \/ <nat> (mult (S (S O)) h') = (plus h (S O)) ->

  (ceildiv2' h) = h'.

 

Lemma pow_ceil_ge_pow_floor:

 (b : Z)

 (Zlt ZERO b) -> (h : nat)  (Zle (pow b (floordiv2 h)) (pow b (ceildiv2' h))).

 

Lemma ceildivPos: (h : nat) (lt O h) ->  (lt O (ceildiv2' h)).

 

Lemma floordiv2_le_ceildiv2: (h : nat)  (le (floordiv2 h) (ceildiv2' h)).

 

Theorem le_ceildiv2': (n : nat)  (le (ceildiv2' n) n).

Hint arith := Resolve le_ceildiv2'.

 

Theorem lt_ceildiv2': (n : nat) (lt (S O) n) ->  (lt (ceildiv2' n) n).

 

Theorem lt_floordiv: (n : nat) (lt (S O) n) ->  (lt O (floordiv2 n)).
Index
This page has been generated by coqdoc