diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:59 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:59 +0000 |
commit | d2bd5d87d23d443f6e41496bdfe5f8e82d675634 (patch) | |
tree | d9cb49b25b4e49ccda4dd424ef2595f53d9e61c0 /theories/Numbers | |
parent | f1c9bb9d37e3bcefb5838c57e7ae45923d99c4ff (diff) |
Modularization of BinInt, related fixes in the stdlib
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers')
-rw-r--r-- | theories/Numbers/BigNumPrelude.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 216 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 4 |
6 files changed, 12 insertions, 220 deletions
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index a60a13eb3..26850688e 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -100,7 +100,7 @@ Hint Resolve Zlt_gt Zle_ge Z_div_pos: zarith. intros b x y (Hx1,Hx2) (Hy1,Hy2);split;auto with zarith. apply Zle_trans with ((b-1)*(b-1)). apply Zmult_le_compat;auto with zarith. - apply Zeq_le;ring. + apply Zeq_le; ring. Qed. Lemma sum_mul_carry : forall xh xl yh yl wc cc beta, @@ -313,7 +313,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a. apply Zdiv_le_lower_bound;auto with zarith. replace (2^p) with 0. destruct x;compute;intro;discriminate. - destruct p;trivial;discriminate z. + destruct p;trivial;discriminate. Qed. Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. @@ -325,7 +325,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a. assert (0 < 2^p);auto with zarith. replace (2^p) with 0. destruct x;change (0<y);auto with zarith. - destruct p;trivial;discriminate z. + destruct p;trivial;discriminate. Qed. Theorem Zgcd_div_pos a b: diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 57b98e860..da501e9ef 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -490,7 +490,7 @@ Module Make (N:NType) <: ZType. rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive; try rewrite Z.eq_opp_l, Z.opp_0 in Hy; rewrite Zrem_Zmod_pos; generalize (N.spec_pos x) (N.spec_pos y); - z_order. + Z.order. Qed. Definition gcd x y := diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 366418035..d7c0abd8a 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -9,224 +9,16 @@ (************************************************************************) -Require Import ZAxioms ZProperties BinInt Zcompare Zorder ZArith_dec - Zbool Zeven Zsqrt_def Zpow_def Zlog_def Zgcd_def Zdiv_def Zdigits_def. +Require Import ZAxioms ZProperties BinInt. Local Open Scope Z_scope. -(** Bi-directional induction for Z. *) - -Theorem Z_bi_induction : - forall A : Z -> Prop, Proper (eq ==> iff) A -> - A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. -Proof. -intros A A_wd A0 AS n; apply Zind; clear n. -assumption. -intros; rewrite <- Zsucc_succ'. now apply -> AS. -intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply AS. -Qed. - -(** * Implementation of [ZAxiomsMiniSig] by [BinInt.Z] *) +(** BinInt.Z is already implementing [ZAxiomsMiniSig] *) Module Z <: ZAxiomsSig <: UsualOrderedTypeFull <: TotalOrder - <: UsualDecidableTypeFull. - -Definition t := Z. -Definition eqb := Zeq_bool. -Definition zero := 0. -Definition one := 1. -Definition two := 2. -Definition succ := Zsucc. -Definition pred := Zpred. -Definition add := Zplus. -Definition sub := Zminus. -Definition mul := Zmult. -Definition lt := Zlt. -Definition le := Zle. -Definition compare := Zcompare. -Definition min := Zmin. -Definition max := Zmax. -Definition opp := Zopp. -Definition abs := Zabs. -Definition sgn := Zsgn. - -Definition eq_dec := Z_eq_dec. - -Definition bi_induction := Z_bi_induction. - -(** Basic operations. *) - -Definition eq_equiv : Equivalence (@eq Z) := eq_equivalence. -Local Obligation Tactic := simpl_relation. -Program Instance succ_wd : Proper (eq==>eq) Zsucc. -Program Instance pred_wd : Proper (eq==>eq) Zpred. -Program Instance add_wd : Proper (eq==>eq==>eq) Zplus. -Program Instance sub_wd : Proper (eq==>eq==>eq) Zminus. -Program Instance mul_wd : Proper (eq==>eq==>eq) Zmult. - -Definition pred_succ n := eq_sym (Zpred_succ n). -Definition add_0_l := Zplus_0_l. -Definition add_succ_l := Zplus_succ_l. -Definition sub_0_r := Zminus_0_r. -Definition sub_succ_r := Zminus_succ_r. -Definition mul_0_l := Zmult_0_l. -Definition mul_succ_l := Zmult_succ_l. - -Lemma one_succ : 1 = Zsucc 0. -Proof. -reflexivity. -Qed. - -Lemma two_succ : 2 = Zsucc 1. -Proof. -reflexivity. -Qed. - -(** Boolean Equality *) - -Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y). - -(** Order *) - -Program Instance lt_wd : Proper (eq==>eq==>iff) Zlt. - -Definition lt_eq_cases := Zle_lt_or_eq_iff. -Definition lt_irrefl := Zlt_irrefl. -Definition lt_succ_r := Zlt_succ_r. - -(** Comparison *) - -Definition compare_spec := Zcompare_spec. - -(** Minimum and maximum *) - -Definition min_l := Zmin_l. -Definition min_r := Zmin_r. -Definition max_l := Zmax_l. -Definition max_r := Zmax_r. - -(** Properties specific to integers, not natural numbers. *) - -Program Instance opp_wd : Proper (eq==>eq) Zopp. - -Definition succ_pred n := eq_sym (Zsucc_pred n). -Definition opp_0 := Zopp_0. -Definition opp_succ := Zopp_succ. - -(** Absolute value and sign *) - -Definition abs_eq := Zabs_eq. -Definition abs_neq := Zabs_non_eq. - -Definition sgn_null := Zsgn_0. -Definition sgn_pos := Zsgn_1. -Definition sgn_neg := Zsgn_m1. - -(** Even and Odd *) - -Definition Even n := exists m, n=2*m. -Definition Odd n := exists m, n=2*m+1. - -Lemma even_spec n : Zeven_bool n = true <-> Even n. -Proof. rewrite Zeven_bool_iff. exact (Zeven_ex_iff n). Qed. - -Lemma odd_spec n : Zodd_bool n = true <-> Odd n. -Proof. rewrite Zodd_bool_iff. exact (Zodd_ex_iff n). Qed. - -Definition even := Zeven_bool. -Definition odd := Zodd_bool. - -(** Power *) - -Program Instance pow_wd : Proper (eq==>eq==>eq) Zpower. - -Definition pow_0_r := Zpower_0_r. -Definition pow_succ_r := Zpower_succ_r. -Definition pow_neg_r := Zpower_neg_r. -Definition pow := Zpower. - -(** Sqrt *) - -(** NB : we use a new Zsqrt defined in Zsqrt_def, the previous - module Zsqrt.v is now Zsqrt_compat.v *) - -Definition sqrt_spec := Zsqrt_spec. -Definition sqrt_neg := Zsqrt_neg. -Definition sqrt := Zsqrt. - -(** Log2 *) - -Definition log2_spec := Zlog2_spec. -Definition log2_nonpos := Zlog2_nonpos. -Definition log2 := Zlog2. - -(** Gcd *) - -Definition gcd_divide_l := Zgcd_divide_l. -Definition gcd_divide_r := Zgcd_divide_r. -Definition gcd_greatest := Zgcd_greatest. -Definition gcd_nonneg := Zgcd_nonneg. -Definition divide := Zdivide'. -Definition gcd := Zgcd. - -(** Div / Mod / Quot / Rem *) - -Program Instance div_wd : Proper (eq==>eq==>eq) Zdiv. -Program Instance mod_wd : Proper (eq==>eq==>eq) Zmod. -Program Instance quot_wd : Proper (eq==>eq==>eq) Zquot. -Program Instance rem_wd : Proper (eq==>eq==>eq) Zrem. - -Definition div_mod := Z_div_mod_eq_full. -Definition mod_pos_bound := Zmod_pos_bound. -Definition mod_neg_bound := Zmod_neg_bound. -Definition mod_bound_pos := fun a b (_:0<=a) => Zmod_pos_bound a b. -Definition div := Zdiv. -Definition modulo := Zmod. - -Definition quot_rem := fun a b (_:b<>0) => Z_quot_rem_eq a b. -Definition rem_bound_pos := Zrem_bound. -Definition rem_opp_l := fun a b (_:b<>0) => Zrem_opp_l a b. -Definition rem_opp_r := fun a b (_:b<>0) => Zrem_opp_r a b. -Definition quot := Zquot. -Definition rem := Zrem. - -(** Bitwise operations *) - -Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) Ztestbit. -Definition testbit_odd_0 := Ztestbit_odd_0. -Definition testbit_even_0 := Ztestbit_even_0. -Definition testbit_odd_succ := Ztestbit_odd_succ. -Definition testbit_even_succ := Ztestbit_even_succ. -Definition testbit_neg_r := Ztestbit_neg_r. -Definition shiftr_spec := Zshiftr_spec. -Definition shiftl_spec_low := Zshiftl_spec_low. -Definition shiftl_spec_high := Zshiftl_spec_high. -Definition land_spec := Zand_spec. -Definition lor_spec := Zor_spec. -Definition ldiff_spec := Zdiff_spec. -Definition lxor_spec := Zxor_spec. -Definition div2_spec := Zdiv2_spec. - -Definition testbit := Ztestbit. -Definition shiftl := Zshiftl. -Definition shiftr := Zshiftr. -Definition land := Zand. -Definition lor := Zor. -Definition ldiff := Zdiff. -Definition lxor := Zxor. -Definition div2 := Zdiv2. - -(** We define [eq] only here to avoid refering to this [eq] above. *) - -Definition eq := (@eq Z). - -(** Now the generic properties. *) - -Include ZProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. - -End Z. + <: UsualDecidableTypeFull + := BinInt.Z. (** * An [order] tactic for integers *) diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index fe0e6567e..a055007f4 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -382,7 +382,7 @@ Qed. Definition divide n m := exists p, n*p == m. Local Notation "( x | y )" := (divide x y) (at level 0). -Lemma spec_divide : forall n m, (n|m) <-> Zdivide' [n] [m]. +Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. Proof. intros n m. split. intros (p,H). exists [p]. revert H; now zify. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index bff52fb37..84682820d 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -304,7 +304,7 @@ Qed. Definition divide n m := exists p, n*p == m. Local Notation "( x | y )" := (divide x y) (at level 0). -Lemma spec_divide : forall n m, (n|m) <-> Zdivide' [n] [m]. +Lemma spec_divide : forall n m, (n|m) <-> Z.divide [n] [m]. Proof. intros n m. split. intros (p,H). exists [p]. revert H; now zify. diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index d0d06cb40..75a548ca9 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -556,11 +556,11 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. destr_eqb; nzsimpl; intros Hz. qsimpl; rewrite Hz; auto. - destruct Z_le_gt_dec; intros. + destruct Z_le_gt_dec as [LE|GT]. qsimpl. rewrite spec_norm_denum. qsimpl. - rewrite Zdiv_gcd_zero in z0; auto with zarith. + rewrite Zdiv_gcd_zero in GT; auto with zarith. rewrite H in *. rewrite Zdiv_0_l in *; discriminate. rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc. rewrite Zgcd_div_swap0; try romega. |