aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/Init/Datatypes.v1
-rw-r--r--theories/NArith/BinNat.v143
-rw-r--r--theories/Numbers/Integer/Abstract/ZAxioms.v10
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v9
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v72
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSig.v50
-rw-r--r--theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v64
-rw-r--r--theories/Numbers/Natural/Abstract/NAxioms.v4
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v9
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v60
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v29
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSig.v48
-rw-r--r--theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v62
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v92
-rw-r--r--theories/PArith/BinPos.v459
-rw-r--r--theories/Structures/Equalities.v56
-rw-r--r--theories/Structures/Orders.v105
-rw-r--r--theories/Structures/OrdersFacts.v322
-rw-r--r--theories/ZArith/BinInt.v190
-rw-r--r--theories/ZArith/BinIntDef.v24
-rw-r--r--theories/ZArith/Zdiv.v22
-rw-r--r--theories/ZArith/Znat.v6
22 files changed, 1107 insertions, 730 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 1ea54e620..bab764bcb 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -120,6 +120,7 @@ Defined.
Inductive BoolSpec (P Q : Prop) : bool -> Prop :=
| BoolSpecT : P -> BoolSpec P Q true
| BoolSpecF : Q -> BoolSpec P Q false.
+Hint Constructors BoolSpec.
(********************************************************************)
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index e54d6b81f..2ca046808 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -8,7 +8,7 @@
Require Export BinNums.
Require Import BinPos RelationClasses Morphisms Setoid
- Equalities GenericMinMax Bool NAxioms NProperties.
+ Equalities OrdersFacts GenericMinMax Bool NAxioms NProperties.
Require BinNatDef.
(**********************************************************************)
@@ -36,6 +36,10 @@ Module N
Include BinNatDef.N.
+(** When including property functors, only inline t eq zero one two *)
+
+Set Inline Level 30.
+
(** Logical predicates *)
Definition eq := @Logic.eq N.
@@ -213,86 +217,50 @@ destruct n, m; simpl; trivial. f_equal. rewrite Pos.add_comm.
apply Pos.mul_succ_l.
Qed.
-(** Properties of comparison *)
-
-Lemma compare_refl n : (n ?= n) = Eq.
-Proof.
-destruct n; simpl; trivial. apply Pos.compare_refl.
-Qed.
+(** Specification of boolean comparisons. *)
-Theorem compare_eq n m : (n ?= m) = Eq -> n = m.
-Proof.
-destruct n, m; simpl; try easy. intros. f_equal.
-now apply Pos.compare_eq.
-Qed.
-
-Theorem 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).
+Lemma eqb_eq n m : eqb n m = true <-> n=m.
Proof.
-destruct n, m; simpl; trivial.
-symmetry. apply Pos.compare_antisym. (* TODO : quel sens ? *)
+destruct n as [|n], m as [|m]; simpl; try easy'.
+rewrite Pos.eqb_eq. split; intro H. now subst. now destr_eq H.
Qed.
-(** Specification of lt and le *)
-
-Theorem lt_irrefl n : ~ n < n.
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
Proof.
-unfold lt. now rewrite compare_refl.
+ unfold ltb, lt. destruct compare; easy'.
Qed.
-Lemma lt_eq_cases n m : n <= m <-> n < m \/ n=m.
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
Proof.
-unfold le, lt. rewrite <- compare_eq_iff.
-destruct (n ?= m); now intuition.
+ unfold leb, le. destruct compare; easy'.
Qed.
-Lemma lt_succ_r n m : n < succ m <-> n<=m.
-Proof.
-destruct n as [|p], m as [|q]; simpl; try easy'.
-split. now destruct p. now destruct 1.
-apply Pos.lt_succ_r.
-Qed.
+(** Basic properties of comparison *)
-Lemma compare_spec n m : CompareSpec (n=m) (n<m) (m<n) (n ?= m).
+Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
Proof.
-case_eq (n ?= m); intro H; constructor; trivial.
-now apply compare_eq.
-red. now rewrite <- compare_antisym, H.
+destruct n, m; simpl; rewrite ?Pos.compare_eq_iff; split; congruence.
Qed.
-(** Properties of boolean comparisons. *)
-
-Lemma eqb_eq n m : eqb n m = true <-> n=m.
+Theorem compare_lt_iff n m : (n ?= m) = Lt <-> n < m.
Proof.
-destruct n as [|n], m as [|m]; simpl; try easy'.
-rewrite Pos.eqb_eq. split; intro H. now subst. now destr_eq H.
+reflexivity.
Qed.
-Lemma ltb_lt n m : (n <? m) = true <-> n < m.
+Theorem compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
Proof.
- unfold ltb, lt. destruct compare; easy'.
+reflexivity.
Qed.
-Lemma leb_le n m : (n <=? m) = true <-> n <= m.
+Theorem compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
Proof.
- unfold leb, le. destruct compare; easy'.
+destruct n, m; simpl; trivial. apply Pos.compare_antisym.
Qed.
-Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m).
-Proof.
- unfold le, lt, leb. rewrite <- (compare_antisym n m).
- case compare; now constructor.
-Qed.
+(** Some more advanced properties of comparison and orders,
+ including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *)
-Lemma ltb_spec n m : BoolSpec (n<m) (m<=n) (n <? m).
-Proof.
- unfold le, lt, ltb. rewrite <- (compare_antisym n m).
- case compare; now constructor.
-Qed.
+Include BoolOrderFacts.
(** We regroup here some results used for proving the correctness
of more advanced functions. These results will also be provided
@@ -321,14 +289,10 @@ Qed.
Lemma sub_add n m : n <= m -> m - n + n = m.
Proof.
- destruct n as [|p], m as [|q]; simpl; try easy'.
- unfold le, compare. rewrite Pos.compare_antisym. intros H.
- assert (H1 := Pos.sub_mask_compare q p).
- assert (H2 := Pos.sub_mask_add q p).
- destruct Pos.sub_mask as [|r|]; simpl in *; f_equal.
- symmetry. now apply Pos.compare_eq.
- rewrite Pos.add_comm. now apply H2.
- rewrite <- H1 in H. now destruct H.
+ destruct n as [|p], m as [|q]; simpl; try easy'. intros H.
+ case Pos.sub_mask_spec; intros; simpl; subst; trivial.
+ now rewrite Pos.add_comm.
+ apply Pos.le_nlt in H. elim H. apply Pos.lt_add_r.
Qed.
Theorem mul_comm n m : n * m = m * n.
@@ -341,11 +305,17 @@ Proof.
now destruct n.
Qed.
+Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m).
+Proof.
+ unfold le, lt, leb. rewrite (compare_antisym n m).
+ case compare; now constructor.
+Qed.
+
Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m.
Proof.
intro H. destruct p. simpl; auto.
destruct n; destruct m.
- elim (lt_irrefl _ H).
+ elim (Pos.lt_irrefl _ H).
red; auto.
rewrite add_0_r in H. simpl in H.
red in H. simpl in H.
@@ -355,6 +325,14 @@ Qed.
End BootStrap.
+(** Specification of lt and le. *)
+
+Lemma lt_succ_r n m : n < succ m <-> n<=m.
+Proof.
+destruct n as [|p], m as [|q]; simpl; try easy'.
+split. now destruct p. now destruct 1.
+apply Pos.lt_succ_r.
+Qed.
(** Properties of [double] and [succ_double] *)
@@ -426,13 +404,13 @@ Qed.
Theorem min_r n m : m <= n -> min n m = m.
Proof.
-unfold min, le. rewrite <- compare_antisym.
+unfold min, le. rewrite compare_antisym.
case compare_spec; trivial. now destruct 2.
Qed.
Theorem max_l n m : m <= n -> max n m = n.
Proof.
-unfold max, le. rewrite <- compare_antisym.
+unfold max, le. rewrite compare_antisym.
case compare_spec; auto. now destruct 2.
Qed.
@@ -762,7 +740,7 @@ Lemma shiftl_spec_low a n m : m<n ->
Proof.
revert a m.
induction n using peano_ind; intros a m H.
- elim (le_0_l m). now rewrite <- compare_antisym, H.
+ elim (le_0_l m). now rewrite compare_antisym, H.
rewrite shiftl_succ_r.
destruct m. now destruct (shiftl a n).
rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l.
@@ -906,8 +884,6 @@ Qed.
(** Instantiation of generic properties of natural numbers *)
-Set Inline Level 30. (* For inlining only t eq zero one two *)
-
Include NProp
<+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
@@ -919,34 +895,34 @@ Bind Scope N_scope with N.
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.
-Qed.
-
-Lemma ge_le_iff n m : n >= m <-> m <= n.
-Proof.
- split. apply ge_le. apply le_ge.
+ apply ge_le_iff.
Qed.
(** Auxiliary results about right shift on positive numbers,
@@ -1097,7 +1073,6 @@ Notation Nle_0 := N.le_0_l (only parsing).
Notation Ncompare_refl := N.compare_refl (only parsing).
Notation Ncompare_Eq_eq := N.compare_eq (only parsing).
Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing).
-Notation Ncompare_antisym := N.compare_antisym (only parsing).
Notation Nlt_irrefl := N.lt_irrefl (only parsing).
Notation Nlt_trans := N.lt_trans (only parsing).
Notation Nle_lteq := N.lt_eq_cases (only parsing).
@@ -1130,6 +1105,8 @@ Lemma Nmult_plus_distr_l n m p : p * (n + m) = p * n + p * m.
Proof (N.mul_add_distr_l p n m).
Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
Proof (fun H => proj1 (N.mul_cancel_r n m p H)).
+Lemma Ncompare_antisym n m : CompOpp (n ?= m) = (m ?= n).
+Proof (eq_sym (N.compare_antisym n m)).
Definition N_ind_double a P f0 f2 fS2 := N.binary_ind P f0 f2 fS2 a.
Definition N_rec_double a P f0 f2 fS2 := N.binary_rec P f0 f2 fS2 a.
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 237ac93ef..a5be98aab 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -111,14 +111,12 @@ Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.
(** Let's group everything *)
-Module Type ZAxiomsSig :=
- ZAxiomsMiniSig <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn
- <+ NZParity.NZParity
+Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions
+ <+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
<+ ZDiv <+ ZQuot <+ NZBits.NZBits.
-Module Type ZAxiomsSig' :=
- ZAxiomsMiniSig' <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn
- <+ NZParity.NZParity
+Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions'
+ <+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
<+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 236c56b9f..71d275601 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -56,6 +56,9 @@ Infix "*" := BigZ.mul : bigZ_scope.
Infix "/" := BigZ.div : bigZ_scope.
Infix "^" := BigZ.pow : bigZ_scope.
Infix "?=" := BigZ.compare : bigZ_scope.
+Infix "=?" := BigZ.eqb (at level 70, no associativity) : bigZ_scope.
+Infix "<=?" := BigZ.leb (at level 70, no associativity) : bigZ_scope.
+Infix "<?" := BigZ.ltb (at level 70, no associativity) : bigZ_scope.
Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope.
Infix "<" := BigZ.lt : bigZ_scope.
@@ -112,7 +115,7 @@ symmetry. apply BigZ.add_opp_r.
exact BigZ.add_opp_diag_r.
Qed.
-Lemma BigZeqb_correct : forall x y, BigZ.eq_bool x y = true -> x==y.
+Lemma BigZeqb_correct : forall x y, (x =? y) = true -> x==y.
Proof. now apply BigZ.eqb_eq. Qed.
Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n).
@@ -127,11 +130,11 @@ induction p; simpl; intros; BigZ.zify; rewrite ?IHp; auto.
Qed.
Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _)
- (fun a b => if BigZ.eq_bool b 0 then (0,a) else BigZ.div_eucl a b).
+ (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b).
Proof.
constructor. unfold id. intros a b.
BigZ.zify.
-generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+case Z.eqb_spec.
BigZ.zify. auto with zarith.
intros NEQ.
generalize (BigZ.spec_div_eucl a b).
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index da501e9ef..8e53e4d62 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -109,21 +109,49 @@ Module Make (N:NType) <: ZType.
exfalso. omega.
Qed.
- Definition eq_bool x y :=
+ Definition eqb x y :=
match compare x y with
| Eq => true
| _ => false
end.
- Theorem spec_eq_bool:
- forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y).
+ Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y).
Proof.
- unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity.
+ apply Bool.eq_iff_eq_true.
+ unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare.
+ split; [now destruct Z.compare | now intros ->].
Qed.
Definition lt n m := to_Z n < to_Z m.
Definition le n m := to_Z n <= to_Z m.
+
+ Definition ltb (x y : t) : bool :=
+ match compare x y with
+ | Lt => true
+ | _ => false
+ end.
+
+ Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare.
+ split; [now destruct Z.compare | now intros ->].
+ Qed.
+
+ Definition leb (x y : t) : bool :=
+ match compare x y with
+ | Gt => false
+ | _ => true
+ end.
+
+ Theorem spec_leb x y : leb x y = Z.leb (to_Z x) (to_Z y).
+ Proof.
+ apply Bool.eq_iff_eq_true.
+ rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
+ destruct Z.compare; split; try easy. now destruct 1.
+ Qed.
+
Definition min n m := match compare n m with Gt => m | _ => n end.
Definition max n m := match compare n m with Lt => m | _ => n end.
@@ -372,12 +400,12 @@ Module Make (N:NType) <: ZType.
(Pos q, Pos r)
| Pos nx, Neg ny =>
let (q, r) := N.div_eucl nx ny in
- if N.eq_bool N.zero r
+ if N.eqb N.zero r
then (Neg q, zero)
else (Neg (N.succ q), Neg (N.sub ny r))
| Neg nx, Pos ny =>
let (q, r) := N.div_eucl nx ny in
- if N.eq_bool N.zero r
+ if N.eqb N.zero r
then (Neg q, zero)
else (Neg (N.succ q), Pos (N.sub ny r))
| Neg nx, Neg ny =>
@@ -401,32 +429,32 @@ Module Make (N:NType) <: ZType.
(* Pos Neg *)
generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
simpl; rewrite Hq, N.spec_0; auto).
change (- Zpos py) with (Zneg py).
assert (GT : Zpos py > 0) by (compute; auto).
generalize (Z_div_mod (Zpos px) (Zpos py) GT).
unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
break_nonneg r pr EQr.
subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
(* Neg Pos *)
generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr;
+ try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr;
simpl; rewrite Hq, N.spec_0; auto).
change (- Zpos px) with (Zneg px).
assert (GT : Zpos py > 0) by (compute; auto).
generalize (Z_div_mod (Zpos px) (Zpos py) GT).
unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r').
intros (EQ,MOD). injection 1. intros Hr' Hq'.
- rewrite N.spec_eq_bool, N.spec_0, Hr'.
+ rewrite N.spec_eqb, N.spec_0, Hr'.
break_nonneg r pr EQr.
subst; simpl. rewrite N.spec_0; auto.
- subst. lazy iota beta delta [Zeq_bool Zcompare].
+ subst. lazy iota beta delta [Z.eqb].
rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *.
(* Neg Neg *)
generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r).
@@ -464,7 +492,7 @@ Module Make (N:NType) <: ZType.
end.
Definition rem x y :=
- if eq_bool y zero then x
+ if eqb y zero then x
else
match x, y with
| Pos nx, Pos ny => Pos (N.modulo nx ny)
@@ -483,8 +511,8 @@ Module Make (N:NType) <: ZType.
Lemma spec_rem : forall x y,
to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
Proof.
- intros x y. unfold rem. rewrite spec_eq_bool, spec_0.
- assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
+ intros x y. unfold rem. rewrite spec_eqb, spec_0.
+ case Z.eqb_spec; intros Hy.
now rewrite Hy, Zrem_0_r.
destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
rewrite N.spec_modulo, ?Zrem_opp_r, ?Zrem_opp_l, ?Zopp_involutive;
@@ -551,7 +579,7 @@ Module Make (N:NType) <: ZType.
Definition norm_pos z :=
match z with
| Pos _ => z
- | Neg n => if N.eq_bool n N.zero then Pos n else z
+ | Neg n => if N.eqb n N.zero then Pos n else z
end.
Definition testbit a n :=
@@ -623,19 +651,17 @@ Module Make (N:NType) <: ZType.
Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x.
Proof.
intros [x|x]; simpl; trivial.
- rewrite N.spec_eq_bool, N.spec_0.
- assert (H := Zeq_bool_if (N.to_Z x) 0).
- destruct Zeq_bool; simpl; auto with zarith.
+ rewrite N.spec_eqb, N.spec_0.
+ case Z.eqb_spec; simpl; auto with zarith.
Qed.
Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y ->
0 < N.to_Z y.
Proof.
intros [x|x] y; simpl; try easy.
- rewrite N.spec_eq_bool, N.spec_0.
- assert (H := Zeq_bool_if (N.to_Z x) 0).
- destruct Zeq_bool; simpl; try easy.
- inversion 1; subst. generalize (N.spec_pos y); auto with zarith.
+ rewrite N.spec_eqb, N.spec_0.
+ case Z.eqb_spec; simpl; try easy.
+ inversion 2. subst. generalize (N.spec_pos y); auto with zarith.
Qed.
Ltac destr_norm_pos x :=
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 9981fab71..0f2862df7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-Require Import ZArith Znumtheory.
+Require Import BinInt.
Open Scope Z_scope.
@@ -33,7 +33,9 @@ Module Type ZType.
Parameter spec_of_Z: forall x, to_Z (of_Z x) = x.
Parameter compare : t -> t -> comparison.
- Parameter eq_bool : t -> t -> bool.
+ Parameter eqb : t -> t -> bool.
+ Parameter ltb : t -> t -> bool.
+ Parameter leb : t -> t -> bool.
Parameter min : t -> t -> t.
Parameter max : t -> t -> t.
Parameter zero : t.
@@ -71,10 +73,12 @@ Module Type ZType.
Parameter lxor : t -> t -> t.
Parameter div2 : t -> t.
- Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
- Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
- Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
- Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
+ Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]).
+ Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]).
+ Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]).
+ Parameter spec_min : forall x y, [min x y] = Z.min [x] [y].
+ Parameter spec_max : forall x y, [max x y] = Z.max [x] [y].
Parameter spec_0: [zero] = 0.
Parameter spec_1: [one] = 1.
Parameter spec_2: [two] = 2.
@@ -89,27 +93,27 @@ Module Type ZType.
Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
- Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
+ Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
+ Parameter spec_log2: forall x, [log2 x] = Z.log2 [x].
Parameter spec_div_eucl: forall x y,
- let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+ let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y].
Parameter spec_div: forall x y, [div x y] = [x] / [y].
Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
Parameter spec_quot: forall x y, [quot x y] = [x] รท [y].
- Parameter spec_rem: forall x y, [rem x y] = Zrem [x] [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
- Parameter spec_abs : forall x, [abs x] = Zabs [x].
- Parameter spec_even : forall x, even x = Zeven_bool [x].
- Parameter spec_odd : forall x, odd x = Zodd_bool [x].
- Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
- Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
- Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
- Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
- Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
- Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
- Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
+ Parameter spec_rem: forall x y, [rem x y] = Z.rem [x] [y].
+ Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
+ Parameter spec_sgn : forall x, [sgn x] = Z.sgn [x].
+ Parameter spec_abs : forall x, [abs x] = Z.abs [x].
+ Parameter spec_even : forall x, even x = Z.even [x].
+ Parameter spec_odd : forall x, odd x = Z.odd [x].
+ Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Z.div2 [x].
End ZType.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index a055007f4..e3fc512e7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import Bool ZArith Nnat ZAxioms ZSig.
+Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig.
(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
@@ -15,9 +15,9 @@ Module ZTypeIsZAxioms (Import Z : ZType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
- spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot spec_rem
- spec_testbit spec_shiftl spec_shiftr
+ spec_compare spec_eqb spec_ltb spec_leb spec_max spec_min
+ spec_abs spec_sgn spec_pow spec_log2 spec_even spec_odd spec_gcd
+ spec_quot spec_rem spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2
: zsimpl.
@@ -138,36 +138,66 @@ Qed.
(** Order *)
-Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
+Lemma eqb_eq x y : eqb x y = true <-> x == y.
Proof.
- intros. zify. destruct (Zcompare_spec [x] [y]); auto.
+ zify. apply Z.eqb_eq.
Qed.
-Definition eqb := eq_bool.
+Lemma leb_le x y : leb x y = true <-> x <= y.
+Proof.
+ zify. apply Z.leb_le.
+Qed.
+
+Lemma ltb_lt x y : ltb x y = true <-> x < y.
+Proof.
+ zify. apply Z.ltb_lt.
+Qed.
+
+Lemma compare_eq_iff n m : compare n m = Eq <-> n == m.
+Proof.
+ intros. zify. apply Z.compare_eq_iff.
+Qed.
+
+Lemma compare_lt_iff n m : compare n m = Lt <-> n < m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
+
+Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
-Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Lemma compare_antisym n m : compare m n = CompOpp (compare n m).
Proof.
- intros. zify. symmetry. apply Zeq_is_eq_bool.
+ intros. zify. apply Z.compare_antisym.
Qed.
+Include BoolOrderFacts Z Z Z [no inline].
+
Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
Proof.
-intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
Proof.
-intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Theorem lt_irrefl : forall n, ~ n < n.
+Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
+Qed.
+
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Proof.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
Qed.
Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
@@ -491,5 +521,5 @@ Qed.
End ZTypeIsZAxioms.
Module ZType_ZAxioms (Z : ZType)
- <: ZAxiomsSig <: HasCompare Z <: HasEqBool Z <: HasMinMax Z
+ <: ZAxiomsSig <: OrderFunctions Z <: HasMinMax Z
:= Z <+ ZTypeIsZAxioms.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 09438628d..45a2cf3e1 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -32,11 +32,11 @@ End NDivSpecific.
(** We now group everything together. *)
-Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions
<+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
<+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits.
-Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions'
<+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
<+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index d2c93bbfd..b06e42ca2 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -62,6 +62,9 @@ Infix "*" := BigN.mul : bigN_scope.
Infix "/" := BigN.div : bigN_scope.
Infix "^" := BigN.pow : bigN_scope.
Infix "?=" := BigN.compare : bigN_scope.
+Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope.
+Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope.
+Infix "<?" := BigN.ltb (at level 70, no associativity) : bigN_scope.
Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope.
Infix "<" := BigN.lt : bigN_scope.
@@ -94,7 +97,7 @@ exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm.
exact BigN.mul_assoc. exact BigN.mul_add_distr_r.
Qed.
-Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y.
+Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y.
Proof. now apply BigN.eqb_eq. Qed.
Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
@@ -107,11 +110,11 @@ induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto.
Qed.
Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
- (fun a b => if BigN.eq_bool b 0 then (0,a) else BigN.div_eucl a b).
+ (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
Proof.
constructor. unfold id. intros a b.
BigN.zify.
-generalize (Zeq_bool_if [b] 0); destruct (Zeq_bool [b] 0).
+case Z.eqb_spec.
BigN.zify. auto with zarith.
intros NEQ.
generalize (BigN.spec_div_eucl a b).
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 23cfec5e9..aabbf87f2 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -301,20 +301,48 @@ Module Make (W0:CyclicType) <: NType.
intros. subst. apply Zcompare_antisym.
Qed.
- Definition eq_bool (x y : t) : bool :=
+ Definition eqb (x y : t) : bool :=
match compare x y with
| Eq => true
| _ => false
end.
- Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y].
+ Theorem spec_eqb x y : eqb x y = Z.eqb [x] [y].
Proof.
- intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity.
+ apply eq_iff_eq_true.
+ unfold eqb. rewrite Z.eqb_eq, <- Z.compare_eq_iff, spec_compare.
+ split; [now destruct Z.compare | now intros ->].
Qed.
Definition lt (n m : t) := [n] < [m].
Definition le (n m : t) := [n] <= [m].
+ Definition ltb (x y : t) : bool :=
+ match compare x y with
+ | Lt => true
+ | _ => false
+ end.
+
+ Theorem spec_ltb x y : ltb x y = Z.ltb [x] [y].
+ Proof.
+ apply eq_iff_eq_true.
+ rewrite Z.ltb_lt. unfold Z.lt, ltb. rewrite spec_compare.
+ split; [now destruct Z.compare | now intros ->].
+ Qed.
+
+ Definition leb (x y : t) : bool :=
+ match compare x y with
+ | Gt => false
+ | _ => true
+ end.
+
+ Theorem spec_leb x y : leb x y = Z.leb [x] [y].
+ Proof.
+ apply eq_iff_eq_true.
+ rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
+ destruct Z.compare; split; try easy. now destruct 1.
+ Qed.
+
Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
Definition max (n m : t) : t := match compare n m with Lt => m | _ => n end.
@@ -560,7 +588,7 @@ Module Make (W0:CyclicType) <: NType.
(** * General Division *)
Definition div_eucl (x y : t) : t * t :=
- if eq_bool y zero then (zero,zero) else
+ if eqb y zero then (zero,zero) else
match compare x y with
| Eq => (one, zero)
| Lt => (zero, x)
@@ -572,8 +600,8 @@ Module Make (W0:CyclicType) <: NType.
([q], [r]) = Zdiv_eucl [x] [y].
Proof.
intros x y. unfold div_eucl.
- rewrite spec_eq_bool, spec_compare, spec_0.
- generalize (Zeq_bool_if [y] 0); case Zeq_bool.
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
intros ->. rewrite spec_0. destruct [x]; auto.
intros H'.
assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
@@ -685,7 +713,7 @@ Module Make (W0:CyclicType) <: NType.
(** * General Modulo *)
Definition modulo (x y : t) : t :=
- if eq_bool y zero then zero else
+ if eqb y zero then zero else
match compare x y with
| Eq => zero
| Lt => x
@@ -696,8 +724,8 @@ Module Make (W0:CyclicType) <: NType.
forall x y, [modulo x y] = [x] mod [y].
Proof.
intros x y. unfold modulo.
- rewrite spec_eq_bool, spec_compare, spec_0.
- generalize (Zeq_bool_if [y] 0). case Zeq_bool.
+ rewrite spec_eqb, spec_compare, spec_0.
+ case Z.eqb_spec.
intros ->; rewrite spec_0. destruct [x]; auto.
intro H'.
assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).
@@ -1157,16 +1185,16 @@ Module Make (W0:CyclicType) <: NType.
Definition log2 : t -> t := Eval red_t in
let log2 := iter_t log2n in
- fun x => if eq_bool x zero then zero else log2 x.
+ fun x => if eqb x zero then zero else log2 x.
Lemma log2_fold :
- log2 = fun x => if eq_bool x zero then zero else iter_t log2n x.
+ log2 = fun x => if eqb x zero then zero else iter_t log2n x.
Proof. red_t; reflexivity. Qed.
Lemma spec_log2_0 : forall x, [x] = 0 -> [log2 x] = 0.
Proof.
intros x H. rewrite log2_fold.
- rewrite spec_eq_bool, H. rewrite spec_0. simpl. exact spec_0.
+ rewrite spec_eqb, H. rewrite spec_0. simpl. exact spec_0.
Qed.
Lemma head0_zdigits : forall n (x : dom_t n),
@@ -1193,8 +1221,8 @@ Module Make (W0:CyclicType) <: NType.
2^[log2 x] <= [x] < 2^([log2 x]+1).
Proof.
intros x H. rewrite log2_fold.
- rewrite spec_eq_bool. rewrite spec_0.
- generalize (Zeq_bool_if [x] 0). destruct Zeq_bool.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
auto with zarith.
clear H.
destr_t x as (n,x). intros H.
@@ -1229,8 +1257,8 @@ Module Make (W0:CyclicType) <: NType.
[log2 x] = Zpos (digits x) - [head0 x] - 1.
Proof.
intros. rewrite log2_fold.
- rewrite spec_eq_bool. rewrite spec_0.
- generalize (Zeq_bool_if [x] 0). destruct Zeq_bool.
+ rewrite spec_eqb. rewrite spec_0.
+ case Z.eqb_spec.
auto with zarith.
intros _. revert H. rewrite digits_fold, head0_fold. destr_t x as (n,x).
rewrite ZnZ.spec_sub_carry.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0cf9ae441..8a26ec6e3 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -14,6 +14,31 @@ Require Import
(** Functions not already defined *)
+Fixpoint leb n m :=
+ match n, m with
+ | O, _ => true
+ | _, O => false
+ | S n', S m' => leb n' m'
+ end.
+
+Definition ltb n m := leb (S n) m.
+
+Infix "<=?" := leb (at level 70) : nat_scope.
+Infix "<?" := ltb (at level 70) : nat_scope.
+
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
+Proof.
+ revert m.
+ induction n. split; auto with arith.
+ destruct m; simpl. now split.
+ rewrite IHn. split; auto with arith.
+Qed.
+
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
+Proof.
+ unfold ltb, lt. apply leb_le.
+Qed.
+
Fixpoint pow n m :=
match m with
| O => 1
@@ -681,6 +706,8 @@ Definition sub := minus.
Definition mul := mult.
Definition lt := lt.
Definition le := le.
+Definition ltb := ltb.
+Definition leb := leb.
Definition min := min.
Definition max := max.
@@ -692,6 +719,8 @@ Definition min_r := min_r.
Definition eqb_eq := beq_nat_true_iff.
Definition compare_spec := nat_compare_spec.
Definition eq_dec := eq_nat_dec.
+Definition leb_le := leb_le.
+Definition ltb_lt := ltb_lt.
Definition Even := Even.
Definition Odd := Odd.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index f186c55b4..662648432 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-Require Import ZArith Znumtheory.
+Require Import BinInt.
Open Scope Z_scope.
@@ -35,7 +35,9 @@ Module Type NType.
Definition le n m := [n] <= [m].
Parameter compare : t -> t -> comparison.
- Parameter eq_bool : t -> t -> bool.
+ Parameter eqb : t -> t -> bool.
+ Parameter ltb : t -> t -> bool.
+ Parameter leb : t -> t -> bool.
Parameter max : t -> t -> t.
Parameter min : t -> t -> t.
Parameter zero : t.
@@ -67,39 +69,41 @@ Module Type NType.
Parameter lxor : t -> t -> t.
Parameter div2 : t -> t.
- Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
- Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
- Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
- Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
+ Parameter spec_compare: forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eqb : forall x y, eqb x y = ([x] =? [y]).
+ Parameter spec_ltb : forall x y, ltb x y = ([x] <? [y]).
+ Parameter spec_leb : forall x y, leb x y = ([x] <=? [y]).
+ Parameter spec_max : forall x y, [max x y] = Z.max [x] [y].
+ Parameter spec_min : forall x y, [min x y] = Z.min [x] [y].
Parameter spec_0: [zero] = 0.
Parameter spec_1: [one] = 1.
Parameter spec_2: [two] = 2.
Parameter spec_succ: forall n, [succ n] = [n] + 1.
Parameter spec_add: forall x y, [add x y] = [x] + [y].
- Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
- Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]).
+ Parameter spec_pred: forall x, [pred x] = Z.max 0 ([x] - 1).
+ Parameter spec_sub: forall x y, [sub x y] = Z.max 0 ([x] - [y]).
Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
Parameter spec_square: forall x, [square x] = [x] * [x].
Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
- Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
+ Parameter spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
+ Parameter spec_log2: forall x, [log2 x] = Z.log2 [x].
Parameter spec_div_eucl: forall x y,
- let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+ let (q,r) := div_eucl x y in ([q], [r]) = Z.div_eucl [x] [y].
Parameter spec_div: forall x y, [div x y] = [x] / [y].
Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
- Parameter spec_even: forall x, even x = Zeven_bool [x].
- Parameter spec_odd: forall x, odd x = Zodd_bool [x].
- Parameter spec_testbit: forall x p, testbit x p = Ztestbit [x] [p].
- Parameter spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p].
- Parameter spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p].
- Parameter spec_land: forall x y, [land x y] = Zand [x] [y].
- Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
- Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
- Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
+ Parameter spec_gcd: forall a b, [gcd a b] = Z.gcd [a] [b].
+ Parameter spec_even: forall x, even x = Z.even [x].
+ Parameter spec_odd: forall x, odd x = Z.odd [x].
+ Parameter spec_testbit: forall x p, testbit x p = Z.testbit [x] [p].
+ Parameter spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p].
+ Parameter spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p].
+ Parameter spec_land: forall x y, [land x y] = Z.land [x] [y].
+ Parameter spec_lor: forall x y, [lor x y] = Z.lor [x] [y].
+ Parameter spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y].
+ Parameter spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y].
+ Parameter spec_div2: forall x, [div2 x] = Z.div2 [x].
End NType.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 84682820d..878e46fea 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Require Import ZArith Nnat Ndigits NAxioms NDiv NSig.
+Require Import ZArith OrdersFacts Nnat Ndigits NAxioms NDiv NSig.
(** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
@@ -15,8 +15,8 @@ Module NTypeIsNAxioms (Import N : NType').
Hint Rewrite
spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
- spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt
- spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
+ spec_div spec_modulo spec_gcd spec_compare spec_eqb spec_ltb spec_leb
+ spec_sqrt spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
: nsimpl.
@@ -126,36 +126,66 @@ Qed.
(** Order *)
-Lemma compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
+Lemma eqb_eq x y : eqb x y = true <-> x == y.
Proof.
- intros. zify. destruct (Zcompare_spec [x] [y]); auto.
+ zify. apply Z.eqb_eq.
Qed.
-Definition eqb := eq_bool.
+Lemma leb_le x y : leb x y = true <-> x <= y.
+Proof.
+ zify. apply Z.leb_le.
+Qed.
+
+Lemma ltb_lt x y : ltb x y = true <-> x < y.
+Proof.
+ zify. apply Z.ltb_lt.
+Qed.
+
+Lemma compare_eq_iff n m : compare n m = Eq <-> n == m.
+Proof.
+ intros. zify. apply Z.compare_eq_iff.
+Qed.
+
+Lemma compare_lt_iff n m : compare n m = Lt <-> n < m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
+
+Lemma compare_le_iff n m : compare n m <> Gt <-> n <= m.
+Proof.
+ intros. zify. reflexivity.
+Qed.
-Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Lemma compare_antisym n m : compare m n = CompOpp (compare n m).
Proof.
- intros. zify. symmetry. apply Zeq_is_eq_bool.
+ intros. zify. apply Z.compare_antisym.
Qed.
+Include BoolOrderFacts N N N [no inline].
+
Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
Proof.
-intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Instance eqb_wd : Proper (eq ==> eq ==> Logic.eq) eqb.
Proof.
-intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Instance ltb_wd : Proper (eq ==> eq ==> Logic.eq) ltb.
Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
Qed.
-Theorem lt_irrefl : forall n, ~ n < n.
+Instance leb_wd : Proper (eq ==> eq ==> Logic.eq) leb.
Proof.
-intros. zify. omega.
+intros x x' Hx y y' Hy. zify. now rewrite Hx, Hy.
+Qed.
+
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Proof.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
Qed.
Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
@@ -474,5 +504,5 @@ Qed.
End NTypeIsNAxioms.
Module NType_NAxioms (N : NType)
- <: NAxiomsSig <: HasCompare N <: HasEqBool N <: HasMinMax N
+ <: NAxiomsSig <: OrderFunctions N <: HasMinMax N
:= N <+ NTypeIsNAxioms.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 75a548ca9..d4db2c66d 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -57,7 +57,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Definition to_Q (q: t) :=
match q with
| Qz x => Z.to_Z x # 1
- | Qq x y => if N.eq_bool y N.zero then 0
+ | Qq x y => if N.eqb y N.zero then 0
else Z.to_Z x # Z2P (N.to_Z y)
end.
@@ -79,15 +79,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
*)
Ltac destr_eqb :=
match goal with
- | |- context [Z.eq_bool ?x ?y] =>
- rewrite (Z.spec_eq_bool x y);
- generalize (Zeq_bool_if (Z.to_Z x) (Z.to_Z y));
- case (Zeq_bool (Z.to_Z x) (Z.to_Z y));
+ | |- context [Z.eqb ?x ?y] =>
+ rewrite (Z.spec_eqb x y);
+ case (Z.eqb_spec (Z.to_Z x) (Z.to_Z y));
destr_eqb
- | |- context [N.eq_bool ?x ?y] =>
- rewrite (N.spec_eq_bool x y);
- generalize (Zeq_bool_if (N.to_Z x) (N.to_Z y));
- case (Zeq_bool (N.to_Z x) (N.to_Z y));
+ | |- context [N.eqb ?x ?y] =>
+ rewrite (N.spec_eqb x y);
+ case (Z.eqb_spec (N.to_Z x) (N.to_Z y));
[ | let H:=fresh "H" in
try (intro H;generalize (N_to_Z_pos _ H); clear H)];
destr_eqb
@@ -145,13 +143,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
match x, y with
| Qz zx, Qz zy => Z.compare zx zy
| Qz zx, Qq ny dy =>
- if N.eq_bool dy N.zero then Z.compare zx Z.zero
+ if N.eqb dy N.zero then Z.compare zx Z.zero
else Z.compare (Z.mul zx (Z_of_N dy)) ny
| Qq nx dx, Qz zy =>
- if N.eq_bool dx N.zero then Z.compare Z.zero zy
+ if N.eqb dx N.zero then Z.compare Z.zero zy
else Z.compare nx (Z.mul zy (Z_of_N dx))
| Qq nx dx, Qq ny dy =>
- match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
+ match N.eqb dx N.zero, N.eqb dy N.zero with
| true, true => Eq
| true, false => Z.compare Z.zero ny
| false, true => Z.compare nx Z.zero
@@ -301,15 +299,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
match y with
| Qz zy => Qz (Z.add zx zy)
| Qq ny dy =>
- if N.eq_bool dy N.zero then x
+ if N.eqb dy N.zero then x
else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
end
| Qq nx dx =>
- if N.eq_bool dx N.zero then y
+ if N.eqb dx N.zero then y
else match y with
| Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx
| Qq ny dy =>
- if N.eq_bool dy N.zero then x
+ if N.eqb dy N.zero then x
else
let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
let d := N.mul dx dy in
@@ -333,15 +331,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
match y with
| Qz zy => Qz (Z.add zx zy)
| Qq ny dy =>
- if N.eq_bool dy N.zero then x
+ if N.eqb dy N.zero then x
else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
end
| Qq nx dx =>
- if N.eq_bool dx N.zero then y
+ if N.eqb dx N.zero then y
else match y with
| Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx
| Qq ny dy =>
- if N.eq_bool dy N.zero then x
+ if N.eqb dy N.zero then x
else
let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in
let d := N.mul dx dy in
@@ -378,8 +376,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Proof.
intros [z | x y]; simpl.
rewrite Z.spec_opp; auto.
- match goal with |- context[N.eq_bool ?X ?Y] =>
- generalize (N.spec_eq_bool X Y); case N.eq_bool
+ match goal with |- context[N.eqb ?X ?Y] =>
+ generalize (N.spec_eqb X Y); case N.eqb
end; auto; rewrite N.spec_0.
rewrite Z.spec_opp; auto.
Qed.
@@ -429,26 +427,29 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
| Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy)
end.
+ Ltac nsubst :=
+ match goal with E : N.to_Z _ = _ |- _ => rewrite E in * end.
+
Theorem spec_mul : forall x y, [mul x y] == [x] * [y].
Proof.
intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl.
rewrite Pmult_1_r, Z2P_correct; auto.
destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
- rewrite H0 in H1; auto with zarith.
- rewrite H0 in H1; auto with zarith.
- rewrite H in H1; nzsimpl; auto with zarith.
+ nsubst; auto with zarith.
+ nsubst; auto with zarith.
+ nsubst; nzsimpl; auto with zarith.
rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
Qed.
Definition norm_denum n d :=
- if N.eq_bool d N.one then Qz n else Qq n d.
+ if N.eqb d N.one then Qz n else Qq n d.
Lemma spec_norm_denum : forall n d,
[norm_denum n d] == [Qq n d].
Proof.
unfold norm_denum; intros; simpl; qsimpl.
congruence.
- rewrite H0 in *; auto with zarith.
+ nsubst; auto with zarith.
Qed.
Definition irred n d :=
@@ -528,7 +529,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
Qed.
Definition mul_norm_Qz_Qq z n d :=
- if Z.eq_bool z Z.zero then zero
+ if Z.eqb z Z.zero then zero
else
let gcd := N.gcd (Zabs_N z) d in
match N.compare gcd N.one with
@@ -561,7 +562,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite spec_norm_denum.
qsimpl.
rewrite Zdiv_gcd_zero in GT; auto with zarith.
- rewrite H in *. rewrite Zdiv_0_l in *; discriminate.
+ nsubst. rewrite Zdiv_0_l in *; discriminate.
rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc.
rewrite Zgcd_div_swap0; try romega.
ring.
@@ -637,13 +638,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite spec_norm_denum.
qsimpl.
- destruct (Zmult_integral _ _ H0) as [Eq|Eq].
+ match goal with E : (_ * _ = 0)%Z |- _ =>
+ destruct (Zmult_integral _ _ E) as [Eq|Eq] end.
rewrite Eq in *; simpl in *.
rewrite <- Hg2' in *; auto with zarith.
rewrite Eq in *; simpl in *.
rewrite <- Hg2 in *; auto with zarith.
- destruct (Zmult_integral _ _ H) as [Eq|Eq].
+ match goal with E : (_ * _ = 0)%Z |- _ =>
+ destruct (Zmult_integral _ _ E) as [Eq|Eq] end.
rewrite Hz' in Eq; rewrite Eq in *; auto with zarith.
rewrite Hz in Eq; rewrite Eq in *; auto with zarith.
@@ -691,13 +694,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
rewrite Zgcd_1_rel_prime in *.
apply bezout_rel_prime.
- destruct (rel_prime_bezout _ _ H4) as [u v Huv].
+ destruct (rel_prime_bezout (Z.to_Z ny) (N.to_Z dy)) as [u v Huv]; trivial.
apply Bezout_intro with (u*g')%Z (v*g)%Z.
rewrite <- Huv, <- Hg1', <- Hg2. ring.
rewrite Zgcd_1_rel_prime in *.
apply bezout_rel_prime.
- destruct (rel_prime_bezout _ _ H3) as [u v Huv].
+ destruct (rel_prime_bezout (Z.to_Z nx) (N.to_Z dx)) as [u v Huv]; trivial.
apply Bezout_intro with (u*g)%Z (v*g')%Z.
rewrite <- Huv, <- Hg2', <- Hg1. ring.
Qed.
@@ -755,10 +758,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destr_eqb; nzsimpl; intros.
intros; rewrite Zabs_eq in *; romega.
intros; rewrite Zabs_eq in *; romega.
- clear H1.
- rewrite H0.
- compute; auto.
- clear H1.
+ nsubst; compute; auto.
set (n':=Z.to_Z n) in *; clearbody n'.
rewrite Zabs_eq by romega.
red; simpl.
@@ -770,9 +770,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destr_eqb; nzsimpl; intros.
intros; rewrite Zabs_non_eq in *; romega.
intros; rewrite Zabs_non_eq in *; romega.
- clear H1.
- red; nzsimpl; rewrite H0; compute; auto.
- clear H1.
+ nsubst; compute; auto.
set (n':=Z.to_Z n) in *; clearbody n'.
red; simpl; nzsimpl.
rewrite Zabs_non_eq by romega.
@@ -791,7 +789,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
| Gt => Qq Z.minus_one (Zabs_N z)
end
| Qq n d =>
- if N.eq_bool d N.zero then zero else
+ if N.eqb d N.zero then zero else
match Z.compare Z.zero n with
| Eq => zero
| Lt =>
@@ -928,9 +926,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
destr_eqb; nzsimpl; intros.
apply Qeq_refl.
rewrite N.spec_square in *; nzsimpl.
- elim (Zmult_integral _ _ H0); romega.
- rewrite N.spec_square in *; nzsimpl.
- rewrite H in H0; romega.
+ match goal with E : (_ * _ = 0)%Z |- _ =>
+ elim (Zmult_integral _ _ E); romega end.
+ rewrite N.spec_square in *; nzsimpl; nsubst; romega.
rewrite Z.spec_square, N.spec_square.
red; simpl.
rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto.
@@ -961,8 +959,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
assert (0 < N.to_Z d ^ ' p)%Z by
(apply Zpower_gt_0; auto with zarith).
romega.
- rewrite N.spec_pow_pos, H in *.
- rewrite Zpower_0_l in H0; [romega|discriminate].
+ exfalso.
+ rewrite N.spec_pow_pos in *. nsubst.
+ rewrite Zpower_0_l in *; [romega|discriminate].
rewrite Qpower_decomp.
red; simpl; do 3 f_equal.
rewrite Z2P_correct by (generalize (N.spec_pos d); romega).
@@ -981,8 +980,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
revert H.
unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl.
destr_eqb; nzsimpl; simpl; intros.
- rewrite N.spec_pow_pos in H0.
- rewrite H, Zpower_0_l in *; [romega|discriminate].
+ exfalso.
+ rewrite N.spec_pow_pos in *. nsubst.
+ rewrite Zpower_0_l in *; [romega|discriminate].
rewrite Z2P_correct in *; auto.
rewrite N.spec_pow_pos, Z.spec_pow_pos; auto.
rewrite Zgcd_1_rel_prime in *.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 81421ba6b..852ae591d 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -9,7 +9,7 @@
Require Export BinNums.
Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
- Equalities Orders GenericMinMax Le Plus.
+ Equalities Orders OrdersFacts GenericMinMax Le Plus.
Require Export BinPosDef.
@@ -38,6 +38,10 @@ Module Pos
Include BinPosDef.Pos.
+(** In functor applications that follow, we only inline t and eq *)
+
+Set Inline Level 30.
+
(** * Logical Predicates *)
Definition eq := @Logic.eq positive.
@@ -625,26 +629,121 @@ Proof.
unfold pow. now rewrite iter_succ.
Qed.
+(** ** Properties of [sub_mask] *)
+
+Lemma sub_mask_succ_r p q :
+ sub_mask p (succ q) = sub_mask_carry p q.
+Proof.
+ revert q. induction p; destruct q; simpl; f_equal; trivial; now destruct p.
+Qed.
+
+Theorem sub_mask_carry_spec p q :
+ sub_mask_carry p q = pred_mask (sub_mask p q).
+Proof.
+ revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl;
+ try reflexivity; try rewrite IHp;
+ destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto.
+Qed.
+
+Inductive SubMaskSpec (p q : positive) : mask -> Prop :=
+ | SubIsNul : p = q -> SubMaskSpec p q IsNul
+ | SubIsPos : forall r, q + r = p -> SubMaskSpec p q (IsPos r)
+ | SubIsNeg : forall r, p + r = q -> SubMaskSpec p q IsNeg.
+
+Theorem sub_mask_spec p q : SubMaskSpec p q (sub_mask p q).
+Proof.
+ revert q. induction p; destruct q; simpl; try constructor; trivial.
+ (* p~1 q~1 *)
+ destruct (IHp q); subst; try now constructor.
+ now apply SubIsNeg with r~0.
+ (* p~1 q~0 *)
+ destruct (IHp q); subst; try now constructor.
+ apply SubIsNeg with (pred_double r). symmetry. apply add_xI_pred_double.
+ (* p~0 q~1 *)
+ rewrite sub_mask_carry_spec.
+ destruct (IHp q); subst; try constructor.
+ now apply SubIsNeg with 1.
+ destruct r; simpl; try constructor; simpl.
+ now rewrite add_carry_spec, <- add_succ_r.
+ now rewrite add_carry_spec, <- add_succ_r, succ_pred_double.
+ now rewrite add_1_r.
+ now apply SubIsNeg with r~1.
+ (* p~0 q~0 *)
+ destruct (IHp q); subst; try now constructor.
+ now apply SubIsNeg with r~0.
+ (* p~0 1 *)
+ now rewrite add_1_l, succ_pred_double.
+ (* 1 q~1 *)
+ now apply SubIsNeg with q~0.
+ (* 1 q~0 *)
+ apply SubIsNeg with (pred_double q). now rewrite add_1_l, succ_pred_double.
+Qed.
+
+Theorem sub_mask_nul_iff p q : sub_mask p q = IsNul <-> p = q.
+Proof.
+ split.
+ now case sub_mask_spec.
+ intros <-. induction p; simpl; now rewrite ?IHp.
+Qed.
+
+Theorem sub_mask_diag p : sub_mask p p = IsNul.
+Proof.
+ now apply sub_mask_nul_iff.
+Qed.
+
+Lemma sub_mask_add p q r : sub_mask p q = IsPos r -> q + r = p.
+Proof.
+ case sub_mask_spec; congruence.
+Qed.
+
+Lemma sub_mask_add_diag_l p q : sub_mask (p+q) p = IsPos q.
+Proof.
+ case sub_mask_spec.
+ intros H. rewrite add_comm in H. elim (add_no_neutral _ _ H).
+ intros r H. apply add_cancel_l in H. now f_equal.
+ intros r H. rewrite <- add_assoc, add_comm in H. elim (add_no_neutral _ _ H).
+Qed.
+
+Lemma sub_mask_pos_iff p q r : sub_mask p q = IsPos r <-> q + r = p.
+Proof.
+ split. apply sub_mask_add. intros <-; apply sub_mask_add_diag_l.
+Qed.
+
+Lemma sub_mask_add_diag_r p q : sub_mask p (p+q) = IsNeg.
+Proof.
+ case sub_mask_spec; trivial.
+ intros H. symmetry in H; rewrite add_comm in H. elim (add_no_neutral _ _ H).
+ intros r H. rewrite <- add_assoc, add_comm in H. elim (add_no_neutral _ _ H).
+Qed.
+
+Lemma sub_mask_neg_iff p q : sub_mask p q = IsNeg <-> exists r, p + r = q.
+Proof.
+ split.
+ case sub_mask_spec; try discriminate. intros r Hr _; now exists r.
+ intros (r,<-). apply sub_mask_add_diag_r.
+Qed.
+
(*********************************************************************)
-(** * Properties of boolean equality *)
+(** * Properties of boolean comparisons *)
-Theorem eqb_refl x : eqb x x = true.
+Theorem eqb_eq p q : (p =? q) = true <-> p=q.
Proof.
- induction x; auto.
+ revert q. induction p; destruct q; simpl; rewrite ?IHp; split; congruence.
Qed.
-Theorem eqb_true_eq x y : eqb x y = true -> x=y.
+Theorem ltb_lt p q : (p <? q) = true <-> p < q.
Proof.
- revert y. induction x; destruct y; simpl; intros;
- try discriminate; f_equal; auto.
+ unfold ltb, lt. destruct compare; easy'.
Qed.
-Theorem eqb_eq x y : eqb x y = true <-> x=y.
+Theorem leb_le p q : (p <=? q) = true <-> p <= q.
Proof.
- split. apply eqb_true_eq.
- intros; subst; apply eqb_refl.
+ unfold leb, le. destruct compare; easy'.
Qed.
+(** More about [eqb] *)
+
+Include BoolEqualityFacts.
(**********************************************************************)
(** * Properties of comparison on binary positive numbers *)
@@ -728,46 +827,50 @@ Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare.
Ltac simpl_compare := autorewrite with compare.
Ltac simpl_compare_in H := autorewrite with compare in H.
-(** Comparison and equality *)
+(** Relation between [compare] and [sub_mask] *)
-Theorem compare_refl p : (p ?= p) = Eq.
+Definition mask2cmp (p:mask) : comparison :=
+ match p with
+ | IsNul => Eq
+ | IsPos _ => Gt
+ | IsNeg => Lt
+ end.
+
+Lemma compare_sub_mask p q : (p ?= q) = mask2cmp (sub_mask p q).
Proof.
- induction p; auto.
+ revert q.
+ induction p as [p IHp| p IHp| ]; intros [q|q| ]; simpl; trivial;
+ specialize (IHp q); rewrite ?sub_mask_carry_spec;
+ destruct (sub_mask p q) as [|r|]; simpl in *;
+ try clear r; try destruct r; simpl; trivial;
+ simpl_compare; now rewrite IHp.
Qed.
-(* A generalization of the last property *)
+(** Alternative characterisation of strict order in term of addition *)
-Theorem compare_cont_refl p c :
- compare_cont p p c = c.
+Lemma lt_iff_add p q : p < q <-> exists r, p + r = q.
Proof.
- now rewrite compare_cont_spec, compare_refl.
+ unfold "<". rewrite <- sub_mask_neg_iff, compare_sub_mask.
+ destruct sub_mask; now split.
Qed.
-Theorem compare_eq p q : (p ?= q) = Eq -> p = q.
+Lemma gt_iff_add p q : p > q <-> exists r, q + r = p.
Proof.
- revert q. induction p; destruct q; intros H;
- simpl; try easy; simpl_compare_in H;
- (f_equal; now auto) || (now destruct compare).
+ unfold ">". rewrite compare_sub_mask.
+ split.
+ case_eq (sub_mask p q); try discriminate; intros r Hr _.
+ exists r. now apply sub_mask_pos_iff.
+ intros (r,Hr). apply sub_mask_pos_iff in Hr. now rewrite Hr.
Qed.
-Lemma compare_eq_iff p q : (p ?= q) = Eq <-> p = q.
+(** Basic facts about [compare_cont] *)
+
+Theorem compare_cont_refl p c :
+ compare_cont p p c = c.
Proof.
- split. apply compare_eq.
- intros; subst; apply compare_refl.
+ now induction p.
Qed.
-Lemma compare_lt_iff p q : (p ?= q) = Lt <-> p < q.
-Proof. reflexivity. Qed.
-
-Lemma compare_gt_iff p q : (p ?= q) = Gt <-> p > q.
-Proof. reflexivity. Qed.
-
-Lemma compare_le_iff p q : (p ?= q) <> Gt <-> p <= q.
-Proof. reflexivity. Qed.
-
-Lemma compare_ge_iff p q : (p ?= q) <> Lt <-> p >= q.
-Proof. reflexivity. Qed.
-
Lemma compare_cont_antisym p q c :
CompOpp (compare_cont p q c) = compare_cont q p (CompOpp c).
Proof.
@@ -776,97 +879,67 @@ Proof.
trivial; apply IHp.
Qed.
-Lemma compare_antisym p q : (q ?= p) = CompOpp (p ?= q).
-Proof.
- unfold compare. now rewrite compare_cont_antisym.
-Qed.
+(** Basic facts about [compare] *)
-Lemma gt_lt p q : p > q -> q < p.
+Lemma compare_eq_iff p q : (p ?= q) = Eq <-> p = q.
Proof.
- unfold lt, gt. intros H. now rewrite compare_antisym, H.
+ rewrite compare_sub_mask, <- sub_mask_nul_iff.
+ destruct sub_mask; now split.
Qed.
-Lemma lt_gt p q : p < q -> q > p.
+Lemma compare_antisym p q : (q ?= p) = CompOpp (p ?= q).
Proof.
- unfold lt, gt. intros H. now rewrite compare_antisym, H.
+ unfold compare. now rewrite compare_cont_antisym.
Qed.
-Lemma gt_lt_iff p q : p > q <-> q < p.
-Proof.
- split. apply gt_lt. apply lt_gt.
-Qed.
+Lemma compare_lt_iff p q : (p ?= q) = Lt <-> p < q.
+Proof. reflexivity. Qed.
-Lemma ge_le p q : p >= q -> q <= p.
-Proof.
- unfold le, ge. intros H. contradict H. now apply gt_lt.
-Qed.
+Lemma compare_le_iff p q : (p ?= q) <> Gt <-> p <= q.
+Proof. reflexivity. Qed.
-Lemma le_ge p q : p <= q -> q >= p.
-Proof.
- unfold le, ge. intros H. contradict H. now apply lt_gt.
-Qed.
+(** More properties about [compare] and boolean comparisons,
+ including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *)
-Lemma ge_le_iff p q : p >= q <-> q <= p.
-Proof.
- split. apply ge_le. apply le_ge.
-Qed.
+Include BoolOrderFacts.
-Lemma le_nlt p q : p <= q <-> ~ q < p.
-Proof.
- now rewrite <- ge_le_iff.
-Qed.
+Definition le_lteq := lt_eq_cases.
-Lemma lt_nle p q : p < q <-> ~ q <= p.
-Proof.
- intros. unfold lt, le. rewrite compare_antisym.
- destruct compare; split; auto; easy'.
-Qed.
+(** ** Facts about [gt] and [ge] *)
-Lemma compare_spec p q : CompareSpec (p=q) (p<q) (q<p) (p ?= q).
-Proof.
- destruct (p ?= q) as [ ]_eqn; constructor.
- now apply compare_eq.
- trivial.
- now apply gt_lt.
-Qed.
+(** The predicates [lt] and [le] are now favored in the statements
+ of theorems, 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 le_lteq p q : p <= q <-> p < q \/ p = q.
+Lemma gt_lt_iff p q : p > q <-> q < p.
Proof.
- unfold le, lt. case compare_spec; split; try easy.
- now right.
- now left.
- now destruct 1.
- destruct 1. discriminate.
- subst. unfold lt in *. now rewrite compare_refl in *.
+ unfold lt, gt. now rewrite compare_antisym, CompOpp_iff.
Qed.
-Lemma lt_le_incl p q : p<q -> p<=q.
+Lemma gt_lt p q : p > q -> q < p.
Proof.
- intros. apply le_lteq. now left.
+ apply gt_lt_iff.
Qed.
-(** ** Boolean comparisons *)
-
-Lemma ltb_lt p q : (p <? q) = true <-> p < q.
+Lemma lt_gt p q : p < q -> q > p.
Proof.
- unfold ltb, lt. destruct compare; easy'.
+ apply gt_lt_iff.
Qed.
-Lemma leb_le p q : (p <=? q) = true <-> p <= q.
+Lemma ge_le_iff p q : p >= q <-> q <= p.
Proof.
- unfold leb, le. destruct compare; easy'.
+ unfold le, ge. now rewrite compare_antisym, CompOpp_iff.
Qed.
-Lemma leb_spec p q : BoolSpec (p<=q) (q<p) (p <=? q).
+Lemma ge_le p q : p >= q -> q <= p.
Proof.
- unfold le, lt, leb. rewrite (compare_antisym p q).
- case compare; now constructor.
+ apply ge_le_iff.
Qed.
-Lemma ltb_spec p q : BoolSpec (p<q) (q<=p) (p <? q).
+Lemma le_ge p q : p <= q -> q >= p.
Proof.
- unfold le, lt, ltb. rewrite (compare_antisym p q).
- case compare; now constructor.
+ apply ge_le_iff.
Qed.
(** ** Comparison and the successor *)
@@ -895,7 +968,7 @@ Qed.
Lemma lt_succ_diag_r p : p < succ p.
Proof.
- rewrite lt_succ_r. apply le_lteq. now right.
+ rewrite lt_iff_add. exists 1. apply add_1_r.
Qed.
Lemma compare_succ_succ p q : (succ p ?= succ q) = (p ?= q).
@@ -913,14 +986,9 @@ Proof.
now destruct p.
Qed.
-Lemma ge_1_r p : p >= 1.
-Proof.
- now destruct p.
-Qed.
-
Lemma nlt_1_r p : ~ p < 1.
Proof.
- exact (ge_1_r p).
+ now destruct p.
Qed.
Lemma lt_1_succ p : 1 < succ p.
@@ -930,6 +998,22 @@ Qed.
(** ** Properties of the order *)
+Lemma le_nlt p q : p <= q <-> ~ q < p.
+Proof.
+ now rewrite <- ge_le_iff.
+Qed.
+
+Lemma lt_nle p q : p < q <-> ~ q <= p.
+Proof.
+ intros. unfold lt, le. rewrite compare_antisym.
+ destruct compare; split; auto; easy'.
+Qed.
+
+Lemma lt_le_incl p q : p<q -> p<=q.
+Proof.
+ intros. apply le_lteq. now left.
+Qed.
+
Lemma lt_lt_succ n m : n < m -> n < succ m.
Proof.
intros. now apply lt_succ_r, lt_le_incl.
@@ -945,17 +1029,10 @@ Proof.
unfold le. now rewrite compare_succ_succ.
Qed.
-Lemma lt_irrefl p : ~ p < p.
-Proof.
- unfold lt. now rewrite compare_refl.
-Qed.
-
Lemma lt_trans n m p : n < m -> m < p -> n < p.
Proof.
- induction p using peano_ind; intros H H'.
- elim (nlt_1_r _ H').
- apply lt_lt_succ.
- apply lt_succ_r, le_lteq in H'. destruct H' as [H'|H']; subst; auto.
+ rewrite 3 lt_iff_add. intros (r,Hr) (s,Hs).
+ exists (r+s). now rewrite add_assoc, Hr, Hs.
Qed.
Theorem lt_ind : forall (A : positive -> Prop) (n : positive),
@@ -1042,6 +1119,11 @@ Qed.
(** ** Order and addition *)
+Lemma lt_add_diag_r p q : p < p + q.
+Proof.
+ rewrite lt_iff_add. now exists q.
+Qed.
+
Lemma add_lt_mono_l p q r : q<r <-> p+q < p+r.
Proof.
unfold lt. rewrite add_compare_mono_l. apply iff_refl.
@@ -1166,137 +1248,30 @@ Proof.
symmetry. apply sub_1_r.
Qed.
-Lemma sub_mask_succ_r p q :
- sub_mask p (succ q) = sub_mask_carry p q.
-Proof.
- revert q. induction p ; destruct q; simpl; f_equal; trivial; now destruct p.
-Qed.
-
-Theorem sub_mask_carry_spec p q :
- sub_mask_carry p q = pred_mask (sub_mask p q).
-Proof.
- revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl;
- try reflexivity; try rewrite IHp;
- destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto.
-Qed.
-
Theorem sub_succ_r p q : p - (succ q) = pred (p - q).
Proof.
unfold sub; rewrite sub_mask_succ_r, sub_mask_carry_spec.
destruct (sub_mask p q) as [|[r|r| ]|]; auto.
Qed.
-Lemma double_eq_0_inversion (p:mask) :
- double_mask p = IsNul -> p = IsNul.
-Proof.
- now destruct p.
-Qed.
-
-Lemma succ_double_0_discr (p:mask) : succ_double_mask p <> IsNul.
-Proof.
- now destruct p.
-Qed.
-
-Lemma succ_double_eq_1_inversion (p:mask) :
- succ_double_mask p = IsPos 1 -> p = IsNul.
-Proof.
- now destruct p.
-Qed.
-
-Lemma double_eq_1_discr (p:mask) : double_mask p <> IsPos 1.
-Proof.
- now destruct p.
-Qed.
-
-Definition mask2cmp (p:mask) : comparison :=
- match p with
- | IsNul => Eq
- | IsPos _ => Gt
- | IsNeg => Lt
- end.
-
-Lemma sub_mask_compare p q :
- mask2cmp (sub_mask p q) = (p ?= q).
-Proof.
- symmetry. revert q.
- induction p as [p IHp| p IHp| ]; intros [q|q| ]; simpl; trivial;
- specialize (IHp q); rewrite ?sub_mask_carry_spec;
- destruct (sub_mask p q) as [|r|]; simpl in *;
- try clear r; try destruct r; simpl; trivial;
- simpl_compare; now rewrite IHp.
-Qed.
-
-Theorem sub_mask_nul_iff p q : sub_mask p q = IsNul <-> p = q.
-Proof.
- rewrite <- compare_eq_iff, <- sub_mask_compare.
- destruct (sub_mask p q); now split.
-Qed.
-
-Theorem sub_mask_diag p : sub_mask p p = IsNul.
-Proof.
- now apply sub_mask_nul_iff.
-Qed.
-
(** ** Properties of subtraction without underflow *)
-Lemma sub_mask_carry_pos p q r :
- sub_mask p q = IsPos r ->
- r = 1 \/ sub_mask_carry p q = IsPos (pred r).
-Proof.
- intros H.
- destruct (eq_dec r 1) as [EQ|NE]; [now left|right].
- rewrite sub_mask_carry_spec, H. destruct r; trivial. now elim NE.
-Qed.
-
-Lemma sub_mask_add p q r :
- sub_mask p q = IsPos r -> q + r = p.
-Proof.
- revert q r.
- induction p as [p IHp|p IHp| ]; intros [q|q| ] r H;
- simpl in H; try destr_eq H; try specialize (IHp q);
- rewrite ?sub_mask_carry_spec in H.
- (* p~1 q~1 *)
- destruct (sub_mask p q) as [|r'|]; destr_eq H. subst r; simpl; f_equal; auto.
- (* p~1 q~0 *)
- assert (H' := proj1 (sub_mask_nul_iff p q)).
- destruct (sub_mask p q) as [|r'|]; destr_eq H; subst r; simpl; f_equal; auto.
- symmetry; auto.
- (* p~1 1 *)
- subst r; simpl; f_equal; auto.
- (* p~0 q~1 *)
- destruct (sub_mask p q) as [|[r'|r'| ]|]; destr_eq H; subst r; simpl; f_equal.
- rewrite add_carry_spec, <- add_succ_r. auto.
- rewrite add_carry_spec, <- add_succ_r, succ_pred_double. auto.
- rewrite <- add_1_r. auto.
- (* p~0 q~0 *)
- destruct (sub_mask p q) as [|r'|]; destr_eq H; subst r; simpl; f_equal. auto.
- (* p~0 1 *)
- subst r; now rewrite add_1_l, succ_pred_double.
-Qed.
-
-Lemma sub_mask_pos_iff p q :
- (exists r, sub_mask p q = IsPos r) <-> p > q.
+Lemma sub_mask_pos' p q :
+ q < p -> exists r, sub_mask p q = IsPos r /\ q + r = p.
Proof.
- unfold gt. rewrite <- sub_mask_compare.
- destruct (sub_mask p q) as [|r|]; split; try easy'. now exists r.
+ rewrite lt_iff_add. intros (r,Hr). exists r. split; trivial.
+ now apply sub_mask_pos_iff.
Qed.
Lemma sub_mask_pos p q :
q < p -> exists r, sub_mask p q = IsPos r.
Proof.
- intros. now apply sub_mask_pos_iff, lt_gt.
-Qed.
-
-Lemma sub_mask_pos' p q :
- q < p -> exists r, sub_mask p q = IsPos r /\ q + r = p.
-Proof.
- intros H. destruct (sub_mask_pos p q H) as (r,Hr).
- exists r. split; trivial. now apply sub_mask_add.
+ intros H. destruct (sub_mask_pos' p q H) as (r & Hr & _). now exists r.
Qed.
Theorem sub_add p q : q < p -> (p-q)+q = p.
Proof.
- intros H; destruct (sub_mask_pos p q H) as (r,U).
+ intros H. destruct (sub_mask_pos p q H) as (r,U).
unfold sub. rewrite U. rewrite add_comm. now apply sub_mask_add.
Qed.
@@ -1414,20 +1389,19 @@ Qed.
(** Properties of subtraction with underflow *)
-Lemma sub_mask_neg_iff p q : sub_mask p q = IsNeg <-> p < q.
+Lemma sub_mask_neg_iff' p q : sub_mask p q = IsNeg <-> p < q.
Proof.
- unfold lt. rewrite <- sub_mask_compare.
- destruct sub_mask; now split.
+ rewrite lt_iff_add. apply sub_mask_neg_iff.
Qed.
Lemma sub_mask_neg p q : p<q -> sub_mask p q = IsNeg.
Proof.
- apply sub_mask_neg_iff.
+ apply sub_mask_neg_iff'.
Qed.
Lemma sub_le p q : p<=q -> p-q = 1.
Proof.
- unfold le, sub. rewrite <- sub_mask_compare.
+ unfold le, sub. rewrite compare_sub_mask.
destruct sub_mask; easy'.
Qed.
@@ -1983,14 +1957,13 @@ Notation iter_pos_invariant := Pos.iter_invariant (only parsing).
Notation Ppow_1_r := Pos.pow_1_r (only parsing).
Notation Ppow_succ_r := Pos.pow_succ_r (only parsing).
Notation Peqb_refl := Pos.eqb_refl (only parsing).
-Notation Peqb_true_eq := Pos.eqb_true_eq (only parsing).
Notation Peqb_eq := Pos.eqb_eq (only parsing).
Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing).
Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing).
Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing).
Notation Pcompare_eq_Lt := Pos.compare_lt_iff (only parsing).
Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing).
-Notation Pcompare_eq_Gt := Pos.compare_gt_iff (only parsing).
+
Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing).
Notation ZC1 := Pos.gt_lt (only parsing).
Notation ZC2 := Pos.lt_gt (only parsing).
@@ -2034,11 +2007,6 @@ Notation Ppred_mask := Pos.pred_mask (only parsing).
Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing).
Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing).
Notation Pminus_succ_r := Pos.sub_succ_r (only parsing).
-Notation double_eq_zero_inversion := Pos.succ_double_0_discr (only parsing).
-Notation double_plus_one_zero_discr := Pos.succ_double_0_discr (only parsing).
-Notation double_plus_one_eq_one_inversion :=
- Pos.succ_double_eq_1_inversion (only parsing).
-Notation double_eq_one_discr := Pos.double_eq_1_discr (only parsing).
Notation Pminus_mask_diag := Pos.sub_mask_diag (only parsing).
Notation Pplus_minus_eq := Pos.add_sub (only parsing).
@@ -2062,6 +2030,10 @@ Notation Psize_pos_le := Pos.size_le (only parsing).
(** More complex compatibility facts, expressed as lemmas
(to preserve scopes for instance) *)
+Lemma Peqb_true_eq x y : Pos.eqb x y = true -> x=y.
+Proof. apply Pos.eqb_eq. Qed.
+Lemma Pcompare_eq_Gt p q : (p ?= q) = Gt <-> p > q.
+Proof. reflexivity. Qed.
Lemma Pplus_one_succ_r p : Psucc p = p + 1.
Proof (eq_sym (Pos.add_1_r p)).
Lemma Pplus_one_succ_l p : Psucc p = 1 + p.
@@ -2082,8 +2054,11 @@ Lemma Pminus_mask_Gt p q :
q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).
Proof.
intros H. apply Pos.gt_lt in H.
- destruct (Pos.sub_mask_pos' p q H) as (r & U & V).
- exists r. repeat split; trivial. now apply Pos.sub_mask_carry_pos.
+ destruct (Pos.sub_mask_pos p q H) as (r & U).
+ exists r. repeat split; trivial.
+ now apply Pos.sub_mask_pos_iff.
+ destruct (Pos.eq_dec r 1) as [EQ|NE]; [now left|right].
+ rewrite Pos.sub_mask_carry_spec, U. destruct r; trivial. now elim NE.
Qed.
Lemma Pplus_minus : forall p q, p > q -> q+(p-q) = p.
@@ -2109,6 +2084,10 @@ Qed.
Pminus_mask_IsNeg
ZL10
ZL11
+ double_eq_zero_inversion
+ double_plus_one_zero_discr
+ double_plus_one_eq_one_inversion
+ double_eq_one_discr
Infix "/" := Pdiv2 : positive_scope.
*)
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 2fbdff624..933c4ea0e 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -66,10 +66,19 @@ End HasEqDec.
(** Having [eq_dec] is the same as having a boolean equality plus
a correctness proof. *)
-Module Type HasEqBool (Import E:Eq').
+Module Type HasEqb (Import T:Typ).
Parameter Inline eqb : t -> t -> bool.
- Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
-End HasEqBool.
+End HasEqb.
+
+Module Type EqbSpec (T:Typ)(X:HasEq T)(Y:HasEqb T).
+ Parameter eqb_eq : forall x y, Y.eqb x y = true <-> X.eq x y.
+End EqbSpec.
+
+Module Type EqbNotation (T:Typ)(E:HasEqb T).
+ Infix "=?" := E.eqb (at level 70, no associativity).
+End EqbNotation.
+
+Module Type HasEqBool (E:Eq) := HasEqb E <+ EqbSpec E E.
(** From these basic blocks, we can build many combinations
of static standalone module types. *)
@@ -107,8 +116,10 @@ Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation.
Module Type DecidableType' := DecidableType <+ EqNotation.
Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation.
Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation.
-Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation.
-Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation.
+Module Type BooleanEqualityType' :=
+ BooleanEqualityType <+ EqNotation <+ EqbNotation.
+Module Type BooleanDecidableType' :=
+ BooleanDecidableType <+ EqNotation <+ EqbNotation.
Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
(** * Compatibility wrapper from/to the old version of
@@ -166,9 +177,12 @@ Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
:= E <+ HasEqBool2Dec.
-(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
-Module BoolEqualityFacts (Import E : BooleanEqualityType).
+(** Some properties of boolean equality *)
+
+Module BoolEqualityFacts (Import E : BooleanEqualityType').
+
+(** [eqb] is compatible with [eq] *)
Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
Proof.
@@ -177,6 +191,34 @@ apply eq_true_iff_eq.
now rewrite 2 eqb_eq, Exx', Eyy'.
Qed.
+(** Alternative specification of [eqb] based on [reflect]. *)
+
+Lemma eqb_spec x y : reflect (x==y) (x =? y).
+Proof.
+apply iff_reflect. symmetry. apply eqb_eq.
+Qed.
+
+(** Negated form of [eqb_eq] *)
+
+Lemma eqb_neq x y : (x =? y) = false <-> x ~= y.
+Proof.
+now rewrite <- not_true_iff_false, eqb_eq.
+Qed.
+
+(** Basic equality laws for [eqb] *)
+
+Lemma eqb_refl x : (x =? x) = true.
+Proof.
+now apply eqb_eq.
+Qed.
+
+Lemma eqb_sym x y : (x =? y) = (y =? x).
+Proof.
+apply eq_true_iff_eq. now rewrite 2 eqb_eq.
+Qed.
+
+(** Transitivity is a particular case of [eqb_compat] *)
+
End BoolEqualityFacts.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 99dfb19d5..1d0254397 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -65,20 +65,34 @@ Module Type LeIsLtEq (Import E:EqLtLe').
Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
End LeIsLtEq.
-Module Type HasCompare (Import E:EqLt').
+Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
+Module Type StrOrder' := StrOrder <+ EqLtNotation.
+
+(** Versions with a decidable ternary comparison *)
+
+Module Type HasCmp (Import T:Typ).
Parameter Inline compare : t -> t -> comparison.
+End HasCmp.
+
+Module Type CmpNotation (T:Typ)(C:HasCmp T).
+ Infix "?=" := C.compare (at level 70, no associativity).
+End CmpNotation.
+
+Module Type CmpSpec (Import E:EqLt')(Import C:HasCmp E).
Axiom compare_spec : forall x y, CompareSpec (x==y) (x<y) (y<x) (compare x y).
-End HasCompare.
+End CmpSpec.
+
+Module Type HasCompare (E:EqLt) := HasCmp E <+ CmpSpec E.
-Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
Module Type DecStrOrder := StrOrder <+ HasCompare.
+Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation <+ CmpNotation.
+
Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
-Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
+Module Type OrderedType' := OrderedType <+ EqLtNotation <+ CmpNotation.
-Module Type StrOrder' := StrOrder <+ EqLtNotation.
-Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
-Module Type OrderedType' := OrderedType <+ EqLtNotation.
-Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.
+Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
+Module Type OrderedTypeFull' :=
+ OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation.
(** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
But adding this redundant field allows to see an [OrderedType] as a
@@ -167,50 +181,63 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
Local Coercion is_true : bool >-> Sortclass.
Hint Unfold is_true.
-Module Type HasLeBool (Import T:Typ).
- Parameter Inline leb : t -> t -> bool.
-End HasLeBool.
-
-Module Type HasLtBool (Import T:Typ).
- Parameter Inline ltb : t -> t -> bool.
-End HasLtBool.
+Module Type HasLeb (Import T:Typ).
+ Parameter Inline leb : t -> t -> bool.
+End HasLeb.
-Module Type LeBool := Typ <+ HasLeBool.
-Module Type LtBool := Typ <+ HasLtBool.
+Module Type HasLtb (Import T:Typ).
+ Parameter Inline ltb : t -> t -> bool.
+End HasLtb.
-Module Type LeBoolNotation (E:LeBool).
- Infix "<=?" := E.leb (at level 35).
-End LeBoolNotation.
+Module Type LebNotation (T:Typ)(E:HasLeb T).
+ Infix "<=?" := E.leb (at level 35).
+End LebNotation.
-Module Type LtBoolNotation (E:LtBool).
- Infix "<?" := E.ltb (at level 35).
-End LtBoolNotation.
+Module Type LtbNotation (T:Typ)(E:HasLtb T).
+ Infix "<?" := E.ltb (at level 35).
+End LtbNotation.
-Module Type LeBool' := LeBool <+ LeBoolNotation.
-Module Type LtBool' := LtBool <+ LtBoolNotation.
+Module Type LebSpec (T:Typ)(X:HasLe T)(Y:HasLeb T).
+ Parameter leb_le : forall x y, Y.leb x y = true <-> X.le x y.
+End LebSpec.
-Module Type LeBool_Le (T:Typ)(X:HasLeBool T)(Y:HasLe T).
- Parameter leb_le : forall x y, X.leb x y = true <-> Y.le x y.
-End LeBool_Le.
+Module Type LtbSpec (T:Typ)(X:HasLt T)(Y:HasLtb T).
+ Parameter ltb_lt : forall x y, Y.ltb x y = true <-> X.lt x y.
+End LtbSpec.
-Module Type LtBool_Lt (T:Typ)(X:HasLtBool T)(Y:HasLt T).
- Parameter ltb_lt : forall x y, X.ltb x y = true <-> Y.lt x y.
-End LtBool_Lt.
+Module Type LeBool := Typ <+ HasLeb.
+Module Type LtBool := Typ <+ HasLtb.
+Module Type LeBool' := LeBool <+ LebNotation.
+Module Type LtBool' := LtBool <+ LtbNotation.
-Module Type LeBoolIsTotal (Import X:LeBool').
+Module Type LebIsTotal (Import X:LeBool').
Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true.
-End LeBoolIsTotal.
+End LebIsTotal.
-Module Type TotalLeBool := LeBool <+ LeBoolIsTotal.
-Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal.
+Module Type TotalLeBool := LeBool <+ LebIsTotal.
+Module Type TotalLeBool' := LeBool' <+ LebIsTotal.
-Module Type LeBoolIsTransitive (Import X:LeBool').
+Module Type LebIsTransitive (Import X:LeBool').
Axiom leb_trans : Transitive X.leb.
-End LeBoolIsTransitive.
+End LebIsTransitive.
+
+Module Type TotalTransitiveLeBool := TotalLeBool <+ LebIsTransitive.
+Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LebIsTransitive.
+
+(** Grouping all boolean comparison functions *)
+
+Module Type HasBoolOrdFuns (T:Typ) := HasEqb T <+ HasLtb T <+ HasLeb T.
+
+Module Type HasBoolOrdFuns' (T:Typ) :=
+ HasBoolOrdFuns T <+ EqbNotation T <+ LtbNotation T <+ LebNotation T.
-Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive.
-Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive.
+Module Type BoolOrdSpecs (O:EqLtLe)(F:HasBoolOrdFuns O) :=
+ EqbSpec O O F <+ LtbSpec O O F <+ LebSpec O O F.
+Module Type OrderFunctions (E:EqLtLe) :=
+ HasCompare E <+ HasBoolOrdFuns E <+ BoolOrdSpecs E.
+Module Type OrderFunctions' (E:EqLtLe) :=
+ HasCompare E <+ CmpNotation E <+ HasBoolOrdFuns' E <+ BoolOrdSpecs E.
(** * From [OrderedTypeFull] to [TotalTransitiveLeBool] *)
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index b328ae2e8..a447e8fb5 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -6,15 +6,76 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-Require Import Basics OrdersTac.
+Require Import Bool Basics OrdersTac.
Require Export Orders.
Set Implicit Arguments.
Unset Strict Implicit.
-(** * Properties of [OrderedTypeFull] *)
+(** * Properties of [compare] *)
-Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
+Module Type CompareFacts (Import O:DecStrOrder').
+
+ Local Infix "?=" := compare (at level 70, no associativity).
+
+ Lemma compare_eq_iff x y : (x ?= y) = Eq <-> x==y.
+ Proof.
+ case compare_spec; intro H; split; try easy; intro EQ;
+ contradict H; rewrite EQ; apply irreflexivity.
+ Qed.
+
+ Lemma compare_eq x y : (x ?= y) = Eq -> x==y.
+ Proof.
+ apply compare_eq_iff.
+ Qed.
+
+ Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y.
+ Proof.
+ case compare_spec; intro H; split; try easy; intro LT;
+ contradict LT; rewrite H; apply irreflexivity.
+ Qed.
+
+ Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x.
+ Proof.
+ case compare_spec; intro H; split; try easy; intro LT;
+ contradict LT; rewrite H; apply irreflexivity.
+ Qed.
+
+ Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y).
+ Proof.
+ rewrite compare_lt_iff; intuition.
+ Qed.
+
+ Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x).
+ Proof.
+ rewrite compare_gt_iff; intuition.
+ Qed.
+
+ Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
+
+ Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
+ Proof.
+ intros x x' Hxx' y y' Hyy'.
+ case (compare_spec x' y'); autorewrite with order; now rewrite Hxx', Hyy'.
+ Qed.
+
+ Lemma compare_refl x : (x ?= x) = Eq.
+ Proof.
+ case compare_spec; intros; trivial; now elim irreflexivity with x.
+ Qed.
+
+ Lemma compare_antisym x y : (y ?= x) = CompOpp (x ?= y).
+ Proof.
+ case (compare_spec x y); simpl; autorewrite with order;
+ trivial; now symmetry.
+ Qed.
+
+End CompareFacts.
+
+
+ (** * Properties of [OrderedTypeFull] *)
+
+Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull').
Module OrderTac := OTF_to_OrderTac O.
Ltac order := OrderTac.order.
@@ -47,6 +108,18 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
Proof. iorder. Qed.
+ Include CompareFacts O.
+
+ Lemma compare_le_iff x y : compare x y <> Gt <-> x<=y.
+ Proof.
+ rewrite le_not_gt_iff. apply compare_ngt_iff.
+ Qed.
+
+ Lemma compare_ge_iff x y : compare x y <> Lt <-> y<=x.
+ Proof.
+ rewrite le_not_gt_iff. apply compare_nlt_iff.
+ Qed.
+
End OrderedTypeFullFacts.
@@ -84,50 +157,9 @@ Module OrderedTypeFacts (Import O: OrderedType').
Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
- (** Some more about [compare] *)
-
- Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
- Proof.
- intros; elim_compare x y; intuition; try discriminate; order.
- Qed.
-
- Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y.
- Proof.
- intros; elim_compare x y; intuition; try discriminate; order.
- Qed.
-
- Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x.
- Proof.
- intros; elim_compare x y; intuition; try discriminate; order.
- Qed.
-
- Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x.
- Proof.
- intros; rewrite compare_lt_iff; intuition.
- Qed.
-
- Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y.
- Proof.
- intros; rewrite compare_gt_iff; intuition.
- Qed.
-
- Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
-
- Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
- Proof.
- intros x x' Hxx' y y' Hyy'.
- elim_compare x' y'; autorewrite with order; order.
- Qed.
-
- Lemma compare_refl : forall x, (x ?= x) = Eq.
- Proof.
- intros; elim_compare x x; auto; order.
- Qed.
-
- Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
- Proof.
- intros; elim_compare x y; simpl; autorewrite with order; order.
- Qed.
+ Include CompareFacts O.
+ Notation compare_le_iff := compare_ngt_iff (only parsing).
+ Notation compare_ge_iff := compare_nlt_iff (only parsing).
(** For compatibility reasons *)
Definition eq_dec := eq_dec.
@@ -162,10 +194,6 @@ Module OrderedTypeFacts (Import O: OrderedType').
End OrderedTypeFacts.
-
-
-
-
(** * Tests of the order tactic
Is it at least capable of proving some basic properties ? *)
@@ -232,3 +260,195 @@ Qed.
End OrderedTypeRev.
+Unset Implicit Arguments.
+
+(** * Order relations derived from a [compare] function.
+
+ We factorize here some common properties for ZArith, NArith
+ and co, where [lt] and [le] are defined in terms of [compare].
+ Note that we do not require anything here concerning compatibility
+ of [compare] w.r.t [eq], nor anything concerning transitivity.
+*)
+
+Module Type CompareBasedOrder (Import E:EqLtLe')(Import C:HasCmp E).
+ Include CmpNotation E C.
+ Include IsEq E.
+ Axiom compare_eq_iff : forall x y, (x ?= y) = Eq <-> x == y.
+ Axiom compare_lt_iff : forall x y, (x ?= y) = Lt <-> x < y.
+ Axiom compare_le_iff : forall x y, (x ?= y) <> Gt <-> x <= y.
+ Axiom compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
+End CompareBasedOrder.
+
+Module Type CompareBasedOrderFacts
+ (Import E:EqLtLe')
+ (Import C:HasCmp E)
+ (Import O:CompareBasedOrder E C).
+
+ Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y).
+ Proof.
+ case_eq (compare x y); intros H; constructor.
+ now apply compare_eq_iff.
+ now apply compare_lt_iff.
+ rewrite compare_antisym, CompOpp_iff in H. now apply compare_lt_iff.
+ Qed.
+
+ Lemma compare_eq x y : (x ?= y) = Eq -> x==y.
+ Proof.
+ apply compare_eq_iff.
+ Qed.
+
+ Lemma compare_refl x : (x ?= x) = Eq.
+ Proof.
+ now apply compare_eq_iff.
+ Qed.
+
+ Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x.
+ Proof.
+ now rewrite <- compare_lt_iff, compare_antisym, CompOpp_iff.
+ Qed.
+
+ Lemma compare_ge_iff x y : (x ?= y) <> Lt <-> y<=x.
+ Proof.
+ now rewrite <- compare_le_iff, compare_antisym, CompOpp_iff.
+ Qed.
+
+ Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x).
+ Proof.
+ rewrite compare_gt_iff; intuition.
+ Qed.
+
+ Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y).
+ Proof.
+ rewrite compare_lt_iff; intuition.
+ Qed.
+
+ Lemma compare_nle_iff x y : (x ?= y) = Gt <-> ~(x<=y).
+ Proof.
+ rewrite <- compare_le_iff.
+ destruct compare; split; easy || now destruct 1.
+ Qed.
+
+ Lemma compare_nge_iff x y : (x ?= y) = Lt <-> ~(y<=x).
+ Proof.
+ now rewrite <- compare_nle_iff, compare_antisym, CompOpp_iff.
+ Qed.
+
+ Lemma lt_irrefl x : ~ (x<x).
+ Proof.
+ now rewrite <- compare_lt_iff, compare_refl.
+ Qed.
+
+ Lemma lt_eq_cases n m : n <= m <-> n < m \/ n==m.
+ Proof.
+ rewrite <- compare_lt_iff, <- compare_le_iff, <- compare_eq_iff.
+ destruct (n ?= m); now intuition.
+ Qed.
+
+End CompareBasedOrderFacts.
+
+(** Basic facts about boolean comparisons *)
+
+Module Type BoolOrderFacts
+ (Import E:EqLtLe')
+ (Import C:HasCmp E)
+ (Import F:HasBoolOrdFuns' E)
+ (Import O:CompareBasedOrder E C)
+ (Import S:BoolOrdSpecs E F).
+
+Include CompareBasedOrderFacts E C O.
+
+(** Nota : apart from [eqb_compare] below, facts about [eqb]
+ are in BoolEqualityFacts *)
+
+(** Alternate specifications based on [BoolSpec] and [reflect] *)
+
+Lemma leb_spec0 x y : reflect (x<=y) (x<=?y).
+Proof.
+ apply iff_reflect. symmetry. apply leb_le.
+Qed.
+
+Lemma leb_spec x y : BoolSpec (x<=y) (y<x) (x<=?y).
+Proof.
+ case leb_spec0; constructor; trivial.
+ now rewrite <- compare_lt_iff, compare_nge_iff.
+Qed.
+
+Lemma ltb_spec0 x y : reflect (x<y) (x<?y).
+Proof.
+ apply iff_reflect. symmetry. apply ltb_lt.
+Qed.
+
+Lemma ltb_spec x y : BoolSpec (x<y) (y<=x) (x<?y).
+Proof.
+ case ltb_spec0; constructor; trivial.
+ now rewrite <- compare_le_iff, compare_ngt_iff.
+Qed.
+
+(** Negated variants of the specifications *)
+
+Lemma leb_nle x y : x <=? y = false <-> ~ (x <= y).
+Proof.
+now rewrite <- not_true_iff_false, leb_le.
+Qed.
+
+Lemma leb_gt x y : x <=? y = false <-> y < x.
+Proof.
+now rewrite leb_nle, <- compare_lt_iff, compare_nge_iff.
+Qed.
+
+Lemma ltb_nlt x y : x <? y = false <-> ~ (x < y).
+Proof.
+now rewrite <- not_true_iff_false, ltb_lt.
+Qed.
+
+Lemma ltb_ge x y : x <? y = false <-> y <= x.
+Proof.
+now rewrite ltb_nlt, <- compare_le_iff, compare_ngt_iff.
+Qed.
+
+(** Basic equality laws for boolean tests *)
+
+Lemma leb_refl x : x <=? x = true.
+Proof.
+apply leb_le. apply lt_eq_cases. now right.
+Qed.
+
+Lemma leb_antisym x y : y <=? x = negb (x <? y).
+Proof.
+apply eq_true_iff_eq. now rewrite negb_true_iff, leb_le, ltb_ge.
+Qed.
+
+Lemma ltb_irrefl x : x <? x = false.
+Proof.
+apply ltb_ge. apply lt_eq_cases. now right.
+Qed.
+
+Lemma ltb_antisym x y : y <? x = negb (x <=? y).
+Proof.
+apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt.
+Qed.
+
+(** Relation bewteen [compare] and the boolean comparisons *)
+
+Lemma eqb_compare x y :
+ (x =? y) = match compare x y with Eq => true | _ => false end.
+Proof.
+apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff.
+destruct compare; now split.
+Qed.
+
+Lemma ltb_compare x y :
+ (x <? y) = match compare x y with Lt => true | _ => false end.
+Proof.
+apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff.
+destruct compare; now split.
+Qed.
+
+Lemma leb_compare x y :
+ (x <=? y) = match compare x y with Gt => false | _ => true end.
+Proof.
+apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff.
+destruct compare; split; try easy. now destruct 1.
+Qed.
+
+End BoolOrderFacts.
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.