diff options
author | thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-18 13:17:20 +0000 |
---|---|---|
committer | thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-18 13:17:20 +0000 |
commit | ae4c0218bb7544a0791620e83024fcc930606bba (patch) | |
tree | 63ec55440200bd65f6d9189170d0c488167ddaab /theories/Ints/num/Nbasic.v | |
parent | 04123975b05b5f275b16d2f16ff7a9a7da09be6e (diff) |
Correct height computation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9892 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Ints/num/Nbasic.v')
-rw-r--r-- | theories/Ints/num/Nbasic.v | 100 |
1 files changed, 98 insertions, 2 deletions
diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v index 23229b52c..e2ce06425 100644 --- a/theories/Ints/num/Nbasic.v +++ b/theories/Ints/num/Nbasic.v @@ -1,6 +1,102 @@ Require Import ZArith. +Require Import ZAux. +Require Import ZDivModAux. Require Import Basic_type. +(* To compute the necessary height *) + +Fixpoint plength (p: positive) : positive := + match p with + xH => xH + | xO p1 => Psucc (plength p1) + | xI p1 => Psucc (plength p1) + end. + +Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z. +assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z). +intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z. +rewrite Zpower_exp; auto with zarith. +rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. +intros p; elim p; simpl plength; auto. +intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI. +assert (tmp: (forall p, 2 * p = p + p)%Z); + try repeat rewrite tmp; auto with zarith. +intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1). +assert (tmp: (forall p, 2 * p = p + p)%Z); + try repeat rewrite tmp; auto with zarith. +rewrite ZPowerAux.Zpower_exp_1; auto with zarith. +Qed. + +Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z. +intros p; case (Psucc_pred p); intros H1. +subst; simpl plength. +rewrite ZPowerAux.Zpower_exp_1; auto with zarith. +pattern p at 1; rewrite <- H1. +rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. +generalize (plength_correct (Ppred p)); auto with zarith. +Qed. + +Definition Pdiv p q := + match Zdiv (Zpos p) (Zpos q) with + Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with + Z0 => q1 + | _ => (Psucc q1) + end + | _ => xH + end. + +Theorem Pdiv_le: forall p q, + Zpos p <= Zpos q * Zpos (Pdiv p q). +intros p q. +unfold Pdiv. +assert (H1: Zpos q > 0); auto with zarith. +assert (H1b: Zpos p >= 0); auto with zarith. +generalize (Z_div_ge0 (Zpos p) (Zpos q) H1 H1b). +generalize (Z_div_mod_eq (Zpos p) (Zpos q) H1); case Zdiv. + intros HH _; rewrite HH; rewrite Zmult_0_r; rewrite Zmult_1_r; simpl. +case (Z_mod_lt (Zpos p) (Zpos q) H1); auto with zarith. +intros q1 H2. +replace (Zpos p - Zpos q * Zpos q1) with (Zpos p mod Zpos q). + 2: pattern (Zpos p) at 2; rewrite H2; auto with zarith. +generalize H2 (Z_mod_lt (Zpos p) (Zpos q) H1); clear H2; + case Zmod. + intros HH _; rewrite HH; auto with zarith. + intros r1 HH (_,HH1); rewrite HH; rewrite Zpos_succ_morphism. + unfold Zsucc; rewrite Zmult_plus_distr_r; auto with zarith. + intros r1 _ (HH,_); case HH; auto. +intros q1 HH; rewrite HH. +unfold Zge; simpl Zcompare; intros HH1; case HH1; auto. +Qed. + +Definition is_one p := match p with xH => true | _ => false end. + +Theorem is_one_one: forall p, is_one p = true -> p = xH. +intros p; case p; auto; intros p1 H1; discriminate H1. +Qed. + +Definition get_height digits p := + let r := Pdiv p digits in + if is_one r then xH else Psucc (plength (Ppred r)). + +Theorem get_height_correct: + forall digits N, + Zpos N <= Zpos digits * (2 ^ (Zpos (get_height digits N) -1)). +intros digits N. +unfold get_height. +assert (H1 := Pdiv_le N digits). +case_eq (is_one (Pdiv N digits)); intros H2. +rewrite (is_one_one _ H2) in H1. +rewrite Zmult_1_r in H1. +change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto. +clear H2. +apply Zle_trans with (1 := H1). +apply Zmult_le_compat_l; auto with zarith. +rewrite Zpos_succ_morphism; unfold Zsucc. +rewrite Zplus_comm; rewrite Zminus_plus. +apply plength_pred_correct. +Qed. + + Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n. fix zn2z_word_comm 2. @@ -115,7 +211,7 @@ Section CompareRec. Fixpoint compare0_mn (n:nat) : word wm n -> comparison := match n return word wm n -> comparison with - | 0 => compare0_m + | O => compare0_m | S m => fun x => match x with | W0 => Eq @@ -129,7 +225,7 @@ Section CompareRec. Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := match n return word wm n -> w -> comparison with - | 0 => compare_m + | O => compare_m | S m => fun x y => match x with | W0 => compare w_0 y |