diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:15 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:15 +0000 |
commit | c0a3544d6351e19c695951796bcee838671d1098 (patch) | |
tree | d87f69afd73340492ac694b2aa837024a90e8692 /theories/NArith/Ngcd_def.v | |
parent | f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 (diff) |
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
Diffstat (limited to 'theories/NArith/Ngcd_def.v')
-rw-r--r-- | theories/NArith/Ngcd_def.v | 14 |
1 files changed, 7 insertions, 7 deletions
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. |