diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-20 17:18:39 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-20 17:18:39 +0000 |
| commit | ca96d3477993d102d6cc42166eab52516630d181 (patch) | |
| tree | 073b17efe149637da819caf527b23cf09f15865d /theories | |
| parent | ca1848177a50e51bde0736e51f506e06efc81b1d (diff) | |
Arithemtic: more concerning compare, eqb, leb, ltb
Start of a uniform treatment of compare, eqb, leb, ltb:
- We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
- Some generic properties are derived in OrdersFacts.BoolOrderFacts
In BinPos, more work about sub_mask with nice implications
on compare (e.g. simplier proof of lt_trans).
In BinNat/BinPos, for uniformity, compare_antisym is now
(y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.
In BigN / BigZ, eq_bool is now eqb
In BinIntDef, gtb and geb are kept for the moment, but
a comment advise to rather use ltb and leb. Z.div now uses
Z.ltb and Z.leb.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
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. |