From c0a3544d6351e19c695951796bcee838671d1098 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:15 +0000 Subject: Modularization of BinPos + fixes in Stdlib BinPos now contain a sub-module Pos, in which are placed functions like add (ex-Pplus), mul (ex-Pmult), ... and properties like add_comm, add_assoc, ... In addition to the name changes, the organisation is changed quite a lot, to try to take advantage more of the orders < and <= instead of speaking only of the comparison function. The main source of incompatibilities in scripts concerns this compare: Pos.compare is now a binary operation, expressed in terms of the ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg), this ternary version being called now Pos.compare_cont. As for everything else, compatibility notations (only parsing) are provided. But notations "_ ?= _" on positive will have to be edited, since they now point to Pos.compare. We also make the sub-module Pos to be directly an OrderedType, and include results about min and max. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/NArith/BinNat.v | 6 +++--- theories/NArith/Ndec.v | 8 ++++---- theories/NArith/Ndiv_def.v | 14 ++++++-------- theories/NArith/Ngcd_def.v | 14 +++++++------- theories/NArith/Nsqrt_def.v | 14 +++++++------- 5 files changed, 27 insertions(+), 29 deletions(-) (limited to 'theories/NArith') diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 3e576a08b..3a4250566 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -128,7 +128,7 @@ Definition Ncompare n m := | 0, 0 => Eq | 0, Npos m' => Lt | Npos n', 0 => Gt - | Npos n', Npos m' => (n' ?= m')%positive Eq + | Npos n', Npos m' => (n' ?= m')%positive end. Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. @@ -497,8 +497,8 @@ Proof. intros [|p] [|q]; simpl; split; intros H; auto. destruct p; discriminate. destruct H; discriminate. -apply Pcompare_p_Sq in H; destruct H; subst; auto. -apply Pcompare_p_Sq; destruct H; [left|right]; congruence. +apply Plt_succ_r, Ple_lteq in H. destruct H; subst; auto. +apply Plt_succ_r, Ple_lteq. destruct H; [left|right]; congruence. Qed. Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y. diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 97b61893f..f2ee29cc0 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -27,14 +27,14 @@ Proof. intros. now apply (Peqb_eq p p'). Qed. -Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq. +Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pos.compare p p' = Eq. Proof. - intros. now rewrite Pcompare_eq_iff, <- Peqb_eq. + intros. now rewrite Pos.compare_eq_iff, <- Peqb_eq. Qed. -Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true. +Lemma Pcompare_Peqb : forall p p', Pos.compare p p' = Eq -> Peqb p p' = true. Proof. - intros; now rewrite Peqb_eq, <- Pcompare_eq_iff. + intros; now rewrite Peqb_eq, <- Pos.compare_eq_iff. Qed. Lemma Neqb_correct : forall n, Neqb n n = true. diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 2a3fd152a..0850a631e 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -14,7 +14,7 @@ Local Open Scope N_scope. Definition NPgeb (a:N)(b:positive) := match a with | 0 => false - | Npos na => match Pcompare na b Eq with Lt => false | _ => true end + | Npos na => match Pos.compare na b with Lt => false | _ => true end end. Local Notation "a >=? b" := (NPgeb a b) (at level 70). @@ -54,24 +54,22 @@ Lemma NPgeb_ge : forall a b, NPgeb a b = true -> a >= Npos b. Proof. destruct a; simpl; intros. discriminate. - unfold Nge, Ncompare. now destruct Pcompare. + unfold Nge, Ncompare. now destruct Pos.compare. Qed. Lemma NPgeb_lt : forall a b, NPgeb a b = false -> a < Npos b. Proof. destruct a; simpl; intros. red; auto. - unfold Nlt, Ncompare. now destruct Pcompare. + unfold Nlt, Ncompare. now destruct Pos.compare. Qed. Theorem NPgeb_correct: forall (a:N)(b:positive), if NPgeb a b then a = a - Npos b + Npos b else True. Proof. destruct a as [|a]; simpl; intros b; auto. - generalize (Pcompare_Eq_eq a b). - case_eq (Pcompare a b Eq); intros; auto. - rewrite H0; auto. + case Pos.compare_spec; intros; subst; auto. now rewrite Pminus_mask_diag. - destruct (Pminus_mask_Gt a b H) as [d [H2 [H3 _]]]. + destruct (Pminus_mask_Gt a b (Pos.lt_gt _ _ H)) as [d [H2 [H3 _]]]. rewrite H2. rewrite <- H3. simpl; f_equal; apply Pplus_comm. Qed. @@ -96,7 +94,7 @@ rewrite Nplus_comm. generalize (NPgeb_correct (2*a+1) p). rewrite GE. intros <-. rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r. destruct a; auto. -red; simpl. apply Pcompare_eq_Lt; auto. +red; simpl. apply Pcompare_Gt_Lt; auto. Qed. (* Proofs of specifications for these euclidean divisions. *) diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v index fe5185c6b..c25af8717 100644 --- a/theories/NArith/Ngcd_def.v +++ b/theories/NArith/Ngcd_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import BinPos BinNat Pgcd. +Require Import BinPos BinNat. Local Open Scope N_scope. @@ -21,7 +21,7 @@ Definition Ngcd (a b : N) := match a, b with | 0, _ => b | _, 0 => a - | Npos p, Npos q => Npos (Pgcd p q) + | Npos p, Npos q => Npos (Pos.gcd p q) end. (** * Generalized Gcd, also computing rests of a and b after @@ -32,7 +32,7 @@ Definition Nggcd (a b : N) := | 0, _ => (b,(0,1)) | _, 0 => (a,(1,0)) | Npos p, Npos q => - let '(g,(aa,bb)) := Pggcd p q in + let '(g,(aa,bb)) := Pos.ggcd p q in (Npos g, (Npos aa, Npos bb)) end. @@ -41,7 +41,7 @@ Definition Nggcd (a b : N) := Lemma Nggcd_gcd : forall a b, fst (Nggcd a b) = Ngcd a b. Proof. intros [ |p] [ |q]; simpl; auto. - generalize (Pggcd_gcd p q). destruct Pggcd as (g,(aa,bb)); simpl; congruence. + generalize (Pos.ggcd_gcd p q). destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence. Qed. (** The other components of Nggcd are indeed the correct factors. *) @@ -53,8 +53,8 @@ Proof. intros [ |p] [ |q]; simpl; auto. now rewrite Pmult_1_r. now rewrite Pmult_1_r. - generalize (Pggcd_correct_divisors p q). - destruct Pggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence. + generalize (Pos.ggcd_correct_divisors p q). + destruct Pos.ggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence. Qed. (** We can use this fact to prove a part of the gcd correctness *) @@ -78,7 +78,7 @@ Proof. intros [ |p] [ |q]; simpl; auto. intros [ |r]. intros (s,H). discriminate. intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *. - destruct (Pgcd_greatest p q r) as (u,H). + destruct (Pos.gcd_greatest p q r) as (u,H). exists s. now inversion Hs. exists t. now inversion Ht. exists (Npos u). simpl; now f_equal. diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index 750da2397..375ed0f90 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -8,7 +8,7 @@ (** Definition of a square root function for N. *) -Require Import BinPos BinNat Psqrt. +Require Import BinPos BinNat. Local Open Scope N_scope. @@ -16,7 +16,7 @@ Definition Nsqrtrem n := match n with | N0 => (N0, N0) | Npos p => - match Psqrtrem p with + match Pos.sqrtrem p with | (s, IsPos r) => (Npos s, Npos r) | (s, _) => (Npos s, N0) end @@ -25,26 +25,26 @@ Definition Nsqrtrem n := Definition Nsqrt n := match n with | N0 => N0 - | Npos p => Npos (Psqrt p) + | Npos p => Npos (Pos.sqrt p) end. Lemma Nsqrtrem_spec : forall n, let (s,r) := Nsqrtrem n in n = s*s + r /\ r <= 2*s. Proof. destruct n. now split. - generalize (Psqrtrem_spec p). simpl. + generalize (Pos.sqrtrem_spec p). simpl. destruct 1; simpl; subst; now split. Qed. Lemma Nsqrt_spec : forall n, let s := Nsqrt n in s*s <= n < (Nsucc s)*(Nsucc s). Proof. - destruct n. now split. apply (Psqrt_spec p). + destruct n. now split. apply (Pos.sqrt_spec p). Qed. Lemma Nsqrtrem_sqrt : forall n, fst (Nsqrtrem n) = Nsqrt n. Proof. destruct n. reflexivity. - unfold Nsqrtrem, Nsqrt, Psqrt. - destruct (Psqrtrem p) as (s,r). now destruct r. + unfold Nsqrtrem, Nsqrt, Pos.sqrt. + destruct (Pos.sqrtrem p) as (s,r). now destruct r. Qed. \ No newline at end of file -- cgit v1.2.3