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

4 files changed, 109 insertions, 133 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 04bb8d881..eaf30e6d0 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -9,7 +9,7 @@
 
 Require Export BinNums BinPos Pnat.
 Require Import BinNat Bool Plus Mult Equalities GenericMinMax
- ZAxioms ZProperties.
+ OrdersFacts ZAxioms ZProperties.
 Require BinIntDef.
 
 (***********************************************************)
@@ -36,6 +36,10 @@ Module Z
 
 Include BinIntDef.Z.
 
+(** When including property functors, only inline t eq zero one two *)
+
+Set Inline Level 30.
+
 (** * Logic Predicates *)
 
 Definition eq := @Logic.eq Z.
@@ -444,65 +448,7 @@ Proof.
  unfold succ. now rewrite mul_add_distr_r, mul_1_l.
 Qed.
 
-(** ** Specification of order *)
-
-Lemma compare_refl n : (n ?= n) = Eq.
-Proof.
- destruct n; simpl; trivial; now rewrite Pos.compare_refl.
-Qed.
-
-Lemma compare_eq n m : (n ?= m) = Eq -> n = m.
-Proof.
-destruct n, m; simpl; try easy; intros; f_equal.
-now apply Pos.compare_eq.
-apply Pos.compare_eq, CompOpp_inj. now rewrite H.
-Qed.
-
-Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
-Proof.
-split; intros. now apply compare_eq. subst; now apply compare_refl.
-Qed.
-
-Lemma compare_antisym n m : CompOpp (n ?= m) = (m ?= n).
-Proof.
-destruct n, m; simpl; trivial.
-symmetry. apply Pos.compare_antisym. (* TODO : quel sens ? *)
-f_equal. symmetry. apply Pos.compare_antisym.
-Qed.
-
-Lemma compare_sub n m : (n ?= m) = (n - m ?= 0).
-Proof.
- destruct n as [|n|n], m as [|m|m]; simpl; trivial;
- rewrite <- ? Pos.compare_antisym, ?pos_sub_spec;
- case Pos.compare_spec; trivial.
-Qed.
-
-Lemma compare_spec n m : CompareSpec (n=m) (n<m) (m<n) (n ?= m).
-Proof.
- case_eq (n ?= m); intros H; constructor; trivial.
- now apply compare_eq.
- red. now rewrite <- compare_antisym, H.
-Qed.
-
-Lemma lt_irrefl n : ~ n < n.
-Proof.
- unfold lt. now rewrite compare_refl.
-Qed.
-
-Lemma lt_eq_cases n m : n <= m <-> n < m \/ n = m.
-Proof.
- unfold le, lt. rewrite <- compare_eq_iff.
- case compare; now intuition.
-Qed.
-
-Lemma lt_succ_r n m : n < succ m <-> n<=m.
-Proof.
- unfold lt, le. rewrite compare_sub, sub_succ_r.
- rewrite (compare_sub n m).
- destruct (n-m) as [|[ | | ]|]; easy'.
-Qed.
-
-(** ** Specification of boolean comparisons *)
+(** ** Specification of comparisons and order *)
 
 Lemma eqb_eq n m : (n =? m) = true <-> n = m.
 Proof.
@@ -521,53 +467,49 @@ Proof.
  unfold leb, le. destruct compare; easy'.
 Qed.
 
-Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m).
+Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
 Proof.
- unfold le, lt, leb. rewrite <- (compare_antisym n m).
- case compare; now constructor.
+destruct n, m; simpl; rewrite ?CompOpp_iff, ?Pos.compare_eq_iff;
+ split; congruence.
 Qed.
 
-Lemma ltb_spec n m : BoolSpec (n<m) (m<=n) (n <? m).
+Lemma compare_sub n m : (n ?= m) = (n - m ?= 0).
 Proof.
- unfold le, lt, ltb. rewrite <- (compare_antisym n m).
- case compare; now constructor.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial;
+ rewrite <- ? Pos.compare_antisym, ?pos_sub_spec;
+ case Pos.compare_spec; trivial.
 Qed.
 
-Lemma gtb_ltb n m : (n >? m) = (m <? n).
+Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
 Proof.
- unfold gtb, ltb. rewrite <- compare_antisym. now case compare.
+destruct n, m; simpl; trivial; now rewrite <- ?Pos.compare_antisym.
 Qed.
 
-Lemma geb_leb n m : (n >=? m) = (m <=? n).
-Proof.
- unfold geb, leb. rewrite <- compare_antisym. now case compare.
-Qed.
+Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.
+Proof. reflexivity. Qed.
 
-Lemma gtb_lt n m : (n >? m) = true <-> m < n.
-Proof.
- rewrite gtb_ltb. apply ltb_lt.
-Qed.
+Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
+Proof. reflexivity. Qed.
 
-Lemma geb_le n m : (n >=? m) = true <-> m <= n.
-Proof.
- rewrite geb_leb. apply leb_le.
-Qed.
+(** Some more advanced properties of comparison and orders,
+    including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *)
 
-Lemma gtb_spec n m : BoolSpec (m<n) (n<=m) (n >? m).
-Proof.
- rewrite gtb_ltb. apply ltb_spec.
-Qed.
+Include BoolOrderFacts.
 
-Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m).
+(** Remaining specification of [lt] and [le] *)
+
+Lemma lt_succ_r n m : n < succ m <-> n<=m.
 Proof.
- rewrite geb_leb. apply leb_spec.
+ unfold lt, le. rewrite compare_sub, sub_succ_r.
+ rewrite (compare_sub n m).
+ destruct (n-m) as [|[ | | ]|]; easy'.
 Qed.
 
 (** ** Specification of minimum and maximum *)
 
 Lemma max_l n m : m<=n -> max n m = n.
 Proof.
- unfold le, max. rewrite <- (compare_antisym n m).
+ unfold le, max. rewrite (compare_antisym n m).
  case compare; intuition.
 Qed.
 
@@ -584,7 +526,7 @@ Qed.
 Lemma min_r n m : m<=n -> min n m = m.
 Proof.
  unfold le, min.
- rewrite <- (compare_antisym n m). case compare_spec; intuition.
+ rewrite (compare_antisym n m). case compare_spec; intuition.
 Qed.
 
 (** ** Specification of absolute value *)
@@ -727,19 +669,19 @@ Proof.
  (* ~1 *)
  destruct pos_div_eucl as (q,r).
  rewrite pos_xI, IHa, mul_add_distr_l, mul_assoc.
- destruct gtb.
+ destruct ltb.
  now rewrite add_assoc.
  rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal.
  unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r.
  (* ~0 *)
  destruct pos_div_eucl as (q,r).
  rewrite (pos_xO a), IHa, mul_add_distr_l, mul_assoc.
- destruct gtb.
+ destruct ltb.
  trivial.
  rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal.
  unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r.
  (* ~1 *)
- case geb_spec; trivial.
+ case leb_spec; trivial.
  intros Hb'.
  destruct b as [|b|b]; try easy; clear Hb.
  replace b with 1%positive; trivial.
@@ -788,21 +730,21 @@ Proof.
  (* ~1 *)
  destruct pos_div_eucl as (q,r).
  simpl in IHa; destruct IHa as (Hr,Hr').
- case gtb_spec; intros H; unfold snd. split; trivial. now destruct r.
+ case ltb_spec; intros H; unfold snd. split; trivial. now destruct r.
  split. unfold le.
-  now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
+  now rewrite compare_antisym, <- compare_sub, <- compare_antisym.
  apply AUX. rewrite <- succ_double_spec.
  destruct r; try easy. unfold lt in *; simpl in *.
   now rewrite Pos.compare_xI_xO, Hr'.
  (* ~0 *)
  destruct pos_div_eucl as (q,r).
  simpl in IHa; destruct IHa as (Hr,Hr').
- case gtb_spec; intros H; unfold snd. split; trivial. now destruct r.
+ case ltb_spec; intros H; unfold snd. split; trivial. now destruct r.
  split. unfold le.
-  now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
+  now rewrite compare_antisym, <- compare_sub, <- compare_antisym.
  apply AUX. destruct r; try easy.
  (* 1 *)
- case geb_spec; intros H; simpl; split; try easy.
+ case leb_spec; intros H; simpl; split; try easy.
  red; simpl. now apply Pos.le_succ_l.
 Qed.
 
@@ -817,7 +759,7 @@ Proof.
  destruct r as [|r|r]; (now destruct Hr) || clear Hr.
  now split.
  split. unfold le.
-  now rewrite <- compare_antisym, <- compare_sub, compare_antisym, Hr'.
+  now rewrite compare_antisym, <- compare_sub, <- compare_antisym, Hr'.
  unfold lt in *; simpl in *. rewrite pos_sub_gt by trivial.
  simpl. now apply Pos.sub_decr.
 Qed.
@@ -1111,7 +1053,7 @@ Proof.
  (* n > 0 *)
  destruct m as [ |m|m]; try (now destruct H).
  assert (0 <= Zpos m - Zpos n).
-  red. now rewrite <- compare_antisym, <- compare_sub, compare_antisym.
+  red. now rewrite compare_antisym, <- compare_sub, <- compare_antisym.
  assert (EQ : to_N (Zpos m - Zpos n) = (Npos m - Npos n)%N).
   red in H. simpl in H. simpl to_N.
   rewrite pos_sub_spec, Pos.compare_antisym.
@@ -1278,8 +1220,6 @@ Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
 Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
 Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
 
-Set Inline Level 30. (* For inlining only t eq zero one two *)
-
 Include ZProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
@@ -1291,34 +1231,68 @@ Bind Scope Z_scope with Z.
   layers. The use of [gt] and [ge] is hence not recommended. We provide
   here the bare minimal results to related them with [lt] and [le]. *)
 
+Lemma gt_lt_iff n m : n > m <-> m < n.
+Proof.
+ unfold lt, gt. now rewrite compare_antisym, CompOpp_iff.
+Qed.
+
 Lemma gt_lt n m : n > m -> m < n.
 Proof.
-  unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+ apply gt_lt_iff.
 Qed.
 
 Lemma lt_gt n m : n < m -> m > n.
 Proof.
-  unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+ apply gt_lt_iff.
 Qed.
 
-Lemma gt_lt_iff n m : n > m <-> m < n.
+Lemma ge_le_iff n m : n >= m <-> m <= n.
 Proof.
-  split. apply gt_lt. apply lt_gt.
+ unfold le, ge. now rewrite compare_antisym, CompOpp_iff.
 Qed.
 
 Lemma ge_le n m : n >= m -> m <= n.
 Proof.
-  unfold le, ge. intros H. contradict H. now apply gt_lt.
+ apply ge_le_iff.
 Qed.
 
 Lemma le_ge n m : n <= m -> m >= n.
 Proof.
-  unfold le, ge. intros H. contradict H. now apply lt_gt.
+ apply ge_le_iff.
 Qed.
 
-Lemma ge_le_iff n m : n >= m <-> m <= n.
+(** Similarly, the boolean comparisons [ltb] and [leb] are favored
+  over their dual [gtb] and [geb]. We prove here the equivalence
+  and a few minimal results. *)
+
+Lemma gtb_ltb n m : (n >? m) = (m <? n).
 Proof.
-  split. apply ge_le. apply le_ge.
+ unfold gtb, ltb. rewrite compare_antisym. now case compare.
+Qed.
+
+Lemma geb_leb n m : (n >=? m) = (m <=? n).
+Proof.
+ unfold geb, leb. rewrite compare_antisym. now case compare.
+Qed.
+
+Lemma gtb_lt n m : (n >? m) = true <-> m < n.
+Proof.
+ rewrite gtb_ltb. apply ltb_lt.
+Qed.
+
+Lemma geb_le n m : (n >=? m) = true <-> m <= n.
+Proof.
+ rewrite geb_leb. apply leb_le.
+Qed.
+
+Lemma gtb_spec n m : BoolSpec (m<n) (n<=m) (n >? m).
+Proof.
+ rewrite gtb_ltb. apply ltb_spec.
+Qed.
+
+Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m).
+Proof.
+ rewrite geb_leb. apply leb_spec.
 Qed.
 
 (** TODO : to add in Numbers *)
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 4c2a19f69..ee9051ff8 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -166,19 +166,23 @@ Definition leb x y :=
     | _ => true
   end.
 
-Definition geb x y := (* TODO : to provide ? to modify ? *)
-  match x ?= y with
-    | Lt => false
-    | _ => true
-  end.
-
 Definition ltb x y :=
   match x ?= y with
     | Lt => true
     | _ => false
   end.
 
-Definition gtb x y := (* TODO : to provide ? to modify ? *)
+(** Nota: [geb] and [gtb] are provided for compatibility,
+  but [leb] and [ltb] should rather be used instead, since
+  more results we be available on them. *)
+
+Definition geb x y :=
+  match x ?= y with
+    | Lt => false
+    | _ => true
+  end.
+
+Definition gtb x y :=
   match x ?= y with
     | Gt => true
     | _ => false
@@ -322,15 +326,15 @@ Definition iter (n:Z) {A} (f:A -> A) (x:A) :=
 
 Fixpoint pos_div_eucl (a:positive) (b:Z) : Z * Z :=
   match a with
-    | xH => if b >=? 2 then (0, 1) else (1, 0)
+    | xH => if 2 <=? b then (0, 1) else (1, 0)
     | xO a' =>
       let (q, r) := pos_div_eucl a' b in
       let r' := 2 * r in
-      if b >? r' then (2 * q, r') else (2 * q + 1, r' - b)
+      if r' <? b then (2 * q, r') else (2 * q + 1, r' - b)
     | xI a' =>
       let (q, r) := pos_div_eucl a' b in
       let r' := 2 * r + 1 in
-      if b >? r' then (2 * q, r') else (2 * q + 1, r' - b)
+      if r' <? b then (2 * q, r') else (2 * q + 1, r' - b)
   end.
 
 (** Then the general euclidean division *)
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' <? b then r' else (r' - b)
    | xO a' =>
       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' <? b then r' else (r' - b)
+   | xH => 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.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 2fdfad5dd..bc3d73484 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -173,7 +173,7 @@ Qed.
 Lemma inj_sub_max n m : Z.of_N (n-m) = Z.max 0 (Z.of_N n - Z.of_N m).
 Proof.
  destruct n as [|n], m as [|m]; simpl; trivial.
- rewrite Z.pos_sub_spec, <- Pos.sub_mask_compare. unfold Pos.sub.
+ rewrite Z.pos_sub_spec, Pos.compare_sub_mask. unfold Pos.sub.
  now destruct (Pos.sub_mask n m).
 Qed.
 
@@ -181,7 +181,7 @@ Lemma inj_sub n m : (m<=n)%N -> Z.of_N (n-m) = Z.of_N n - Z.of_N m.
 Proof.
  intros H. rewrite inj_sub_max.
  unfold N.le in H.
- rewrite <- N.compare_antisym, <- inj_compare, Z.compare_sub in H.
+ rewrite N.compare_antisym, <- inj_compare, Z.compare_sub in H.
  destruct (Z.of_N n - Z.of_N m); trivial; now destruct H.
 Qed.
 
@@ -275,7 +275,7 @@ Lemma inj_sub n m : 0<=m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N.
 Proof.
  destruct n as [|n|n], m as [|m|m]; trivial; try (now destruct 1).
  intros _. simpl.
- rewrite Z.pos_sub_spec, <- Pos.sub_mask_compare. unfold Pos.sub.
+ rewrite Z.pos_sub_spec, Pos.compare_sub_mask. unfold Pos.sub.
  now destruct (Pos.sub_mask n m).
 Qed.