From b3f67a99cf1013343d99f7cf8036bbabb566dce0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 6 Nov 2007 02:18:53 +0000 Subject: Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of Zdiv Some details: - ZAux.v is the only file left in Ints/Z. The few elements that remain in it are rather specific or compatibility oriented. Others parts and files have been either deleted when unused or pushed into some place of ZArith. - Ints/List/ is removed since it was not needed anymore - Ints/Tactic.v disappear: some of its tactic were unused, some already in Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict has been added to Tactics.v - Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ... - A new file Zpow_facts inherits lots of results about Zpower. Placing them into Zpower would have been difficult with respect to compatibility (import of ring) - A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder - Adequate adaptations to Ints/num/* (mainly renaming of lemmas) Now, concerning Zdiv, the behavior when dividing by a negative number is now fully proved. When this was possible, existing lemmas has been extended, either from strictly positive to non-zero divisor, or even to arbitrary divisor (especially when playing with Zmod). These extended lemmas are named with the suffix _full, whereas the original restrictive lemmas are retained for compatibility. Several lemmas now have shorter proofs (based on unicity lemmas). Lemmas are now more or less organized by themes (division and order, division and usual operations, etc). Three possible choices of spec for divisions on negative numbers are presented: this Zdiv, the ocaml approach and the remainder-always-positive approach. The ugly behavior of Zopp with the current choice of Zdiv/Zmod is now fully covered. A embryo of division "a la Ocaml" is given: Odiv and Omod. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10291 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Ints/num/Nbasic.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'theories/Ints/num/Nbasic.v') diff --git a/theories/Ints/num/Nbasic.v b/theories/Ints/num/Nbasic.v index f7731ae6a6..0d85c92ed1 100644 --- a/theories/Ints/num/Nbasic.v +++ b/theories/Ints/num/Nbasic.v @@ -1,6 +1,5 @@ Require Import ZArith. Require Import ZAux. -Require Import ZDivModAux. Require Import Basic_type. Require Import Max. Require Import GenBase. @@ -28,13 +27,13 @@ assert (tmp: (forall p, 2 * p = p + p)%Z); 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. +rewrite Zpower_1_r; 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. +rewrite Zpower_1_r; 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. @@ -296,7 +295,7 @@ Section CompareRec. Lemma base_xO: forall n, base (xO n) = (base n)^2. Proof. intros n1; unfold base. - rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite ZAux.Zpower_mult; auto with zarith. + rewrite (Zpos_xO n1); rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith. Qed. Let gen_to_Z_pos: forall n x, 0 <= gen_to_Z n x < gen_wB n := -- cgit v1.2.3