From ca96d3477993d102d6cc42166eab52516630d181 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 20 Jun 2011 17:18:39 +0000 Subject: Arithemtic: more concerning compare, eqb, leb, ltb Start of a uniform treatment of compare, eqb, leb, ltb: - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos - Some generic properties are derived in OrdersFacts.BoolOrderFacts In BinPos, more work about sub_mask with nice implications on compare (e.g. simplier proof of lt_trans). In BinNat/BinPos, for uniformity, compare_antisym is now (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result. In BigN / BigZ, eq_bool is now eqb In BinIntDef, gtb and geb are kept for the moment, but a comment advise to rather use ltb and leb. Z.div now uses Z.ltb and Z.leb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zdiv.v | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) (limited to 'theories/ZArith/Zdiv.v') diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index a5f42d6d1..ff221f35e 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -600,12 +600,12 @@ Fixpoint Zmod_POS (a : positive) (b : Z) : Z := | xI a' => let r := Zmod_POS a' b in let r' := (2 * r + 1) in - if Zgt_bool b r' then r' else (r' - b) + if r' let r := Zmod_POS a' b in let r' := (2 * r) in - if Zgt_bool b r' then r' else (r' - b) - | xH => if Zge_bool b 2 then 1 else 0 + if r' if 2 <=? b then 1 else 0 end. Definition Zmod' a b := @@ -630,16 +630,14 @@ Definition Zmod' a b := end. -Theorem Zmod_POS_correct: forall a b, Zmod_POS a b = (snd (Zdiv_eucl_POS a b)). +Theorem Zmod_POS_correct a b : Zmod_POS a b = snd (Zdiv_eucl_POS a b). Proof. - intros a b; elim a; simpl; auto. - intros p Rec; rewrite Rec. - case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto. - match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto. - intros p Rec; rewrite Rec. - case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto. - match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto. - case (Zge_bool b 2); auto. + induction a as [a IH|a IH| ]; simpl; rewrite ?IH. + destruct (Z.pos_div_eucl a b) as (p,q); simpl; + case Z.ltb_spec; reflexivity. + destruct (Z.pos_div_eucl a b) as (p,q); simpl; + case Z.ltb_spec; reflexivity. + case Z.leb_spec; trivial. Qed. Theorem Zmod'_correct: forall a b, Zmod' a b = Zmod a b. -- cgit v1.2.3