diff options
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v | 356 |
1 files changed, 0 insertions, 356 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v deleted file mode 100644 index a2df2600..00000000 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v +++ /dev/null @@ -1,356 +0,0 @@ - -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) -(************************************************************************) - -Set Implicit Arguments. - -Require Import ZArith. -Require Import BigNumPrelude. -Require Import DoubleType. -Require Import DoubleBase. - -Local Open Scope Z_scope. - -Section DoubleSub. - Variable w : Type. - Variable w_0 : w. - Variable w_Bm1 : w. - Variable w_WW : w -> w -> zn2z w. - Variable ww_Bm1 : zn2z w. - Variable w_opp_c : w -> carry w. - Variable w_opp_carry : w -> w. - Variable w_pred_c : w -> carry w. - Variable w_sub_c : w -> w -> carry w. - Variable w_sub_carry_c : w -> w -> carry w. - Variable w_opp : w -> w. - Variable w_pred : w -> w. - Variable w_sub : w -> w -> w. - Variable w_sub_carry : w -> w -> w. - - (* ** Opposites ** *) - Definition ww_opp_c x := - match x with - | W0 => C0 W0 - | WW xh xl => - match w_opp_c xl with - | C0 _ => - match w_opp_c xh with - | C0 h => C0 W0 - | C1 h => C1 (WW h w_0) - end - | C1 l => C1 (WW (w_opp_carry xh) l) - end - end. - - Definition ww_opp x := - match x with - | W0 => W0 - | WW xh xl => - match w_opp_c xl with - | C0 _ => WW (w_opp xh) w_0 - | C1 l => WW (w_opp_carry xh) l - end - end. - - Definition ww_opp_carry x := - match x with - | W0 => ww_Bm1 - | WW xh xl => w_WW (w_opp_carry xh) (w_opp_carry xl) - end. - - Definition ww_pred_c x := - match x with - | W0 => C1 ww_Bm1 - | WW xh xl => - match w_pred_c xl with - | C0 l => C0 (w_WW xh l) - | C1 _ => - match w_pred_c xh with - | C0 h => C0 (WW h w_Bm1) - | C1 _ => C1 ww_Bm1 - end - end - end. - - Definition ww_pred x := - match x with - | W0 => ww_Bm1 - | WW xh xl => - match w_pred_c xl with - | C0 l => w_WW xh l - | C1 l => WW (w_pred xh) w_Bm1 - end - end. - - Definition ww_sub_c x y := - match y, x with - | W0, _ => C0 x - | WW yh yl, W0 => ww_opp_c (WW yh yl) - | WW yh yl, WW xh xl => - match w_sub_c xl yl with - | C0 l => - match w_sub_c xh yh with - | C0 h => C0 (w_WW h l) - | C1 h => C1 (WW h l) - end - | C1 l => - match w_sub_carry_c xh yh with - | C0 h => C0 (WW h l) - | C1 h => C1 (WW h l) - end - end - end. - - Definition ww_sub x y := - match y, x with - | W0, _ => x - | WW yh yl, W0 => ww_opp (WW yh yl) - | WW yh yl, WW xh xl => - match w_sub_c xl yl with - | C0 l => w_WW (w_sub xh yh) l - | C1 l => WW (w_sub_carry xh yh) l - end - end. - - Definition ww_sub_carry_c x y := - match y, x with - | W0, W0 => C1 ww_Bm1 - | W0, WW xh xl => ww_pred_c (WW xh xl) - | WW yh yl, W0 => C1 (ww_opp_carry (WW yh yl)) - | WW yh yl, WW xh xl => - match w_sub_carry_c xl yl with - | C0 l => - match w_sub_c xh yh with - | C0 h => C0 (w_WW h l) - | C1 h => C1 (WW h l) - end - | C1 l => - match w_sub_carry_c xh yh with - | C0 h => C0 (w_WW h l) - | C1 h => C1 (w_WW h l) - end - end - end. - - Definition ww_sub_carry x y := - match y, x with - | W0, W0 => ww_Bm1 - | W0, WW xh xl => ww_pred (WW xh xl) - | WW yh yl, W0 => ww_opp_carry (WW yh yl) - | WW yh yl, WW xh xl => - match w_sub_carry_c xl yl with - | C0 l => w_WW (w_sub xh yh) l - | C1 l => w_WW (w_sub_carry xh yh) l - end - end. - - (*Section DoubleProof.*) - Variable w_digits : positive. - Variable w_to_Z : w -> Z. - - - Notation wB := (base w_digits). - Notation wwB := (base (ww_digits w_digits)). - Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). - Notation "[+| c |]" := - (interp_carry 1 wB w_to_Z c) (at level 0, c at level 99). - Notation "[-| c |]" := - (interp_carry (-1) wB w_to_Z c) (at level 0, c at level 99). - - Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99). - Notation "[+[ c ]]" := - (interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, c at level 99). - Notation "[-[ c ]]" := - (interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c) - (at level 0, c at level 99). - - Variable spec_w_0 : [|w_0|] = 0. - Variable spec_w_Bm1 : [|w_Bm1|] = wB - 1. - Variable spec_ww_Bm1 : [[ww_Bm1]] = wwB - 1. - Variable spec_to_Z : forall x, 0 <= [|x|] < wB. - Variable spec_w_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|]. - - Variable spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|]. - Variable spec_opp : forall x, [|w_opp x|] = (-[|x|]) mod wB. - Variable spec_opp_carry : forall x, [|w_opp_carry x|] = wB - [|x|] - 1. - - Variable spec_pred_c : forall x, [-|w_pred_c x|] = [|x|] - 1. - Variable spec_sub_c : forall x y, [-|w_sub_c x y|] = [|x|] - [|y|]. - Variable spec_sub_carry_c : - forall x y, [-|w_sub_carry_c x y|] = [|x|] - [|y|] - 1. - - Variable spec_pred : forall x, [|w_pred x|] = ([|x|] - 1) mod wB. - Variable spec_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB. - Variable spec_sub_carry : - forall x y, [|w_sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB. - - - Lemma spec_ww_opp_c : forall x, [-[ww_opp_c x]] = -[[x]]. - Proof. - destruct x as [ |xh xl];simpl. reflexivity. - rewrite Z.opp_add_distr;generalize (spec_opp_c xl);destruct (w_opp_c xl) - as [l|l];intros H;unfold interp_carry in H;rewrite <- H; - rewrite <- Z.mul_opp_l. - assert ([|l|] = 0). - assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);omega. - rewrite H0;generalize (spec_opp_c xh);destruct (w_opp_c xh) - as [h|h];intros H1;unfold interp_carry in *;rewrite <- H1. - assert ([|h|] = 0). - assert (H3:= spec_to_Z h);assert (H2 := spec_to_Z xh);omega. - rewrite H2;reflexivity. - simpl ww_to_Z;rewrite wwB_wBwB;rewrite spec_w_0;ring. - unfold interp_carry;simpl ww_to_Z;rewrite wwB_wBwB;rewrite spec_opp_carry; - ring. - Qed. - - Lemma spec_ww_opp : forall x, [[ww_opp x]] = (-[[x]]) mod wwB. - Proof. - destruct x as [ |xh xl];simpl. reflexivity. - rewrite Z.opp_add_distr, <- Z.mul_opp_l. - generalize (spec_opp_c xl);destruct (w_opp_c xl) - as [l|l];intros H;unfold interp_carry in H;rewrite <- H;simpl ww_to_Z. - rewrite spec_w_0;rewrite Z.add_0_r;rewrite wwB_wBwB. - assert ([|l|] = 0). - assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);omega. - rewrite H0;rewrite Z.add_0_r; rewrite Z.pow_2_r; - rewrite Zmult_mod_distr_r;try apply lt_0_wB. - rewrite spec_opp;trivial. - apply Zmod_unique with (q:= -1). - exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW (w_opp_carry xh) l)). - rewrite spec_opp_carry;rewrite wwB_wBwB;ring. - Qed. - - Lemma spec_ww_opp_carry : forall x, [[ww_opp_carry x]] = wwB - [[x]] - 1. - Proof. - destruct x as [ |xh xl];simpl. rewrite spec_ww_Bm1;ring. - rewrite spec_w_WW;simpl;repeat rewrite spec_opp_carry;rewrite wwB_wBwB;ring. - Qed. - - Lemma spec_ww_pred_c : forall x, [-[ww_pred_c x]] = [[x]] - 1. - Proof. - destruct x as [ |xh xl];unfold ww_pred_c. - unfold interp_carry;rewrite spec_ww_Bm1;simpl ww_to_Z;ring. - simpl ww_to_Z;replace (([|xh|]*wB+[|xl|])-1) with ([|xh|]*wB+([|xl|]-1)). - 2:ring. generalize (spec_pred_c xl);destruct (w_pred_c xl) as [l|l]; - intros H;unfold interp_carry in H;rewrite <- H. simpl;apply spec_w_WW. - rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. - assert ([|l|] = wB - 1). - assert (H1:= spec_to_Z l);assert (H2 := spec_to_Z xl);omega. - rewrite H0;change ([|xh|] + -1) with ([|xh|] - 1). - generalize (spec_pred_c xh);destruct (w_pred_c xh) as [h|h]; - intros H1;unfold interp_carry in H1;rewrite <- H1. - simpl;rewrite spec_w_Bm1;ring. - assert ([|h|] = wB - 1). - assert (H3:= spec_to_Z h);assert (H2 := spec_to_Z xh);omega. - rewrite H2;unfold interp_carry;rewrite spec_ww_Bm1;rewrite wwB_wBwB;ring. - Qed. - - Lemma spec_ww_sub_c : forall x y, [-[ww_sub_c x y]] = [[x]] - [[y]]. - Proof. - destruct y as [ |yh yl];simpl. ring. - destruct x as [ |xh xl];simpl. exact (spec_ww_opp_c (WW yh yl)). - replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|])) - with (([|xh|]-[|yh|])*wB + ([|xl|]-[|yl|])). 2:ring. - generalize (spec_sub_c xl yl);destruct (w_sub_c xl yl) as [l|l];intros H; - unfold interp_carry in H;rewrite <- H. - generalize (spec_sub_c xh yh);destruct (w_sub_c xh yh) as [h|h];intros H1; - unfold interp_carry in H1;rewrite <- H1;unfold interp_carry; - try rewrite spec_w_WW;simpl ww_to_Z;try rewrite wwB_wBwB;ring. - rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. - change ([|xh|] - [|yh|] + -1) with ([|xh|] - [|yh|] - 1). - generalize (spec_sub_carry_c xh yh);destruct (w_sub_carry_c xh yh) as [h|h]; - intros H1;unfold interp_carry in *;rewrite <- H1;simpl ww_to_Z; - try rewrite wwB_wBwB;ring. - Qed. - - Lemma spec_ww_sub_carry_c : - forall x y, [-[ww_sub_carry_c x y]] = [[x]] - [[y]] - 1. - Proof. - destruct y as [ |yh yl];simpl. - unfold Z.sub;simpl;rewrite Z.add_0_r;exact (spec_ww_pred_c x). - destruct x as [ |xh xl]. - unfold interp_carry;rewrite spec_w_WW;simpl ww_to_Z;rewrite wwB_wBwB; - repeat rewrite spec_opp_carry;ring. - simpl ww_to_Z. - replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|]) - 1) - with (([|xh|]-[|yh|])*wB + ([|xl|]-[|yl|]-1)). 2:ring. - generalize (spec_sub_carry_c xl yl);destruct (w_sub_carry_c xl yl) - as [l|l];intros H;unfold interp_carry in H;rewrite <- H. - generalize (spec_sub_c xh yh);destruct (w_sub_c xh yh) as [h|h];intros H1; - unfold interp_carry in H1;rewrite <- H1;unfold interp_carry; - try rewrite spec_w_WW;simpl ww_to_Z;try rewrite wwB_wBwB;ring. - rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. - change ([|xh|] - [|yh|] + -1) with ([|xh|] - [|yh|] - 1). - generalize (spec_sub_carry_c xh yh);destruct (w_sub_carry_c xh yh) as [h|h]; - intros H1;unfold interp_carry in *;rewrite <- H1;try rewrite spec_w_WW; - simpl ww_to_Z; try rewrite wwB_wBwB;ring. - Qed. - - Lemma spec_ww_pred : forall x, [[ww_pred x]] = ([[x]] - 1) mod wwB. - Proof. - destruct x as [ |xh xl];simpl. - apply Zmod_unique with (-1). apply spec_ww_to_Z;trivial. - rewrite spec_ww_Bm1;ring. - replace ([|xh|]*wB + [|xl|] - 1) with ([|xh|]*wB + ([|xl|] - 1)). 2:ring. - generalize (spec_pred_c xl);destruct (w_pred_c xl) as [l|l];intro H; - unfold interp_carry in H;rewrite <- H;simpl ww_to_Z. - rewrite Zmod_small. apply spec_w_WW. - exact (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW xh l)). - rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. - change ([|xh|] + -1) with ([|xh|] - 1). - assert ([|l|] = wB - 1). - assert (H1:= spec_to_Z l);assert (H2:= spec_to_Z xl);omega. - rewrite (mod_wwB w_digits w_to_Z);trivial. - rewrite spec_pred;rewrite spec_w_Bm1;rewrite <- H0;trivial. - Qed. - - Lemma spec_ww_sub : forall x y, [[ww_sub x y]] = ([[x]] - [[y]]) mod wwB. - Proof. - destruct y as [ |yh yl];simpl. - ring_simplify ([[x]] - 0);rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial. - destruct x as [ |xh xl];simpl. exact (spec_ww_opp (WW yh yl)). - replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|])) - with (([|xh|] - [|yh|]) * wB + ([|xl|] - [|yl|])). 2:ring. - generalize (spec_sub_c xl yl);destruct (w_sub_c xl yl)as[l|l];intros H; - unfold interp_carry in H;rewrite <- H. - rewrite spec_w_WW;rewrite (mod_wwB w_digits w_to_Z spec_to_Z). - rewrite spec_sub;trivial. - simpl ww_to_Z;rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. - rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub_carry;trivial. - Qed. - - Lemma spec_ww_sub_carry : - forall x y, [[ww_sub_carry x y]] = ([[x]] - [[y]] - 1) mod wwB. - Proof. - destruct y as [ |yh yl];simpl. - ring_simplify ([[x]] - 0);exact (spec_ww_pred x). - destruct x as [ |xh xl];simpl. - apply Zmod_unique with (-1). - apply spec_ww_to_Z;trivial. - fold (ww_opp_carry (WW yh yl)). - rewrite (spec_ww_opp_carry (WW yh yl));simpl ww_to_Z;ring. - replace ([|xh|] * wB + [|xl|] - ([|yh|] * wB + [|yl|]) - 1) - with (([|xh|] - [|yh|]) * wB + ([|xl|] - [|yl|] - 1)). 2:ring. - generalize (spec_sub_carry_c xl yl);destruct (w_sub_carry_c xl yl)as[l|l]; - intros H;unfold interp_carry in H;rewrite <- H;rewrite spec_w_WW. - rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub;trivial. - rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. - rewrite (mod_wwB w_digits w_to_Z spec_to_Z);rewrite spec_sub_carry;trivial. - Qed. - -(* End DoubleProof. *) - -End DoubleSub. - - - - - |