diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 46 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 14 |
2 files changed, 25 insertions, 35 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 59656eed..9a8a7691 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -111,7 +111,7 @@ Module ZnZ. (* Conversion functions with Z *) spec_to_Z : forall x, 0 <= [| x |] < wB; spec_of_pos : forall p, - Zpos p = (Z_of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|]; + Zpos p = (Z.of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|]; spec_zdigits : [| zdigits |] = Zpos digits; spec_more_than_1_digit: 1 < Zpos digits; @@ -284,11 +284,11 @@ Module ZnZ. generalize (spec_of_pos p). case (of_pos p); intros n w1; simpl. case n; simpl Npos; auto with zarith. - intros p1 Hp1; contradict Hp; apply Zle_not_lt. + intros p1 Hp1; contradict Hp; apply Z.le_ngt. replace (base digits) with (1 * base digits + 0) by ring. rewrite Hp1. - apply Zplus_le_compat. - apply Zmult_le_compat; auto with zarith. + apply Z.add_le_mono. + apply Z.mul_le_mono_nonneg; auto with zarith. case p1; simpl; intros; red; simpl; intros; discriminate. unfold base; auto with zarith. case (spec_to_Z w1); auto with zarith. @@ -305,7 +305,7 @@ Module ZnZ. Proof. intros p; case p; simpl; try rewrite spec_0; auto. intros; rewrite of_pos_correct; auto with zarith. - intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto. + intros p1 (H1, _); contradict H1; apply Z.lt_nge; red; simpl; auto. Qed. End Of_Z. @@ -346,46 +346,46 @@ Ltac zify := unfold eq in *; autorewrite with cyclic. Lemma add_0_l : forall x, 0 + x == x. Proof. -intros. zify. rewrite Zplus_0_l. +intros. zify. rewrite Z.add_0_l. apply Zmod_small. apply ZnZ.spec_to_Z. Qed. Lemma add_comm : forall x y, x + y == y + x. Proof. -intros. zify. now rewrite Zplus_comm. +intros. zify. now rewrite Z.add_comm. Qed. Lemma add_assoc : forall x y z, x + (y + z) == x + y + z. Proof. -intros. zify. now rewrite Zplus_mod_idemp_r, Zplus_mod_idemp_l, Zplus_assoc. +intros. zify. now rewrite Zplus_mod_idemp_r, Zplus_mod_idemp_l, Z.add_assoc. Qed. Lemma mul_1_l : forall x, 1 * x == x. Proof. -intros. zify. rewrite Zmult_1_l. +intros. zify. rewrite Z.mul_1_l. apply Zmod_small. apply ZnZ.spec_to_Z. Qed. Lemma mul_comm : forall x y, x * y == y * x. Proof. -intros. zify. now rewrite Zmult_comm. +intros. zify. now rewrite Z.mul_comm. Qed. Lemma mul_assoc : forall x y z, x * (y * z) == x * y * z. Proof. -intros. zify. now rewrite Zmult_mod_idemp_r, Zmult_mod_idemp_l, Zmult_assoc. +intros. zify. now rewrite Zmult_mod_idemp_r, Zmult_mod_idemp_l, Z.mul_assoc. Qed. Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z. Proof. -intros. zify. now rewrite <- Zplus_mod, Zmult_mod_idemp_l, Zmult_plus_distr_l. +intros. zify. now rewrite <- Zplus_mod, Zmult_mod_idemp_l, Z.mul_add_distr_r. Qed. Lemma add_opp_r : forall x y, x + - y == x-y. Proof. -intros. zify. rewrite <- Zminus_mod_idemp_r. unfold Zminus. -destruct (Z_eq_dec ([|y|] mod wB) 0) as [EQ|NEQ]. -rewrite Z_mod_zero_opp_full, EQ, 2 Zplus_0_r; auto. +intros. zify. rewrite <- Zminus_mod_idemp_r. unfold Z.sub. +destruct (Z.eq_dec ([|y|] mod wB) 0) as [EQ|NEQ]. +rewrite Z_mod_zero_opp_full, EQ, 2 Z.add_0_r; auto. rewrite Z_mod_nz_opp_full by auto. rewrite <- Zplus_mod_idemp_r, <- Zminus_mod_idemp_l. rewrite Z_mod_same_full. simpl. now rewrite Zplus_mod_idemp_r. @@ -393,7 +393,7 @@ Qed. Lemma add_opp_diag_r : forall x, x + - x == 0. Proof. -intros. red. rewrite add_opp_r. zify. now rewrite Zminus_diag, Zmod_0_l. +intros. red. rewrite add_opp_r. zify. now rewrite Z.sub_diag, Zmod_0_l. Qed. Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq. @@ -413,19 +413,9 @@ Lemma eqb_eq : forall x y, eqb x y = true <-> x == y. Proof. intros. unfold eqb, eq. rewrite ZnZ.spec_compare. - case Zcompare_spec; intuition; try discriminate. + case Z.compare_spec; intuition; try discriminate. Qed. -(* POUR HUGO: -Lemma eqb_eq : forall x y, eqb x y = true <-> x == y. -Proof. - intros. unfold eqb, eq. generalize (ZnZ.spec_compare x y). - case (ZnZ.compare x y); intuition; try discriminate. - (* BUG ?! using destruct instead of case won't work: - it gives 3 subcases, but ZnZ.compare x y is still there in them! *) -Qed. -*) - Lemma eqb_correct : forall x y, eqb x y = true -> x==y. Proof. now apply eqb_eq. Qed. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index c52cbe10..1d5b78ec 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -69,7 +69,7 @@ Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul. Theorem gt_wB_1 : 1 < wB. Proof. -unfold base. apply Zpower_gt_1; unfold Zlt; auto with zarith. +unfold base. apply Zpower_gt_1; unfold Z.lt; auto with zarith. Qed. Theorem gt_wB_0 : 0 < wB. @@ -161,20 +161,20 @@ End Induction. Theorem add_0_l : forall n, 0 + n == n. Proof. intro n. zify. -rewrite Zplus_0_l. apply Zmod_small. apply ZnZ.spec_to_Z. +rewrite Z.add_0_l. apply Zmod_small. apply ZnZ.spec_to_Z. Qed. Theorem add_succ_l : forall n m, (S n) + m == S (n + m). Proof. intros n m. zify. rewrite succ_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0. -rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. -rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc. +rewrite <- (Z.add_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. +rewrite (Z.add_comm 1 [| m |]); now rewrite Z.add_assoc. Qed. Theorem sub_0_r : forall n, n - 0 == n. Proof. -intro n. zify. rewrite Zminus_0_r. apply NZ_to_Z_mod. +intro n. zify. rewrite Z.sub_0_r. apply NZ_to_Z_mod. Qed. Theorem sub_succ_r : forall n m, n - (S m) == P (n - m). @@ -192,7 +192,7 @@ Qed. Theorem mul_succ_l : forall n m, (S n) * m == n * m + m. Proof. intros n m. zify. rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. -now rewrite Zmult_plus_distr_l, Zmult_1_l. +now rewrite Z.mul_add_distr_r, Z.mul_1_l. Qed. Definition t := t. |