diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:16 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:16 +0000 |
| commit | fc2613e871dffffa788d90044a81598f671d0a3b (patch) | |
| tree | f6f308b3d6b02e1235446b2eb4a2d04b135a0462 /theories/ZArith | |
| parent | f93f073df630bb46ddd07802026c0326dc72dafd (diff) | |
ZArith + other : favor the use of modern names instead of compat notations
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
28 files changed, 1236 insertions, 1273 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 0f709d686..a5c8affe7 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -82,8 +82,8 @@ Lemma pos_sub_spec p q : pos_sub p q = match (p ?= q)%positive with | Eq => 0 - | Lt => Zneg (q - p) - | Gt => Zpos (p - q) + | Lt => neg (q - p) + | Gt => pos (p - q) end. Proof. revert q. induction p; destruct q; simpl; trivial; @@ -95,6 +95,18 @@ Proof. subst; unfold Pos.sub; simpl; now rewrite Pos.sub_mask_diag. Qed. +Lemma pos_sub_discr p q : + match pos_sub p q with + | Z0 => p = q + | pos k => p = q + k + | neg k => q = p + k + end%positive. +Proof. + rewrite pos_sub_spec. + case Pos.compare_spec; auto; intros; + now rewrite Pos.add_comm, Pos.sub_add. +Qed. + (** Particular cases of the previous result *) Lemma pos_sub_diag p : pos_sub p p = 0. @@ -102,12 +114,12 @@ Proof. now rewrite pos_sub_spec, Pos.compare_refl. Qed. -Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = Zneg (q - p). +Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = neg (q - p). Proof. intros H. now rewrite pos_sub_spec, H. Qed. -Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = Zpos (p - q). +Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = pos (p - q). Proof. intros H. now rewrite pos_sub_spec, Pos.compare_antisym, H. Qed. @@ -120,89 +132,6 @@ Proof. rewrite <- IHp; now destruct pos_sub. Qed. -(** * Results concerning [Zpos] and [Zneg] and the operators *) - -Lemma opp_Zneg p : - Zneg p = Zpos p. -Proof. - reflexivity. -Qed. - -Lemma opp_Zpos p : - Zpos p = Zneg p. -Proof. - reflexivity. -Qed. - -Lemma succ_Zpos p : succ (Zpos p) = Zpos (Pos.succ p). -Proof. - simpl. f_equal. apply Pos.add_1_r. -Qed. - -Lemma add_Zpos p q : Zpos p + Zpos q = Zpos (p+q). -Proof. - reflexivity. -Qed. - -Lemma add_Zneg p q : Zneg p + Zneg q = Zneg (p+q). -Proof. - reflexivity. -Qed. - -Lemma add_Zpos_Zneg p q : Zpos p + Zneg q = pos_sub p q. -Proof. - reflexivity. -Qed. - -Lemma add_Zneg_Zpos p q : Zneg p + Zpos q = pos_sub q p. -Proof. - reflexivity. -Qed. - -Lemma sub_Zpos n m : (n < m)%positive -> Zpos m - Zpos n = Zpos (m-n). -Proof. - intros H. simpl. now apply pos_sub_gt. -Qed. - -Lemma mul_Zpos (p q : positive) : Zpos p * Zpos q = Zpos (p*q). -Proof. - reflexivity. -Qed. - -Lemma pow_Zpos p q : (Zpos p)^(Zpos q) = Zpos (p^q). -Proof. - unfold Pos.pow, pow, pow_pos. - symmetry. now apply Pos.iter_swap_gen. -Qed. - -Lemma inj_Zpos p q : Zpos p = Zpos q <-> p = q. -Proof. - split; intros H. now injection H. now f_equal. -Qed. - -Lemma inj_Zneg p q : Zneg p = Zneg q <-> p = q. -Proof. - split; intros H. now injection H. now f_equal. -Qed. - -Lemma pos_xI p : Zpos p~1 = 2 * Zpos p + 1. -Proof. - reflexivity. -Qed. - -Lemma pos_xO p : Zpos p~0 = 2 * Zpos p. -Proof. - reflexivity. -Qed. - -Lemma neg_xI p : Zneg p~1 = 2 * Zneg p - 1. -Proof. - reflexivity. -Qed. - -Lemma neg_xO p : Zneg p~0 = 2 * Zneg p. -Proof. - reflexivity. -Qed. - (** In the following module, we group results that are needed now to prove specifications of operations, but will also be provided later by the generic functor of properties. *) @@ -242,7 +171,7 @@ Qed. (** ** Addition is associative *) Lemma pos_sub_add p q r : - pos_sub (p + q) r = Zpos p + pos_sub q r. + pos_sub (p + q) r = pos p + pos_sub q r. Proof. simpl. rewrite !pos_sub_spec. case (Pos.compare_spec q r); intros E0. @@ -269,19 +198,19 @@ Qed. Lemma add_assoc n m p : n + (m + p) = n + m + p. Proof. - assert (AUX : forall x y z, Zpos x + (y + z) = Zpos x + y + z). + assert (AUX : forall x y z, pos x + (y + z) = pos x + y + z). { intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial. - simpl. now rewrite Pos.add_assoc. - - simpl (_ + Zneg _). symmetry. apply pos_sub_add. - - simpl (Zneg _ + _); simpl (_ + Zneg _). - now rewrite (add_comm _ (Zpos _)), <- 2 pos_sub_add, Pos.add_comm. - - apply opp_inj. rewrite !opp_add_distr, opp_Zpos, !opp_Zneg. - simpl (Zneg _ + _); simpl (_ + Zneg _). + - simpl (_ + neg _). symmetry. apply pos_sub_add. + - simpl (neg _ + _); simpl (_ + neg _). + now rewrite (add_comm _ (pos _)), <- 2 pos_sub_add, Pos.add_comm. + - apply opp_inj. rewrite !opp_add_distr. simpl opp. + simpl (neg _ + _); simpl (_ + neg _). rewrite add_comm, Pos.add_comm. apply pos_sub_add. } destruct n. - trivial. - apply AUX. - - apply opp_inj. rewrite !opp_add_distr, opp_Zneg. apply AUX. + - apply opp_inj. rewrite !opp_add_distr. simpl opp. apply AUX. Qed. (** ** Subtraction and successor *) @@ -354,7 +283,7 @@ Qed. (** ** Distributivity of multiplication over addition *) Lemma mul_add_distr_pos (p:positive) n m : - Zpos p * (n + m) = Zpos p * n + Zpos p * m. + pos p * (n + m) = pos p * n + pos p * m. Proof. destruct n as [|n|n], m as [|m|m]; simpl; trivial; rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec; @@ -365,7 +294,8 @@ Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p. Proof. destruct n as [|n|n]. trivial. apply mul_add_distr_pos. - rewrite <- opp_Zpos, !mul_opp_l, <- opp_add_distr. f_equal. + change (neg n) with (- pos n). + rewrite !mul_opp_l, <- opp_add_distr. f_equal. apply mul_add_distr_pos. Qed. @@ -374,6 +304,57 @@ Proof. rewrite !(mul_comm _ p). apply mul_add_distr_l. Qed. +(** ** Basic properties of divisibility *) + +Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive. +Proof. + split. + intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. + intros (r,H). exists (pos r); simpl; now f_equal. +Qed. + +Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. +Qed. + +Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. +Qed. + +(** ** Conversions between [Z.testbit] and [N.testbit] *) + +Lemma testbit_of_N a n : + testbit (of_N a) (of_N n) = N.testbit a n. +Proof. + destruct a as [|a], n; simpl; trivial. now destruct a. +Qed. + +Lemma testbit_of_N' a n : 0<=n -> + testbit (of_N a) n = N.testbit a (to_N n). +Proof. + intro Hn. rewrite <- testbit_of_N. f_equal. + destruct n; trivial; now destruct Hn. +Qed. + +Lemma testbit_Zpos a n : 0<=n -> + testbit (pos a) n = N.testbit (N.pos a) (to_N n). +Proof. + intro Hn. now rewrite <- testbit_of_N'. +Qed. + +Lemma testbit_Zneg a n : 0<=n -> + testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). +Proof. + intro Hn. + rewrite <- testbit_of_N' by trivial. + destruct n as [ |n|n]; + [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn]. + unfold testbit. + now destruct a as [|[ | | ]| ]. +Qed. + End Private_BootStrap. (** * Proofs of specifications *) @@ -454,9 +435,8 @@ Qed. Lemma eqb_eq n m : (n =? m) = true <-> n = m. Proof. - destruct n, m; simpl; try (now split). - rewrite inj_Zpos. apply Pos.eqb_eq. - rewrite inj_Zneg. apply Pos.eqb_eq. + destruct n, m; simpl; try (now split); rewrite Pos.eqb_eq; + split; (now injection 1) || (intros; now f_equal). Qed. Lemma ltb_lt n m : (n <? m) = true <-> n < m. @@ -580,7 +560,7 @@ Qed. (** For folding back a [pow_pos] into a [pow] *) -Lemma pow_pos_fold n p : pow_pos n p = n ^ (Zpos p). +Lemma pow_pos_fold n p : pow_pos n p = n ^ (pos p). Proof. reflexivity. Qed. @@ -607,7 +587,7 @@ Lemma sqrt_spec n : 0<=n -> let s := sqrt n in s*s <= n < (succ s)*(succ s). Proof. destruct n. now repeat split. unfold sqrt. - rewrite succ_Zpos. intros _. apply (Pos.sqrt_spec p). + intros _. simpl succ. rewrite Pos.add_1_r. apply (Pos.sqrt_spec p). now destruct 1. Qed. @@ -627,8 +607,10 @@ Qed. Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)). Proof. + assert (Pow : forall p q, pos (p^q) = (pos p)^(pos q)). + { intros. now apply Pos.iter_swap_gen. } destruct n as [|[p|p|]|]; intros Hn; split; try easy; unfold log2; - rewrite ?succ_Zpos, pow_Zpos. + simpl succ; rewrite ?Pos.add_1_r, <- Pow. change (2^Pos.size p <= Pos.succ (p~0))%positive. apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le. apply Pos.size_gt. @@ -678,20 +660,22 @@ Qed. (** ** Correctness proofs for Trunc division *) Lemma pos_div_eucl_eq a b : 0 < b -> - let (q, r) := pos_div_eucl a b in Zpos a = q * b + r. + let (q, r) := pos_div_eucl a b in pos a = q * b + r. Proof. intros Hb. induction a; unfold pos_div_eucl; fold pos_div_eucl. - (* ~1 *) destruct pos_div_eucl as (q,r). - rewrite pos_xI, IHa, mul_add_distr_l, mul_assoc. + change (pos a~1) with (2*(pos a)+1). + rewrite IHa, mul_add_distr_l, mul_assoc. 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. + change (pos a~0) with (2*pos a). + rewrite IHa, mul_add_distr_l, mul_assoc. destruct ltb. trivial. rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal. @@ -709,21 +693,23 @@ Lemma div_eucl_eq a b : b<>0 -> Proof. destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial; (now destruct 1) || intros _; - generalize (pos_div_eucl_eq a (Zpos b) (eq_refl _)); - destruct pos_div_eucl as (q,r); rewrite <- ?opp_Zpos, mul_comm; - intros ->. - - (* Zpos Zpos *) + generalize (pos_div_eucl_eq a (pos b) (eq_refl _)); + destruct pos_div_eucl as (q,r); rewrite mul_comm. + - (* pos pos *) trivial. - - (* Zpos Zneg *) - destruct r as [ |r|r]; rewrite !mul_opp_opp; trivial; + - (* pos neg *) + intros ->. + destruct r as [ |r|r]; rewrite <- !mul_opp_comm; trivial; rewrite mul_add_distr_l, mul_1_r, <- add_assoc; f_equal; now rewrite add_assoc, add_opp_diag_r. - - (* Zneg Zpos *) + - (* neg pos *) + change (neg a) with (- pos a). intros ->. rewrite (opp_add_distr _ r), <- mul_opp_r. destruct r as [ |r|r]; trivial; rewrite opp_add_distr, mul_add_distr_l, <- add_assoc; f_equal; unfold sub; now rewrite add_assoc, mul_opp_r, mul_1_r, add_opp_diag_l. - - (* Zneg Zneg *) + - (* neg neg *) + change (neg a) with (- pos a). intros ->. now rewrite opp_add_distr, <- mul_opp_l. Qed. @@ -735,10 +721,10 @@ Qed. Lemma pos_div_eucl_bound a b : 0<b -> 0 <= snd (pos_div_eucl a b) < b. Proof. - assert (AUX : forall m p, m < Zpos (p~0) -> m - Zpos p < Zpos p). + assert (AUX : forall m p, m < pos (p~0) -> m - pos p < pos p). intros m p. unfold lt. - rewrite (compare_sub m), (compare_sub _ (Zpos _)). unfold sub. - rewrite <- add_assoc. simpl opp; simpl (Zneg _ + _). + rewrite (compare_sub m), (compare_sub _ (pos _)). unfold sub. + rewrite <- add_assoc. simpl opp; simpl (neg _ + _). now rewrite Pos.add_diag. intros Hb. destruct b as [|b|b]; discriminate Hb || clear Hb. @@ -770,7 +756,7 @@ Proof. destruct a as [|a|a]; unfold modulo, div_eucl. now split. now apply pos_div_eucl_bound. - generalize (pos_div_eucl_bound a (Zpos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). destruct r as [|r|r]; (now destruct Hr) || clear Hr. now split. @@ -787,17 +773,17 @@ Proof. destruct b as [|b|b]; try easy; intros _. destruct a as [|a|a]; unfold modulo, div_eucl. now split. - generalize (pos_div_eucl_bound a (Zpos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). destruct r as [|r|r]; (now destruct Hr) || clear Hr. now split. split. unfold lt in *; simpl in *. rewrite pos_sub_lt by trivial. rewrite <- Pos.compare_antisym. now apply Pos.sub_decr. - change (Zneg b - Zneg r <= 0). unfold le, lt in *. + change (neg b - neg r <= 0). unfold le, lt in *. rewrite <- compare_sub. simpl in *. now rewrite <- Pos.compare_antisym, Hr'. - generalize (pos_div_eucl_bound a (Zpos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). split; destruct r; try easy. red; simpl; now rewrite <- Pos.compare_antisym. @@ -808,9 +794,10 @@ Qed. Theorem quotrem_eq a b : let (q,r) := quotrem a b in a = q * b + r. Proof. destruct a as [|a|a], b as [|b|b]; simpl; trivial; - generalize (N.pos_div_eucl_spec a (Npos b)); case N.pos_div_eucl; trivial; - intros q r; rewrite <- ?opp_Zpos; - change (Zpos a) with (of_N (Npos a)); intros ->; now destruct q, r. + generalize (N.pos_div_eucl_spec a (N.pos b)); case N.pos_div_eucl; trivial; + intros q r; + try change (neg a) with (-pos a); + change (pos a) with (of_N (N.pos a)); intros ->; now destruct q, r. Qed. Lemma quot_rem' a b : a = b*(a÷b) + rem a b. @@ -829,7 +816,7 @@ Proof. destruct a as [|a|a]; (now destruct Ha) || clear Ha. compute. now split. unfold rem, quotrem. - assert (H := N.pos_div_eucl_remainder a (Npos b)). + assert (H := N.pos_div_eucl_remainder a (N.pos b)). destruct N.pos_div_eucl as (q,[|r]); simpl; split; try easy. now apply H. Qed. @@ -852,25 +839,6 @@ Proof. intros _. apply rem_opp_l'. Qed. Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b. Proof. intros _. apply rem_opp_r'. Qed. -(** ** Basic properties of divisibility *) - -Lemma divide_Zpos p q : (Zpos p|Zpos q) <-> (p|q)%positive. -Proof. - split. - intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. - intros (r,H). exists (Zpos r); simpl; now f_equal. -Qed. - -Lemma divide_Zpos_Zneg_r n p : (n|Zpos p) <-> (n|Zneg p). -Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. -Qed. - -Lemma divide_Zpos_Zneg_l n p : (Zpos p|n) <-> (Zneg p|n). -Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. -Qed. - (** ** Correctness proofs for gcd *) Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b. @@ -905,7 +873,7 @@ Qed. Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b). Proof. - assert (H : forall p q r, (r|Zpos p) -> (r|Zpos q) -> (r|Zpos (Pos.gcd p q))). + assert (H : forall p q r, (r|pos p) -> (r|pos q) -> (r|pos (Pos.gcd p q))). { intros p q [|r|r] H H'. destruct H; now rewrite mul_comm in *. apply divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos. @@ -930,38 +898,6 @@ Proof. destruct (Pos.ggcd a b) as (g,(aa,bb)); auto. Qed. -(** ** Conversions between [Z.testbit] and [N.testbit] *) - -Lemma testbit_of_N a n : - testbit (of_N a) (of_N n) = N.testbit a n. -Proof. - destruct a as [|a], n; simpl; trivial. now destruct a. -Qed. - -Lemma testbit_of_N' a n : 0<=n -> - testbit (of_N a) n = N.testbit a (to_N n). -Proof. - intro Hn. rewrite <- testbit_of_N. f_equal. - destruct n; trivial; now destruct Hn. -Qed. - -Lemma testbit_Zpos a n : 0<=n -> - testbit (Zpos a) n = N.testbit (Npos a) (to_N n). -Proof. - intro Hn. now rewrite <- testbit_of_N'. -Qed. - -Lemma testbit_Zneg a n : 0<=n -> - testbit (Zneg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). -Proof. - intro Hn. - rewrite <- testbit_of_N' by trivial. - destruct n as [ |n|n]; - [ | simpl; now destruct (Ppred_N a) | now destruct Hn]. - unfold testbit. - now destruct a as [|[ | | ]| ]. -Qed. - (** ** Proofs of specifications for bitwise operations *) Lemma div2_spec a : div2 a = shiftr a 1. @@ -994,9 +930,9 @@ Lemma testbit_odd_succ a n : 0<=n -> Proof. destruct n as [|n|n]; (now destruct 1) || intros _. destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. - unfold testbit. rewrite succ_Zpos. + unfold testbit; simpl. destruct a as [|a|[a|a|]]; simpl; trivial; - rewrite ?Pos.pred_N_succ; now destruct n. + rewrite ?Pos.add_1_r, ?Pos.pred_N_succ; now destruct n. Qed. Lemma testbit_even_succ a n : 0<=n -> @@ -1004,9 +940,9 @@ Lemma testbit_even_succ a n : 0<=n -> Proof. destruct n as [|n|n]; (now destruct 1) || intros _. destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. - unfold testbit. rewrite succ_Zpos. + unfold testbit; simpl. destruct a as [|a|[a|a|]]; simpl; trivial; - rewrite ?Pos.pred_N_succ; now destruct n. + rewrite ?Pos.add_1_r, ?Pos.pred_N_succ; now destruct n. Qed. (** Correctness proofs about [Z.shiftr] and [Z.shiftl] *) @@ -1017,9 +953,9 @@ Proof. intros Hn Hm. unfold shiftr. destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl. now rewrite add_0_r. - assert (forall p, to_N (m + Zpos p) = (to_N m + Npos p)%N). + assert (forall p, to_N (m + pos p) = (to_N m + N.pos p)%N). destruct m; trivial; now destruct Hm. - assert (forall p, 0 <= m + Zpos p). + assert (forall p, 0 <= m + pos p). destruct m; easy || now destruct Hm. destruct a as [ |a|a]. (* a = 0 *) @@ -1027,15 +963,15 @@ Proof. by (apply Pos.iter_invariant; intros; subst; trivial). now rewrite 2 testbit_0_l. (* a > 0 *) - change (Zpos a) with (of_N (Npos a)) at 1. - rewrite <- (Pos.iter_swap_gen _ _ _ Ndiv2) by now intros [|[ | | ]]. + change (pos a) with (of_N (N.pos a)) at 1. + rewrite <- (Pos.iter_swap_gen _ _ _ N.div2) by now intros [|[ | | ]]. rewrite testbit_Zpos, testbit_of_N', H; trivial. - exact (N.shiftr_spec' (Npos a) (Npos n) (to_N m)). + exact (N.shiftr_spec' (N.pos a) (N.pos n) (to_N m)). (* a < 0 *) - rewrite <- (Pos.iter_swap_gen _ _ _ Pdiv2_up) by trivial. + rewrite <- (Pos.iter_swap_gen _ _ _ Pos.div2_up) by trivial. rewrite 2 testbit_Zneg, H; trivial. f_equal. - rewrite (Pos.iter_swap_gen _ _ _ _ Ndiv2) by exact N.pred_div2_up. - exact (N.shiftr_spec' (Ppred_N a) (Npos n) (to_N m)). + rewrite (Pos.iter_swap_gen _ _ _ _ N.div2) by exact N.pred_div2_up. + exact (N.shiftr_spec' (Pos.pred_N a) (N.pos n) (to_N m)). Qed. Lemma shiftl_spec_low a n m : m<n -> @@ -1052,11 +988,11 @@ Proof. (* a > 0 *) rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite testbit_Zpos by easy. - exact (N.shiftl_spec_low (Npos a) (Npos n) (Npos m) H). + exact (N.shiftl_spec_low (N.pos a) (N.pos n) (N.pos m) H). (* a < 0 *) rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite testbit_Zneg by easy. - now rewrite (N.pos_pred_shiftl_low a (Npos n)). + now rewrite (N.pos_pred_shiftl_low a (N.pos n)). Qed. Lemma shiftl_spec_high a n m : 0<=m -> n<=m -> @@ -1066,9 +1002,9 @@ Proof. destruct n as [ |n|n]. simpl. now rewrite sub_0_r. (* n > 0 *) destruct m as [ |m|m]; try (now destruct H). - assert (0 <= Zpos m - Zpos n). + assert (0 <= pos m - pos n). red. now rewrite compare_antisym, <- compare_sub, <- compare_antisym. - assert (EQ : to_N (Zpos m - Zpos n) = (Npos m - Npos n)%N). + assert (EQ : to_N (pos m - pos n) = (N.pos m - N.pos n)%N). red in H. simpl in H. simpl to_N. rewrite pos_sub_spec, Pos.compare_antisym. destruct (Pos.compare_spec n m) as [H'|H'|H']; try (now destruct H). @@ -1083,16 +1019,16 @@ Proof. (* ... a > 0 *) rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite 2 testbit_Zpos, EQ by easy. - exact (N.shiftl_spec_high' (Npos p) (Npos n) (Npos m) H). + exact (N.shiftl_spec_high' (N.pos p) (N.pos n) (N.pos m) H). (* ... a < 0 *) rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite 2 testbit_Zneg, EQ by easy. f_equal. simpl to_N. rewrite <- N.shiftl_spec_high by easy. - now apply (N.pos_pred_shiftl_high p (Npos n)). + now apply (N.pos_pred_shiftl_high p (N.pos n)). (* n < 0 *) unfold sub. simpl. - now apply (shiftr_spec_aux a (Zpos n) m). + now apply (shiftr_spec_aux a (pos n) m). Qed. Lemma shiftr_spec a n m : 0<=m -> @@ -1180,11 +1116,11 @@ Proof. induction p using Pos.peano_ind. now apply (Hs 0). rewrite <- Pos.add_1_r. - now apply (Hs (Zpos p)). + now apply (Hs (pos p)). induction p using Pos.peano_ind. now apply (Hp 0). rewrite <- Pos.add_1_r. - now apply (Hp (Zneg p)). + now apply (Hp (neg p)). Qed. Lemma bi_induction (P : Z -> Prop) : @@ -1341,7 +1277,7 @@ Qed. End Z. -(** Export Notations *) +(** Re-export Notations *) Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. @@ -1351,27 +1287,271 @@ Infix "^" := Z.pow : Z_scope. Infix "/" := Z.div : Z_scope. Infix "mod" := Z.modulo (at level 40, no associativity) : Z_scope. Infix "÷" := Z.quot (at level 40, left associativity) : Z_scope. - -(* TODO : transition from Zdivide *) -Notation "( x | y )" := (Z.divide x y) (at level 0) : Z_scope. - Infix "?=" := Z.compare (at level 70, no associativity) : Z_scope. - +Infix "=?" := Z.eqb (at level 70, no associativity) : Z_scope. +Infix "<=?" := Z.leb (at level 70, no associativity) : Z_scope. +Infix "<?" := Z.ltb (at level 70, no associativity) : Z_scope. +Infix ">=?" := Z.geb (at level 70, no associativity) : Z_scope. +Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope. +Notation "( x | y )" := (Z.divide x y) (at level 0) : Z_scope. Infix "<=" := Z.le : Z_scope. Infix "<" := Z.lt : Z_scope. Infix ">=" := Z.ge : Z_scope. Infix ">" := Z.gt : Z_scope. - Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope. Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope. Notation "x < y < z" := (x < y /\ y < z) : Z_scope. Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope. -Infix "=?" := Z.eqb (at level 70, no associativity) : Z_scope. -Infix "<=?" := Z.leb (at level 70, no associativity) : Z_scope. -Infix "<?" := Z.ltb (at level 70, no associativity) : Z_scope. -Infix ">=?" := Z.geb (at level 70, no associativity) : Z_scope. -Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope. +(** Conversions from / to positive numbers *) + +Module Pos2Z. + +Lemma id p : Z.to_pos (Z.pos p) = p. +Proof. reflexivity. Qed. + +Lemma inj p q : Z.pos p = Z.pos q -> p = q. +Proof. now injection 1. Qed. + +Lemma inj_iff p q : Z.pos p = Z.pos q <-> p = q. +Proof. split. apply inj. intros; now f_equal. Qed. + +Lemma is_pos p : 0 < Z.pos p. +Proof. reflexivity. Qed. + +Lemma is_nonneg p : 0 <= Z.pos p. +Proof. easy. Qed. + +Lemma inj_1 : Z.pos 1 = 1. +Proof. reflexivity. Qed. + +Lemma inj_xO p : Z.pos p~0 = 2 * Z.pos p. +Proof. reflexivity. Qed. + +Lemma inj_xI p : Z.pos p~1 = 2 * Z.pos p + 1. +Proof. reflexivity. Qed. + +Lemma inj_succ p : Z.pos (Pos.succ p) = Z.succ (Z.pos p). +Proof. simpl. now rewrite Pos.add_1_r. Qed. + +Lemma inj_add p q : Z.pos (p+q) = Z.pos p + Z.pos q. +Proof. reflexivity. Qed. + +Lemma inj_sub p q : (p < q)%positive -> + Z.pos (q-p) = Z.pos q - Z.pos p. +Proof. intros. simpl. now rewrite Z.pos_sub_gt. Qed. + +Lemma inj_sub_max p q : Z.pos (p - q) = Z.max 1 (Z.pos p - Z.pos q). +Proof. + simpl. rewrite Z.pos_sub_spec. case Pos.compare_spec; intros. + - subst; now rewrite Pos.sub_diag. + - now rewrite Pos.sub_lt. + - now destruct (p-q)%positive. +Qed. + +Lemma inj_pred p : p <> 1%positive -> + Z.pos (Pos.pred p) = Z.pred (Z.pos p). +Proof. destruct p; easy || now destruct 1. Qed. + +Lemma inj_mul p q : Z.pos (p*q) = Z.pos p * Z.pos q. +Proof. reflexivity. Qed. + +Lemma inj_pow_pos p q : Z.pos (p^q) = Z.pow_pos (Z.pos p) q. +Proof. now apply Pos.iter_swap_gen. Qed. + +Lemma inj_pow p q : Z.pos (p^q) = (Z.pos p)^(Z.pos q). +Proof. apply inj_pow_pos. Qed. + +Lemma inj_square p : Z.pos (Pos.square p) = Z.square (Z.pos p). +Proof. reflexivity. Qed. + +Lemma inj_compare p q : (p ?= q)%positive = (Z.pos p ?= Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_leb p q : (p <=? q)%positive = (Z.pos p <=? Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_ltb p q : (p <? q)%positive = (Z.pos p <? Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_eqb p q : (p =? q)%positive = (Z.pos p =? Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_max p q : Z.pos (Pos.max p q) = Z.max (Z.pos p) (Z.pos q). +Proof. + unfold Z.max, Pos.max. rewrite inj_compare. now case Z.compare_spec. +Qed. + +Lemma inj_min p q : Z.pos (Pos.min p q) = Z.min (Z.pos p) (Z.pos q). +Proof. + unfold Z.min, Pos.min. rewrite inj_compare. now case Z.compare_spec. +Qed. + +Lemma inj_sqrt p : Z.pos (Pos.sqrt p) = Z.sqrt (Z.pos p). +Proof. reflexivity. Qed. + +Lemma inj_gcd p q : Z.pos (Pos.gcd p q) = Z.gcd (Z.pos p) (Z.pos q). +Proof. reflexivity. Qed. + +Definition inj_divide p q : (Z.pos p|Z.pos q) <-> (p|q)%positive. +Proof. apply Z.Private_BootStrap.divide_Zpos. Qed. + +Lemma inj_testbit a n : 0<=n -> + Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). +Proof. apply Z.Private_BootStrap.testbit_Zpos. Qed. + +(** Some results concerning Z.neg *) + +Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q. +Proof. now injection 1. Qed. + +Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q. +Proof. split. apply inj_neg. intros; now f_equal. Qed. + +Lemma neg_is_neg p : Z.neg p < 0. +Proof. reflexivity. Qed. + +Lemma neg_is_nonpos p : Z.neg p <= 0. +Proof. easy. Qed. + +Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p. +Proof. reflexivity. Qed. + +Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1. +Proof. reflexivity. Qed. + +Lemma opp_neg p : - Z.neg p = Z.pos p. +Proof. reflexivity. Qed. + +Lemma opp_pos p : - Z.pos p = Z.neg p. +Proof. reflexivity. Qed. + +Lemma add_neg_neg p q : Z.neg p + Z.neg q = Z.neg (p+q). +Proof. reflexivity. Qed. + +Lemma add_pos_neg p q : Z.pos p + Z.neg q = Z.pos_sub p q. +Proof. reflexivity. Qed. + +Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p. +Proof. reflexivity. Qed. + +Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p). +Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_r. Qed. + +Lemma divide_pos_neg_l n p : (Z.pos p|n) <-> (Z.neg p|n). +Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_l. Qed. + +Lemma testbit_neg a n : 0<=n -> + Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)). +Proof. apply Z.Private_BootStrap.testbit_Zneg. Qed. + +End Pos2Z. + +Module Z2Pos. + +Lemma id x : 0 < x -> Z.pos (Z.to_pos x) = x. +Proof. now destruct x. Qed. + +Lemma inj x y : 0 < x -> 0 < y -> Z.to_pos x = Z.to_pos y -> x = y. +Proof. + destruct x; simpl; try easy. intros _ H ->. now apply id. +Qed. + +Lemma inj_iff x y : 0 < x -> 0 < y -> (Z.to_pos x = Z.to_pos y <-> x = y). +Proof. split. now apply inj. intros; now f_equal. Qed. + +Lemma to_pos_nonpos x : x <= 0 -> Z.to_pos x = 1%positive. +Proof. destruct x; trivial. now destruct 1. Qed. + +Lemma inj_1 : Z.to_pos 1 = 1%positive. +Proof. reflexivity. Qed. + +Lemma inj_double x : 0 < x -> + Z.to_pos (Z.double x) = (Z.to_pos x)~0%positive. +Proof. now destruct x. Qed. + +Lemma inj_succ_double x : 0 < x -> + Z.to_pos (Z.succ_double x) = (Z.to_pos x)~1%positive. +Proof. now destruct x. Qed. + +Lemma inj_succ x : 0 < x -> Z.to_pos (Z.succ x) = Pos.succ (Z.to_pos x). +Proof. + destruct x; try easy. simpl. now rewrite Pos.add_1_r. +Qed. + +Lemma inj_add x y : 0 < x -> 0 < y -> + Z.to_pos (x+y) = (Z.to_pos x + Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_sub x y : 0 < x < y -> + Z.to_pos (y-x) = (Z.to_pos y - Z.to_pos x)%positive. +Proof. + destruct x; try easy. destruct y; try easy. simpl. + intros. now rewrite Z.pos_sub_gt. +Qed. + +Lemma inj_pred x : 1 < x -> Z.to_pos (Z.pred x) = Pos.pred (Z.to_pos x). +Proof. now destruct x as [|[x|x|]|]. Qed. + +Lemma inj_mul x y : 0 < x -> 0 < y -> + Z.to_pos (x*y) = (Z.to_pos x * Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_pow x y : 0 < x -> 0 < y -> + Z.to_pos (x^y) = (Z.to_pos x ^ Z.to_pos y)%positive. +Proof. + intros. apply Pos2Z.inj. rewrite Pos2Z.inj_pow, !id; trivial. + apply Z.pow_pos_nonneg. trivial. now apply Z.lt_le_incl. +Qed. + +Lemma inj_pow_pos x p : 0 < x -> + Z.to_pos (Z.pow_pos x p) = ((Z.to_pos x)^p)%positive. +Proof. intros. now apply (inj_pow x (Z.pos p)). Qed. + +Lemma inj_compare x y : 0 < x -> 0 < y -> + (x ?= y) = (Z.to_pos x ?= Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_leb x y : 0 < x -> 0 < y -> + (x <=? y) = (Z.to_pos x <=? Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_ltb x y : 0 < x -> 0 < y -> + (x <? y) = (Z.to_pos x <? Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_eqb x y : 0 < x -> 0 < y -> + (x =? y) = (Z.to_pos x =? Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_max x y : + Z.to_pos (Z.max x y) = Pos.max (Z.to_pos x) (Z.to_pos y). +Proof. + destruct x; simpl; try rewrite Pos.max_1_l. + - now destruct y. + - destruct y; simpl; now rewrite ?Pos.max_1_r, <- ?Pos2Z.inj_max. + - destruct y; simpl; rewrite ?Pos.max_1_r; trivial. + apply to_pos_nonpos. now apply Z.max_lub. +Qed. + +Lemma inj_min x y : + Z.to_pos (Z.min x y) = Pos.min (Z.to_pos x) (Z.to_pos y). +Proof. + destruct x; simpl; try rewrite Pos.min_1_l. + - now destruct y. + - destruct y; simpl; now rewrite ?Pos.min_1_r, <- ?Pos2Z.inj_min. + - destruct y; simpl; rewrite ?Pos.min_1_r; trivial. + apply to_pos_nonpos. apply Z.min_le_iff. now left. +Qed. + +Lemma inj_sqrt x : Z.to_pos (Z.sqrt x) = Pos.sqrt (Z.to_pos x). +Proof. now destruct x. Qed. + +Lemma inj_gcd x y : 0 < x -> 0 < y -> + Z.to_pos (Z.gcd x y) = Pos.gcd (Z.to_pos x) (Z.to_pos y). +Proof. destruct x; easy || now destruct y. Qed. + +End Z2Pos. (** Compatibility Notations *) @@ -1404,7 +1584,6 @@ Notation Z_of_N := Z.of_N (compat "8.3"). Notation Zind := Z.peano_ind (compat "8.3"). Notation Zopp_0 := Z.opp_0 (compat "8.3"). -Notation Zopp_neg := Z.opp_Zneg (compat "8.3"). Notation Zopp_involutive := Z.opp_involutive (compat "8.3"). Notation Zopp_inj := Z.opp_inj (compat "8.3"). Notation Zplus_0_l := Z.add_0_l (compat "8.3"). @@ -1452,10 +1631,18 @@ Notation Zmult_reg_l := Z.mul_reg_l (compat "8.3"). Notation Zmult_reg_r := Z.mul_reg_r (compat "8.3"). Notation Zmult_succ_l := Z.mul_succ_l (compat "8.3"). Notation Zmult_succ_r := Z.mul_succ_r (compat "8.3"). -Notation Zpos_xI := Z.pos_xI (compat "8.3"). -Notation Zpos_xO := Z.pos_xO (compat "8.3"). -Notation Zneg_xI := Z.neg_xI (compat "8.3"). -Notation Zneg_xO := Z.neg_xO (compat "8.3"). + +Notation Zpos_xI := Pos2Z.inj_xI (compat "8.3"). +Notation Zpos_xO := Pos2Z.inj_xO (compat "8.3"). +Notation Zneg_xI := Pos2Z.neg_xI (compat "8.3"). +Notation Zneg_xO := Pos2Z.neg_xO (compat "8.3"). +Notation Zopp_neg := Pos2Z.opp_neg (compat "8.3"). +Notation Zpos_succ_morphism := Pos2Z.inj_succ (compat "8.3"). +Notation Zpos_mult_morphism := Pos2Z.inj_mul (compat "8.3"). +Notation Zpos_minus_morphism := Pos2Z.inj_sub (compat "8.3"). +Notation Zpos_eq_rev := Pos2Z.inj (compat "8.3"). +Notation Zpos_plus_distr := Pos2Z.inj_add (compat "8.3"). +Notation Zneg_plus_distr := Pos2Z.add_neg_neg (compat "8.3"). Notation Z := Z (only parsing). Notation Z_rect := Z_rect (only parsing). @@ -1482,8 +1669,6 @@ Lemma Zplus_0_r_reverse : forall n, n = n + 0. Proof (SYM1 Z.add_0_r). Lemma Zplus_eq_compat : forall n m p q, n=m -> p=q -> n+p=m+q. Proof (f_equal2 Z.add). -Lemma Zpos_succ_morphism : forall p, Zpos (Psucc p) = Zsucc (Zpos p). -Proof (SYM1 Z.succ_Zpos). Lemma Zsucc_pred : forall n, n = Z.succ (Z.pred n). Proof (SYM1 Z.succ_pred). Lemma Zpred_succ : forall n, n = Z.pred (Z.succ n). @@ -1506,15 +1691,10 @@ Lemma Zminus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). Proof (SYM3 Zminus_plus_simpl_l). Lemma Zminus_plus_simpl_r : forall n m p, n + p - (m + p) = n - m. Proof (fun n m p => Z.add_add_simpl_r_r n p m). -Lemma Zpos_minus_morphism : forall a b, - Pcompare a b Eq = Lt -> Zpos (b - a) = Zpos b - Zpos a. -Proof. intros. now rewrite Z.sub_Zpos. Qed. Lemma Zeq_minus : forall n m, n = m -> n - m = 0. Proof (fun n m => proj2 (Z.sub_move_0_r n m)). Lemma Zminus_eq : forall n m, n - m = 0 -> n = m. Proof (fun n m => proj1 (Z.sub_move_0_r n m)). -Lemma Zpos_mult_morphism : forall p q, Zpos (p * q) = Zpos p * Zpos q. -Proof (SYM2 Z.mul_Zpos). Lemma Zmult_0_r_reverse : forall n, 0 = n * 0. Proof (SYM1 Z.mul_0_r). Lemma Zmult_assoc_reverse : forall n m p, n * m * p = n * (m * p). @@ -1529,20 +1709,14 @@ Lemma Zopp_mult_distr_r : forall n m, - (n * m) = n * - m. Proof (SYM2 Z.mul_opp_r). Lemma Zmult_minus_distr_l : forall n m p, p * (n - m) = p * n - p * m. Proof (fun n m p => Z.mul_sub_distr_l p n m). -Lemma Zmult_succ_r_reverse : forall n m, n * m + n = n * Zsucc m. +Lemma Zmult_succ_r_reverse : forall n m, n * m + n = n * Z.succ m. Proof (SYM2 Z.mul_succ_r). -Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Zsucc n * m. +Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Z.succ n * m. Proof (SYM2 Z.mul_succ_l). -Lemma Zpos_eq : forall p q, p = q -> Zpos p = Zpos q. -Proof (fun p q => proj2 (Z.inj_Zpos p q)). -Lemma Zpos_eq_rev : forall p q, Zpos p = Zpos q -> p = q. -Proof (fun p q => proj1 (Z.inj_Zpos p q)). -Lemma Zpos_eq_iff : forall p q, p = q <-> Zpos p = Zpos q. -Proof (fun p q => iff_sym (Z.inj_Zpos p q)). -Lemma Zpos_plus_distr : forall p q, Zpos (p + q) = Zpos p + Zpos q. -Proof (SYM2 Z.add_Zpos). -Lemma Zneg_plus_distr : forall p q, Zneg (p + q) = Zneg p + Zneg q. -Proof (SYM2 Z.add_Zneg). +Lemma Zpos_eq : forall p q, p = q -> Z.pos p = Z.pos q. +Proof. congruence. Qed. +Lemma Zpos_eq_iff : forall p q, p = q <-> Z.pos p = Z.pos q. +Proof (fun p q => iff_sym (Pos2Z.inj_iff p q)). Hint Immediate Zsucc_pred: zarith. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index c03b8517b..6e75e53b9 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -22,6 +22,11 @@ Module Z. Definition t := Z. +(** ** Nicer names [Z.pos] and [Z.neg] for contructors *) + +Notation pos := Zpos. +Notation neg := Zneg. + (** ** Constants *) Definition zero := 0. @@ -33,22 +38,22 @@ Definition two := 2. Definition double x := match x with | 0 => 0 - | Zpos p => Zpos p~0 - | Zneg p => Zneg p~0 + | pos p => pos p~0 + | neg p => neg p~0 end. Definition succ_double x := match x with | 0 => 1 - | Zpos p => Zpos p~1 - | Zneg p => Zneg (Pos.pred_double p) + | pos p => pos p~1 + | neg p => neg (Pos.pred_double p) end. Definition pred_double x := match x with | 0 => -1 - | Zneg p => Zneg p~1 - | Zpos p => Zpos (Pos.pred_double p) + | neg p => neg p~1 + | pos p => pos (Pos.pred_double p) end. (** ** Subtraction of positive into Z *) @@ -57,12 +62,12 @@ Fixpoint pos_sub (x y:positive) {struct y} : Z := match x, y with | p~1, q~1 => double (pos_sub p q) | p~1, q~0 => succ_double (pos_sub p q) - | p~1, 1 => Zpos p~0 + | p~1, 1 => pos p~0 | p~0, q~1 => pred_double (pos_sub p q) | p~0, q~0 => double (pos_sub p q) - | p~0, 1 => Zpos (Pos.pred_double p) - | 1, q~1 => Zneg q~0 - | 1, q~0 => Zneg (Pos.pred_double q) + | p~0, 1 => pos (Pos.pred_double p) + | 1, q~1 => neg q~0 + | 1, q~0 => neg (Pos.pred_double q) | 1, 1 => Z0 end%positive. @@ -72,10 +77,10 @@ Definition add x y := match x, y with | 0, y => y | x, 0 => x - | Zpos x', Zpos y' => Zpos (x' + y') - | Zpos x', Zneg y' => pos_sub x' y' - | Zneg x', Zpos y' => pos_sub y' x' - | Zneg x', Zneg y' => Zneg (x' + y') + | pos x', pos y' => pos (x' + y') + | pos x', neg y' => pos_sub x' y' + | neg x', pos y' => pos_sub y' x' + | neg x', neg y' => neg (x' + y') end. Infix "+" := add : Z_scope. @@ -85,8 +90,8 @@ Infix "+" := add : Z_scope. Definition opp x := match x with | 0 => 0 - | Zpos x => Zneg x - | Zneg x => Zpos x + | pos x => neg x + | neg x => pos x end. Notation "- x" := (opp x) : Z_scope. @@ -111,10 +116,10 @@ Definition mul x y := match x, y with | 0, _ => 0 | _, 0 => 0 - | Zpos x', Zpos y' => Zpos (x' * y') - | Zpos x', Zneg y' => Zneg (x' * y') - | Zneg x', Zpos y' => Zneg (x' * y') - | Zneg x', Zneg y' => Zpos (x' * y') + | pos x', pos y' => pos (x' * y') + | pos x', neg y' => neg (x' * y') + | neg x', pos y' => neg (x' * y') + | neg x', neg y' => pos (x' * y') end. Infix "*" := mul : Z_scope. @@ -125,9 +130,9 @@ Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1. Definition pow x y := match y with - | Zpos p => pow_pos x p + | pos p => pow_pos x p | 0 => 1 - | Zneg _ => 0 + | neg _ => 0 end. Infix "^" := pow : Z_scope. @@ -137,8 +142,8 @@ Infix "^" := pow : Z_scope. Definition square x := match x with | 0 => 0 - | Zpos p => Zpos (Pos.square p) - | Zneg p => Zpos (Pos.square p) + | pos p => pos (Pos.square p) + | neg p => pos (Pos.square p) end. (** ** Comparison *) @@ -146,14 +151,14 @@ Definition square x := Definition compare x y := match x, y with | 0, 0 => Eq - | 0, Zpos y' => Lt - | 0, Zneg y' => Gt - | Zpos x', 0 => Gt - | Zpos x', Zpos y' => (x' ?= y')%positive - | Zpos x', Zneg y' => Gt - | Zneg x', 0 => Lt - | Zneg x', Zpos y' => Lt - | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive) + | 0, pos y' => Lt + | 0, neg y' => Gt + | pos x', 0 => Gt + | pos x', pos y' => (x' ?= y')%positive + | pos x', neg y' => Gt + | neg x', 0 => Lt + | neg x', pos y' => Lt + | neg x', neg y' => CompOpp ((x' ?= y')%positive) end. Infix "?=" := compare (at level 70, no associativity) : Z_scope. @@ -163,8 +168,8 @@ Infix "?=" := compare (at level 70, no associativity) : Z_scope. Definition sgn z := match z with | 0 => 0 - | Zpos p => 1 - | Zneg p => -1 + | pos p => 1 + | neg p => -1 end. (** Boolean equality and comparisons *) @@ -200,8 +205,8 @@ Definition gtb x y := Fixpoint eqb x y := match x, y with | 0, 0 => true - | Zpos p, Zpos q => Pos.eqb p q - | Zneg p, Zneg q => Pos.eqb p q + | pos p, pos q => Pos.eqb p q + | neg p, neg q => Pos.eqb p q | _, _ => false end. @@ -230,8 +235,8 @@ Definition min n m := Definition abs z := match z with | 0 => 0 - | Zpos p => Zpos p - | Zneg p => Zpos p + | pos p => pos p + | neg p => pos p end. (** ** Conversions *) @@ -241,24 +246,24 @@ Definition abs z := Definition abs_nat (z:Z) : nat := match z with | 0 => 0%nat - | Zpos p => Pos.to_nat p - | Zneg p => Pos.to_nat p + | pos p => Pos.to_nat p + | neg p => Pos.to_nat p end. (** From [Z] to [N] via absolute value *) Definition abs_N (z:Z) : N := match z with - | Z0 => 0%N - | Zpos p => Npos p - | Zneg p => Npos p + | 0 => 0%N + | pos p => N.pos p + | neg p => N.pos p end. (** From [Z] to [nat] by rounding negative numbers to 0 *) Definition to_nat (z:Z) : nat := match z with - | Zpos p => Pos.to_nat p + | pos p => Pos.to_nat p | _ => O end. @@ -266,7 +271,7 @@ Definition to_nat (z:Z) : nat := Definition to_N (z:Z) : N := match z with - | Zpos p => Npos p + | pos p => N.pos p | _ => 0%N end. @@ -275,15 +280,23 @@ Definition to_N (z:Z) : N := Definition of_nat (n:nat) : Z := match n with | O => 0 - | S n => Zpos (Pos.of_succ_nat n) + | S n => pos (Pos.of_succ_nat n) end. (** From [N] to [Z] *) Definition of_N (n:N) : Z := match n with - | N0 => 0 - | Npos p => Zpos p + | 0%N => 0 + | N.pos p => pos p + end. + +(** From [Z] to [positive] by rounding nonpositive numbers to 1 *) + +Definition to_pos (z:Z) : positive := + match z with + | pos p => p + | _ => 1%positive end. (** ** Iteration of a function @@ -293,7 +306,7 @@ Definition of_N (n:N) : Z := Definition iter (n:Z) {A} (f:A -> A) (x:A) := match n with - | Zpos p => Pos.iter p f x + | pos p => Pos.iter p f x | _ => x end. @@ -348,17 +361,17 @@ Definition div_eucl (a b:Z) : Z * Z := match a, b with | 0, _ => (0, 0) | _, 0 => (0, 0) - | Zpos a', Zpos _ => pos_div_eucl a' b - | Zneg a', Zpos _ => + | pos a', pos _ => pos_div_eucl a' b + | neg a', pos _ => let (q, r) := pos_div_eucl a' b in match r with | 0 => (- q, 0) | _ => (- (q + 1), b - r) end - | Zneg a', Zneg b' => - let (q, r) := pos_div_eucl a' (Zpos b') in (q, - r) - | Zpos a', Zneg b' => - let (q, r) := pos_div_eucl a' (Zpos b') in + | neg a', neg b' => + let (q, r) := pos_div_eucl a' (pos b') in (q, - r) + | pos a', neg b' => + let (q, r) := pos_div_eucl a' (pos b') in match r with | 0 => (- q, 0) | _ => (- (q + 1), b + r) @@ -392,14 +405,14 @@ Definition quotrem (a b:Z) : Z * Z := match a, b with | 0, _ => (0, 0) | _, 0 => (0, a) - | Zpos a, Zpos b => - let (q, r) := N.pos_div_eucl a (Npos b) in (of_N q, of_N r) - | Zneg a, Zpos b => - let (q, r) := N.pos_div_eucl a (Npos b) in (-of_N q, - of_N r) - | Zpos a, Zneg b => - let (q, r) := N.pos_div_eucl a (Npos b) in (-of_N q, of_N r) - | Zneg a, Zneg b => - let (q, r) := N.pos_div_eucl a (Npos b) in (of_N q, - of_N r) + | pos a, pos b => + let (q, r) := N.pos_div_eucl a (N.pos b) in (of_N q, of_N r) + | neg a, pos b => + let (q, r) := N.pos_div_eucl a (N.pos b) in (-of_N q, - of_N r) + | pos a, neg b => + let (q, r) := N.pos_div_eucl a (N.pos b) in (-of_N q, of_N r) + | neg a, neg b => + let (q, r) := N.pos_div_eucl a (N.pos b) in (of_N q, - of_N r) end. Definition quot a b := fst (quotrem a b). @@ -414,16 +427,16 @@ Infix "÷" := quot (at level 40, left associativity) : Z_scope. Definition even z := match z with | 0 => true - | Zpos (xO _) => true - | Zneg (xO _) => true + | pos (xO _) => true + | neg (xO _) => true | _ => false end. Definition odd z := match z with | 0 => false - | Zpos (xO _) => false - | Zneg (xO _) => false + | pos (xO _) => false + | neg (xO _) => false | _ => true end. @@ -437,9 +450,9 @@ Definition odd z := Definition div2 z := match z with | 0 => 0 - | Zpos 1 => 0 - | Zpos p => Zpos (Pos.div2 p) - | Zneg p => Zneg (Pos.div2_up p) + | pos 1 => 0 + | pos p => pos (Pos.div2 p) + | neg p => neg (Pos.div2_up p) end. (** [quot2] performs rounding toward zero, it is hence a particular @@ -449,21 +462,21 @@ Definition div2 z := Definition quot2 (z:Z) := match z with | 0 => 0 - | Zpos 1 => 0 - | Zpos p => Zpos (Pos.div2 p) - | Zneg 1 => 0 - | Zneg p => Zneg (Pos.div2 p) + | pos 1 => 0 + | pos p => pos (Pos.div2 p) + | neg 1 => 0 + | neg p => neg (Pos.div2 p) end. -(** NB: [Z.quot2] used to be named [Zdiv2] in Coq <= 8.3 *) +(** NB: [Z.quot2] used to be named [Z.div2] in Coq <= 8.3 *) (** * Base-2 logarithm *) Definition log2 z := match z with - | Zpos (p~1) => Zpos (Pos.size p) - | Zpos (p~0) => Zpos (Pos.size p) + | pos (p~1) => pos (Pos.size p) + | pos (p~0) => pos (Pos.size p) | _ => 0 end. @@ -473,17 +486,17 @@ Definition log2 z := Definition sqrtrem n := match n with | 0 => (0, 0) - | Zpos p => + | pos p => match Pos.sqrtrem p with - | (s, IsPos r) => (Zpos s, Zpos r) - | (s, _) => (Zpos s, 0) + | (s, IsPos r) => (pos s, pos r) + | (s, _) => (pos s, 0) end - | Zneg _ => (0,0) + | neg _ => (0,0) end. Definition sqrt n := match n with - | Zpos p => Zpos (Pos.sqrt p) + | pos p => pos (Pos.sqrt p) | _ => 0 end. @@ -494,10 +507,10 @@ Definition gcd a b := match a,b with | 0, _ => abs b | _, 0 => abs a - | Zpos a, Zpos b => Zpos (Pos.gcd a b) - | Zpos a, Zneg b => Zpos (Pos.gcd a b) - | Zneg a, Zpos b => Zpos (Pos.gcd a b) - | Zneg a, Zneg b => Zpos (Pos.gcd a b) + | pos a, pos b => pos (Pos.gcd a b) + | pos a, neg b => pos (Pos.gcd a b) + | neg a, pos b => pos (Pos.gcd a b) + | neg a, neg b => pos (Pos.gcd a b) end. (** A generalized gcd, also computing division of a and b by gcd. *) @@ -506,14 +519,14 @@ Definition ggcd a b : Z*(Z*Z) := match a,b with | 0, _ => (abs b,(0, sgn b)) | _, 0 => (abs a,(sgn a, 0)) - | Zpos a, Zpos b => - let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zpos bb)) - | Zpos a, Zneg b => - let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zpos aa, Zneg bb)) - | Zneg a, Zpos b => - let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zpos bb)) - | Zneg a, Zneg b => - let '(g,(aa,bb)) := Pos.ggcd a b in (Zpos g, (Zneg aa, Zneg bb)) + | pos a, pos b => + let '(g,(aa,bb)) := Pos.ggcd a b in (pos g, (pos aa, pos bb)) + | pos a, neg b => + let '(g,(aa,bb)) := Pos.ggcd a b in (pos g, (pos aa, neg bb)) + | neg a, pos b => + let '(g,(aa,bb)) := Pos.ggcd a b in (pos g, (neg aa, pos bb)) + | neg a, neg b => + let '(g,(aa,bb)) := Pos.ggcd a b in (pos g, (neg aa, neg bb)) end. @@ -532,13 +545,13 @@ Definition ggcd a b : Z*(Z*Z) := Definition testbit a n := match n with | 0 => odd a - | Zpos p => + | pos p => match a with | 0 => false - | Zpos a => Pos.testbit a (Npos p) - | Zneg a => negb (N.testbit (Pos.pred_N a) (Npos p)) + | pos a => Pos.testbit a (N.pos p) + | neg a => negb (N.testbit (Pos.pred_N a) (N.pos p)) end - | Zneg _ => false + | neg _ => false end. (** Shifts @@ -555,8 +568,8 @@ Definition testbit a n := Definition shiftl a n := match n with | 0 => a - | Zpos p => Pos.iter p (mul 2) a - | Zneg p => Pos.iter p div2 a + | pos p => Pos.iter p (mul 2) a + | neg p => Pos.iter p div2 a end. Definition shiftr a n := shiftl a (-n). @@ -567,40 +580,40 @@ Definition lor a b := match a, b with | 0, _ => b | _, 0 => a - | Zpos a, Zpos b => Zpos (Pos.lor a b) - | Zneg a, Zpos b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N a) (Npos b))) - | Zpos a, Zneg b => Zneg (N.succ_pos (N.ldiff (Pos.pred_N b) (Npos a))) - | Zneg a, Zneg b => Zneg (N.succ_pos (N.land (Pos.pred_N a) (Pos.pred_N b))) + | pos a, pos b => pos (Pos.lor a b) + | neg a, pos b => neg (N.succ_pos (N.ldiff (Pos.pred_N a) (N.pos b))) + | pos a, neg b => neg (N.succ_pos (N.ldiff (Pos.pred_N b) (N.pos a))) + | neg a, neg b => neg (N.succ_pos (N.land (Pos.pred_N a) (Pos.pred_N b))) end. Definition land a b := match a, b with | 0, _ => 0 | _, 0 => 0 - | Zpos a, Zpos b => of_N (Pos.land a b) - | Zneg a, Zpos b => of_N (N.ldiff (Npos b) (Pos.pred_N a)) - | Zpos a, Zneg b => of_N (N.ldiff (Npos a) (Pos.pred_N b)) - | Zneg a, Zneg b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Pos.pred_N b))) + | pos a, pos b => of_N (Pos.land a b) + | neg a, pos b => of_N (N.ldiff (N.pos b) (Pos.pred_N a)) + | pos a, neg b => of_N (N.ldiff (N.pos a) (Pos.pred_N b)) + | neg a, neg b => neg (N.succ_pos (N.lor (Pos.pred_N a) (Pos.pred_N b))) end. Definition ldiff a b := match a, b with | 0, _ => 0 | _, 0 => a - | Zpos a, Zpos b => of_N (Pos.ldiff a b) - | Zneg a, Zpos b => Zneg (N.succ_pos (N.lor (Pos.pred_N a) (Npos b))) - | Zpos a, Zneg b => of_N (N.land (Npos a) (Pos.pred_N b)) - | Zneg a, Zneg b => of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a)) + | pos a, pos b => of_N (Pos.ldiff a b) + | neg a, pos b => neg (N.succ_pos (N.lor (Pos.pred_N a) (N.pos b))) + | pos a, neg b => of_N (N.land (N.pos a) (Pos.pred_N b)) + | neg a, neg b => of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a)) end. Definition lxor a b := match a, b with | 0, _ => b | _, 0 => a - | Zpos a, Zpos b => of_N (Pos.lxor a b) - | Zneg a, Zpos b => Zneg (N.succ_pos (N.lxor (Pos.pred_N a) (Npos b))) - | Zpos a, Zneg b => Zneg (N.succ_pos (N.lxor (Npos a) (Pos.pred_N b))) - | Zneg a, Zneg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) + | pos a, pos b => of_N (Pos.lxor a b) + | neg a, pos b => neg (N.succ_pos (N.lxor (Pos.pred_N a) (N.pos b))) + | pos a, neg b => neg (N.succ_pos (N.lxor (N.pos a) (Pos.pred_N b))) + | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. End Z.
\ No newline at end of file diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 7c840c563..384c046f3 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -250,7 +250,7 @@ Module MoreInt (Import I:Int). | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z - | EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2) + | EZmax e1 e2 => Z.max (ez2z e1) (ez2z e2) | EZopp e => (-(ez2z e))%Z | EZofI e => i2z (ei2i e) | EZraw z => z @@ -367,14 +367,14 @@ Module Z_as_Int <: Int. Definition _1 := 1. Definition _2 := 2. Definition _3 := 3. - Definition plus := Zplus. - Definition opp := Zopp. - Definition minus := Zminus. - Definition mult := Zmult. - Definition max := Zmax. + Definition plus := Z.add. + Definition opp := Z.opp. + Definition minus := Z.sub. + Definition mult := Z.mul. + Definition max := Z.max. Definition gt_le_dec := Z_gt_le_dec. Definition ge_lt_dec := Z_ge_lt_dec. - Definition eq_dec := Z_eq_dec. + Definition eq_dec := Z.eq_dec. Definition i2z : int -> Z := fun n => n. Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed. Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed. @@ -385,5 +385,5 @@ Module Z_as_Int <: Int. Lemma i2z_opp n : i2z (- n) = - i2z n. Proof. auto. Qed. Lemma i2z_minus n p : i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. Lemma i2z_mult n p : i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. - Lemma i2z_max n p : i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed. + Lemma i2z_max n p : i2z (max n p) = Z.max (i2z n) (i2z p). Proof. auto. Qed. End Z_as_Int. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index bcccc1269..bb84d0c8c 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -39,7 +39,7 @@ Proof. Qed. Lemma Z_of_nat_complete_inf (x : Z) : - 0 <= x -> {n : nat | x = Z_of_nat n}. + 0 <= x -> {n : nat | x = Z.of_nat n}. Proof. intros H. exists (Z.to_nat x). symmetry. now apply Z2Nat.id. Qed. @@ -53,7 +53,7 @@ Qed. Lemma Z_of_nat_set : forall P:Z -> Set, - (forall n:nat, P (Z_of_nat n)) -> forall x:Z, 0 <= x -> P x. + (forall n:nat, P (Z.of_nat n)) -> forall x:Z, 0 <= x -> P x. Proof. intros P H x Hx. now destruct (Z_of_nat_complete_inf x Hx) as (n,->). Qed. @@ -129,7 +129,7 @@ Section Efficient_Rec. - now destruct Hz. Qed. - (** A more general induction principle on non-negative numbers using [Zlt]. *) + (** A more general induction principle on non-negative numbers using [Z.lt]. *) Lemma Zlt_0_rec : forall P:Z -> Type, @@ -155,7 +155,7 @@ Section Efficient_Rec. exact Zlt_0_rec. Qed. - (** Obsolete version of [Zlt] induction principle on non-negative numbers *) + (** Obsolete version of [Z.lt] induction principle on non-negative numbers *) Lemma Z_lt_rec : forall P:Z -> Type, @@ -173,7 +173,7 @@ Section Efficient_Rec. exact Z_lt_rec. Qed. - (** An even more general induction principle using [Zlt]. *) + (** An even more general induction principle using [Z.lt]. *) Lemma Zlt_lower_bound_rec : forall P:Z -> Type, forall z:Z, diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index ca26787bd..cac3cd4e5 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -21,20 +21,16 @@ Proof. Defined. (* end hide *) -Lemma Zcompare_rect : - forall (P:Type) (n m:Z), - ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. +Lemma Zcompare_rect (P:Type) (n m:Z) : + ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. Proof. - intros * H1 H2 H3. + intros H1 H2 H3. destruct (n ?= m); auto. Defined. -Lemma Zcompare_rec : - forall (P:Set) (n m:Z), - ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. -Proof. - intro; apply Zcompare_rect. -Defined. +Lemma Zcompare_rec (P:Set) (n m:Z) : + ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. +Proof. apply Zcompare_rect. Defined. Notation Z_eq_dec := Z.eq_dec (compat "8.3"). @@ -46,38 +42,22 @@ Section decidability. Definition Z_lt_dec : {x < y} + {~ x < y}. Proof. - unfold Zlt in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - right. rewrite H. discriminate. - left; assumption. - right. rewrite H. discriminate. + unfold Z.lt; case Z.compare; (now left) || (now right). Defined. Definition Z_le_dec : {x <= y} + {~ x <= y}. Proof. - unfold Zle in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - left. rewrite H. discriminate. - left. rewrite H. discriminate. - right. tauto. + unfold Z.le; case Z.compare; (now left) || (right; tauto). Defined. Definition Z_gt_dec : {x > y} + {~ x > y}. Proof. - unfold Zgt in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - right. rewrite H. discriminate. - right. rewrite H. discriminate. - left; assumption. + unfold Z.gt; case Z.compare; (now left) || (now right). Defined. Definition Z_ge_dec : {x >= y} + {~ x >= y}. Proof. - unfold Zge in |- *. - apply Zcompare_rec with (n := x) (m := y); intro H. - left. rewrite H. discriminate. - right. tauto. - left. rewrite H. discriminate. + unfold Z.ge; case Z.compare; (now left) || (right; tauto). Defined. Definition Z_lt_ge_dec : {x < y} + {x >= y}. @@ -87,16 +67,15 @@ Section decidability. Lemma Z_lt_le_dec : {x < y} + {y <= x}. Proof. - intros. elim Z_lt_ge_dec. - intros; left; assumption. - intros; right; apply Zge_le; assumption. + * now left. + * right; now apply Z.ge_le. Defined. Definition Z_le_gt_dec : {x <= y} + {x > y}. Proof. elim Z_le_dec; auto with arith. - intro. right. apply Znot_le_gt; auto with arith. + intro. right. Z.swap_greater. now apply Z.nle_gt. Defined. Definition Z_gt_le_dec : {x > y} + {x <= y}. @@ -107,15 +86,15 @@ Section decidability. Definition Z_ge_lt_dec : {x >= y} + {x < y}. Proof. elim Z_ge_dec; auto with arith. - intro. right. apply Znot_ge_lt; auto with arith. + intro. right. Z.swap_greater. now apply Z.lt_nge. Defined. Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}. Proof. intro H. apply Zcompare_rec with (n := x) (m := y). - intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith. - intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith. + intro. right. elim (Z.compare_eq_iff x y); auto with arith. + intro. left. elim (Z.compare_eq_iff x y); auto with arith. intro H1. absurd (x > y); auto with arith. Defined. @@ -132,8 +111,8 @@ Proof. assumption. intro. right. - apply Zle_lt_trans with (m := x). - apply Zge_le. + apply Z.le_lt_trans with (m := x). + apply Z.ge_le. assumption. assumption. Defined. @@ -142,20 +121,16 @@ Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}. Proof. intros x y H. case (Zlt_cotrans 0 (x + y) H x). - intro. - left. - assumption. - intro. - right. - apply Zplus_lt_reg_l with (p := x). - rewrite Zplus_0_r. - assumption. + - now left. + - right. + apply Z.add_lt_mono_l with (p := x). + now rewrite Z.add_0_r. Defined. Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}. Proof. intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy; - [ right; apply Zplus_lt_reg_l with (p := x); rewrite Zplus_0_r | left ]; + [ right; apply Z.add_lt_mono_l with (p := x); rewrite Z.add_0_r | left ]; assumption. Defined. @@ -167,7 +142,7 @@ Proof. left. assumption. intro H0. - generalize (Zge_le _ _ H0). + generalize (Z.ge_le _ _ H0). intro. case (Z_le_lt_eq_dec _ _ H1). intro. @@ -189,13 +164,13 @@ Proof. left. assumption. intro H. - generalize (Zge_le _ _ H). + generalize (Z.ge_le _ _ H). intro H0. case (Z_le_lt_eq_dec y x H0). intro H1. left. right. - apply Zlt_gt. + apply Z.lt_gt. assumption. intro. right. @@ -207,7 +182,7 @@ Defined. Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}. Proof. intros x y. - case (Z_eq_dec x y); intro H; + case (Z.eq_dec x y); intro H; [ right; assumption | left; apply (not_Zeq_inf _ _ H) ]. Defined. @@ -215,12 +190,12 @@ Defined. (* To deprecate ? *) Corollary Z_zerop : forall x:Z, {x = 0} + {x <> 0}. Proof. - exact (fun x:Z => Z_eq_dec x 0). + exact (fun x:Z => Z.eq_dec x 0). Defined. Corollary Z_notzerop : forall (x:Z), {x <> 0} + {x = 0}. Proof (fun x => sumbool_not _ _ (Z_zerop x)). Corollary Z_noteq_dec : forall (x y:Z), {x <> y} + {x = y}. -Proof (fun x y => sumbool_not _ _ (Z_eq_dec x y)). +Proof (fun x y => sumbool_not _ _ (Z.eq_dec x y)). (* end hide *) diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 2e43b3554..1eaae5df0 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -77,9 +77,9 @@ Notation Zsgn_null := Z.sgn_null_iff (compat "8.3"). (** A characterization of the sign function: *) Lemma Zsgn_spec x : - 0 < x /\ Zsgn x = 1 \/ - 0 = x /\ Zsgn x = 0 \/ - 0 > x /\ Zsgn x = -1. + 0 < x /\ Z.sgn x = 1 \/ + 0 = x /\ Z.sgn x = 0 \/ + 0 > x /\ Z.sgn x = -1. Proof. intros. Z.swap_greater. apply Z.sgn_spec. Qed. @@ -99,7 +99,7 @@ Proof. intros (H,H'). apply Zabs2Nat.inj_le; trivial. now transitivity n. Qed. -Lemma Zabs_nat_lt n m : 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat. +Lemma Zabs_nat_lt n m : 0 <= n < m -> (Z.abs_nat n < Z.abs_nat m)%nat. Proof. intros (H,H'). apply Zabs2Nat.inj_lt; trivial. transitivity n; trivial. now apply Z.lt_le_incl. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 7c1e096ed..3a86a821b 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -25,7 +25,7 @@ Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y). Definition Z_le_gt_bool (x y:Z) := bool_of_sumbool (Z_le_gt_dec x y). Definition Z_gt_le_bool (x y:Z) := bool_of_sumbool (Z_gt_le_dec x y). -Definition Z_eq_bool (x y:Z) := bool_of_sumbool (Z_eq_dec x y). +Definition Z_eq_bool (x y:Z) := bool_of_sumbool (Z.eq_dec x y). Definition Z_noteq_bool (x y:Z) := bool_of_sumbool (Z_noteq_dec x y). Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x). diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 703a3972f..e369aa6ab 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Binary Integers : results about Zcompare *) +(** Binary Integers : results about Z.compare *) (** Initial author: Pierre Crégut (CNET, Lannion, France *) (** THIS FILE IS DEPRECATED. @@ -85,7 +85,7 @@ Qed. Lemma Zcompare_succ_compat n m : (Z.succ n ?= Z.succ m) = (n ?= m). Proof. - rewrite <- 2 Z.add_1_l. apply Zcompare_plus_compat. + rewrite <- 2 Z.add_1_l. apply Z.add_compare_mono_l. Qed. (** * Multiplication and comparison *) @@ -106,7 +106,7 @@ Qed. Lemma Zmult_compare_compat_r n m p : p > 0 -> (n ?= m) = (n * p ?= m * p). Proof. - intros; rewrite 2 (Zmult_comm _ p); now apply Zmult_compare_compat_l. + intros; rewrite 2 (Z.mul_comm _ p); now apply Zmult_compare_compat_l. Qed. (** * Relating [x ?= y] to [=], [<=], [<], [>=] or [>] *) diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 5a2c3cc32..dde0745eb 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -39,8 +39,8 @@ Proof. reflexivity. Qed. Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. Proof. unfold floor. induction p; simpl. - - rewrite !Z.pos_xI, (Z.pos_xO (xO _)), Z.pos_xO. omega. - - rewrite (Z.pos_xO (xO _)), (Z.pos_xO p), Z.pos_xO. omega. + - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. omega. + - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. omega. - omega. Qed. @@ -107,7 +107,7 @@ Require Import List. Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z := match l with | nil => acc - | _ :: l => Zlength_aux (Zsucc acc) A l + | _ :: l => Zlength_aux (Z.succ acc) A l end. Definition Zlength := Zlength_aux 0. diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index ff1d96df4..a9348785a 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -64,7 +64,7 @@ Section ENCODING_VALUE. (** We compute the binary value via a Horner scheme. Computation stops at the vector length without checks. - We define a function Zmod2 similar to Zdiv2 returning the + We define a function Zmod2 similar to Z.div2 returning the quotient of division z=2q+r with 0<=r<=1. The two's complement value is also computed via a Horner scheme with Zmod2, the parameter is the size minus one. @@ -88,7 +88,7 @@ Section ENCODING_VALUE. Lemma Zmod2_twice : - forall z:Z, z = (2 * Zmod2 z + bit_value (Zeven.Zodd_bool z))%Z. + forall z:Z, z = (2 * Zmod2 z + bit_value (Z.odd z))%Z. Proof. destruct z; simpl in |- *. trivial. @@ -97,7 +97,7 @@ Section ENCODING_VALUE. destruct p; simpl in |- *. destruct p as [p| p| ]; simpl in |- *. - rewrite <- (Pdouble_minus_one_o_succ_eq_xI p); trivial. + rewrite <- (Pos.pred_double_succ p); trivial. trivial. @@ -113,15 +113,15 @@ Section ENCODING_VALUE. simple induction n; intros. exact Bnil. - exact (Bcons (Zeven.Zodd_bool H0) n0 (H (Zeven.Zdiv2 H0))). + exact (Bcons (Z.odd H0) n0 (H (Z.div2 H0))). Defined. Lemma Z_to_two_compl : forall n:nat, Z -> Bvector (S n). Proof. simple induction n; intros. - exact (Bcons (Zeven.Zodd_bool H) 0 Bnil). + exact (Bcons (Z.odd H) 0 Bnil). - exact (Bcons (Zeven.Zodd_bool H0) (S n0) (H (Zmod2 H0))). + exact (Bcons (Z.odd H0) (S n0) (H (Zmod2 H0))). Defined. End ENCODING_VALUE. @@ -175,27 +175,27 @@ Section Z_BRIC_A_BRAC. destruct b; destruct z as [| p| p]; auto. destruct p as [p| p| ]; auto. destruct p as [p| p| ]; simpl in |- *; auto. - intros; rewrite (Psucc_o_double_minus_one_eq_xO p); trivial. + intros; rewrite (Pos.succ_pred_double p); trivial. Qed. Lemma Z_to_binary_Sn_z : forall (n:nat) (z:Z), Z_to_binary (S n) z = - Bcons (Zeven.Zodd_bool z) n (Z_to_binary n (Zeven.Zdiv2 z)). + Bcons (Z.odd z) n (Z_to_binary n (Z.div2 z)). Proof. intros; auto. Qed. Lemma Z_div2_value : forall z:Z, - (z >= 0)%Z -> (bit_value (Zeven.Zodd_bool z) + 2 * Zeven.Zdiv2 z)%Z = z. + (z >= 0)%Z -> (bit_value (Z.odd z) + 2 * Z.div2 z)%Z = z. Proof. destruct z as [| p| p]; auto. destruct p; auto. intro H; elim H; trivial. Qed. - Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Zeven.Zdiv2 z >= 0)%Z. + Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Z.div2 z >= 0)%Z. Proof. destruct z as [| p| p]. auto. @@ -209,10 +209,10 @@ Section Z_BRIC_A_BRAC. Lemma Zdiv2_two_power_nat : forall (z:Z) (n:nat), (z >= 0)%Z -> - (z < two_power_nat (S n))%Z -> (Zeven.Zdiv2 z < two_power_nat n)%Z. + (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z. Proof. intros. - cut (2 * Zeven.Zdiv2 z < 2 * two_power_nat n)%Z; intros. + cut (2 * Z.div2 z < 2 * two_power_nat n)%Z; intros. omega. rewrite <- two_power_nat_S. @@ -225,13 +225,13 @@ Section Z_BRIC_A_BRAC. Lemma Z_to_two_compl_Sn_z : forall (n:nat) (z:Z), Z_to_two_compl (S n) z = - Bcons (Zeven.Zodd_bool z) (S n) (Z_to_two_compl n (Zmod2 z)). + Bcons (Z.odd z) (S n) (Z_to_two_compl n (Zmod2 z)). Proof. intros; auto. Qed. Lemma Zeven_bit_value : - forall z:Z, Zeven.Zeven z -> bit_value (Zeven.Zodd_bool z) = 0%Z. + forall z:Z, Zeven.Zeven z -> bit_value (Z.odd z) = 0%Z. Proof. destruct z; unfold bit_value in |- *; auto. destruct p; tauto || (intro H; elim H). @@ -239,7 +239,7 @@ Section Z_BRIC_A_BRAC. Qed. Lemma Zodd_bit_value : - forall z:Z, Zeven.Zodd z -> bit_value (Zeven.Zodd_bool z) = 1%Z. + forall z:Z, Zeven.Zodd z -> bit_value (Z.odd z) = 1%Z. Proof. destruct z; unfold bit_value in |- *; auto. intros; elim H. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 057fd6d34..0546c3f6f 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -63,8 +63,8 @@ Definition Remainder r b := 0 <= r < b \/ b < r <= 0. Definition Remainder_alt r b := Z.abs r < Z.abs b /\ Z.sgn r <> - Z.sgn b. -(* In the last formulation, [ Zsgn r <> - Zsgn b ] is less nice than saying - [ Zsgn r = Zsgn b ], but at least it works even when [r] is null. *) +(* In the last formulation, [ Z.sgn r <> - Z.sgn b ] is less nice than saying + [ Z.sgn r = Z.sgn b ], but at least it works even when [r] is null. *) Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b. Proof. @@ -89,7 +89,7 @@ Proof. now destruct Hb. left; now apply POS. right; now apply NEG. Qed. -(** The same results as before, stated separately in terms of Zdiv and Zmod *) +(** The same results as before, stated separately in terms of Z.div and Z.modulo *) Lemma Z_mod_remainder a b : b<>0 -> Remainder (a mod b) b. Proof. @@ -98,7 +98,7 @@ Proof. Qed. Lemma Z_mod_lt a b : b > 0 -> 0 <= a mod b < b. -Proof (fun Hb => Z.mod_pos_bound a b (Zgt_lt _ _ Hb)). +Proof (fun Hb => Z.mod_pos_bound a b (Z.gt_lt _ _ Hb)). Lemma Z_mod_neg a b : b < 0 -> b < a mod b <= 0. Proof (Z.mod_neg_bound a b). @@ -220,7 +220,7 @@ Proof. intros. zero_or_not b. apply Z.mod_mul. auto. Qed. Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a. Proof Z.div_mul. -(** * Order results about Zmod and Zdiv *) +(** * Order results about Z.modulo and Z.div *) (* Division of positive numbers is positive. *) @@ -248,12 +248,12 @@ Proof Z.div_small. Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a. Proof Z.mod_small. -(** [Zge] is compatible with a positive division. *) +(** [Z.ge] is compatible with a positive division. *) Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c. -Proof. intros. apply Zle_ge. apply Z.div_le_mono; auto with zarith. Qed. +Proof. intros. apply Z.le_ge. apply Z.div_le_mono; auto with zarith. Qed. -(** Same, with [Zle]. *) +(** Same, with [Z.le]. *) Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c. Proof. intros. apply Z.div_le_mono; auto with zarith. Qed. @@ -264,7 +264,7 @@ Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a. Proof. intros. apply Z.mul_div_le; auto with zarith. Qed. Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a. -Proof. intros. apply Zle_ge. apply Z.mul_div_ge; auto with zarith. Qed. +Proof. intros. apply Z.le_ge. apply Z.mul_div_ge; auto with zarith. Qed. (** The previous inequalities are exact iff the modulo is zero. *) @@ -279,7 +279,7 @@ Proof. intros; rewrite Z.div_exact; auto. Qed. Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a. Proof. intros. apply Z.mod_le; auto. Qed. -(** Some additionnal inequalities about Zdiv. *) +(** Some additionnal inequalities about Z.div. *) Theorem Zdiv_lt_upper_bound: forall a b q, 0 < b -> a < q*b -> a/b < q. @@ -307,7 +307,7 @@ Proof. destruct Z.pos_div_eucl as (q,r); destruct r; omega with *. Qed. -(** * Relations between usual operations and Zmod and Zdiv *) +(** * Relations between usual operations and Z.modulo and Z.div *) Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c. Proof. intros. zero_or_not c. apply Z.mod_add; auto. Qed. @@ -318,9 +318,9 @@ Proof Z.div_add. Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof Z.div_add_l. -(** [Zopp] and [Zdiv], [Zmod]. +(** [Z.opp] and [Z.div], [Z.modulo]. Due to the choice of convention for our Euclidean division, - some of the relations about [Zopp] and divisions are rather complex. *) + some of the relations about [Z.opp] and divisions are rather complex. *) Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. Proof. intros. zero_or_not b. apply Z.div_opp_opp; auto. Qed. @@ -365,22 +365,22 @@ Proof. intros. zero_or_not b. apply Z.div_mul_cancel_r; auto. Qed. Lemma Zdiv_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)/(c*b) = a/b. Proof. - intros. rewrite (Zmult_comm c b); zero_or_not b. - rewrite (Zmult_comm b c). apply Z.div_mul_cancel_l; auto. + intros. rewrite (Z.mul_comm c b); zero_or_not b. + rewrite (Z.mul_comm b c). apply Z.div_mul_cancel_l; auto. Qed. Lemma Zmult_mod_distr_l: forall a b c, (c*a) mod (c*b) = c * (a mod b). Proof. - intros. zero_or_not c. rewrite (Zmult_comm c b); zero_or_not b. - rewrite (Zmult_comm b c). apply Z.mul_mod_distr_l; auto. + intros. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b. + rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto. Qed. Lemma Zmult_mod_distr_r: forall a b c, (a*c) mod (b*c) = (a mod b) * c. Proof. - intros. zero_or_not b. rewrite (Zmult_comm b c); zero_or_not c. - rewrite (Zmult_comm c b). apply Z.mul_mod_distr_r; auto. + intros. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c. + rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto. Qed. (** Operations modulo. *) @@ -464,22 +464,22 @@ Proof. constructor; [exact eqm_refl | exact eqm_sym | exact eqm_trans]. Qed. -Instance Zplus_eqm : Proper (eqm ==> eqm ==> eqm) Zplus. +Instance Zplus_eqm : Proper (eqm ==> eqm ==> eqm) Z.add. Proof. unfold eqm; repeat red; intros. rewrite Zplus_mod, H, H0, <- Zplus_mod; auto. Qed. -Instance Zminus_eqm : Proper (eqm ==> eqm ==> eqm) Zminus. +Instance Zminus_eqm : Proper (eqm ==> eqm ==> eqm) Z.sub. Proof. unfold eqm; repeat red; intros. rewrite Zminus_mod, H, H0, <- Zminus_mod; auto. Qed. -Instance Zmult_eqm : Proper (eqm ==> eqm ==> eqm) Zmult. +Instance Zmult_eqm : Proper (eqm ==> eqm ==> eqm) Z.mul. Proof. unfold eqm; repeat red; intros. rewrite Zmult_mod, H, H0, <- Zmult_mod; auto. Qed. -Instance Zopp_eqm : Proper (eqm ==> eqm) Zopp. +Instance Zopp_eqm : Proper (eqm ==> eqm) Z.opp. Proof. intros x y H. change ((-x)==(-y)) with ((0-x)==(0-y)). now rewrite H. Qed. @@ -489,7 +489,7 @@ Proof. intros; exact (Zmod_mod a N). Qed. -(* NB: Zmod and Zdiv are not morphisms with respect to eqm. +(* NB: Z.modulo and Z.div are not morphisms with respect to eqm. For instance, let (==) be (eqm 2). Then we have (3 == 1) but: ~ (3 mod 3 == 1 mod 3) ~ (1 mod 3 == 1 mod 1) @@ -501,7 +501,7 @@ End EqualityModulo. Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c). Proof. - intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c. + intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. rewrite Z.mul_comm. apply Z.div_div; auto with zarith. Qed. @@ -515,7 +515,7 @@ Theorem Zdiv_mult_le: Proof. intros. zero_or_not b. apply Z.div_mul_le; auto with zarith. Qed. -(** Zmod is related to divisibility (see more in Znumtheory) *) +(** Z.modulo is related to divisibility (see more in Znumtheory) *) Lemma Zmod_divides : forall a b, b<>0 -> (a mod b = 0 <-> exists c, a = b*c). @@ -536,17 +536,17 @@ Qed. Lemma Zmod_even : forall a, a mod 2 = if Z.even a then 0 else 1. Proof. - intros a. rewrite Zmod_odd, Zodd_even_bool. now destruct Zeven_bool. + intros a. rewrite Zmod_odd, Zodd_even_bool. now destruct Z.even. Qed. Lemma Zodd_mod : forall a, Z.odd a = Zeq_bool (a mod 2) 1. Proof. - intros a. rewrite Zmod_odd. now destruct Zodd_bool. + intros a. rewrite Zmod_odd. now destruct Z.odd. Qed. Lemma Zeven_mod : forall a, Z.even a = Zeq_bool (a mod 2) 0. Proof. - intros a. rewrite Zmod_even. now destruct Zeven_bool. + intros a. rewrite Zmod_even. now destruct Z.even. Qed. (** * Compatibility *) @@ -593,7 +593,7 @@ Proof. intros; apply Z_mod_zero_opp_full; auto with zarith. Qed. -(** * A direct way to compute Zmod *) +(** * A direct way to compute Z.modulo *) Fixpoint Zmod_POS (a : positive) (b : Z) : Z := match a with @@ -675,7 +675,7 @@ Proof. exists (- q, r). elim Hqr; intros. split. - rewrite <- Zmult_opp_comm; assumption. + rewrite <- Z.mul_opp_comm; assumption. rewrite Z.abs_neq; [ assumption | omega ]. Qed. @@ -692,7 +692,7 @@ Proof. apply (Zdiv_unique _ _ _ (Z.of_nat (n mod m))). split. auto with zarith. now apply inj_lt, Nat.mod_upper_bound. - rewrite <- inj_mult, <- inj_plus. + rewrite <- Nat2Z.inj_mul, <- Nat2Z.inj_add. now apply inj_eq, Nat.div_mod. Qed. @@ -703,6 +703,6 @@ Proof. apply (Zmod_unique _ _ (Z.of_nat n / Z.of_nat m)). split. auto with zarith. now apply inj_lt, Nat.mod_upper_bound. - rewrite <- div_Zdiv, <- inj_mult, <- inj_plus by trivial. + rewrite <- div_Zdiv, <- Nat2Z.inj_mul, <- Nat2Z.inj_add by trivial. now apply inj_eq, Nat.div_mod. Qed. diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index a032a801d..bef8ee78b 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -136,7 +136,7 @@ Notation Zodd_bool_succ := Z.odd_succ (compat "8.3"). Notation Zodd_bool_pred := Z.odd_pred (compat "8.3"). (******************************************************************) -(** * Definition of [Zquot2], [Zdiv2] and properties wrt [Zeven] +(** * Definition of [Z.quot2], [Z.div2] and properties wrt [Zeven] and [Zodd] *) Notation Zdiv2 := Z.div2 (compat "8.3"). @@ -225,7 +225,7 @@ Lemma Zsplit2 n : {p : Z * Z | let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}. Proof. destruct (Z_modulo_2 n) as [(y,Hy)|(y,Hy)]; - rewrite Z.mul_comm, <- Zplus_diag_eq_mult_2 in Hy. + rewrite <- Z.add_diag in Hy. - exists (y, y). split. assumption. now left. - exists (y, y + 1). split. now rewrite Z.add_assoc. now right. Qed. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index ebf3d0246..a1fedd536 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** * Zgcd_alt : an alternate version of Zgcd, based on Euclid's algorithm *) +(** * Zgcd_alt : an alternate version of Z.gcd, based on Euclid's algorithm *) (** Author: Pierre Letouzey *) -(** The alternate [Zgcd_alt] given here used to be the main [Zgcd] - function (see file [Znumtheory]), but this main [Zgcd] is now +(** The alternate [Zgcd_alt] given here used to be the main [Z.gcd] + function (see file [Znumtheory]), but this main [Z.gcd] is now based on a modern binary-efficient algorithm. This earlier version, based on Euclid's algorithm of iterated modulo, is kept here due to both its intrinsic interest and its use as reference @@ -35,22 +35,22 @@ Open Scope Z_scope. match n with | O => 1 (* arbitrary, since n should be big enough *) | S n => match a with - | Z0 => Zabs b - | Zpos _ => Zgcdn n (Zmod b a) a - | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a) + | Z0 => Z.abs b + | Zpos _ => Zgcdn n (Z.modulo b a) a + | Zneg a => Zgcdn n (Z.modulo b (Zpos a)) (Zpos a) end end. Definition Zgcd_bound (a:Z) := match a with | Z0 => S O - | Zpos p => let n := Psize p in (n+n)%nat - | Zneg p => let n := Psize p in (n+n)%nat + | Zpos p => let n := Pos.size_nat p in (n+n)%nat + | Zneg p => let n := Pos.size_nat p in (n+n)%nat end. Definition Zgcd_alt a b := Zgcdn (Zgcd_bound a) a b. - (** A first obvious fact : [Zgcd a b] is positive. *) + (** A first obvious fact : [Z.gcd a b] is positive. *) Lemma Zgcdn_pos : forall n a b, 0 <= Zgcdn n a b. @@ -62,28 +62,28 @@ Open Scope Z_scope. Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b. Proof. - intros; unfold Zgcd; apply Zgcdn_pos; auto. + intros; unfold Z.gcd; apply Zgcdn_pos; auto. Qed. - (** We now prove that Zgcd is indeed a gcd. *) + (** We now prove that Z.gcd is indeed a gcd. *) (** 1) We prove a weaker & easier bound. *) Lemma Zgcdn_linear_bound : forall n a b, - Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b). + Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b). Proof. induction n. simpl; intros. - exfalso; generalize (Zabs_pos a); omega. + exfalso; generalize (Z.abs_nonneg a); omega. destruct a; intros; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; - unfold Zmod; - generalize (Z_div_mod b (Zpos p) (refl_equal Gt)); - destruct (Zdiv_eucl b (Zpos p)) as (q,r); + unfold Z.modulo; + generalize (Z_div_mod b (Zpos p) (eq_refl Gt)); + destruct (Z.div_eucl b (Zpos p)) as (q,r); intros (H0,H1); - rewrite inj_S in H; simpl Zabs in H; - (assert (H2: Zabs r < Z_of_nat n) by - (rewrite Zabs_eq; auto with zarith)); + rewrite Nat2Z.inj_succ in H; simpl Z.abs in H; + (assert (H2: Z.abs r < Z.of_nat n) by + (rewrite Z.abs_eq; auto with zarith)); assert (IH:=IHn r (Zpos p) H2); clear IHn; simpl in IH |- *; rewrite H0. @@ -122,7 +122,7 @@ Open Scope Z_scope. Proof. induction 1. auto with zarith. - apply Zle_trans with (fibonacci m); auto. + apply Z.le_trans with (fibonacci m); auto. clear. destruct m. simpl; auto with zarith. @@ -142,53 +142,38 @@ Open Scope Z_scope. fibonacci (S (S n)) <= b. Proof. induction n. - simpl; intros. - destruct a; omega. - intros. - destruct a; [simpl in *; omega| | destruct H; discriminate]. - revert H1; revert H0. - set (m:=S n) in *; (assert (m=S n) by auto); clearbody m. - pattern m at 2; rewrite H0. - simpl Zgcdn. - unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). - destruct (Zdiv_eucl b (Zpos p)) as (q,r). - intros (H1,H2). - destruct H2. - destruct (Zle_lt_or_eq _ _ H2). - generalize (IHn _ _ (conj H4 H3)). - intros H5 H6 H7. - replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. - assert (r = Zpos p * (-q) + b) by (rewrite H1; ring). - destruct H5; auto. - pattern r at 1; rewrite H8. - apply Zis_gcd_sym. - apply Zis_gcd_for_euclid2; auto. - apply Zis_gcd_sym; auto. - split; auto. - rewrite H1. - apply Zplus_le_compat; auto. - apply Zle_trans with (Zpos p * 1); auto. - ring_simplify (Zpos p * 1); auto. - apply Zmult_le_compat_l. - destruct q. - omega. - assert (0 < Zpos p0) by (compute; auto). - omega. - assert (Zpos p * Zneg p0 < 0) by (compute; auto). - omega. - compute; intros; discriminate. - (* r=0 *) - subst r. - simpl; rewrite H0. - intros. - simpl in H4. - simpl in H5. - destruct n. - simpl in H5. - simpl. - omega. - simpl in H5. - elim H5; auto. + intros [|a|a]; intros; simpl; omega. + intros [|a|a] b (Ha,Ha'); [simpl; omega | | easy ]. + remember (S n) as m. + rewrite Heqm at 2. simpl Zgcdn. + unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl). + destruct (Z.div_eucl b (Zpos a)) as (q,r). + intros (EQ,(Hr,Hr')). + Z.le_elim Hr. + - (* r > 0 *) + replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. + intros. + destruct (IHn r (Zpos a) (conj Hr Hr')); auto. + + assert (EQ' : r = Zpos a * (-q) + b) by (rewrite EQ; ring). + rewrite EQ' at 1. + apply Zis_gcd_sym. + apply Zis_gcd_for_euclid2; auto. + apply Zis_gcd_sym; auto. + + split; auto. + rewrite EQ. + apply Z.add_le_mono; auto. + apply Z.le_trans with (Zpos a * 1); auto. + now rewrite Z.mul_1_r. + apply Z.mul_le_mono_nonneg_l; auto with zarith. + change 1 with (Z.succ 0). apply Z.le_succ_l. + destruct q; auto with zarith. + assert (Zpos a * Zneg p < 0) by now compute. omega. + - (* r = 0 *) + clear IHn EQ Hr'; intros _. + subst r; simpl; rewrite Heqm. + destruct n. + + simpl. omega. + + now destruct 1. Qed. (** 3b) We reformulate the previous result in a more positive way. *) @@ -199,18 +184,18 @@ Open Scope Z_scope. Proof. destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate]. cut (forall k n b, - k = (S (nat_of_P p) - n)%nat -> + k = (S (Pos.to_nat p) - n)%nat -> 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). destruct 2; eauto. clear n; induction k. intros. - assert (nat_of_P p < n)%nat by omega. + assert (Pos.to_nat p < n)%nat by omega. apply Zgcdn_linear_bound. simpl. generalize (inj_le _ _ H2). - rewrite inj_S. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto. + rewrite Nat2Z.inj_succ. + rewrite positive_nat_Z; auto. omega. intros. generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. @@ -233,77 +218,69 @@ Open Scope Z_scope. induction p; [ | | compute; auto ]; simpl Zgcd_bound in *; rewrite plus_comm; simpl plus; - set (n:= (Psize p+Psize p)%nat) in *; simpl; + set (n:= (Pos.size_nat p+Pos.size_nat p)%nat) in *; simpl; assert (n <> O) by (unfold n; destruct p; simpl; auto). destruct n as [ |m]; [elim H; auto| ]. - generalize (fibonacci_pos m); rewrite Zpos_xI; omega. + generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; omega. destruct n as [ |m]; [elim H; auto| ]. - generalize (fibonacci_pos m); rewrite Zpos_xO; omega. + generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; omega. Qed. (* 5) the end: we glue everything together and take care of situations not corresponding to [0<a<b]. *) - Lemma Zgcdn_is_gcd : - forall n a b, (Zgcd_bound a <= n)%nat -> - Zis_gcd a b (Zgcdn n a b). + Lemma Zgcd_bound_opp a : Zgcd_bound (-a) = Zgcd_bound a. + Proof. + now destruct a. + Qed. + + Lemma Zgcdn_opp n a b : Zgcdn n (-a) b = Zgcdn n a b. + Proof. + induction n; simpl; auto. + destruct a; simpl; auto. + Qed. + + Lemma Zgcdn_is_gcd_pos n a b : (Zgcd_bound (Zpos a) <= n)%nat -> + Zis_gcd (Zpos a) b (Zgcdn n (Zpos a) b). + Proof. + intros. + generalize (Zgcd_bound_fibonacci (Zpos a)). + simpl Zgcd_bound in *. + remember (Pos.size_nat a+Pos.size_nat a)%nat as m. + assert (1 < m)%nat. + { rewrite Heqm; destruct a; simpl; rewrite 1?plus_comm; + auto with arith. } + destruct m as [ |m]; [inversion H0; auto| ]. + destruct n as [ |n]; [inversion H; auto| ]. + simpl Zgcdn. + unfold Z.modulo. + generalize (Z_div_mod b (Zpos a) (eq_refl Gt)). + destruct (Z.div_eucl b (Zpos a)) as (q,r). + intros (->,(H1,H2)) H3. + apply Zis_gcd_for_euclid2. + Z.le_elim H1. + + apply Zgcdn_ok_before_fibonacci; auto. + apply Z.lt_le_trans with (fibonacci (S m)); + [ omega | apply fibonacci_incr; auto]. + + subst r; simpl. + destruct m as [ |m]; [exfalso; omega| ]. + destruct n as [ |n]; [exfalso; omega| ]. + simpl; apply Zis_gcd_sym; apply Zis_gcd_0. + Qed. + + Lemma Zgcdn_is_gcd n a b : + (Zgcd_bound a <= n)%nat -> Zis_gcd a b (Zgcdn n a b). Proof. - destruct a; intros. - simpl in H. - destruct n; [exfalso; omega | ]. - simpl; generalize (Zis_gcd_0_abs b); intuition. - (*Zpos*) - generalize (Zgcd_bound_fibonacci (Zpos p)). - simpl Zgcd_bound in *. - remember (Psize p+Psize p)%nat as m. - assert (1 < m)%nat. - rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; - auto with arith. - destruct m as [ |m]; [inversion H0; auto| ]. - destruct n as [ |n]; [inversion H; auto| ]. - simpl Zgcdn. - unfold Zmod. - generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). - destruct (Zdiv_eucl b (Zpos p)) as (q,r). - intros (H2,H3) H4. - rewrite H2. - apply Zis_gcd_for_euclid2. - destruct H3. - destruct (Zle_lt_or_eq _ _ H1). - apply Zgcdn_ok_before_fibonacci; auto. - apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto]. - subst r; simpl. - destruct m as [ |m]; [exfalso; omega| ]. - destruct n as [ |n]; [exfalso; omega| ]. - simpl; apply Zis_gcd_sym; apply Zis_gcd_0. - (*Zneg*) - generalize (Zgcd_bound_fibonacci (Zpos p)). - simpl Zgcd_bound in *. - remember (Psize p+Psize p)%nat as m. - assert (1 < m)%nat. - rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; - auto with arith. - destruct m as [ |m]; [inversion H0; auto| ]. - destruct n as [ |n]; [inversion H; auto| ]. - simpl Zgcdn. - unfold Zmod. - generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). - destruct (Zdiv_eucl b (Zpos p)) as (q,r). - intros (H1,H2) H3. - rewrite H1. - apply Zis_gcd_minus. - apply Zis_gcd_sym. - apply Zis_gcd_for_euclid2. - destruct H2. - destruct (Zle_lt_or_eq _ _ H2). - apply Zgcdn_ok_before_fibonacci; auto. - apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto]. - subst r; simpl. - destruct m as [ |m]; [exfalso; omega| ]. - destruct n as [ |n]; [exfalso; omega| ]. - simpl; apply Zis_gcd_sym; apply Zis_gcd_0. + destruct a. + - simpl; intros. + destruct n; [exfalso; omega | ]. + simpl; generalize (Zis_gcd_0_abs b); intuition. + - apply Zgcdn_is_gcd_pos. + - rewrite <- Zgcd_bound_opp, <- Zgcdn_opp. + intros. apply Zis_gcd_minus, Zis_gcd_sym. simpl Z.opp. + now apply Zgcdn_is_gcd_pos. Qed. Lemma Zgcd_is_gcd : diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 6a14d6934..e50a5e445 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -43,58 +43,59 @@ Hint Resolve (** Should clearly be declared as hints *) (** Lemmas ending by eq *) - Zsucc_eq_compat (* :(n,m:Z)`n = m`->`(Zs n) = (Zs m)` *) - - (** Lemmas ending by Zgt *) - Zsucc_gt_compat (* :(n,m:Z)`m > n`->`(Zs m) > (Zs n)` *) - Zgt_succ (* :(n:Z)`(Zs n) > n` *) - Zorder.Zgt_pos_0 (* :(p:positive)`(POS p) > 0` *) - Zplus_gt_compat_l (* :(n,m,p:Z)`n > m`->`p+n > p+m` *) - Zplus_gt_compat_r (* :(n,m,p:Z)`n > m`->`n+p > m+p` *) - - (** Lemmas ending by Zlt *) - Zlt_succ (* :(n:Z)`n < (Zs n)` *) - Zsucc_lt_compat (* :(n,m:Z)`n < m`->`(Zs n) < (Zs m)` *) - Zlt_pred (* :(n:Z)`(Zpred n) < n` *) - Zplus_lt_compat_l (* :(n,m,p:Z)`n < m`->`p+n < p+m` *) - Zplus_lt_compat_r (* :(n,m,p:Z)`n < m`->`n+p < m+p` *) - - (** Lemmas ending by Zle *) - Zle_0_nat (* :(n:nat)`0 <= (inject_nat n)` *) - Zorder.Zle_0_pos (* :(p:positive)`0 <= (POS p)` *) - Zle_refl (* :(n:Z)`n <= n` *) - Zle_succ (* :(n:Z)`n <= (Zs n)` *) - Zsucc_le_compat (* :(n,m:Z)`m <= n`->`(Zs m) <= (Zs n)` *) - Zle_pred (* :(n:Z)`(Zpred n) <= n` *) - Zle_min_l (* :(n,m:Z)`(Zmin n m) <= n` *) - Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *) - Zplus_le_compat_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *) - Zplus_le_compat_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *) - Zabs_pos (* :(x:Z)`0 <= |x|` *) + Zsucc_eq_compat (* n = m -> Z.succ n = Z.succ m *) + + (** Lemmas ending by Z.gt *) + Zsucc_gt_compat (* m > n -> Z.succ m > Z.succ n *) + Zgt_succ (* Z.succ n > n *) + Zorder.Zgt_pos_0 (* Z.pos p > 0 *) + Zplus_gt_compat_l (* n > m -> p+n > p+m *) + Zplus_gt_compat_r (* n > m -> n+p > m+p *) + + (** Lemmas ending by Z.lt *) + Pos2Z.is_pos (* 0 < Z.pos p *) + Z.lt_succ_diag_r (* n < Z.succ n *) + Zsucc_lt_compat (* n < m -> Z.succ n < Z.succ m *) + Z.lt_pred_l (* Z.pred n < n *) + Zplus_lt_compat_l (* n < m -> p+n < p+m *) + Zplus_lt_compat_r (* n < m -> n+p < m+p *) + + (** Lemmas ending by Z.le *) + Nat2Z.is_nonneg (* 0 <= Z.of_nat n *) + Pos2Z.is_nonneg (* 0 <= Z.pos p *) + Z.le_refl (* n <= n *) + Z.le_succ_diag_r (* n <= Z.succ n *) + Zsucc_le_compat (* m <= n -> Z.succ m <= Z.succ n *) + Z.le_pred_l (* Z.pred n <= n *) + Z.le_min_l (* Z.min n m <= n *) + Z.le_min_r (* Z.min n m <= m *) + Zplus_le_compat_l (* n <= m -> p+n <= p+m *) + Zplus_le_compat_r (* a <= b -> a+c <= b+c *) + Z.abs_nonneg (* 0 <= |x| *) (** ** Irreversible simplification lemmas *) (** Probably to be declared as hints, when no other simplification is possible *) (** Lemmas ending by eq *) - BinInt.Z_eq_mult (* :(x,y:Z)`y = 0`->`y*x = 0` *) - Zplus_eq_compat (* :(n,m,p,q:Z)`n = m`->`p = q`->`n+p = m+q` *) + Z_eq_mult (* y = 0 -> y*x = 0 *) + Zplus_eq_compat (* n = m -> p = q -> n+p = m+q *) - (** Lemmas ending by Zge *) - Zorder.Zmult_ge_compat_r (* :(a,b,c:Z)`a >= b`->`c >= 0`->`a*c >= b*c` *) - Zorder.Zmult_ge_compat_l (* :(a,b,c:Z)`a >= b`->`c >= 0`->`c*a >= c*b` *) + (** Lemmas ending by Z.ge *) + Zorder.Zmult_ge_compat_r (* a >= b -> c >= 0 -> a*c >= b*c *) + Zorder.Zmult_ge_compat_l (* a >= b -> c >= 0 -> c*a >= c*b *) Zorder.Zmult_ge_compat (* : - (a,b,c,d:Z)`a >= c`->`b >= d`->`c >= 0`->`d >= 0`->`a*b >= c*d` *) - - (** Lemmas ending by Zlt *) - Zorder.Zmult_gt_0_compat (* :(a,b:Z)`a > 0`->`b > 0`->`a*b > 0` *) - Zlt_lt_succ (* :(n,m:Z)`n < m`->`n < (Zs m)` *) - - (** Lemmas ending by Zle *) - Zorder.Zmult_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x*y` *) - Zorder.Zmult_le_compat_r (* :(a,b,c:Z)`a <= b`->`0 <= c`->`a*c <= b*c` *) - Zorder.Zmult_le_compat_l (* :(a,b,c:Z)`a <= b`->`0 <= c`->`c*a <= c*b` *) - Zplus_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x+y` *) - Zle_le_succ (* :(x,y:Z)`x <= y`->`x <= (Zs y)` *) - Zplus_le_compat (* :(n,m,p,q:Z)`n <= m`->`p <= q`->`n+p <= m+q` *) + a >= c -> b >= d -> c >= 0 -> d >= 0 -> a*b >= c*d *) + + (** Lemmas ending by Z.lt *) + Zorder.Zmult_gt_0_compat (* a > 0 -> b > 0 -> a*b > 0 *) + Z.lt_lt_succ_r (* n < m -> n < Z.succ m *) + + (** Lemmas ending by Z.le *) + Z.mul_nonneg_nonneg (* 0 <= x -> 0 <= y -> 0 <= x*y *) + Zorder.Zmult_le_compat_r (* a <= b -> 0 <= c -> a*c <= b*c *) + Zorder.Zmult_le_compat_l (* a <= b -> 0 <= c -> c*a <= c*b *) + Z.add_nonneg_nonneg (* 0 <= x -> 0 <= y -> 0 <= x+y *) + Z.le_le_succ_r (* x <= y -> x <= Z.succ y *) + Z.add_le_mono (* n <= m -> p <= q -> n+p <= m+q *) : zarith. diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 30948ca7a..3711ea021 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -34,22 +34,22 @@ Section Log_pos. (* Log of positive integers *) Fixpoint log_inf (p:positive) : Z := match p with | xH => 0 (* 1 *) - | xO q => Zsucc (log_inf q) (* 2n *) - | xI q => Zsucc (log_inf q) (* 2n+1 *) + | xO q => Z.succ (log_inf q) (* 2n *) + | xI q => Z.succ (log_inf q) (* 2n+1 *) end. Fixpoint log_sup (p:positive) : Z := match p with | xH => 0 (* 1 *) - | xO n => Zsucc (log_sup n) (* 2n *) - | xI n => Zsucc (Zsucc (log_inf n)) (* 2n+1 *) + | xO n => Z.succ (log_sup n) (* 2n *) + | xI n => Z.succ (Z.succ (log_inf n)) (* 2n+1 *) end. Hint Unfold log_inf log_sup. Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p). Proof. - induction p; simpl; now rewrite <- ?Z.succ_Zpos, ?IHp. + induction p; simpl; now rewrite ?Pos2Z.inj_succ, ?IHp. Qed. Lemma Zlog2_log_inf : forall p, Z.log2 (Zpos p) = log_inf p. @@ -71,24 +71,24 @@ Section Log_pos. (* Log of positive integers *) (** Then we give the specifications of [log_inf] and [log_sup] and prove their validity *) - Hint Resolve Zle_trans: zarith. + Hint Resolve Z.le_trans: zarith. Theorem log_inf_correct : forall x:positive, - 0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Zsucc (log_inf x)). + 0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Z.succ (log_inf x)). Proof. simple induction x; intros; simpl in |- *; [ elim H; intros Hp HR; clear H; split; [ auto with zarith - | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial); rewrite two_p_S by trivial; - rewrite two_p_S in HR by trivial; rewrite (BinInt.Zpos_xI p); + rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xI p); omega ] | elim H; intros Hp HR; clear H; split; [ auto with zarith - | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial); rewrite two_p_S by trivial; - rewrite two_p_S in HR by trivial; rewrite (BinInt.Zpos_xO p); + rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xO p); omega ] | unfold two_power_pos in |- *; unfold shift_pos in |- *; simpl in |- *; omega ]. @@ -112,12 +112,12 @@ Section Log_pos. (* Log of positive integers *) Theorem log_sup_log_inf : forall p:positive, IF Zpos p = two_p (log_inf p) then Zpos p = two_p (log_sup p) - else log_sup p = Zsucc (log_inf p). + else log_sup p = Z.succ (log_inf p). Proof. simple induction p; intros; [ elim H; right; simpl in |- *; rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite BinInt.Zpos_xI; unfold Zsucc in |- *; omega + rewrite BinInt.Pos2Z.inj_xI; unfold Z.succ; omega | elim H; clear H; intro Hif; [ left; simpl in |- *; rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); @@ -126,21 +126,21 @@ Section Log_pos. (* Log of positive integers *) auto | right; simpl in |- *; rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite BinInt.Zpos_xO; unfold Zsucc in |- *; + rewrite BinInt.Pos2Z.inj_xO; unfold Z.succ; omega ] | left; auto ]. Qed. Theorem log_sup_correct2 : - forall x:positive, two_p (Zpred (log_sup x)) < Zpos x <= two_p (log_sup x). + forall x:positive, two_p (Z.pred (log_sup x)) < Zpos x <= two_p (log_sup x). Proof. intro. elim (log_sup_log_inf x). (* x is a power of two and [log_sup = log_inf] *) intros [E1 E2]; rewrite E2. - split; [ apply two_p_pred; apply log_sup_correct1 | apply Zle_refl ]. + split; [ apply two_p_pred; apply log_sup_correct1 | apply Z.le_refl ]. intros [E1 E2]; rewrite E2. - rewrite <- (Zpred_succ (log_inf x)). + rewrite (Z.pred_succ (log_inf x)). generalize (log_inf_correct2 x); omega. Qed. @@ -149,7 +149,7 @@ Section Log_pos. (* Log of positive integers *) simple induction p; simpl in |- *; intros; omega. Qed. - Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Zsucc (log_inf p). + Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Z.succ (log_inf p). Proof. simple induction p; simpl in |- *; intros; omega. Qed. @@ -161,8 +161,8 @@ Section Log_pos. (* Log of positive integers *) | xH => 0 | xO xH => 1 | xI xH => 2 - | xO y => Zsucc (log_near y) - | xI y => Zsucc (log_near y) + | xO y => Z.succ (log_near y) + | xI y => Z.succ (log_near y) end. Theorem log_near_correct1 : forall p:positive, 0 <= log_near p. @@ -171,12 +171,10 @@ Section Log_pos. (* Log of positive integers *) [ elim p0; auto with zarith | elim p0; auto with zarith | trivial with zarith ]. - intros; apply Zle_le_succ. - generalize H0; elim p1; intros; simpl in |- *; - [ assumption | assumption | apply Zorder.Zle_0_pos ]. - intros; apply Zle_le_succ. - generalize H0; elim p1; intros; simpl in |- *; - [ assumption | assumption | apply Zorder.Zle_0_pos ]. + intros; apply Z.le_le_succ_r. + generalize H0; now elim p1. + intros; apply Z.le_le_succ_r. + generalize H0; now elim p1. Qed. Theorem log_near_correct2 : @@ -219,19 +217,19 @@ Section divers. Lemma ZERO_le_N_digits : forall x:Z, 0 <= N_digits x. Proof. simple induction x; simpl in |- *; - [ apply Zle_refl | exact log_inf_correct1 | exact log_inf_correct1 ]. + [ apply Z.le_refl | exact log_inf_correct1 | exact log_inf_correct1 ]. Qed. - Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z_of_nat n. + Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z.of_nat n. Proof. simple induction n; intros; - [ try trivial | rewrite Znat.inj_S; rewrite <- H; reflexivity ]. + [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ]. Qed. - Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z_of_nat n. + Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z.of_nat n. Proof. simple induction n; intros; - [ try trivial | rewrite Znat.inj_S; rewrite <- H; reflexivity ]. + [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ]. Qed. (** [Is_power p] means that p is a power of two *) diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index a3eeb4160..86e26a605 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -12,12 +12,38 @@ Require Export BinInt Zcompare Zorder. Local Open Scope Z_scope. -(** Definition [Zmax] is now [BinInt.Z.max]. *) - -(** * Characterization of maximum on binary integer numbers *) +(** Definition [Z.max] is now [BinInt.Z.max]. *) + +(** Exact compatibility *) + +Notation Zmax_case := Z.max_case (compat "8.3"). +Notation Zmax_case_strong := Z.max_case_strong (compat "8.3"). +Notation Zmax_right := Z.max_r (compat "8.3"). +Notation Zle_max_l := Z.le_max_l (compat "8.3"). +Notation Zle_max_r := Z.le_max_r (compat "8.3"). +Notation Zmax_lub := Z.max_lub (compat "8.3"). +Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.3"). +Notation Zle_max_compat_r := Z.max_le_compat_r (compat "8.3"). +Notation Zle_max_compat_l := Z.max_le_compat_l (compat "8.3"). +Notation Zmax_idempotent := Z.max_id (compat "8.3"). +Notation Zmax_n_n := Z.max_id (compat "8.3"). +Notation Zmax_comm := Z.max_comm (compat "8.3"). +Notation Zmax_assoc := Z.max_assoc (compat "8.3"). +Notation Zmax_irreducible_dec := Z.max_dec (compat "8.3"). +Notation Zmax_le_prime := Z.max_le (compat "8.3"). +Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.3"). +Notation Zmax_SS := Z.succ_max_distr (compat "8.3"). +Notation Zplus_max_distr_l := Z.add_max_distr_l (compat "8.3"). +Notation Zplus_max_distr_r := Z.add_max_distr_r (compat "8.3"). +Notation Zmax_plus := Z.add_max_distr_r (compat "8.3"). +Notation Zmax1 := Z.le_max_l (compat "8.3"). +Notation Zmax2 := Z.le_max_r (compat "8.3"). +Notation Zmax_irreducible_inf := Z.max_dec (compat "8.3"). +Notation Zmax_le_prime_inf := Z.max_le (compat "8.3"). +Notation Zpos_max := Pos2Z.inj_max (compat "8.3"). +Notation Zpos_minus := Pos2Z.inj_sub_max (compat "8.3"). -Definition Zmax_case := Z.max_case. -Definition Zmax_case_strong := Z.max_case_strong. +(** Slightly different lemmas *) Lemma Zmax_spec x y : x >= y /\ Z.max x y = x \/ x < y /\ Z.max x y = y. @@ -26,86 +52,9 @@ Proof. Qed. Lemma Zmax_left n m : n>=m -> Z.max n m = n. -Proof. Z.swap_greater. apply Zmax_l. Qed. - -Lemma Zmax_right : forall n m, n<=m -> Z.max n m = m. Proof Zmax_r. - -(** * Least upper bound properties of max *) - -Lemma Zle_max_l : forall n m, n <= Z.max n m. Proof Z.le_max_l. -Lemma Zle_max_r : forall n m, m <= Z.max n m. Proof Z.le_max_r. - -Lemma Zmax_lub : forall n m p, n <= p -> m <= p -> Z.max n m <= p. -Proof Z.max_lub. - -Lemma Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Z.max n m < p. -Proof Z.max_lub_lt. - - -(** * Compatibility with order *) - -Lemma Zle_max_compat_r : forall n m p, n <= m -> Z.max n p <= Z.max m p. -Proof Z.max_le_compat_r. - -Lemma Zle_max_compat_l : forall n m p, n <= m -> Z.max p n <= Z.max p m. -Proof Z.max_le_compat_l. - - -(** * Semi-lattice properties of max *) - -Lemma Zmax_idempotent : forall n, Z.max n n = n. Proof Z.max_id. -Lemma Zmax_comm : forall n m, Z.max n m = Z.max m n. Proof Z.max_comm. -Lemma Zmax_assoc : forall n m p, Z.max n (Z.max m p) = Z.max (Z.max n m) p. -Proof Z.max_assoc. - -(** * Additional properties of max *) - -Lemma Zmax_irreducible_dec : forall n m, {Z.max n m = n} + {Z.max n m = m}. -Proof Z.max_dec. +Proof. Z.swap_greater. apply Z.max_l. Qed. -Lemma Zmax_le_prime : forall n m p, p <= Z.max n m -> p <= n \/ p <= m. -Proof Z.max_le. - - -(** * Operations preserving max *) - -Lemma Zsucc_max_distr : - forall n m, Z.succ (Z.max n m) = Z.max (Z.succ n) (Z.succ m). -Proof Z.succ_max_distr. - -Lemma Zplus_max_distr_l : forall n m p, Z.max (p + n) (p + m) = p + Z.max n m. -Proof Z.add_max_distr_l. - -Lemma Zplus_max_distr_r : forall n m p, Z.max (n + p) (m + p) = Z.max n m + p. -Proof Z.add_max_distr_r. - -(** * Maximum and Zpos *) - -Lemma Zpos_max p q : Zpos (Pos.max p q) = Z.max (Zpos p) (Zpos q). -Proof. - unfold Zmax, Pmax. simpl. - case Pos.compare_spec; auto; congruence. -Qed. - -Lemma Zpos_max_1 p : Z.max 1 (Zpos p) = Zpos p. +Lemma Zpos_max_1 p : Z.max 1 (Z.pos p) = Z.pos p. Proof. now destruct p. Qed. - -(** * Characterization of Pos.sub in term of Z.sub and Z.max *) - -Lemma Zpos_minus p q : Zpos (p - q) = Z.max 1 (Zpos p - Zpos q). -Proof. - simpl. rewrite Z.pos_sub_spec. case Pos.compare_spec; intros H. - subst; now rewrite Pos.sub_diag. - now rewrite Pos.sub_lt. - symmetry. apply Zpos_max_1. -Qed. - -(* begin hide *) -(* Compatibility *) -Notation Zmax1 := Z.le_max_l (compat "8.3"). -Notation Zmax2 := Z.le_max_r (compat "8.3"). -Notation Zmax_irreducible_inf := Z.max_dec (compat "8.3"). -Notation Zmax_le_prime_inf := Z.max_le (compat "8.3"). -(* end hide *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index fbb31632c..d0b29f31f 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -12,12 +12,30 @@ Require Import BinInt Zcompare Zorder. Local Open Scope Z_scope. -(** Definition [Zmin] is now [BinInt.Z.min]. *) - -(** * Characterization of the minimum on binary integer numbers *) +(** Definition [Z.min] is now [BinInt.Z.min]. *) + +(** Exact compatibility *) + +Notation Zmin_case := Z.min_case (compat "8.3"). +Notation Zmin_case_strong := Z.min_case_strong (compat "8.3"). +Notation Zle_min_l := Z.le_min_l (compat "8.3"). +Notation Zle_min_r := Z.le_min_r (compat "8.3"). +Notation Zmin_glb := Z.min_glb (compat "8.3"). +Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.3"). +Notation Zle_min_compat_r := Z.min_le_compat_r (compat "8.3"). +Notation Zle_min_compat_l := Z.min_le_compat_l (compat "8.3"). +Notation Zmin_idempotent := Z.min_id (compat "8.3"). +Notation Zmin_n_n := Z.min_id (compat "8.3"). +Notation Zmin_comm := Z.min_comm (compat "8.3"). +Notation Zmin_assoc := Z.min_assoc (compat "8.3"). +Notation Zmin_irreducible_inf := Z.min_dec (compat "8.3"). +Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.3"). +Notation Zmin_SS := Z.succ_min_distr (compat "8.3"). +Notation Zplus_min_distr_r := Z.add_min_distr_r (compat "8.3"). +Notation Zmin_plus := Z.add_min_distr_r (compat "8.3"). +Notation Zpos_min := Pos2Z.inj_min (compat "8.3"). -Definition Zmin_case := Z.min_case. -Definition Zmin_case_strong := Z.min_case_strong. +(** Slightly different lemmas *) Lemma Zmin_spec x y : x <= y /\ Z.min x y = x \/ x > y /\ Z.min x y = y. @@ -25,71 +43,15 @@ Proof. Z.swap_greater. rewrite Z.min_comm. destruct (Z.min_spec y x); auto. Qed. -(** * Greatest lower bound properties of min *) - -Lemma Zle_min_l : forall n m, Z.min n m <= n. Proof Z.le_min_l. -Lemma Zle_min_r : forall n m, Z.min n m <= m. Proof Z.le_min_r. - -Lemma Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Z.min n m. -Proof Z.min_glb. -Lemma Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Z.min n m. -Proof Z.min_glb_lt. - -(** * Compatibility with order *) - -Lemma Zle_min_compat_r : forall n m p, n <= m -> Z.min n p <= Z.min m p. -Proof Z.min_le_compat_r. -Lemma Zle_min_compat_l : forall n m p, n <= m -> Z.min p n <= Z.min p m. -Proof Z.min_le_compat_l. - -(** * Semi-lattice properties of min *) - -Lemma Zmin_idempotent : forall n, Z.min n n = n. Proof Z.min_id. -Notation Zmin_n_n := Z.min_id (compat "8.3"). -Lemma Zmin_comm : forall n m, Z.min n m = Z.min m n. Proof Z.min_comm. -Lemma Zmin_assoc : forall n m p, Z.min n (Z.min m p) = Z.min (Z.min n m) p. -Proof Z.min_assoc. - -(** * Additional properties of min *) - -Lemma Zmin_irreducible_inf : forall n m, {Z.min n m = n} + {Z.min n m = m}. -Proof Z.min_dec. - Lemma Zmin_irreducible n m : Z.min n m = n \/ Z.min n m = m. Proof. destruct (Z.min_dec n m); auto. Qed. -Notation Zmin_or := Zmin_irreducible (only parsing). +Notation Zmin_or := Zmin_irreducible (compat "8.3"). Lemma Zmin_le_prime_inf n m p : Z.min n m <= p -> {n <= p} + {m <= p}. -Proof. apply Zmin_case; auto. Qed. - -(** * Operations preserving min *) - -Lemma Zsucc_min_distr : - forall n m, Z.succ (Z.min n m) = Z.min (Z.succ n) (Z.succ m). -Proof Z.succ_min_distr. - -Notation Zmin_SS := Z.succ_min_distr (only parsing). - -Lemma Zplus_min_distr_r : - forall n m p, Z.min (n + p) (m + p) = Z.min n m + p. -Proof Z.add_min_distr_r. - -Notation Zmin_plus := Z.add_min_distr_r (only parsing). - -(** * Minimum and Zpos *) - -Lemma Zpos_min p q : Zpos (Pos.min p q) = Z.min (Zpos p) (Zpos q). -Proof. - unfold Z.min, Pos.min; simpl. destruct Pos.compare; auto. -Qed. +Proof. apply Z.min_case; auto. Qed. Lemma Zpos_min_1 p : Z.min 1 (Zpos p) = 1. Proof. now destruct p. Qed. - - - - - diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index a6da9d7e7..bfd57d758 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -21,8 +21,9 @@ Open Local Scope Z_scope. Notation iter := @Z.iter (compat "8.3"). Lemma iter_nat_of_Z : forall n A f x, 0 <= n -> - iter n A f x = iter_nat (Z.abs_nat n) A f x. + Z.iter n f x = iter_nat (Z.abs_nat n) A f x. +Proof. intros n A f x; case n; auto. -intros p _; unfold Z.iter, Z.abs_nat; apply iter_nat_of_P. +intros p _; unfold Z.iter, Z.abs_nat; apply Pos2Nat.inj_iter. intros p abs; case abs; trivial. Qed. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 2c3288f6c..7cb2b7060 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -14,6 +14,18 @@ Require Import BinPos BinInt BinNat Pnat Nnat. Local Open Scope Z_scope. +(** Conversions between integers and natural numbers + + Seven sections: + - chains of conversions (combining two conversions) + - module N2Z : from N to Z + - module Z2N : from Z to N (negative numbers rounded to 0) + - module Zabs2N : from Z to N (via the absolute value) + - module Nat2Z : from nat to Z + - module Z2Nat : from Z to nat (negative numbers rounded to 0) + - module Zabs2Nat : from Z to nat (via the absolute value) +*) + (** * Chains of conversions *) (** When combining successive conversions, we have the following @@ -254,9 +266,13 @@ Qed. Lemma inj_pow n m : Z.of_N (n^m) = (Z.of_N n)^(Z.of_N m). Proof. - symmetry. destruct n, m; trivial. now apply Z.pow_0_l. apply Z.pow_Zpos. + destruct n, m; trivial. now rewrite Z.pow_0_l. apply Pos2Z.inj_pow. Qed. +Lemma inj_testbit a n : + Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n. +Proof. apply Z.Private_BootStrap.testbit_of_N. Qed. + End N2Z. Module Z2N. @@ -408,6 +424,10 @@ Proof. - now destruct 2. Qed. +Lemma inj_testbit a n : 0<=n -> + Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n). +Proof. apply Z.Private_BootStrap.testbit_of_N'. Qed. + End Z2N. Module Zabs2N. @@ -526,9 +546,9 @@ Proof. intros. rewrite abs_N_nonneg. now apply Z2N.inj_quot. now apply Z.quot_pos. destruct n, m; trivial; simpl. - trivial. - - now rewrite <- Z.opp_Zpos, Z.quot_opp_r, inj_opp. - - now rewrite <- Z.opp_Zpos, Z.quot_opp_l, inj_opp. - - now rewrite <- 2 Z.opp_Zpos, Z.quot_opp_opp. + - now rewrite <- Pos2Z.opp_pos, Z.quot_opp_r, inj_opp. + - now rewrite <- Pos2Z.opp_pos, Z.quot_opp_l, inj_opp. + - now rewrite <- 2 Pos2Z.opp_pos, Z.quot_opp_opp. Qed. Lemma inj_rem n m : Z.abs_N (Z.rem n m) = ((Z.abs_N n) mod (Z.abs_N m))%N. @@ -538,9 +558,9 @@ Proof. intros. rewrite abs_N_nonneg. now apply Z2N.inj_rem. now apply Z.rem_nonneg. destruct n, m; trivial; simpl. - trivial. - - now rewrite <- Z.opp_Zpos, Z.rem_opp_r. - - now rewrite <- Z.opp_Zpos, Z.rem_opp_l, inj_opp. - - now rewrite <- 2 Z.opp_Zpos, Z.rem_opp_opp, inj_opp. + - now rewrite <- Pos2Z.opp_pos, Z.rem_opp_r. + - now rewrite <- Pos2Z.opp_pos, Z.rem_opp_l, inj_opp. + - now rewrite <- 2 Pos2Z.opp_pos, Z.rem_opp_opp, inj_opp. Qed. Lemma inj_pow n m : 0<=m -> Z.abs_N (n^m) = ((Z.abs_N n)^(Z.abs_N m))%N. @@ -584,7 +604,7 @@ Qed. Lemma inj_succ n : Z.of_nat (S n) = Z.succ (Z.of_nat n). Proof. - destruct n. trivial. simpl. symmetry. apply Z.succ_Zpos. + destruct n. trivial. simpl. apply Pos2Z.inj_succ. Qed. (** [Z.of_N] produce non-negative integers *) @@ -915,10 +935,10 @@ End Zabs2Nat. Definition neq (x y:nat) := x <> y. -Lemma inj_neq n m : neq n m -> Zne (Z_of_nat n) (Z_of_nat m). +Lemma inj_neq n m : neq n m -> Zne (Z.of_nat n) (Z.of_nat m). Proof. intros H H'. now apply H, Nat2Z.inj. Qed. -Lemma Zpos_P_of_succ_nat n : Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n). +Lemma Zpos_P_of_succ_nat n : Zpos (Pos.of_succ_nat n) = Z.succ (Z.of_nat n). Proof (Nat2Z.inj_succ n). (** For these one, used in omega, a Definition is necessary *) @@ -953,7 +973,7 @@ Notation inj_max := Nat2Z.inj_max (compat "8.3"). Notation Z_of_nat_of_P := positive_nat_Z (compat "8.3"). Notation Zpos_eq_Z_of_nat_o_nat_of_P := - (fun p => sym_eq (positive_nat_Z p)) (compat "8.3"). + (fun p => eq_sym (positive_nat_Z p)) (compat "8.3"). Notation Z_of_nat_of_N := N_nat_Z (compat "8.3"). Notation Z_of_N_of_nat := nat_N_Z (compat "8.3"). @@ -991,7 +1011,7 @@ Notation Zabs_N_plus := Zabs2N.inj_add (compat "8.3"). Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (compat "8.3"). Notation Zabs_N_mult := Zabs2N.inj_mul (compat "8.3"). -Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0. +Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0. Proof. intros. rewrite not_le_minus_0; auto with arith. Qed. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 00019b1a3..33f4dc7f4 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -17,7 +17,7 @@ Require Import Wf_nat. Open Scope Z_scope. (** This file contains some notions of number theory upon Z numbers: - - a divisibility predicate [Zdivide] + - a divisibility predicate [Z.divide] - a gcd predicate [gcd] - Euclid algorithm [euclid] - a relatively prime predicate [rel_prime] @@ -35,7 +35,7 @@ Notation Zgcd_greatest := Z.gcd_greatest (compat "8.3"). Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.3"). Notation Zggcd_opp := Z.ggcd_opp (compat "8.3"). -(** The former specialized inductive predicate [Zdivide] is now +(** The former specialized inductive predicate [Z.divide] is now a generic existential predicate. *) Notation Zdivide := Z.divide (compat "8.3"). @@ -76,11 +76,11 @@ Proof. apply Z.divide_abs_l. Qed. Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b). Proof. apply Z.divide_abs_l. Qed. -Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith. -Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r: zarith. -Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l - Zdivide_opp_l_rev Zdivide_minus_l Zdivide_mult_l Zdivide_mult_r - Zdivide_factor_r Zdivide_factor_l: zarith. +Hint Resolve Z.divide_refl Z.divide_1_l Z.divide_0_r: zarith. +Hint Resolve Z.mul_divide_mono_l Z.mul_divide_mono_r: zarith. +Hint Resolve Z.divide_add_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l + Zdivide_opp_l_rev Z.divide_sub_r Z.divide_mul_l Z.divide_mul_r + Z.divide_factor_l Z.divide_factor_r: zarith. (** Auxiliary result. *) @@ -108,7 +108,7 @@ Proof. now apply Z.divide_pos_le. Qed. -(** [Zdivide] can be expressed using [Zmod]. *) +(** [Z.divide] can be expressed using [Z.modulo]. *) Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a). Proof. @@ -120,7 +120,7 @@ Proof. intros a b (c,->); apply Z_mod_mult. Qed. -(** [Zdivide] is hence decidable *) +(** [Z.divide] is hence decidable *) Lemma Zdivide_dec a b : {(a | b)} + {~ (a | b)}. Proof. @@ -193,14 +193,16 @@ Qed. (** * Greatest common divisor (gcd). *) -(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] - expressing that [d] is a gcd of [a] and [b]. - (We show later that the [gcd] is actually unique if we discard its sign.) *) +(** There is no unicity of the gcd; hence we define the predicate + [Zis_gcd a b g] expressing that [g] is a gcd of [a] and [b]. + (We show later that the [gcd] is actually unique if we discard its sign.) *) -Inductive Zis_gcd (a b d:Z) : Prop := - Zis_gcd_intro : - (d | a) -> - (d | b) -> (forall x:Z, (x | a) -> (x | b) -> (x | d)) -> Zis_gcd a b d. +Inductive Zis_gcd (a b g:Z) : Prop := + Zis_gcd_intro : + (g | a) -> + (g | b) -> + (forall x, (x | a) -> (x | b) -> (x | g)) -> + Zis_gcd a b g. (** Trivial properties of [gcd] *) @@ -246,12 +248,10 @@ Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. Theorem Zis_gcd_unique: forall a b c d : Z, Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = (- d). Proof. -intros a b c d H1 H2. -inversion_clear H1 as [Hc1 Hc2 Hc3]. -inversion_clear H2 as [Hd1 Hd2 Hd3]. -assert (H3: Zdivide c d); auto. -assert (H4: Zdivide d c); auto. -apply Zdivide_antisym; auto. +intros a b c d [Hc1 Hc2 Hc3] [Hd1 Hd2 Hd3]. +assert (c|d) by auto. +assert (d|c) by auto. +apply Z.divide_antisym; auto. Qed. @@ -357,7 +357,7 @@ Proof. intros H1 H2 H3; simple induction 1; intros. generalize (H3 d' H4 H5); intro Hd'd. generalize (H6 d H1 H2); intro Hdd'. - exact (Zdivide_antisym d d' Hdd' Hd'd). + exact (Z.divide_antisym d d' Hdd' Hd'd). Qed. (** * Bezout's coefficients *) @@ -450,18 +450,18 @@ Lemma rel_prime_cross_prod : rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d. Proof. intros a b c d; intros. - elim (Zdivide_antisym b d). + elim (Z.divide_antisym b d). split; auto with zarith. rewrite H4 in H3. - rewrite Zmult_comm in H3. - apply Zmult_reg_l with d; auto with zarith. + rewrite Z.mul_comm in H3. + apply Z.mul_reg_l with d; auto with zarith. intros; omega. apply Gauss with a. rewrite H3. auto with zarith. red in |- *; auto with zarith. apply Gauss with c. - rewrite Zmult_comm. + rewrite Z.mul_comm. rewrite <- H3. auto with zarith. red in |- *; auto with zarith. @@ -492,12 +492,12 @@ Proof. exists b'; auto with zarith. intros x (xa,H5) (xb,H6). destruct (H4 (x*g)) as (x',Hx'). - exists xa; rewrite Zmult_assoc; rewrite <- H5; auto. - exists xb; rewrite Zmult_assoc; rewrite <- H6; auto. + exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto. + exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto. replace g with (1*g) in Hx'; auto with zarith. - do 2 rewrite Zmult_assoc in Hx'. - apply Zmult_reg_r in Hx'; trivial. - rewrite Zmult_1_r in Hx'. + do 2 rewrite Z.mul_assoc in Hx'. + apply Z.mul_reg_r in Hx'; trivial. + rewrite Z.mul_1_r in Hx'. exists x'; auto with zarith. Qed. @@ -512,9 +512,9 @@ Theorem rel_prime_div: forall p q r, Proof. intros p q r H (u, H1); subst. inversion_clear H as [H1 H2 H3]. - red; apply Zis_gcd_intro; try apply Zone_divide. + red; apply Zis_gcd_intro; try apply Z.divide_1_l. intros x H4 H5; apply H3; auto. - apply Zdivide_mult_r; auto. + apply Z.divide_mul_r; auto. Qed. Theorem rel_prime_1: forall n, rel_prime 1 n. @@ -578,10 +578,10 @@ Proof. destruct 1; intros. assert (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). - { assert (Zabs a <= Zabs p) as H2. + { assert (Z.abs a <= Z.abs p) as H2. apply Zdivide_bounds; [ assumption | omega ]. revert H2. - pattern (Zabs a); apply Zabs_ind; pattern (Zabs p); apply Zabs_ind; + pattern (Z.abs a); apply Zabs_ind; pattern (Z.abs p); apply Zabs_ind; intros; omega. } intuition idtac. (* -p < a < -1 *) @@ -589,7 +589,7 @@ Proof. inversion H2. assert (- a | - a) by auto with zarith. assert (- a | p) by auto with zarith. - apply H7, Zdivide_1 in H8; intuition. + apply H7, Z.divide_1_r in H8; intuition. (* a = 0 *) - inversion H1. subst a; omega. (* 1 < a < p *) @@ -597,7 +597,7 @@ Proof. inversion H2. assert (a | a) by auto with zarith. assert (a | p) by auto with zarith. - apply H7, Zdivide_1 in H8; intuition. + apply H7, Z.divide_1_r in H8; intuition. Qed. (** A prime number is relatively prime with any number it does not divide *) @@ -621,7 +621,7 @@ Proof. intros a p Hp [H1 H2]. apply rel_prime_sym; apply prime_rel_prime; auto. intros [q Hq]; subst a. - case (Zle_or_lt q 0); intros Hl. + case (Z.le_gt_cases q 0); intros Hl. absurd (q * p <= 0 * p); auto with zarith. absurd (1 * p <= q * p); auto with zarith. Qed. @@ -651,87 +651,79 @@ Qed. Lemma prime_2: prime 2. Proof. apply prime_intro; auto with zarith. - intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith; - clear H1; intros H1. - contradict H2; auto with zarith. - subst n; red; auto with zarith. - apply Zis_gcd_intro; auto with zarith. + intros n (H,H'); Z.le_elim H; auto with zarith. + - contradict H'; auto with zarith. + - subst n. constructor; auto with zarith. Qed. Theorem prime_3: prime 3. Proof. apply prime_intro; auto with zarith. - intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith; - clear H1; intros H1. - case (Zle_lt_or_eq 2 n); auto with zarith; clear H1; intros H1. - contradict H2; auto with zarith. - subst n; red; auto with zarith. - apply Zis_gcd_intro; auto with zarith. - intros x [q1 Hq1] [q2 Hq2]. - exists (q2 - q1). - apply trans_equal with (3 - 2); auto with zarith. - rewrite Hq1; rewrite Hq2; ring. - subst n; red; auto with zarith. - apply Zis_gcd_intro; auto with zarith. + intros n (H,H'); Z.le_elim H; auto with zarith. + - replace n with 2 by omega. + constructor; auto with zarith. + intros x (q,Hq) (q',Hq'). + exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'. + - replace n with 1 by trivial. + constructor; auto with zarith. Qed. -Theorem prime_ge_2: forall p, prime p -> 2 <= p. +Theorem prime_ge_2 p : prime p -> 2 <= p. Proof. - intros p Hp; inversion Hp; auto with zarith. + intros (Hp,_); auto with zarith. Qed. Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)). -Theorem prime_alt: - forall p, prime' p <-> prime p. -Proof. - split; destruct 1; intros. - (* prime -> prime' *) - constructor; auto; intros. - red; apply Zis_gcd_intro; auto with zarith; intros. - case (Zle_lt_or_eq 0 (Zabs x)); auto with zarith; intros H6. - case (Zle_lt_or_eq 1 (Zabs x)); auto with zarith; intros H7. - case (Zle_lt_or_eq (Zabs x) p); auto with zarith. - apply Zdivide_le; auto with zarith. - apply Zdivide_Zabs_inv_l; auto. - intros H8; case (H0 (Zabs x)); auto. - apply Zdivide_Zabs_inv_l; auto. - intros H8; subst p; absurd (Zabs x <= n); auto with zarith. - apply Zdivide_le; auto with zarith. - apply Zdivide_Zabs_inv_l; auto. - rewrite H7; pattern (Zabs x); apply Zabs_intro; auto with zarith. - absurd (0%Z = p); auto with zarith. - assert (x=0) by (destruct x; simpl in *; now auto). - subst x; elim H3; intro q; rewrite Zmult_0_r; auto. - (* prime' -> prime *) - split; auto; intros. - intros H2. - case (Zis_gcd_unique n p n 1); auto with zarith. - apply Zis_gcd_intro; auto with zarith. - apply H0; auto with zarith. +Lemma Z_0_1_more x : 0<=x -> x=0 \/ x=1 \/ 1<x. +Proof. + intros H. Z.le_elim H; auto. + apply Z.le_succ_l in H. change (1 <= x) in H. Z.le_elim H; auto. +Qed. + +Theorem prime_alt p : prime' p <-> prime p. +Proof. + split; intros (Hp,H). + - (* prime -> prime' *) + constructor; trivial; intros n Hn. + constructor; auto with zarith; intros x Hxn Hxp. + rewrite <- Z.divide_abs_l in Hxn, Hxp |- *. + assert (Hx := Z.abs_nonneg x). + set (y:=Z.abs x) in *; clearbody y; clear x; rename y into x. + destruct (Z_0_1_more x Hx) as [->|[->|Hx']]. + + exfalso. apply Z.divide_0_l in Hxn. omega. + + now exists 1. + + elim (H x); auto. + split; trivial. + apply Z.le_lt_trans with n; auto with zarith. + apply Z.divide_pos_le; auto with zarith. + - (* prime' -> prime *) + constructor; trivial. intros n Hn Hnp. + case (Zis_gcd_unique n p n 1); auto with zarith. + constructor; auto with zarith. + apply H; auto with zarith. Qed. Theorem square_not_prime: forall a, ~ prime (a * a). Proof. intros a Ha. - rewrite <- (Zabs_square a) in Ha. - assert (0 <= Zabs a) by auto with zarith. - set (b:=Zabs a) in *; clearbody b. - rewrite <- prime_alt in Ha; destruct Ha. - case (Zle_lt_or_eq 0 b); auto with zarith; intros Hza1; [ | subst; omega]. - case (Zle_lt_or_eq 1 b); auto with zarith; intros Hza2; [ | subst; omega]. - assert (Hza3 := Zmult_lt_compat_r 1 b b Hza1 Hza2). - rewrite Zmult_1_l in Hza3. - elim (H1 _ (conj Hza2 Hza3)). - exists b; auto. + rewrite <- (Z.abs_square a) in Ha. + assert (H:=Z.abs_nonneg a). + set (b:=Z.abs a) in *; clearbody b; clear a; rename b into a. + rewrite <- prime_alt in Ha; destruct Ha as (Ha,Ha'). + assert (H' : 1 < a) by now apply (Z.square_lt_simpl_nonneg 1). + apply (Ha' a). + + split; trivial. + rewrite <- (Z.mul_1_l a) at 1. apply Z.mul_lt_mono_pos_r; omega. + + exists a; auto. Qed. Theorem prime_div_prime: forall p q, prime p -> prime q -> (p | q) -> p = q. Proof. intros p q H H1 H2; - assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. - assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. + assert (Hp: 0 < p); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. + assert (Hq: 0 < q); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. case prime_divisors with (2 := H2); auto. intros H4; contradict Hp; subst; auto with zarith. intros [H4| [H4 | H4]]; subst; auto. @@ -768,11 +760,11 @@ Theorem Zis_gcd_gcd: forall a b c : Z, 0 <= c -> Zis_gcd a b c -> Z.gcd a b = c. Proof. intros a b c H1 H2. - case (Zis_gcd_uniqueness_apart_sign a b c (Zgcd a b)); auto. + case (Zis_gcd_uniqueness_apart_sign a b c (Z.gcd a b)); auto. apply Zgcd_is_gcd; auto. Z.le_elim H1. - generalize (Z.gcd_nonneg a b); auto with zarith. - subst. now case (Z.gcd a b). + - generalize (Z.gcd_nonneg a b); auto with zarith. + - subst. now case (Z.gcd a b). Qed. Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (compat "8.3"). @@ -786,8 +778,8 @@ Proof. intros a b Hg Hb. assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3]. pattern b at 2; rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b); auto. - repeat rewrite Zmult_assoc; f_equal. - rewrite Zmult_comm. + repeat rewrite Z.mul_assoc; f_equal. + rewrite Z.mul_comm. rewrite <- Zdivide_Zdiv_eq; auto. Qed. @@ -798,17 +790,17 @@ Theorem Zgcd_div_swap : forall a b c : Z, Proof. intros a b c Hg Hb. assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3]. - pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. - repeat rewrite Zmult_assoc; f_equal. + pattern b at 2; rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b); auto. + repeat rewrite Z.mul_assoc; f_equal. rewrite Zdivide_Zdiv_eq_2; auto. - repeat rewrite <- Zmult_assoc; f_equal. - rewrite Zmult_comm. + repeat rewrite <- Z.mul_assoc; f_equal. + rewrite Z.mul_comm. rewrite <- Zdivide_Zdiv_eq; auto. Qed. Notation Zgcd_comm := Z.gcd_comm (compat "8.3"). -Lemma Zgcd_ass a b c : Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c). +Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c). Proof. symmetry. apply Z.gcd_assoc. Qed. @@ -817,23 +809,23 @@ Notation Zgcd_Zabs := Z.gcd_abs_l (compat "8.3"). Notation Zgcd_0 := Z.gcd_0_r (compat "8.3"). Notation Zgcd_1 := Z.gcd_1_r (compat "8.3"). -Hint Resolve Zgcd_0 Zgcd_1 : zarith. +Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith. Theorem Zgcd_1_rel_prime : forall a b, Z.gcd a b = 1 <-> rel_prime a b. Proof. unfold rel_prime; split; intro H. rewrite <- H; apply Zgcd_is_gcd. - case (Zis_gcd_unique a b (Zgcd a b) 1); auto. + case (Zis_gcd_unique a b (Z.gcd a b) 1); auto. apply Zgcd_is_gcd. - intros H2; absurd (0 <= Zgcd a b); auto with zarith. - generalize (Zgcd_is_pos a b); auto with zarith. + intros H2; absurd (0 <= Z.gcd a b); auto with zarith. + generalize (Z.gcd_nonneg a b); auto with zarith. Qed. Definition rel_prime_dec: forall a b, { rel_prime a b }+{ ~ rel_prime a b }. Proof. - intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1. + intros a b; case (Z.eq_dec (Z.gcd a b) 1); intros H1. left; apply -> Zgcd_1_rel_prime; auto. right; contradict H1; apply <- Zgcd_1_rel_prime; auto. Defined. @@ -851,25 +843,24 @@ Proof. intros x Hx IH; destruct IH as [F|E]. destruct (rel_prime_dec x p) as [Y|N]. left; intros n [HH1 HH2]. - case (Zgt_succ_gt_or_eq x n); auto with zarith. - intros HH3; subst x; auto. - case (Z_lt_dec 1 x); intros HH1. - right; exists x; split; auto with zarith. - left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith. - right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith. + rewrite Z.lt_succ_r in HH2. + Z.le_elim HH2; subst; auto with zarith. + - case (Z_lt_dec 1 x); intros HH1. + * right; exists x; split; auto with zarith. + * left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith. + - right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith. Defined. Definition prime_dec: forall p, { prime p }+{ ~ prime p }. Proof. intros p; case (Z_lt_dec 1 p); intros H1. - case (prime_dec_aux p p); intros H2. - left; apply prime_intro; auto. - intros n [Hn1 Hn2]; case Zle_lt_or_eq with ( 1 := Hn1 ); auto. - intros HH; subst n. - red; apply Zis_gcd_intro; auto with zarith. - right; intros H3; inversion_clear H3 as [Hp1 Hp2]. - case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith. - right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto. + + case (prime_dec_aux p p); intros H2. + * left; apply prime_intro; auto. + intros n (Hn1,Hn2). Z.le_elim Hn1; auto; subst n. + constructor; auto with zarith. + * right; intros H3; inversion_clear H3 as [Hp1 Hp2]. + case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith. + + right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto. Defined. Theorem not_prime_divide: @@ -877,29 +868,16 @@ Theorem not_prime_divide: Proof. intros p Hp Hp1. case (prime_dec_aux p p); intros H1. - elim Hp1; constructor; auto. - intros n [Hn1 Hn2]. - case Zle_lt_or_eq with ( 1 := Hn1 ); auto with zarith. - intros H2; subst n; red; apply Zis_gcd_intro; auto with zarith. - case H1; intros n [Hn1 Hn2]. - generalize (Zgcd_is_pos n p); intros Hpos. - case (Zle_lt_or_eq 0 (Zgcd n p)); auto with zarith; intros H3. - case (Zle_lt_or_eq 1 (Zgcd n p)); auto with zarith; intros H4. - exists (Zgcd n p); split; auto. - split; auto. - apply Zle_lt_trans with n; auto with zarith. - generalize (Zgcd_is_gcd n p); intros tmp; inversion_clear tmp as [Hr1 Hr2 Hr3]. - case Hr1; intros q Hq. - case (Zle_or_lt q 0); auto with zarith; intros Ht. - absurd (n <= 0 * Zgcd n p) ; auto with zarith. - pattern n at 1; rewrite Hq; auto with zarith. - apply Zle_trans with (1 * Zgcd n p); auto with zarith. - pattern n at 2; rewrite Hq; auto with zarith. - generalize (Zgcd_is_gcd n p); intros Ht; inversion Ht; auto. - case Hn2; red. - rewrite H4; apply Zgcd_is_gcd. - generalize (Zgcd_is_gcd n p); rewrite <- H3; intros tmp; - inversion_clear tmp as [Hr1 Hr2 Hr3]. - absurd (n = 0); auto with zarith. - case Hr1; auto with zarith. + - elim Hp1; constructor; auto. + intros n (Hn1,Hn2). + Z.le_elim Hn1; auto with zarith. + subst n; constructor; auto with zarith. + - case H1; intros n (Hn1,Hn2). + destruct (Z_0_1_more _ (Z.gcd_nonneg n p)) as [H|[H|H]]. + + exfalso. apply Z.gcd_eq_0_l in H. omega. + + elim Hn2. red. rewrite <- H. apply Zgcd_is_gcd. + + exists (Z.gcd n p); split; [ split; auto | apply Z.gcd_divide_r ]. + apply Z.le_lt_trans with n; auto with zarith. + apply Z.divide_pos_le; auto with zarith. + apply Z.gcd_divide_l. Qed. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index d22e2d57c..0d5b9feb7 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -167,8 +167,10 @@ Notation Zle_or_lt := Z.le_gt_cases (compat "8.3"). Notation Zlt_trans := Z.lt_trans (compat "8.3"). -Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p. -Proof Zcompare_Gt_trans. +Lemma Zgt_trans n m p : n > m -> m > p -> n > p. +Proof. + Z.swap_greater. intros; now transitivity m. +Qed. (** Mixed transitivity *) @@ -304,7 +306,7 @@ Proof. Qed. Hint Resolve Z.le_succ_diag_r: zarith. -Hint Resolve Zle_le_succ: zarith. +Hint Resolve Z.le_le_succ_r: zarith. (** Relating order wrt successor and order wrt predecessor *) @@ -345,7 +347,7 @@ Proof. easy. Qed. -(* weaker but useful (in [Zpower] for instance) *) +(* weaker but useful (in [Z.pow] for instance) *) Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p. Proof. easy. @@ -361,7 +363,7 @@ Proof. induction n; simpl; intros. apply Z.le_refl. easy. Qed. -Hint Immediate Zeq_le: zarith. +Hint Immediate Z.eq_le_incl: zarith. (** Derived lemma *) diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v index a90eedb41..880245c53 100644 --- a/theories/ZArith/Zpow_alt.v +++ b/theories/ZArith/Zpow_alt.v @@ -79,5 +79,5 @@ Qed. Lemma Zpower_alt_Ppow p q : (Zpos p)^^(Zpos q) = Zpos (p^q). Proof. - now rewrite Zpower_equiv, Z.pow_Zpos. + now rewrite Zpower_equiv, Pos2Z.inj_pow. Qed. diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 4fe411584..2e23e982e 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -19,7 +19,7 @@ Notation Zpower := Z.pow (compat "8.3"). Notation Zpower_0_r := Z.pow_0_r (compat "8.3"). Notation Zpower_succ_r := Z.pow_succ_r (compat "8.3"). Notation Zpower_neg_r := Z.pow_neg_r (compat "8.3"). -Notation Zpower_Ppow := Z.pow_Zpos (compat "8.3"). +Notation Zpower_Ppow := Pos2Z.inj_pow (compat "8.3"). Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow. Proof. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 5d025322b..fa63a190e 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -85,15 +85,15 @@ Proof. assert (Hn := Nat2Z.is_nonneg n). destruct p; simpl Pos.size_nat. - specialize IHn with p. - rewrite Z.pos_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega. + rewrite Pos2Z.inj_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega. - specialize IHn with p. - rewrite Z.pos_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega. + rewrite Pos2Z.inj_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega. - split; auto with zarith. intros _. apply Z.pow_gt_1. easy. now rewrite Nat2Z.inj_succ, Z.lt_succ_r. Qed. -(** * Zpower and modulo *) +(** * Z.pow and modulo *) Theorem Zpower_mod p q n : 0 < n -> (p^q) mod n = ((p mod n)^q) mod n. @@ -106,7 +106,7 @@ Proof. - rewrite !Z.pow_neg_r; auto with zarith. Qed. -(** A direct way to compute Zpower modulo **) +(** A direct way to compute Z.pow modulo **) Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z := match m with @@ -231,7 +231,7 @@ Proof. exists n; destruct H; rewrite Z.mul_0_r in H; auto. Qed. -(** * Zsquare: a direct definition of [z^2] *) +(** * Z.square: a direct definition of [z^2] *) Notation Psquare := Pos.square (compat "8.3"). Notation Zsquare := Z.square (compat "8.3"). diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 5052d01a0..880c4376d 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -78,7 +78,7 @@ Proof. Qed. Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith. -Hint Unfold Zpower_pos Zpower_nat: zarith. +Hint Unfold Z.pow_pos Zpower_nat: zarith. Theorem Zpower_exp x n m : n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. @@ -181,7 +181,7 @@ Section Powers_of_2. Qed. Theorem shift_pos_correct p x : - Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x. + Zpos (shift_pos p x) = Z.pow_pos 2 p * Zpos x. Proof. now rewrite shift_pos_nat, Zpower_pos_nat, shift_nat_correct. Qed. @@ -266,13 +266,13 @@ Section power_div_with_rest. apply Pos.iter_invariant; [|omega]. intros ((q,r),d) (H,H'). unfold Zdiv_rest_aux. destruct q as [ |[q|q| ]|[q|q| ]]; try omega. - - rewrite Z.pos_xI, Z.mul_add_distr_r in H. + - rewrite Pos2Z.inj_xI, Z.mul_add_distr_r in H. rewrite Z.mul_shuffle3, Z.mul_assoc. omega. - - rewrite Z.pos_xO in H. + - rewrite Pos2Z.inj_xO in H. rewrite Z.mul_shuffle3, Z.mul_assoc. omega. - - rewrite Z.neg_xI, Z.mul_sub_distr_r in H. + - rewrite Pos2Z.neg_xI, Z.mul_sub_distr_r in H. rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. omega. - - rewrite Z.neg_xO in H. + - rewrite Pos2Z.neg_xO in H. rewrite Z.mul_shuffle3, Z.mul_assoc. omega. Qed. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index 5b79fbce8..accce71f1 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -11,51 +11,95 @@ Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms. Local Open Scope Z_scope. (** This file provides results about the Round-Toward-Zero Euclidean - division [Zquotrem], whose projections are [Zquot] and [Zrem]. - Definition of this division can be found in file [BinIntDef]. + division [Z.quotrem], whose projections are [Z.quot] (noted ÷) + and [Z.rem]. - This division and the one defined in Zdiv agree only on positive - numbers. Otherwise, Zdiv performs Round-Toward-Bottom (a.k.a Floor). + This division and [Z.div] agree only on positive numbers. + Otherwise, [Z.div] performs Round-Toward-Bottom (a.k.a Floor). - The current approach is compatible with the division of usual + This [Z.quot] is compatible with the division of usual programming languages such as Ocaml. In addition, it has nicer properties with respect to opposite and other usual operations. + + The definition of this division is now in file [BinIntDef], + while most of the results about here are now in the main module + [BinInt.Z], thanks to the generic "Numbers" layer. Remain here: + + - some compatibility notation for old names. + + - some extra results with less preconditions (in particular + exploiting the arbitrary value of division by 0). *) -(** * Relation between division on N and on Z. *) +Notation Ndiv_Zquot := N2Z.inj_quot (compat "8.3"). +Notation Nmod_Zrem := N2Z.inj_rem (compat "8.3"). +Notation Z_quot_rem_eq := Z.quot_rem' (compat "8.3"). +Notation Zrem_lt := Z.rem_bound_abs (compat "8.3"). +Notation Zquot_unique := Z.quot_unique (compat "8.3"). +Notation Zrem_unique := Z.rem_unique (compat "8.3"). +Notation Zrem_1_r := Z.rem_1_r (compat "8.3"). +Notation Zquot_1_r := Z.quot_1_r (compat "8.3"). +Notation Zrem_1_l := Z.rem_1_l (compat "8.3"). +Notation Zquot_1_l := Z.quot_1_l (compat "8.3"). +Notation Z_quot_same := Z.quot_same (compat "8.3"). +Notation Z_quot_mult := Z.quot_mul (compat "8.3"). +Notation Zquot_small := Z.quot_small (compat "8.3"). +Notation Zrem_small := Z.rem_small (compat "8.3"). +Notation Zquot2_quot := Zquot2_quot (compat "8.3"). + +(** Particular values taken for [a÷0] and [(Z.rem a 0)]. + We avise to not rely on these arbitrary values. *) + +Lemma Zquot_0_r a : a ÷ 0 = 0. +Proof. now destruct a. Qed. + +Lemma Zrem_0_r a : Z.rem a 0 = a. +Proof. now destruct a. Qed. + +(** The following results are expressed without the [b<>0] condition + whenever possible. *) + +Lemma Zrem_0_l a : Z.rem 0 a = 0. +Proof. now destruct a. Qed. + +Lemma Zquot_0_l a : 0÷a = 0. +Proof. now destruct a. Qed. + +Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r + : zarith. -Lemma Ndiv_Zquot : forall a b:N, - Z_of_N (a/b) = (Z_of_N a ÷ Z_of_N b). -Proof. - intros. - destruct a; destruct b; simpl; auto. - unfold N.div, Z.quot; simpl. destruct N.pos_div_eucl; auto. -Qed. +Ltac zero_or_not a := + destruct (Z.eq_decidable a 0) as [->|?]; + [rewrite ?Zquot_0_l, ?Zrem_0_l, ?Zquot_0_r, ?Zrem_0_r; + auto with zarith|]. -Lemma Nmod_Zrem : forall a b:N, - Z.of_N (a mod b) = Z.rem (Z.of_N a) (Z.of_N b). -Proof. - intros. - destruct a; destruct b; simpl; auto. - unfold N.modulo, Z.rem; simpl; destruct N.pos_div_eucl; auto. -Qed. +Lemma Z_rem_same a : Z.rem a a = 0. +Proof. zero_or_not a. now apply Z.rem_same. Qed. -(** * Characterization of this euclidean division. *) +Lemma Z_rem_mult a b : Z.rem (a*b) b = 0. +Proof. zero_or_not b. now apply Z.rem_mul. Qed. -(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] - has been chosen to be [a], so this equation holds even for [b=0]. -*) +(** * Division and Opposite *) -Notation Z_quot_rem_eq := Z.quot_rem' (compat "8.3"). +(* The precise equalities that are invalid with "historic" Zdiv. *) + +Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b). +Proof. zero_or_not b. now apply Z.quot_opp_l. Qed. -(** Then, the inequalities constraining the remainder: - The remainder is bounded by the divisor, in term of absolute values *) +Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b). +Proof. zero_or_not b. now apply Z.quot_opp_r. Qed. -Theorem Zrem_lt : forall a b:Z, b<>0 -> - Z.abs (Z.rem a b) < Z.abs b. -Proof. - apply Z.rem_bound_abs. -Qed. +Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b). +Proof. zero_or_not b. now apply Z.rem_opp_l. Qed. + +Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b. +Proof. zero_or_not b. now apply Z.rem_opp_r. Qed. + +Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b. +Proof. zero_or_not b. now apply Z.quot_opp_opp. Qed. + +Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b). +Proof. zero_or_not b. now apply Z.rem_opp_opp. Qed. (** The sign of the remainder is the one of [a]. Due to the possible nullity of [a], a general result is to be stated in the following form: @@ -63,41 +107,33 @@ Qed. Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a. Proof. - destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; - simpl; destruct n0; simpl; auto with zarith. + zero_or_not b. + - apply Z.square_nonneg. + - zero_or_not (Z.rem a b). + rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg. Qed. (** This can also be said in a simplier way: *) Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a. Proof. - rewrite <-Z.sgn_nonneg, Z.sgn_mul; apply Zrem_sgn. + zero_or_not b. + - apply Z.square_nonneg. + - now apply Z.rem_sign_mul. Qed. -(** Reformulation of [Zquot_lt] and [Zrem_sgn] in 2 - then 4 particular cases. *) +(** Reformulation of [Z.rem_bound_abs] in 2 then 4 particular cases. *) Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b. Proof. - intros. - assert (0 <= Z.rem a b). - generalize (Zrem_sgn a b). - destruct (Zle_lt_or_eq 0 a H). - rewrite <- Zsgn_pos in H1; rewrite H1. romega with *. - subst a; simpl; auto. - generalize (Zrem_lt a b H0); romega with *. + intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b); + romega with *. Qed. Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0. Proof. - intros. - assert (Z.rem a b <= 0). - generalize (Zrem_sgn a b). - destruct (Zle_lt_or_eq a 0 H). - rewrite <- Zsgn_neg in H1; rewrite H1; romega with *. - subst a; simpl; auto. - generalize (Zrem_lt a b H0); romega with *. + intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b); + romega with *. Qed. Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b. @@ -120,45 +156,6 @@ Proof. intros; generalize (Zrem_lt_neg a b); romega with *. Qed. -(** * Division and Opposite *) - -(* The precise equalities that are invalid with "historic" Zdiv. *) - -Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zquot_opp_r a b : a÷(-b) = -(a÷b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zrem_opp_l a b : Z.rem (-a) b = -(Z.rem a b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zrem_opp_r a b : Z.rem a (-b) = Z.rem a b. -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zquot_opp_opp a b : (-a)÷(-b) = a÷b. -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.quot, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. - -Theorem Zrem_opp_opp a b : Z.rem (-a) (-b) = -(Z.rem a b). -Proof. - destruct a; destruct b; simpl; auto; - unfold Z.rem, Z.quotrem; destruct N.pos_div_eucl; simpl; auto with zarith. -Qed. (** * Unicity results *) @@ -172,170 +169,93 @@ Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r. Proof. unfold Remainder, Remainder_alt; intuition. - romega with *. - romega with *. - rewrite <-(Zmult_opp_opp). - apply Zmult_le_0_compat; romega. - assert (0 <= Z.sgn r * Z.sgn a) by (rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto). - destruct r; simpl Z.sgn in *; romega with *. + - romega with *. + - romega with *. + - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega. + - assert (0 <= Z.sgn r * Z.sgn a). + { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } + destruct r; simpl Z.sgn in *; romega with *. Qed. -Theorem Zquot_mod_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> q = a÷b /\ r = Z.rem a b. +Theorem Zquot_mod_unique_full a b q r : + Remainder a b r -> a = b*q + r -> q = a÷b /\ r = Z.rem a b. Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. apply Zdiv_mod_unique with b; auto. apply Zrem_lt_pos; auto. romega with *. - rewrite <- H1; apply Z_quot_rem_eq. + rewrite <- H1; apply Z.quot_rem'. - rewrite <- (Zopp_involutive a). + rewrite <- (Z.opp_involutive a). rewrite Zquot_opp_l, Zrem_opp_l. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). - rewrite <-Z_quot_rem_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1. + rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. romega with *. Qed. -Theorem Zquot_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> q = a÷b. +Theorem Zquot_unique_full a b q r : + Remainder a b r -> a = b*q + r -> q = a÷b. Proof. intros; destruct (Zquot_mod_unique_full a b q r); auto. Qed. -Theorem Zquot_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> - a = b*q + r -> q = a÷b. -Proof. exact Z.quot_unique. Qed. - -Theorem Zrem_unique_full: - forall a b q r, Remainder a b r -> - a = b*q + r -> r = Z.rem a b. +Theorem Zrem_unique_full a b q r : + Remainder a b r -> a = b*q + r -> r = Z.rem a b. Proof. intros; destruct (Zquot_mod_unique_full a b q r); auto. Qed. -Theorem Zrem_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> - a = b*q + r -> r = Z.rem a b. -Proof. exact Z.rem_unique. Qed. - -(** * Basic values of divisions and modulo. *) - -Lemma Zrem_0_l: forall a, Z.rem 0 a = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zrem_0_r: forall a, Z.rem a 0 = a. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zquot_0_l: forall a, 0÷a = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zquot_0_r: forall a, a÷0 = 0. -Proof. - destruct a; simpl; auto. -Qed. - -Lemma Zrem_1_r: forall a, Z.rem a 1 = 0. -Proof. exact Z.rem_1_r. Qed. - -Lemma Zquot_1_r: forall a, a÷1 = a. -Proof. exact Z.quot_1_r. Qed. - -Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Zquot_1_r Zrem_1_r - : zarith. - -Lemma Zquot_1_l: forall a, 1 < a -> 1÷a = 0. -Proof. exact Z.quot_1_l. Qed. - -Lemma Zrem_1_l: forall a, 1 < a -> Z.rem 1 a = 1. -Proof. exact Z.rem_1_l. Qed. - -Lemma Z_quot_same : forall a:Z, a<>0 -> a÷a = 1. -Proof. exact Z.quot_same. Qed. - -Ltac zero_or_not a := - destruct (Z.eq_dec a 0); - [subst; rewrite ?Zrem_0_l, ?Zquot_0_l, ?Zrem_0_r, ?Zquot_0_r; - auto with zarith|]. - -Lemma Z_rem_same : forall a, Z.rem a a = 0. -Proof. intros. zero_or_not a. apply Z.rem_same; auto. Qed. - -Lemma Z_rem_mult : forall a b, Z.rem (a*b) b = 0. -Proof. intros. zero_or_not b. apply Z.rem_mul; auto. Qed. - -Lemma Z_quot_mult : forall a b:Z, b <> 0 -> (a*b)÷b = a. -Proof. exact Z.quot_mul. Qed. - (** * Order results about Zrem and Zquot *) (* Division of positive numbers is positive. *) -Lemma Z_quot_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a÷b. +Lemma Z_quot_pos a b : 0 <= a -> 0 <= b -> 0 <= a÷b. Proof. intros. zero_or_not b. apply Z.quot_pos; auto with zarith. Qed. (** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) -Lemma Z_quot_lt : forall a b:Z, 0 < a -> 2 <= b -> a÷b < a. +Lemma Z_quot_lt a b : 0 < a -> 2 <= b -> a÷b < a. Proof. intros. apply Z.quot_lt; auto with zarith. Qed. -(** A division of a small number by a bigger one yields zero. *) +(** [<=] is compatible with a positive division. *) -Theorem Zquot_small: forall a b, 0 <= a < b -> a÷b = 0. -Proof. exact Z.quot_small. Qed. - -(** Same situation, in term of modulo: *) - -Theorem Zrem_small: forall a n, 0 <= a < n -> Z.rem a n = a. -Proof. exact Z.rem_small. Qed. - -(** [Zge] is compatible with a positive division. *) - -Lemma Z_quot_monotone : forall a b c, 0<=c -> a<=b -> a÷c <= b÷c. +Lemma Z_quot_monotone a b c : 0<=c -> a<=b -> a÷c <= b÷c. Proof. intros. zero_or_not c. apply Z.quot_le_mono; auto with zarith. Qed. -(** With our choice of division, rounding of (a÷b) is always done toward zero: *) +(** With our choice of division, rounding of (a÷b) is always done toward 0: *) -Lemma Z_mult_quot_le : forall a b:Z, 0 <= a -> 0 <= b*(a÷b) <= a. +Lemma Z_mult_quot_le a b : 0 <= a -> 0 <= b*(a÷b) <= a. Proof. intros. zero_or_not b. apply Z.mul_quot_le; auto with zarith. Qed. -Lemma Z_mult_quot_ge : forall a b:Z, a <= 0 -> a <= b*(a÷b) <= 0. +Lemma Z_mult_quot_ge a b : a <= 0 -> a <= b*(a÷b) <= 0. Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed. (** The previous inequalities between [b*(a÷b)] and [a] are exact iff the modulo is zero. *) -Lemma Z_quot_exact_full : forall a b:Z, a = b*(a÷b) <-> Z.rem a b = 0. +Lemma Z_quot_exact_full a b : a = b*(a÷b) <-> Z.rem a b = 0. Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. (** A modulo cannot grow beyond its starting point. *) -Theorem Zrem_le: forall a b, 0 <= a -> 0 <= b -> Z.rem a b <= a. +Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. (** Some additionnal inequalities about Zdiv. *) Theorem Zquot_le_upper_bound: forall a b q, 0 < b -> a <= q*b -> a÷b <= q. -Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_upper_bound. Qed. +Proof. intros a b q; rewrite Z.mul_comm; apply Z.quot_le_upper_bound. Qed. Theorem Zquot_lt_upper_bound: forall a b q, 0 <= a -> 0 < b -> a < q*b -> a÷b < q. -Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_lt_upper_bound. Qed. +Proof. intros a b q; rewrite Z.mul_comm; apply Z.quot_lt_upper_bound. Qed. Theorem Zquot_le_lower_bound: forall a b q, 0 < b -> q*b <= a -> q <= a÷b. -Proof. intros a b q; rewrite Zmult_comm; apply Z.quot_le_lower_bound. Qed. +Proof. intros a b q; rewrite Z.mul_comm; apply Z.quot_le_lower_bound. Qed. Theorem Zquot_sgn: forall a b, 0 <= Z.sgn (a÷b) * Z.sgn a * Z.sgn b. @@ -374,22 +294,22 @@ Proof. intros. zero_or_not b. apply Z.quot_mul_cancel_r; auto. Qed. Lemma Zquot_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)÷(c*b) = a÷b. Proof. - intros. rewrite (Zmult_comm c b). zero_or_not b. - rewrite (Zmult_comm b c). apply Z.quot_mul_cancel_l; auto. + intros. rewrite (Z.mul_comm c b). zero_or_not b. + rewrite (Z.mul_comm b c). apply Z.quot_mul_cancel_l; auto. Qed. Lemma Zmult_rem_distr_l: forall a b c, Z.rem (c*a) (c*b) = c * (Z.rem a b). Proof. - intros. zero_or_not c. rewrite (Zmult_comm c b). zero_or_not b. - rewrite (Zmult_comm b c). apply Z.mul_rem_distr_l; auto. + intros. zero_or_not c. rewrite (Z.mul_comm c b). zero_or_not b. + rewrite (Z.mul_comm b c). apply Z.mul_rem_distr_l; auto. Qed. Lemma Zmult_rem_distr_r: forall a b c, Z.rem (a*c) (b*c) = (Z.rem a b) * c. Proof. - intros. zero_or_not b. rewrite (Zmult_comm b c). zero_or_not c. - rewrite (Zmult_comm c b). apply Z.mul_rem_distr_r; auto. + intros. zero_or_not b. rewrite (Z.mul_comm b c). zero_or_not c. + rewrite (Z.mul_comm c b). apply Z.mul_rem_distr_r; auto. Qed. (** Operations modulo. *) @@ -424,7 +344,7 @@ Lemma Zplus_rem_idemp_r: forall a b n, Z.rem (b + Z.rem a n) n = Z.rem (b + a) n. Proof. intros. zero_or_not n. apply Z.add_rem_idemp_r; auto. - rewrite Zmult_comm; auto. + rewrite Z.mul_comm; auto. Qed. Lemma Zmult_rem_idemp_l: forall a b n, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. @@ -437,8 +357,8 @@ Proof. intros. zero_or_not n. apply Z.mul_rem_idemp_r; auto. Qed. Lemma Zquot_Zquot : forall a b c, (a÷b)÷c = a÷(b*c). Proof. - intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c. - rewrite Zmult_comm. apply Z.quot_quot; auto. + intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. + rewrite Z.mul_comm. apply Z.quot_quot; auto. Qed. (** A last inequality: *) @@ -468,28 +388,26 @@ Proof. right. destruct p; simpl; split; now auto with zarith. Qed. -Notation Zquot2_quot := Zquot2_quot (only parsing). - Lemma Zrem_odd : forall a, Z.rem a 2 = if Z.odd a then Z.sgn a else 0. Proof. intros. symmetry. - apply Zrem_unique_full with (Zquot2 a). + apply Zrem_unique_full with (Z.quot2 a). apply Zquot2_odd_remainder. apply Zquot2_odd_eqn. Qed. Lemma Zrem_even : forall a, Z.rem a 2 = if Z.even a then 0 else Z.sgn a. Proof. - intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Zeven_bool. + intros a. rewrite Zrem_odd, Zodd_even_bool. now destruct Z.even. Qed. -Lemma Zeven_rem : forall a, Z.even a = Zeq_bool (Z.rem a 2) 0. +Lemma Zeven_rem : forall a, Z.even a = Z.eqb (Z.rem a 2) 0. Proof. intros a. rewrite Zrem_even. destruct a as [ |p|p]; trivial; now destruct p. Qed. -Lemma Zodd_rem : forall a, Z.odd a = negb (Zeq_bool (Z.rem a 2) 0). +Lemma Zodd_rem : forall a, Z.odd a = negb (Z.eqb (Z.rem a 2) 0). Proof. intros a. rewrite Zrem_odd. destruct a as [ |p|p]; trivial; now destruct p. @@ -505,18 +423,17 @@ Proof. intros. apply Zdiv_mod_unique with b. apply Zrem_lt_pos; auto with zarith. - rewrite Zabs_eq; auto with *; apply Z_mod_lt; auto with *. + rewrite Z.abs_eq; auto with *; apply Z_mod_lt; auto with *. rewrite <- Z_div_mod_eq; auto with *. - symmetry; apply Z_quot_rem_eq; auto with *. + symmetry; apply Z.quot_rem; auto with *. Qed. Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> a÷b = a/b. Proof. - intros a b Ha Hb. - destruct (Zle_lt_or_eq _ _ Hb). - generalize (Zquotrem_Zdiv_eucl_pos a b Ha H); intuition. - subst; rewrite Zquot_0_r, Zdiv_0_r; reflexivity. + intros a b Ha Hb. Z.le_elim Hb. + - generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb); intuition. + - subst; now rewrite Zquot_0_r, Zdiv_0_r. Qed. Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b -> diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index 4584c3f8f..54f6f2e9a 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -32,12 +32,12 @@ Ltac compute_POS := | |- context [(Zpos (xI ?X1))] => match constr:X1 with | context [1%positive] => fail 1 - | _ => rewrite (BinInt.Zpos_xI X1) + | _ => rewrite (Pos2Z.inj_xI X1) end | |- context [(Zpos (xO ?X1))] => match constr:X1 with | context [1%positive] => fail 1 - | _ => rewrite (BinInt.Zpos_xO X1) + | _ => rewrite (Pos2Z.inj_xO X1) end end. @@ -115,7 +115,7 @@ Definition Zsqrt : fun h => match sqrtrempos p with | c_sqrt s r Heq Hint => - existS + existT (fun s:Z => {r : Z | Zpos p = s * s + r /\ s * s <= Zpos p < (s + 1) * (s + 1)}) @@ -131,10 +131,10 @@ Definition Zsqrt : {s : Z & {r : Z | Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} - (h (refl_equal Datatypes.Gt)) + (h (eq_refl Datatypes.Gt)) | Z0 => fun h => - existS + existT (fun s:Z => {r : Z | 0 = s * s + r /\ s * s <= 0 < (s + 1) * (s + 1)}) 0 (exist @@ -149,8 +149,8 @@ Defined. Definition Zsqrt_plain (x:Z) : Z := match x with | Zpos p => - match Zsqrt (Zpos p) (Zorder.Zle_0_pos p) with - | existS s _ => s + match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with + | existT s _ => s end | Zneg p => 0 | Z0 => 0 @@ -164,12 +164,11 @@ Theorem Zsqrt_interval : Zsqrt_plain n * Zsqrt_plain n <= n < (Zsqrt_plain n + 1) * (Zsqrt_plain n + 1). Proof. - intros x; case x. - unfold Zsqrt_plain in |- *; omega. - intros p; unfold Zsqrt_plain in |- *; - case (Zsqrt (Zpos p) (Zorder.Zle_0_pos p)). - intros s [r [Heq Hint]] Hle; assumption. - intros p Hle; elim Hle; auto. + intros [|p|p] Hp. + - now compute. + - unfold Zsqrt_plain. + now destruct Zsqrt as (s & r & Heq & Hint). + - now elim Hp. Qed. (** Positivity *) @@ -177,9 +176,9 @@ Qed. Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n. Proof. intros n m; case (Zsqrt_interval n); auto with zarith. - intros H1 H2; case (Zle_or_lt 0 (Zsqrt_plain n)); auto. - intros H3; contradict H2; auto; apply Zle_not_lt. - apply Zle_trans with ( 2 := H1 ). + intros H1 H2; case (Z.le_gt_cases 0 (Zsqrt_plain n)); auto. + intros H3; contradict H2; auto; apply Z.le_ngt. + apply Z.le_trans with ( 2 := H1 ). replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1)) with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1)); auto with zarith. @@ -194,13 +193,13 @@ Proof. generalize (Zsqrt_plain_is_pos (a * a)); auto with zarith; intros Haa. case (Zsqrt_interval (a * a)); auto with zarith. intros H1 H2. - case (Zle_or_lt a (Zsqrt_plain (a * a))); intros H3; auto. - case Zle_lt_or_eq with (1:=H3); auto; clear H3; intros H3. - contradict H1; auto; apply Zlt_not_le; auto with zarith. - apply Zle_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith. - apply Zmult_lt_compat_r; auto with zarith. - contradict H2; auto; apply Zle_not_lt; auto with zarith. - apply Zmult_le_compat; auto with zarith. + case (Z.le_gt_cases a (Zsqrt_plain (a * a))); intros H3. + - Z.le_elim H3; auto. + contradict H1; auto; apply Z.lt_nge; auto with zarith. + apply Z.le_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith. + apply Z.mul_lt_mono_pos_r; auto with zarith. + - contradict H2; auto; apply Z.le_ngt; auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. Qed. (** [Zsqrt_plain] is increasing *) @@ -208,16 +207,16 @@ Qed. Theorem Zsqrt_le: forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q. Proof. - intros p q [H1 H2]; case Zle_lt_or_eq with (1:=H2); clear H2; intros H2; - [ | subst q; auto with zarith]. - case (Zle_or_lt (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3. + intros p q [H1 H2]. + Z.le_elim H2; [ | subst q; auto with zarith]. + case (Z.le_gt_cases (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3. assert (Hp: (0 <= Zsqrt_plain q)). - apply Zsqrt_plain_is_pos; auto with zarith. + { apply Zsqrt_plain_is_pos; auto with zarith. } absurd (q <= p); auto with zarith. - apply Zle_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)). + apply Z.le_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)). case (Zsqrt_interval q); auto with zarith. - apply Zle_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith. - apply Zmult_le_compat; auto with zarith. + apply Z.le_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith. + apply Z.mul_le_mono_nonneg; auto with zarith. case (Zsqrt_interval p); auto with zarith. Qed. diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 30802f824..efe5b6847 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -29,7 +29,7 @@ Section wf_proof. (** The proof of well-foundness is classic: we do the proof by induction on a measure in nat, which is here [|x-c|] *) - Let f (z:Z) := Zabs_nat (z - c). + Let f (z:Z) := Z.abs_nat (z - c). Lemma Zwf_well_founded : well_founded (Zwf c). red in |- *; intros. @@ -45,12 +45,12 @@ Section wf_proof. apply Acc_intro; intros. apply H. unfold Zwf in H1. - case (Zle_or_lt c y); intro; auto with zarith. + case (Z.le_gt_cases c y); intro; auto with zarith. left. red in H0. apply lt_le_trans with (f a); auto with arith. - unfold f in |- *. - apply Zabs.Zabs_nat_lt; omega. + unfold f. + apply Zabs2Nat.inj_lt; omega. apply (H (S (f a))); auto. Qed. @@ -75,18 +75,15 @@ Section wf_proof_up. (** The proof of well-foundness is classic: we do the proof by induction on a measure in nat, which is here [|c-x|] *) - Let f (z:Z) := Zabs_nat (c - z). + Let f (z:Z) := Z.abs_nat (c - z). Lemma Zwf_up_well_founded : well_founded (Zwf_up c). Proof. apply well_founded_lt_compat with (f := f). - unfold Zwf_up, f in |- *. + unfold Zwf_up, f. intros. - apply Zabs.Zabs_nat_lt. - unfold Zminus in |- *. split. - apply Zle_left; intuition. - apply Zplus_lt_compat_l; unfold Zlt in |- *; rewrite <- Zcompare_opp; - intuition. + apply Zabs2Nat.inj_lt; try (apply Z.le_0_sub; intuition). + now apply Z.sub_lt_mono_l. Qed. End wf_proof_up. |