diff options
author | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-08-20 18:27:01 +0200 |
commit | e0d682ec25282a348d35c5b169abafec48555690 (patch) | |
tree | 1a46f0142a85df553388c932110793881f3af52f /theories/ZArith | |
parent | 86535d84cc3cffeee1dcd8545343f234e7285530 (diff) |
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'theories/ZArith')
33 files changed, 1636 insertions, 1678 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 3a5eb885..eeec9042 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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) : @@ -1217,11 +1153,11 @@ Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _. Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. -Include ZProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +(** The Bind Scope prevents Z to stay associated with abstract_scope. + (TODO FIX) *) -(** Otherwise Z stays associated with abstract_scope : (TODO FIX) *) -Bind Scope Z_scope with Z. +Include ZProp. Bind Scope Z_scope with Z. +Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract @@ -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,111 +1287,362 @@ 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). - 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 *) -Notation Zdouble_plus_one := Z.succ_double (only parsing). -Notation Zdouble_minus_one := Z.pred_double (only parsing). -Notation Zdouble := Z.double (only parsing). -Notation ZPminus := Z.pos_sub (only parsing). -Notation Zsucc' := Z.succ (only parsing). -Notation Zpred' := Z.pred (only parsing). -Notation Zplus' := Z.add (only parsing). -Notation Zplus := Z.add (only parsing). (* Slightly incompatible *) -Notation Zopp := Z.opp (only parsing). -Notation Zsucc := Z.succ (only parsing). -Notation Zpred := Z.pred (only parsing). -Notation Zminus := Z.sub (only parsing). -Notation Zmult := Z.mul (only parsing). -Notation Zcompare := Z.compare (only parsing). -Notation Zsgn := Z.sgn (only parsing). -Notation Zle := Z.le (only parsing). -Notation Zge := Z.ge (only parsing). -Notation Zlt := Z.lt (only parsing). -Notation Zgt := Z.gt (only parsing). -Notation Zmax := Z.max (only parsing). -Notation Zmin := Z.min (only parsing). -Notation Zabs := Z.abs (only parsing). -Notation Zabs_nat := Z.abs_nat (only parsing). -Notation Zabs_N := Z.abs_N (only parsing). -Notation Z_of_nat := Z.of_nat (only parsing). -Notation Z_of_N := Z.of_N (only parsing). - -Notation Zind := Z.peano_ind (only parsing). -Notation Zopp_0 := Z.opp_0 (only parsing). -Notation Zopp_neg := Z.opp_Zneg (only parsing). -Notation Zopp_involutive := Z.opp_involutive (only parsing). -Notation Zopp_inj := Z.opp_inj (only parsing). -Notation Zplus_0_l := Z.add_0_l (only parsing). -Notation Zplus_0_r := Z.add_0_r (only parsing). -Notation Zplus_comm := Z.add_comm (only parsing). -Notation Zopp_plus_distr := Z.opp_add_distr (only parsing). -Notation Zopp_succ := Z.opp_succ (only parsing). -Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing). -Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing). -Notation Zplus_assoc := Z.add_assoc (only parsing). -Notation Zplus_permute := Z.add_shuffle3 (only parsing). -Notation Zplus_reg_l := Z.add_reg_l (only parsing). -Notation Zplus_succ_l := Z.add_succ_l (only parsing). -Notation Zplus_succ_comm := Z.add_succ_comm (only parsing). -Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing). -Notation Zsucc_inj := Z.succ_inj (only parsing). -Notation Zsucc'_inj := Z.succ_inj (only parsing). -Notation Zsucc'_pred' := Z.succ_pred (only parsing). -Notation Zpred'_succ' := Z.pred_succ (only parsing). -Notation Zpred'_inj := Z.pred_inj (only parsing). -Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing). -Notation Zminus_0_r := Z.sub_0_r (only parsing). -Notation Zminus_diag := Z.sub_diag (only parsing). -Notation Zminus_plus_distr := Z.sub_add_distr (only parsing). -Notation Zminus_succ_r := Z.sub_succ_r (only parsing). -Notation Zminus_plus := Z.add_simpl_l (only parsing). -Notation Zmult_0_l := Z.mul_0_l (only parsing). -Notation Zmult_0_r := Z.mul_0_r (only parsing). -Notation Zmult_1_l := Z.mul_1_l (only parsing). -Notation Zmult_1_r := Z.mul_1_r (only parsing). -Notation Zmult_comm := Z.mul_comm (only parsing). -Notation Zmult_assoc := Z.mul_assoc (only parsing). -Notation Zmult_permute := Z.mul_shuffle3 (only parsing). -Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing). -Notation Zdouble_mult := Z.double_spec (only parsing). -Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing). -Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing). -Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing). -Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing). -Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing). -Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing). -Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing). -Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing). -Notation Zmult_reg_l := Z.mul_reg_l (only parsing). -Notation Zmult_reg_r := Z.mul_reg_r (only parsing). -Notation Zmult_succ_l := Z.mul_succ_l (only parsing). -Notation Zmult_succ_r := Z.mul_succ_r (only parsing). -Notation Zpos_xI := Z.pos_xI (only parsing). -Notation Zpos_xO := Z.pos_xO (only parsing). -Notation Zneg_xI := Z.neg_xI (only parsing). -Notation Zneg_xO := Z.neg_xO (only parsing). +Notation Zdouble_plus_one := Z.succ_double (compat "8.3"). +Notation Zdouble_minus_one := Z.pred_double (compat "8.3"). +Notation Zdouble := Z.double (compat "8.3"). +Notation ZPminus := Z.pos_sub (compat "8.3"). +Notation Zsucc' := Z.succ (compat "8.3"). +Notation Zpred' := Z.pred (compat "8.3"). +Notation Zplus' := Z.add (compat "8.3"). +Notation Zplus := Z.add (compat "8.3"). (* Slightly incompatible *) +Notation Zopp := Z.opp (compat "8.3"). +Notation Zsucc := Z.succ (compat "8.3"). +Notation Zpred := Z.pred (compat "8.3"). +Notation Zminus := Z.sub (compat "8.3"). +Notation Zmult := Z.mul (compat "8.3"). +Notation Zcompare := Z.compare (compat "8.3"). +Notation Zsgn := Z.sgn (compat "8.3"). +Notation Zle := Z.le (compat "8.3"). +Notation Zge := Z.ge (compat "8.3"). +Notation Zlt := Z.lt (compat "8.3"). +Notation Zgt := Z.gt (compat "8.3"). +Notation Zmax := Z.max (compat "8.3"). +Notation Zmin := Z.min (compat "8.3"). +Notation Zabs := Z.abs (compat "8.3"). +Notation Zabs_nat := Z.abs_nat (compat "8.3"). +Notation Zabs_N := Z.abs_N (compat "8.3"). +Notation Z_of_nat := Z.of_nat (compat "8.3"). +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_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"). +Notation Zplus_0_r := Z.add_0_r (compat "8.3"). +Notation Zplus_comm := Z.add_comm (compat "8.3"). +Notation Zopp_plus_distr := Z.opp_add_distr (compat "8.3"). +Notation Zopp_succ := Z.opp_succ (compat "8.3"). +Notation Zplus_opp_r := Z.add_opp_diag_r (compat "8.3"). +Notation Zplus_opp_l := Z.add_opp_diag_l (compat "8.3"). +Notation Zplus_assoc := Z.add_assoc (compat "8.3"). +Notation Zplus_permute := Z.add_shuffle3 (compat "8.3"). +Notation Zplus_reg_l := Z.add_reg_l (compat "8.3"). +Notation Zplus_succ_l := Z.add_succ_l (compat "8.3"). +Notation Zplus_succ_comm := Z.add_succ_comm (compat "8.3"). +Notation Zsucc_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zsucc_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_pred' := Z.succ_pred (compat "8.3"). +Notation Zpred'_succ' := Z.pred_succ (compat "8.3"). +Notation Zpred'_inj := Z.pred_inj (compat "8.3"). +Notation Zsucc'_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zminus_0_r := Z.sub_0_r (compat "8.3"). +Notation Zminus_diag := Z.sub_diag (compat "8.3"). +Notation Zminus_plus_distr := Z.sub_add_distr (compat "8.3"). +Notation Zminus_succ_r := Z.sub_succ_r (compat "8.3"). +Notation Zminus_plus := Z.add_simpl_l (compat "8.3"). +Notation Zmult_0_l := Z.mul_0_l (compat "8.3"). +Notation Zmult_0_r := Z.mul_0_r (compat "8.3"). +Notation Zmult_1_l := Z.mul_1_l (compat "8.3"). +Notation Zmult_1_r := Z.mul_1_r (compat "8.3"). +Notation Zmult_comm := Z.mul_comm (compat "8.3"). +Notation Zmult_assoc := Z.mul_assoc (compat "8.3"). +Notation Zmult_permute := Z.mul_shuffle3 (compat "8.3"). +Notation Zmult_1_inversion_l := Z.mul_eq_1 (compat "8.3"). +Notation Zdouble_mult := Z.double_spec (compat "8.3"). +Notation Zdouble_plus_one_mult := Z.succ_double_spec (compat "8.3"). +Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (compat "8.3"). +Notation Zmult_opp_opp := Z.mul_opp_opp (compat "8.3"). +Notation Zmult_opp_comm := Z.mul_opp_comm (compat "8.3"). +Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (compat "8.3"). +Notation Zmult_plus_distr_r := Z.mul_add_distr_l (compat "8.3"). +Notation Zmult_plus_distr_l := Z.mul_add_distr_r (compat "8.3"). +Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (compat "8.3"). +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 := 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 d96d20fb..958ce2ef 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 *) @@ -183,7 +188,7 @@ Definition ltb x y := (** Nota: [geb] and [gtb] are provided for compatibility, but [leb] and [ltb] should rather be used instead, since - more results we be available on them. *) + more results will be available on them. *) Definition geb x y := match x ?= y with @@ -197,15 +202,11 @@ Definition gtb x y := | _ => false end. -(** Nota: this [eqb] is not convertible with the generated [Z_beq], - since the underlying [Pos.eqb] differs from [positive_beq] - (cf BinIntDef). *) - 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. @@ -234,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 *) @@ -245,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. @@ -270,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. @@ -279,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 @@ -297,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. @@ -352,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) @@ -396,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). @@ -418,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. @@ -441,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 @@ -453,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. @@ -477,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. @@ -498,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. *) @@ -510,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. @@ -536,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 @@ -559,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). @@ -571,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 7c840c56..384c046f 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 bcccc126..3935e124 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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.v b/theories/ZArith/ZArith.v index 265e62f0..033dc11f 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 8eeca3b9..38b6c44d 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 76308e60..ff4f5e7b 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,7 +11,7 @@ Require Import Sumbool. Require Import BinInt. Require Import Zorder. Require Import Zcompare. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (* begin hide *) (* Trivial, to deprecate? *) @@ -21,22 +21,18 @@ 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 (only parsing). +Notation Z_eq_dec := Z.eq_dec (compat "8.3"). Section decidability. @@ -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. @@ -176,7 +151,7 @@ Proof. intro. apply False_rec. apply H. - symmetry in |- *. + symmetry . assumption. Defined. @@ -189,17 +164,17 @@ 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. - symmetry in |- *. + symmetry . assumption. Defined. @@ -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 23473e93..08d1a931 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -27,17 +27,17 @@ Local Open Scope Z_scope. (**********************************************************************) (** * Properties of absolute value *) -Notation Zabs_eq := Z.abs_eq (only parsing). -Notation Zabs_non_eq := Z.abs_neq (only parsing). -Notation Zabs_Zopp := Z.abs_opp (only parsing). -Notation Zabs_pos := Z.abs_nonneg (only parsing). -Notation Zabs_involutive := Z.abs_involutive (only parsing). -Notation Zabs_eq_case := Z.abs_eq_cases (only parsing). -Notation Zabs_triangle := Z.abs_triangle (only parsing). -Notation Zsgn_Zabs := Z.sgn_abs (only parsing). -Notation Zabs_Zsgn := Z.abs_sgn (only parsing). -Notation Zabs_Zmult := Z.abs_mul (only parsing). -Notation Zabs_square := Z.abs_square (only parsing). +Notation Zabs_eq := Z.abs_eq (compat "8.3"). +Notation Zabs_non_eq := Z.abs_neq (compat "8.3"). +Notation Zabs_Zopp := Z.abs_opp (compat "8.3"). +Notation Zabs_pos := Z.abs_nonneg (compat "8.3"). +Notation Zabs_involutive := Z.abs_involutive (compat "8.3"). +Notation Zabs_eq_case := Z.abs_eq_cases (compat "8.3"). +Notation Zabs_triangle := Z.abs_triangle (compat "8.3"). +Notation Zsgn_Zabs := Z.sgn_abs (compat "8.3"). +Notation Zabs_Zsgn := Z.abs_sgn (compat "8.3"). +Notation Zabs_Zmult := Z.abs_mul (compat "8.3"). +Notation Zabs_square := Z.abs_square (compat "8.3"). (** * Proving a property of the absolute value by cases *) @@ -68,38 +68,38 @@ Qed. (** * Some results about the sign function. *) -Notation Zsgn_Zmult := Z.sgn_mul (only parsing). -Notation Zsgn_Zopp := Z.sgn_opp (only parsing). -Notation Zsgn_pos := Z.sgn_pos_iff (only parsing). -Notation Zsgn_neg := Z.sgn_neg_iff (only parsing). -Notation Zsgn_null := Z.sgn_null_iff (only parsing). +Notation Zsgn_Zmult := Z.sgn_mul (compat "8.3"). +Notation Zsgn_Zopp := Z.sgn_opp (compat "8.3"). +Notation Zsgn_pos := Z.sgn_pos_iff (compat "8.3"). +Notation Zsgn_neg := Z.sgn_neg_iff (compat "8.3"). +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. (** Compatibility *) -Notation inj_Zabs_nat := Zabs2Nat.id_abs (only parsing). -Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (only parsing). -Notation Zabs_nat_mult := Zabs2Nat.inj_mul (only parsing). -Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (only parsing). -Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (only parsing). -Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (only parsing). -Notation Zabs_nat_compare := Zabs2Nat.inj_compare (only parsing). +Notation inj_Zabs_nat := Zabs2Nat.id_abs (compat "8.3"). +Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (compat "8.3"). +Notation Zabs_nat_mult := Zabs2Nat.inj_mul (compat "8.3"). +Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (compat "8.3"). +Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (compat "8.3"). +Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (compat "8.3"). +Notation Zabs_nat_compare := Zabs2Nat.inj_compare (compat "8.3"). Lemma Zabs_nat_le n m : 0 <= n <= m -> (Z.abs_nat n <= Z.abs_nat m)%nat. 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 d0901282..f20bc4bb 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,7 +13,7 @@ Require Import Zcompare. Require Import ZArith_dec. Require Import Sumbool. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (** * Boolean operations from decidability of order *) (** The decidability of equality and order relations over @@ -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). @@ -33,10 +33,10 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x). (**********************************************************************) (** * Boolean comparisons of binary integers *) -Notation Zle_bool := Z.leb (only parsing). -Notation Zge_bool := Z.geb (only parsing). -Notation Zlt_bool := Z.ltb (only parsing). -Notation Zgt_bool := Z.gtb (only parsing). +Notation Zle_bool := Z.leb (compat "8.3"). +Notation Zge_bool := Z.geb (compat "8.3"). +Notation Zlt_bool := Z.ltb (compat "8.3"). +Notation Zgt_bool := Z.gtb (compat "8.3"). (** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare]. The old [Zeq_bool] is kept for compatibility. *) @@ -87,7 +87,7 @@ Proof. apply Z.leb_le. Qed. -Notation Zle_bool_refl := Z.leb_refl (only parsing). +Notation Zle_bool_refl := Z.leb_refl (compat "8.3"). Lemma Zle_bool_antisym n m : (n <=? m) = true -> (m <=? n) = true -> n = m. diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 20e1b006..fe91698f 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 [>] *) @@ -181,18 +181,18 @@ Qed. (** Compatibility notations *) -Notation Zcompare_refl := Z.compare_refl (only parsing). -Notation Zcompare_Eq_eq := Z.compare_eq (only parsing). -Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing). -Notation Zcompare_spec := Z.compare_spec (only parsing). -Notation Zmin_l := Z.min_l (only parsing). -Notation Zmin_r := Z.min_r (only parsing). -Notation Zmax_l := Z.max_l (only parsing). -Notation Zmax_r := Z.max_r (only parsing). -Notation Zabs_eq := Z.abs_eq (only parsing). -Notation Zabs_non_eq := Z.abs_neq (only parsing). -Notation Zsgn_0 := Z.sgn_null (only parsing). -Notation Zsgn_1 := Z.sgn_pos (only parsing). -Notation Zsgn_m1 := Z.sgn_neg (only parsing). +Notation Zcompare_refl := Z.compare_refl (compat "8.3"). +Notation Zcompare_Eq_eq := Z.compare_eq (compat "8.3"). +Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (compat "8.3"). +Notation Zcompare_spec := Z.compare_spec (compat "8.3"). +Notation Zmin_l := Z.min_l (compat "8.3"). +Notation Zmin_r := Z.min_r (compat "8.3"). +Notation Zmax_l := Z.max_l (compat "8.3"). +Notation Zmax_r := Z.max_r (compat "8.3"). +Notation Zabs_eq := Z.abs_eq (compat "8.3"). +Notation Zabs_non_eq := Z.abs_neq (compat "8.3"). +Notation Zsgn_0 := Z.sgn_null (compat "8.3"). +Notation Zsgn_1 := Z.sgn_pos (compat "8.3"). +Notation Zsgn_m1 := Z.sgn_neg (compat "8.3"). (** Not kept: Zcompare_egal_dec *) diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 5a2c3cc3..b4163ef9 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,7 @@ Require Import ZArithRing. Require Import ZArith_base. Require Export Omega. Require Import Wf_nat. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (**********************************************************************) @@ -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. @@ -56,7 +56,7 @@ Proof. set (Q := fun z => 0 <= z -> P z * P (- z)) in *. cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q in |- *; clear Q; intros. + unfold Q; clear Q; intros. split; apply HP. rewrite Z.abs_eq; auto; intros. elim (H (Z.abs m)); intros; auto with zarith. @@ -75,7 +75,7 @@ Proof. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. - unfold Q in |- *; clear Q; intros. + unfold Q; clear Q; intros. split; apply HP. rewrite Z.abs_eq; auto; intros. elim (H (Z.abs m)); intros; auto with zarith. @@ -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 ff1d96df..fa8f5c27 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,16 +88,16 @@ 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 |- *. + destruct z; simpl. trivial. - destruct p; simpl in |- *; trivial. + destruct p; simpl; trivial. - destruct p; simpl in |- *. - destruct p as [p| p| ]; simpl in |- *. - rewrite <- (Pdouble_minus_one_o_succ_eq_xI p); trivial. + destruct p; simpl. + destruct p as [p| p| ]; simpl. + 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. @@ -145,17 +145,17 @@ Section Z_BRIC_A_BRAC. (z >= 0)%Z -> Z_to_binary (S n) (bit_value b + 2 * z) = Bcons b n (Z_to_binary n z). Proof. - destruct b; destruct z; simpl in |- *; auto. + destruct b; destruct z; simpl; auto. intro H; elim H; trivial. Qed. Lemma binary_value_pos : forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z. Proof. - induction bv as [| a n v IHbv]; simpl in |- *. + induction bv as [| a n v IHbv]; simpl. omega. - destruct a; destruct (binary_value n v); simpl in |- *; auto. + destruct a; destruct (binary_value n v); simpl; auto. auto with zarith. Qed. @@ -174,34 +174,34 @@ Section Z_BRIC_A_BRAC. Proof. 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. + destruct p as [p| p| ]; simpl; auto. + 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. destruct p; auto. - simpl in |- *; intros; omega. + simpl; intros; omega. intro H; elim H; trivial. Qed. @@ -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,23 +225,23 @@ 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 z; unfold bit_value; auto. destruct p; tauto || (intro H; elim H). destruct p; tauto || (intro H; elim H). 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. + destruct z; unfold bit_value; auto. intros; elim H. destruct p; tauto || (intros; elim H). destruct p; tauto || (intros; elim H). @@ -310,7 +310,7 @@ Section COHERENT_VALUE. (z < two_power_nat n)%Z -> binary_value n (Z_to_binary n z) = z. Proof. induction n as [| n IHn]. - unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros; omega. + unfold two_power_nat, shift_nat; simpl; intros; omega. intros; rewrite Z_to_binary_Sn_z. rewrite binary_value_Sn. @@ -328,7 +328,7 @@ Section COHERENT_VALUE. (z < two_power_nat n)%Z -> two_compl_value n (Z_to_two_compl n z) = z. Proof. induction n as [| n IHn]. - unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros. + unfold two_power_nat, shift_nat; simpl; intros. assert (z = (-1)%Z \/ z = 0%Z). omega. intuition; subst z; trivial. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 314f696a..27fb21bc 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,16 +18,16 @@ Local Open Scope Z_scope. (** The definition of the division is now in [BinIntDef], the initial specifications and properties are in [BinInt]. *) -Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing). -Notation Zdiv_eucl := Z.div_eucl (only parsing). -Notation Zdiv := Z.div (only parsing). -Notation Zmod := Z.modulo (only parsing). +Notation Zdiv_eucl_POS := Z.pos_div_eucl (compat "8.3"). +Notation Zdiv_eucl := Z.div_eucl (compat "8.3"). +Notation Zdiv := Z.div (compat "8.3"). +Notation Zmod := Z.modulo (compat "8.3"). -Notation Zdiv_eucl_eq := Z.div_eucl_eq (only parsing). -Notation Z_div_mod_eq_full := Z.div_mod (only parsing). -Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing). -Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing). -Notation Zmod_neg_bound := Z.mod_neg_bound (only parsing). +Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.3"). +Notation Z_div_mod_eq_full := Z.div_mod (compat "8.3"). +Notation Zmod_POS_bound := Z.pos_div_eucl_bound (compat "8.3"). +Notation Zmod_pos_bound := Z.mod_pos_bound (compat "8.3"). +Notation Zmod_neg_bound := Z.mod_neg_bound (compat "8.3"). (** * Main division theorems *) @@ -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/Zeuclid.v b/theories/ZArith/Zeuclid.v index f1b59749..1dfe2fb3 100644 --- a/theories/ZArith/Zeuclid.v +++ b/theories/ZArith/Zeuclid.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index f4d702b2..dd48e84f 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -58,8 +58,8 @@ Proof (Zodd_equiv n). (** Boolean tests of parity (now in BinInt.Z) *) -Notation Zeven_bool := Z.even (only parsing). -Notation Zodd_bool := Z.odd (only parsing). +Notation Zeven_bool := Z.even (compat "8.3"). +Notation Zodd_bool := Z.odd (compat "8.3"). Lemma Zeven_bool_iff n : Z.even n = true <-> Zeven n. Proof. @@ -130,17 +130,17 @@ Qed. Hint Unfold Zeven Zodd: zarith. -Notation Zeven_bool_succ := Z.even_succ (only parsing). -Notation Zeven_bool_pred := Z.even_pred (only parsing). -Notation Zodd_bool_succ := Z.odd_succ (only parsing). -Notation Zodd_bool_pred := Z.odd_pred (only parsing). +Notation Zeven_bool_succ := Z.even_succ (compat "8.3"). +Notation Zeven_bool_pred := Z.even_pred (compat "8.3"). +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 (only parsing). -Notation Zquot2 := Z.quot2 (only parsing). +Notation Zdiv2 := Z.div2 (compat "8.3"). +Notation Zquot2 := Z.quot2 (compat "8.3"). (** Properties of [Z.div2] *) @@ -223,7 +223,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 ebf3d024..40d2b129 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -1,19 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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 6a14d693..8b879fbe 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 30948ca7..319e2c26 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,26 +71,26 @@ 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 |- *; + simple induction x; intros; simpl; [ 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 |- *; + | unfold two_power_pos; unfold shift_pos; simpl; omega ]. Qed. @@ -103,7 +103,7 @@ Section Log_pos. (* Log of positive integers *) Lemma log_sup_correct1 : forall p:positive, 0 <= log_sup p. Proof. - simple induction p; intros; simpl in |- *; auto with zarith. + simple induction p; intros; simpl; auto with zarith. Qed. (** For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)] @@ -112,46 +112,46 @@ 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 |- *; + [ elim H; right; simpl; 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 |- *; + [ left; simpl; rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0)); rewrite <- (proj1 Hif); rewrite <- (proj2 Hif); auto - | right; simpl in |- *; + | right; simpl; 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. Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p. Proof. - simple induction p; simpl in |- *; intros; omega. + simple induction p; simpl; 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. + simple induction p; simpl; intros; omega. Qed. (** Now it's possible to specify and build the [Log] rounded to the nearest *) @@ -161,22 +161,20 @@ 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. Proof. - simple induction p; simpl in |- *; intros; + simple induction p; simpl; intros; [ 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 : @@ -184,9 +182,9 @@ Section Log_pos. (* Log of positive integers *) Proof. simple induction p. intros p0 [Einf| Esup]. - simpl in |- *. rewrite Einf. + simpl. rewrite Einf. case p0; [ left | left | right ]; reflexivity. - simpl in |- *; rewrite Esup. + simpl; rewrite Esup. elim (log_sup_log_inf p0). generalize (log_inf_le_log_sup p0). generalize (log_sup_le_Slog_inf p0). @@ -194,10 +192,10 @@ Section Log_pos. (* Log of positive integers *) intros; omega. case p0; intros; auto with zarith. intros p0 [Einf| Esup]. - simpl in |- *. + simpl. repeat rewrite Einf. case p0; intros; auto with zarith. - simpl in |- *. + simpl. repeat rewrite Esup. case p0; intros; auto with zarith. auto. @@ -218,20 +216,20 @@ 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 ]. + simple induction x; simpl; + [ 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 *) @@ -247,21 +245,21 @@ Section divers. Proof. split; [ elim p; - [ simpl in |- *; tauto - | simpl in |- *; intros; generalize (H H0); intro H1; elim H1; + [ simpl; tauto + | simpl; intros; generalize (H H0); intro H1; elim H1; intros y0 Hy0; exists (S y0); rewrite Hy0; reflexivity | intro; exists 0%nat; reflexivity ] - | intros; elim H; intros; rewrite H0; elim x; intros; simpl in |- *; trivial ]. + | intros; elim H; intros; rewrite H0; elim x; intros; simpl; trivial ]. Qed. Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p. Proof. simple induction p; - [ intros; right; simpl in |- *; tauto + [ intros; right; simpl; tauto | intros; elim H; - [ intros; left; simpl in |- *; exact H0 - | intros; right; simpl in |- *; exact H0 ] - | left; simpl in |- *; trivial ]. + [ intros; left; simpl; exact H0 + | intros; right; simpl; exact H0 ] + | left; simpl; trivial ]. Qed. End divers. diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 999564f0..31880c17 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 Zmax_case := Z.max_case. -Definition Zmax_case_strong := Z.max_case_strong. +(** 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"). + +(** 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 (only parsing). -Notation Zmax2 := Z.le_max_r (only parsing). -Notation Zmax_irreducible_inf := Z.max_dec (only parsing). -Notation Zmax_le_prime_inf := Z.max_le (only parsing). -(* end hide *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 2c5003a6..30b88d8f 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 Zmin_case := Z.min_case. -Definition Zmin_case_strong := Z.min_case_strong. +(** 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"). + +(** 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 (only parsing). -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/Zminmax.v b/theories/ZArith/Zminmax.v index 8908175f..ce589e28 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,11 +12,11 @@ Require Import Orders BinInt Zcompare Zorder. (*begin hide*) (* Compatibility with names of the old Zminmax file *) -Notation Zmin_max_absorption_r_r := Z.min_max_absorption (only parsing). -Notation Zmax_min_absorption_r_r := Z.max_min_absorption (only parsing). -Notation Zmax_min_distr_r := Z.max_min_distr (only parsing). -Notation Zmin_max_distr_r := Z.min_max_distr (only parsing). -Notation Zmax_min_modular_r := Z.max_min_modular (only parsing). -Notation Zmin_max_modular_r := Z.min_max_modular (only parsing). -Notation max_min_disassoc := Z.max_min_disassoc (only parsing). +Notation Zmin_max_absorption_r_r := Z.min_max_absorption (compat "8.3"). +Notation Zmax_min_absorption_r_r := Z.max_min_absorption (compat "8.3"). +Notation Zmax_min_distr_r := Z.max_min_distr (compat "8.3"). +Notation Zmin_max_distr_r := Z.min_max_distr (compat "8.3"). +Notation Zmax_min_modular_r := Z.max_min_modular (compat "8.3"). +Notation Zmin_max_modular_r := Z.min_max_modular (compat "8.3"). +Notation max_min_disassoc := Z.max_min_disassoc (compat "8.3"). (*end hide*) diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index ff844ec2..d0ec1916 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,18 +11,19 @@ Require Import BinInt. Require Import Zcompare. Require Import Zorder. Require Import Bool. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (**********************************************************************) (** Iterators *) (** [n]th iteration of the function [f] *) -Notation iter := @Z.iter (only parsing). +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 e3843990..27b7e6a0 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 *) @@ -931,67 +951,67 @@ Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m). (** For the others, a Notation is fine *) -Notation inj_0 := Nat2Z.inj_0 (only parsing). -Notation inj_S := Nat2Z.inj_succ (only parsing). -Notation inj_compare := Nat2Z.inj_compare (only parsing). -Notation inj_eq_rev := Nat2Z.inj (only parsing). -Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (only parsing). -Notation inj_le_iff := Nat2Z.inj_le (only parsing). -Notation inj_lt_iff := Nat2Z.inj_lt (only parsing). -Notation inj_ge_iff := Nat2Z.inj_ge (only parsing). -Notation inj_gt_iff := Nat2Z.inj_gt (only parsing). -Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (only parsing). -Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (only parsing). -Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (only parsing). -Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (only parsing). -Notation inj_plus := Nat2Z.inj_add (only parsing). -Notation inj_mult := Nat2Z.inj_mul (only parsing). -Notation inj_minus1 := Nat2Z.inj_sub (only parsing). -Notation inj_minus := Nat2Z.inj_sub_max (only parsing). -Notation inj_min := Nat2Z.inj_min (only parsing). -Notation inj_max := Nat2Z.inj_max (only parsing). - -Notation Z_of_nat_of_P := positive_nat_Z (only parsing). +Notation inj_0 := Nat2Z.inj_0 (compat "8.3"). +Notation inj_S := Nat2Z.inj_succ (compat "8.3"). +Notation inj_compare := Nat2Z.inj_compare (compat "8.3"). +Notation inj_eq_rev := Nat2Z.inj (compat "8.3"). +Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (compat "8.3"). +Notation inj_le_iff := Nat2Z.inj_le (compat "8.3"). +Notation inj_lt_iff := Nat2Z.inj_lt (compat "8.3"). +Notation inj_ge_iff := Nat2Z.inj_ge (compat "8.3"). +Notation inj_gt_iff := Nat2Z.inj_gt (compat "8.3"). +Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (compat "8.3"). +Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (compat "8.3"). +Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (compat "8.3"). +Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (compat "8.3"). +Notation inj_plus := Nat2Z.inj_add (compat "8.3"). +Notation inj_mult := Nat2Z.inj_mul (compat "8.3"). +Notation inj_minus1 := Nat2Z.inj_sub (compat "8.3"). +Notation inj_minus := Nat2Z.inj_sub_max (compat "8.3"). +Notation inj_min := Nat2Z.inj_min (compat "8.3"). +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)) (only parsing). - -Notation Z_of_nat_of_N := N_nat_Z (only parsing). -Notation Z_of_N_of_nat := nat_N_Z (only parsing). - -Notation Z_of_N_eq := (f_equal Z.of_N) (only parsing). -Notation Z_of_N_eq_rev := N2Z.inj (only parsing). -Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (only parsing). -Notation Z_of_N_compare := N2Z.inj_compare (only parsing). -Notation Z_of_N_le_iff := N2Z.inj_le (only parsing). -Notation Z_of_N_lt_iff := N2Z.inj_lt (only parsing). -Notation Z_of_N_ge_iff := N2Z.inj_ge (only parsing). -Notation Z_of_N_gt_iff := N2Z.inj_gt (only parsing). -Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (only parsing). -Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (only parsing). -Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (only parsing). -Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (only parsing). -Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (only parsing). -Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (only parsing). -Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (only parsing). -Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (only parsing). -Notation Z_of_N_pos := N2Z.inj_pos (only parsing). -Notation Z_of_N_abs := N2Z.inj_abs_N (only parsing). -Notation Z_of_N_le_0 := N2Z.is_nonneg (only parsing). -Notation Z_of_N_plus := N2Z.inj_add (only parsing). -Notation Z_of_N_mult := N2Z.inj_mul (only parsing). -Notation Z_of_N_minus := N2Z.inj_sub_max (only parsing). -Notation Z_of_N_succ := N2Z.inj_succ (only parsing). -Notation Z_of_N_min := N2Z.inj_min (only parsing). -Notation Z_of_N_max := N2Z.inj_max (only parsing). -Notation Zabs_of_N := Zabs2N.id (only parsing). -Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (only parsing). -Notation Zabs_N_succ := Zabs2N.inj_succ (only parsing). -Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (only parsing). -Notation Zabs_N_plus := Zabs2N.inj_add (only parsing). -Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (only parsing). -Notation Zabs_N_mult := Zabs2N.inj_mul (only parsing). - -Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0. + (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"). + +Notation Z_of_N_eq := (f_equal Z.of_N) (compat "8.3"). +Notation Z_of_N_eq_rev := N2Z.inj (compat "8.3"). +Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (compat "8.3"). +Notation Z_of_N_compare := N2Z.inj_compare (compat "8.3"). +Notation Z_of_N_le_iff := N2Z.inj_le (compat "8.3"). +Notation Z_of_N_lt_iff := N2Z.inj_lt (compat "8.3"). +Notation Z_of_N_ge_iff := N2Z.inj_ge (compat "8.3"). +Notation Z_of_N_gt_iff := N2Z.inj_gt (compat "8.3"). +Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (compat "8.3"). +Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (compat "8.3"). +Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (compat "8.3"). +Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (compat "8.3"). +Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (compat "8.3"). +Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (compat "8.3"). +Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (compat "8.3"). +Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (compat "8.3"). +Notation Z_of_N_pos := N2Z.inj_pos (compat "8.3"). +Notation Z_of_N_abs := N2Z.inj_abs_N (compat "8.3"). +Notation Z_of_N_le_0 := N2Z.is_nonneg (compat "8.3"). +Notation Z_of_N_plus := N2Z.inj_add (compat "8.3"). +Notation Z_of_N_mult := N2Z.inj_mul (compat "8.3"). +Notation Z_of_N_minus := N2Z.inj_sub_max (compat "8.3"). +Notation Z_of_N_succ := N2Z.inj_succ (compat "8.3"). +Notation Z_of_N_min := N2Z.inj_min (compat "8.3"). +Notation Z_of_N_max := N2Z.inj_max (compat "8.3"). +Notation Zabs_of_N := Zabs2N.id (compat "8.3"). +Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (compat "8.3"). +Notation Zabs_N_succ := Zabs2N.inj_succ (compat "8.3"). +Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (compat "8.3"). +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. Proof. intros. rewrite not_le_minus_0; auto with arith. Qed. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 6eb1a709..c1e01451 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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] @@ -25,20 +25,20 @@ Open Scope Z_scope. - properties of the efficient [Z.gcd] function *) -Notation Zgcd := Z.gcd (only parsing). -Notation Zggcd := Z.ggcd (only parsing). -Notation Zggcd_gcd := Z.ggcd_gcd (only parsing). -Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing). -Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing). -Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing). -Notation Zgcd_greatest := Z.gcd_greatest (only parsing). -Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing). -Notation Zggcd_opp := Z.ggcd_opp (only parsing). - -(** The former specialized inductive predicate [Zdivide] is now +Notation Zgcd := Z.gcd (compat "8.3"). +Notation Zggcd := Z.ggcd (compat "8.3"). +Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.3"). +Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.3"). +Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.3"). +Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.3"). +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 [Z.divide] is now a generic existential predicate. *) -Notation Zdivide := Z.divide (only parsing). +Notation Zdivide := Z.divide (compat "8.3"). (** Its former constructor is now a pseudo-constructor. *) @@ -46,17 +46,17 @@ Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H. (** Results concerning divisibility*) -Notation Zdivide_refl := Z.divide_refl (only parsing). -Notation Zone_divide := Z.divide_1_l (only parsing). -Notation Zdivide_0 := Z.divide_0_r (only parsing). -Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing). -Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing). -Notation Zdivide_plus_r := Z.divide_add_r (only parsing). -Notation Zdivide_minus_l := Z.divide_sub_r (only parsing). -Notation Zdivide_mult_l := Z.divide_mul_l (only parsing). -Notation Zdivide_mult_r := Z.divide_mul_r (only parsing). -Notation Zdivide_factor_r := Z.divide_factor_l (only parsing). -Notation Zdivide_factor_l := Z.divide_factor_r (only parsing). +Notation Zdivide_refl := Z.divide_refl (compat "8.3"). +Notation Zone_divide := Z.divide_1_l (compat "8.3"). +Notation Zdivide_0 := Z.divide_0_r (compat "8.3"). +Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (compat "8.3"). +Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (compat "8.3"). +Notation Zdivide_plus_r := Z.divide_add_r (compat "8.3"). +Notation Zdivide_minus_l := Z.divide_sub_r (compat "8.3"). +Notation Zdivide_mult_l := Z.divide_mul_l (compat "8.3"). +Notation Zdivide_mult_r := Z.divide_mul_r (compat "8.3"). +Notation Zdivide_factor_r := Z.divide_factor_l (compat "8.3"). +Notation Zdivide_factor_l := Z.divide_factor_r (compat "8.3"). Lemma Zdivide_opp_r a b : (a | b) -> (a | - b). Proof. apply Z.divide_opp_r. Qed. @@ -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. *) @@ -91,12 +91,12 @@ Qed. (** Only [1] and [-1] divide [1]. *) -Notation Zdivide_1 := Z.divide_1_r (only parsing). +Notation Zdivide_1 := Z.divide_1_r (compat "8.3"). (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) -Notation Zdivide_antisym := Z.divide_antisym (only parsing). -Notation Zdivide_trans := Z.divide_trans (only parsing). +Notation Zdivide_antisym := Z.divide_antisym (compat "8.3"). +Notation Zdivide_trans := Z.divide_trans (compat "8.3"). (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) @@ -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. @@ -305,7 +305,7 @@ Section extended_euclid_algorithm. v1 * a + v2 * b = v3 -> (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid. Proof. - intros v3 Hv3; generalize Hv3; pattern v3 in |- *. + intros v3 Hv3; generalize Hv3; pattern v3. apply Zlt_0_rec. clear v3 Hv3; intros. elim (Z_zerop x); intro. @@ -319,8 +319,8 @@ Section extended_euclid_algorithm. apply Z_mod_lt; omega. assert (xpos : x > 0). omega. generalize (Z_div_mod_eq u3 x xpos). - unfold q in |- *. - intro eq; pattern u3 at 2 in |- *; rewrite eq; ring. + unfold q. + intro eq; pattern u3 at 2; rewrite eq; ring. apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)). tauto. replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with @@ -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,21 +450,21 @@ 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. + red; auto with zarith. apply Gauss with c. - rewrite Zmult_comm. + rewrite Z.mul_comm. rewrite <- H3. auto with zarith. - red in |- *; auto with zarith. + red; auto with zarith. Qed. (** After factorization by a gcd, the original numbers are relatively prime. *) @@ -479,7 +479,7 @@ Proof. elim H1; intros. elim H4; intros. rewrite H2 in H6; subst b; omega. - unfold rel_prime in |- *. + unfold rel_prime. destruct H1. destruct H1 as (a',H1). destruct H3 as (b',H3). @@ -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. @@ -575,30 +575,29 @@ Lemma prime_divisors : forall p:Z, prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p. Proof. - simple induction 1; intros. + 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). apply Zdivide_bounds; [ assumption | omega ]. - generalize H3. - pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *; - apply Zabs_ind; intros; omega. + { assert (Z.abs a <= Z.abs p) as H2. + apply Zdivide_bounds; [ assumption | omega ]. + revert H2. + pattern (Z.abs a); apply Zabs_ind; pattern (Z.abs p); apply Zabs_ind; + intros; omega. } intuition idtac. (* -p < a < -1 *) - absurd (rel_prime (- a) p); intuition. - inversion H3. - assert (- a | - a); auto with zarith. - assert (- a | p); auto with zarith. - generalize (H8 (- a) H9 H10); intuition idtac. - generalize (Zdivide_1 (- a) H11); intuition. + - absurd (rel_prime (- a) p); intuition. + inversion H2. + assert (- a | - a) by auto with zarith. + assert (- a | p) by auto with zarith. + apply H7, Z.divide_1_r in H8; intuition. (* a = 0 *) - inversion H2. subst a; omega. + - inversion H1. subst a; omega. (* 1 < a < p *) - absurd (rel_prime a p); intuition. - inversion H3. - assert (a | a); auto with zarith. - assert (a | p); auto with zarith. - generalize (H8 a H9 H10); intuition idtac. - generalize (Zdivide_1 a H11); intuition. + - absurd (rel_prime a p); intuition. + inversion H2. + assert (a | a) by auto with zarith. + assert (a | p) by auto with zarith. + apply H7, Z.divide_1_r in H8; intuition. Qed. (** A prime number is relatively prime with any number it does not divide *) @@ -623,7 +622,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. @@ -653,87 +652,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. @@ -744,7 +735,7 @@ Qed. (** we now prove that [Z.gcd] is indeed a gcd in the sense of [Zis_gcd]. *) -Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing). +Notation Zgcd_is_pos := Z.gcd_nonneg (compat "8.3"). Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b). Proof. @@ -770,15 +761,15 @@ 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 (only parsing). -Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing). +Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (compat "8.3"). +Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (compat "8.3"). Theorem Zgcd_div_swap0 : forall a b : Z, 0 < Z.gcd a b -> @@ -788,8 +779,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. @@ -800,42 +791,42 @@ 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 (only parsing). +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. -Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing). -Notation Zgcd_0 := Z.gcd_0_r (only parsing). -Notation Zgcd_1 := Z.gcd_1_r (only parsing). +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. @@ -853,25 +844,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: @@ -879,29 +869,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 a8cd69bb..b1d1f8b5 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -38,9 +38,9 @@ Qed. (**********************************************************************) (** * Decidability of equality and order on Z *) -Notation dec_eq := Z.eq_decidable (only parsing). -Notation dec_Zle := Z.le_decidable (only parsing). -Notation dec_Zlt := Z.lt_decidable (only parsing). +Notation dec_eq := Z.eq_decidable (compat "8.3"). +Notation dec_Zle := Z.le_decidable (compat "8.3"). +Notation dec_Zlt := Z.lt_decidable (compat "8.3"). Theorem dec_Zne n m : decidable (Zne n m). Proof. @@ -64,12 +64,12 @@ Qed. (** * Relating strict and large orders *) -Notation Zgt_lt := Z.gt_lt (only parsing). -Notation Zlt_gt := Z.lt_gt (only parsing). -Notation Zge_le := Z.ge_le (only parsing). -Notation Zle_ge := Z.le_ge (only parsing). -Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing). -Notation Zge_iff_le := Z.ge_le_iff (only parsing). +Notation Zgt_lt := Z.gt_lt (compat "8.3"). +Notation Zlt_gt := Z.lt_gt (compat "8.3"). +Notation Zge_le := Z.ge_le (compat "8.3"). +Notation Zle_ge := Z.le_ge (compat "8.3"). +Notation Zgt_iff_lt := Z.gt_lt_iff (compat "8.3"). +Notation Zge_iff_le := Z.ge_le_iff (compat "8.3"). Lemma Zle_not_lt n m : n <= m -> ~ m < n. Proof. @@ -121,18 +121,18 @@ Qed. (** Reflexivity *) -Notation Zle_refl := Z.le_refl (only parsing). -Notation Zeq_le := Z.eq_le_incl (only parsing). +Notation Zle_refl := Z.le_refl (compat "8.3"). +Notation Zeq_le := Z.eq_le_incl (compat "8.3"). Hint Resolve Z.le_refl: zarith. (** Antisymmetry *) -Notation Zle_antisym := Z.le_antisymm (only parsing). +Notation Zle_antisym := Z.le_antisymm (compat "8.3"). (** Asymmetry *) -Notation Zlt_asym := Z.lt_asymm (only parsing). +Notation Zlt_asym := Z.lt_asymm (compat "8.3"). Lemma Zgt_asym n m : n > m -> ~ m > n. Proof. @@ -141,8 +141,8 @@ Qed. (** Irreflexivity *) -Notation Zlt_irrefl := Z.lt_irrefl (only parsing). -Notation Zlt_not_eq := Z.lt_neq (only parsing). +Notation Zlt_irrefl := Z.lt_irrefl (compat "8.3"). +Notation Zlt_not_eq := Z.lt_neq (compat "8.3"). Lemma Zgt_irrefl n : ~ n > n. Proof. @@ -151,8 +151,8 @@ Qed. (** Large = strict or equal *) -Notation Zlt_le_weak := Z.lt_le_incl (only parsing). -Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (only parsing). +Notation Zlt_le_weak := Z.lt_le_incl (compat "8.3"). +Notation Zle_lt_or_eq_iff := Z.lt_eq_cases (compat "8.3"). Lemma Zle_lt_or_eq n m : n <= m -> n < m \/ n = m. Proof. @@ -161,19 +161,21 @@ Qed. (** Dichotomy *) -Notation Zle_or_lt := Z.le_gt_cases (only parsing). +Notation Zle_or_lt := Z.le_gt_cases (compat "8.3"). (** Transitivity of strict orders *) -Notation Zlt_trans := Z.lt_trans (only parsing). +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 *) -Notation Zlt_le_trans := Z.lt_le_trans (only parsing). -Notation Zle_lt_trans := Z.le_lt_trans (only parsing). +Notation Zlt_le_trans := Z.lt_le_trans (compat "8.3"). +Notation Zle_lt_trans := Z.le_lt_trans (compat "8.3"). Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p. Proof. @@ -187,7 +189,7 @@ Qed. (** Transitivity of large orders *) -Notation Zle_trans := Z.le_trans (only parsing). +Notation Zle_trans := Z.le_trans (compat "8.3"). Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p. Proof. @@ -238,8 +240,8 @@ Qed. (** Special base instances of order *) -Notation Zlt_succ := Z.lt_succ_diag_r (only parsing). -Notation Zlt_pred := Z.lt_pred_l (only parsing). +Notation Zlt_succ := Z.lt_succ_diag_r (compat "8.3"). +Notation Zlt_pred := Z.lt_pred_l (compat "8.3"). Lemma Zgt_succ n : Z.succ n > n. Proof. @@ -253,8 +255,8 @@ Qed. (** Relating strict and large order using successor or predecessor *) -Notation Zlt_succ_r := Z.lt_succ_r (only parsing). -Notation Zle_succ_l := Z.le_succ_l (only parsing). +Notation Zlt_succ_r := Z.lt_succ_r (compat "8.3"). +Notation Zle_succ_l := Z.le_succ_l (compat "8.3"). Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m. Proof. @@ -293,10 +295,10 @@ Qed. (** Weakening order *) -Notation Zle_succ := Z.le_succ_diag_r (only parsing). -Notation Zle_pred := Z.le_pred_l (only parsing). -Notation Zlt_lt_succ := Z.lt_lt_succ_r (only parsing). -Notation Zle_le_succ := Z.le_le_succ_r (only parsing). +Notation Zle_succ := Z.le_succ_diag_r (compat "8.3"). +Notation Zle_pred := Z.le_pred_l (compat "8.3"). +Notation Zlt_lt_succ := Z.lt_lt_succ_r (compat "8.3"). +Notation Zle_le_succ := Z.le_le_succ_r (compat "8.3"). Lemma Zle_succ_le n m : Z.succ n <= m -> n <= m. Proof. @@ -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 *) @@ -332,8 +334,8 @@ Qed. (** Special cases of ordered integers *) -Notation Zlt_0_1 := Z.lt_0_1 (only parsing). -Notation Zle_0_1 := Z.le_0_1 (only parsing). +Notation Zlt_0_1 := Z.lt_0_1 (compat "8.3"). +Notation Zle_0_1 := Z.le_0_1 (compat "8.3"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. @@ -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 *) @@ -373,10 +375,10 @@ Qed. (** ** Addition *) (** Compatibility of addition wrt to order *) -Notation Zplus_lt_le_compat := Z.add_lt_le_mono (only parsing). -Notation Zplus_le_lt_compat := Z.add_le_lt_mono (only parsing). -Notation Zplus_le_compat := Z.add_le_mono (only parsing). -Notation Zplus_lt_compat := Z.add_lt_mono (only parsing). +Notation Zplus_lt_le_compat := Z.add_lt_le_mono (compat "8.3"). +Notation Zplus_le_lt_compat := Z.add_le_lt_mono (compat "8.3"). +Notation Zplus_le_compat := Z.add_le_mono (compat "8.3"). +Notation Zplus_lt_compat := Z.add_lt_mono (compat "8.3"). Lemma Zplus_gt_compat_l n m p : n > m -> p + n > p + m. Proof. @@ -410,7 +412,7 @@ Qed. (** Compatibility of addition wrt to being positive *) -Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (only parsing). +Notation Zplus_le_0_compat := Z.add_nonneg_nonneg (compat "8.3"). (** Simplification of addition wrt to order *) @@ -568,9 +570,9 @@ Qed. (** Compatibility of multiplication by a positive wrt to being positive *) -Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (only parsing). -Notation Zmult_lt_0_compat := Z.mul_pos_pos (only parsing). -Notation Zmult_lt_O_compat := Z.mul_pos_pos (only parsing). +Notation Zmult_le_0_compat := Z.mul_nonneg_nonneg (compat "8.3"). +Notation Zmult_lt_0_compat := Z.mul_pos_pos (compat "8.3"). +Notation Zmult_lt_O_compat := Z.mul_pos_pos (compat "8.3"). Lemma Zmult_gt_0_compat n m : n > 0 -> m > 0 -> n * m > 0. Proof. @@ -622,9 +624,9 @@ Qed. (** * Equivalence between inequalities *) -Notation Zle_plus_swap := Z.le_add_le_sub_r (only parsing). -Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (only parsing). -Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (only parsing). +Notation Zle_plus_swap := Z.le_add_le_sub_r (compat "8.3"). +Notation Zlt_plus_swap := Z.lt_add_lt_sub_r (compat "8.3"). +Notation Zlt_minus_simpl_swap := Z.lt_sub_pos (compat "8.3"). Lemma Zeq_plus_swap n m p : n + p = m <-> n = m - p. Proof. diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v index a90eedb4..f3eb63a8 100644 --- a/theories/ZArith/Zpow_alt.v +++ b/theories/ZArith/Zpow_alt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 6f1ebc06..a1c60bf2 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,12 +14,12 @@ Local Open Scope Z_scope. (** Nota : this file is mostly deprecated. The definition of [Z.pow] and its usual properties are now provided by module [BinInt.Z]. *) -Notation Zpower_pos := Z.pow_pos (only parsing). -Notation Zpower := Z.pow (only parsing). -Notation Zpower_0_r := Z.pow_0_r (only parsing). -Notation Zpower_succ_r := Z.pow_succ_r (only parsing). -Notation Zpower_neg_r := Z.pow_neg_r (only parsing). -Notation Zpower_Ppow := Z.pow_Zpos (only parsing). +Notation Zpower_pos := Z.pow_pos (compat "8.3"). +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 := 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 27e3def4..8ff641a3 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,17 +29,17 @@ Proof. now apply (Z.pow_0_l (Zpos p)). Qed. Lemma Zpower_pos_pos x p : 0 < x -> 0 < Z.pow_pos x p. Proof. intros. now apply (Z.pow_pos_nonneg x (Zpos p)). Qed. -Notation Zpower_1_r := Z.pow_1_r (only parsing). -Notation Zpower_1_l := Z.pow_1_l (only parsing). -Notation Zpower_0_l := Z.pow_0_l' (only parsing). -Notation Zpower_0_r := Z.pow_0_r (only parsing). -Notation Zpower_2 := Z.pow_2_r (only parsing). -Notation Zpower_gt_0 := Z.pow_pos_nonneg (only parsing). -Notation Zpower_ge_0 := Z.pow_nonneg (only parsing). -Notation Zpower_Zabs := Z.abs_pow (only parsing). -Notation Zpower_Zsucc := Z.pow_succ_r (only parsing). -Notation Zpower_mult := Z.pow_mul_r (only parsing). -Notation Zpower_le_monotone2 := Z.pow_le_mono_r (only parsing). +Notation Zpower_1_r := Z.pow_1_r (compat "8.3"). +Notation Zpower_1_l := Z.pow_1_l (compat "8.3"). +Notation Zpower_0_l := Z.pow_0_l' (compat "8.3"). +Notation Zpower_0_r := Z.pow_0_r (compat "8.3"). +Notation Zpower_2 := Z.pow_2_r (compat "8.3"). +Notation Zpower_gt_0 := Z.pow_pos_nonneg (compat "8.3"). +Notation Zpower_ge_0 := Z.pow_nonneg (compat "8.3"). +Notation Zpower_Zabs := Z.abs_pow (compat "8.3"). +Notation Zpower_Zsucc := Z.pow_succ_r (compat "8.3"). +Notation Zpower_mult := Z.pow_mul_r (compat "8.3"). +Notation Zpower_le_monotone2 := Z.pow_le_mono_r (compat "8.3"). Theorem Zpower_le_monotone a b c : 0 < a -> 0 <= b <= c -> a^b <= a^c. @@ -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,9 +231,9 @@ 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 (only parsing). -Notation Zsquare := Z.square (only parsing). -Notation Psquare_correct := Pos.square_spec (only parsing). -Notation Zsquare_correct := Z.square_spec (only parsing). +Notation Psquare := Pos.square (compat "8.3"). +Notation Zsquare := Z.square (compat "8.3"). +Notation Psquare_correct := Pos.square_spec (compat "8.3"). +Notation Zsquare_correct := Z.square_spec (compat "8.3"). diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 5052d01a..0d9b08d6 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 9a95669f..c02f0ae6 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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' (only parsing). +(* The precise equalities that are invalid with "historic" Zdiv. *) -(** Then, the inequalities constraining the remainder: - The remainder is bounded by the divisor, in term of absolute values *) +Theorem Zquot_opp_l a b : (-a)÷b = -(a÷b). +Proof. zero_or_not b. now apply Z.quot_opp_l. 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 Zquot_opp_r a b : a÷(-b) = -(a÷b). +Proof. zero_or_not b. now apply Z.quot_opp_r. 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 4584c3f8..a6c83241 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ Require Import ZArithRing. Require Import Omega. Require Export ZArith_base. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (** THIS FILE IS DEPRECATED @@ -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 30802f82..e07fc715 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ Require Import ZArith_base. Require Export Wf_nat. Require Import Omega. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (** Well-founded relations on Z. *) @@ -29,28 +29,28 @@ 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. + red; intros. assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a). clear a; simple induction n; intros. (** n= 0 *) case H; intros. case (lt_n_O (f a)); auto. - apply Acc_intro; unfold Zwf in |- *; intros. + apply Acc_intro; unfold Zwf; intros. assert False; omega || contradiction. (** inductive case *) case H0; clear H0; intro; auto. 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. diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 742f4bde..af7d5a2e 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |