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 --- plugins/micromega/EnvRing.v | 20 ++++++++++---------- plugins/micromega/ZCoeff.v | 6 +++--- 2 files changed, 13 insertions(+), 13 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index f72933f99..309ebdef1 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -105,12 +105,12 @@ Section MakeRingPol. match P, P' with | Pc c, Pc c' => c ?=! c' | Pinj j Q, Pinj j' Q' => - match Pcompare j j' Eq with + match j ?= j' with | Eq => Peq Q Q' | _ => false end | PX P i Q, PX P' i' Q' => - match Pcompare i i' Eq with + match i ?= i' with | Eq => if Peq P P' then Peq Q Q' else false | _ => false end @@ -421,7 +421,7 @@ Section MakeRingPol. _, mon0 => (Pc cO, P) | Pc _, _ => (P, Pc cO) | Pinj j1 P1, zmon j2 M1 => - match (j1 ?= j2) Eq with + match (j1 ?= j2) with Eq => let (R,S) := MFactor P1 M1 in (mkPinj j1 R, mkPinj j1 S) | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in @@ -435,7 +435,7 @@ Section MakeRingPol. let (R2, S2) := MFactor Q1 M2 in (mkPX R1 i R2, mkPX S1 i S2) | PX P1 i Q1, vmon j M1 => - match (i ?= j) Eq with + match (i ?= j) with Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in (mkPX R1 i Q1, S1) | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in @@ -537,10 +537,10 @@ Section MakeRingPol. Proof. induction P;destruct P';simpl;intros;try discriminate;trivial. apply (morph_eq CRmorph);trivial. - assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq); + assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0); try discriminate H. rewrite (IHP P' H); rewrite H1;trivial;rrefl. - assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq); + assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0); try discriminate H. rewrite H1;trivial. clear H1. assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2); @@ -1019,8 +1019,8 @@ Qed. intros i P Hrec M l; case M; simpl; clear M. rewrite (morph0 CRmorph); rsimpl. intros j M. - case_eq ((i ?= j) Eq); intros He; simpl. - rewrite (Pcompare_Eq_eq _ _ He). + case_eq (i ?= j); intros He; simpl. + rewrite (Pos.compare_eq _ _ He). generalize (Hrec M (jump j l)); case (MFactor P M); simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto. generalize (Hrec (zmon (j -i) M) (jump i l)); @@ -1048,8 +1048,8 @@ Qed. rewrite (ARadd_comm ARth); rsimpl. rewrite zmon_pred_ok;rsimpl. intros j M1. - case_eq ((i ?= j) Eq); intros He; simpl. - rewrite (Pcompare_Eq_eq _ _ He). + case_eq (i ?= j); intros He; simpl. + rewrite (Pos.compare_eq _ _ He). generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1)); simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. rewrite H; rewrite mkPX_ok; rsimpl. diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index f8df97489..2bf3d8c35 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -138,7 +138,7 @@ Qed. Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y]. Proof. -unfold Zlt; intros x y H; +intros x y H. do 2 rewrite (same_genZ sor.(SORsetoid) ring_ops_wd sor.(SORrt)); destruct x; destruct y; simpl in *; try discriminate. apply phi_pos1_pos. @@ -146,8 +146,8 @@ now apply clt_pos_morph. apply <- (Ropp_neg_pos sor); apply phi_pos1_pos. apply (Rlt_trans sor) with 0. apply <- (Ropp_neg_pos sor); apply phi_pos1_pos. apply phi_pos1_pos. -rewrite Pcompare_antisym in H; simpl in H. apply -> (Ropp_lt_mono sor). -now apply clt_pos_morph. +apply -> (Ropp_lt_mono sor); apply clt_pos_morph. +red. now rewrite Pos.compare_antisym. Qed. Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y]. -- cgit v1.2.3