diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 80 |
1 files changed, 37 insertions, 43 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index 3d44f96b..e6c5a0e0 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,16 +8,16 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: DoubleBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. -Require Import ZArith. +Require Import ZArith Ndigits. Require Import BigNumPrelude. Require Import DoubleType. Local Open Scope Z_scope. +Local Infix "<<" := Pos.shiftl_nat (at level 30). + Section DoubleBase. Variable w : Type. Variable w_0 : w. @@ -70,13 +70,7 @@ Section DoubleBase. end end. - Fixpoint double_digits (n:nat) : positive := - match n with - | O => w_digits - | S n => xO (double_digits n) - end. - - Definition double_wB n := base (double_digits n). + Definition double_wB n := base (w_digits << n). Fixpoint double_to_Z (n:nat) : word w n -> Z := match n return word w n -> Z with @@ -167,11 +161,7 @@ Section DoubleBase. Variable spec_w_0W : forall l, [[w_0W l]] = [|l|]. Variable spec_to_Z : forall x, 0 <= [|x|] < wB. Variable spec_w_compare : forall x y, - match w_compare x y with - | Eq => [|x|] = [|y|] - | Lt => [|x|] < [|y|] - | Gt => [|x|] > [|y|] - end. + w_compare x y = Zcompare [|x|] [|y|]. Lemma wwB_wBwB : wwB = wB^2. Proof. @@ -297,11 +287,10 @@ Section DoubleBase. Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n). Proof. intros n;unfold double_wB;simpl. - unfold base;rewrite (Zpos_xO (double_digits n)). - replace (2 * Zpos (double_digits n)) with - (Zpos (double_digits n) + Zpos (double_digits n)). + unfold base. rewrite Pshiftl_nat_S, (Zpos_xO (_ << _)). + replace (2 * Zpos (w_digits << n)) with + (Zpos (w_digits << n) + Zpos (w_digits << n)) by ring. symmetry; apply Zpower_exp;intro;discriminate. - ring. Qed. Lemma double_wB_pos: @@ -315,7 +304,7 @@ Section DoubleBase. Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. intros n; elim n; clear n; auto. - unfold double_wB, double_digits; auto with zarith. + unfold double_wB, "<<"; auto with zarith. intros n H1; rewrite <- double_wB_wwB. apply Zle_trans with (wB * 1). rewrite Zmult_1_r; apply Zle_refl. @@ -408,35 +397,40 @@ Section DoubleBase. intros a b c d H1; apply beta_lex_inv with (1 := H1); auto. Qed. + Ltac comp2ord := match goal with + | |- Lt = (?x ?= ?y) => symmetry; change (x < y) + | |- Gt = (?x ?= ?y) => symmetry; change (x > y); apply Zlt_gt + end. + Lemma spec_ww_compare : forall x y, - match ww_compare x y with - | Eq => [[x]] = [[y]] - | Lt => [[x]] < [[y]] - | Gt => [[x]] > [[y]] - end. + ww_compare x y = Zcompare [[x]] [[y]]. Proof. destruct x as [ |xh xl];destruct y as [ |yh yl];simpl;trivial. - generalize (spec_w_compare w_0 yh);destruct (w_compare w_0 yh); - intros H;rewrite spec_w_0 in H. - rewrite <- H;simpl;rewrite <- spec_w_0;apply spec_w_compare. - change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0. + (* 1st case *) + rewrite 2 spec_w_compare, spec_w_0. + destruct (Zcompare_spec 0 [|yh|]) as [H|H|H]. + rewrite <- H;simpl. reflexivity. + symmetry. change (0 < [|yh|]*wB+[|yl|]). + change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. - absurd (0 <= [|yh|]). apply Zgt_not_le;trivial. + absurd (0 <= [|yh|]). apply Zlt_not_le; trivial. destruct (spec_to_Z yh);trivial. - generalize (spec_w_compare xh w_0);destruct (w_compare xh w_0); - intros H;rewrite spec_w_0 in H. - rewrite H;simpl;rewrite <- spec_w_0;apply spec_w_compare. - absurd (0 <= [|xh|]). apply Zgt_not_le;apply Zlt_gt;trivial. + (* 2nd case *) + rewrite 2 spec_w_compare, spec_w_0. + destruct (Zcompare_spec [|xh|] 0) as [H|H|H]. + rewrite H;simpl;reflexivity. + absurd (0 <= [|xh|]). apply Zlt_not_le; trivial. destruct (spec_to_Z xh);trivial. - apply Zlt_gt;change 0 with (0*wB+0);pattern 0 at 2;rewrite <- spec_w_0. - apply wB_lex_inv;apply Zgt_lt;trivial. - - generalize (spec_w_compare xh yh);destruct (w_compare xh yh);intros H. - rewrite H;generalize (spec_w_compare xl yl);destruct (w_compare xl yl); - intros H1;[rewrite H1|apply Zplus_lt_compat_l|apply Zplus_gt_compat_l]; - trivial. + comp2ord. + change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. - apply Zlt_gt;apply wB_lex_inv;apply Zgt_lt;trivial. + (* 3rd case *) + rewrite 2 spec_w_compare. + destruct (Zcompare_spec [|xh|] [|yh|]) as [H|H|H]. + rewrite H. + symmetry. apply Zcompare_plus_compat. + comp2ord. apply wB_lex_inv;trivial. + comp2ord. apply wB_lex_inv;trivial. Qed. |