From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- theories/Numbers/Integer/Abstract/ZAdd.v | 2 +- theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZAxioms.v | 2 +- theories/Numbers/Integer/Abstract/ZBase.v | 2 +- theories/Numbers/Integer/Abstract/ZBits.v | 4 +- theories/Numbers/Integer/Abstract/ZDivEucl.v | 2 +- theories/Numbers/Integer/Abstract/ZDivFloor.v | 4 +- theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +- theories/Numbers/Integer/Abstract/ZGcd.v | 2 +- theories/Numbers/Integer/Abstract/ZLcm.v | 2 +- theories/Numbers/Integer/Abstract/ZLt.v | 2 +- theories/Numbers/Integer/Abstract/ZMaxMin.v | 2 +- theories/Numbers/Integer/Abstract/ZMul.v | 2 +- theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 +- theories/Numbers/Integer/Abstract/ZParity.v | 2 +- theories/Numbers/Integer/Abstract/ZPow.v | 13 +- theories/Numbers/Integer/Abstract/ZProperties.v | 2 +- theories/Numbers/Integer/Abstract/ZSgnAbs.v | 2 +- theories/Numbers/Integer/BigZ/BigZ.v | 10 +- theories/Numbers/Integer/BigZ/ZMake.v | 454 ++++++++++++------------ theories/Numbers/Integer/Binary/ZBinary.v | 4 +- theories/Numbers/Integer/NatPairs/ZNatPairs.v | 4 +- theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 +- theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 6 +- 24 files changed, 271 insertions(+), 260 deletions(-) (limited to 'theories/Numbers/Integer') diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 647ab0ac..ac113dfd 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* even (a^b) = even a. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index c0455196..8973df35 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* x==y. Proof. now apply BigZ.eqb_eq. Qed. -Definition BigZ_of_N n := BigZ.of_Z (Z_of_N n). +Definition BigZ_of_N n := BigZ.of_Z (Z.of_N n). Lemma BigZpower : power_theory 1 BigZ.mul BigZ.eq BigZ_of_N BigZ.pow. Proof. @@ -139,7 +139,7 @@ BigZ.zify. auto with zarith. intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). -destruct BigZ.div_eucl as (q,r), Zdiv_eucl as (q',r'). +destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). intros (EQ,_). injection 1. intros EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 0142b36b..180fe0a9 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* t_ - | Neg : N.t -> t_. + | Pos : NN.t -> t_ + | Neg : NN.t -> t_. Definition t := t_. Bind Scope abstract_scope with t t_. - Definition zero := Pos N.zero. - Definition one := Pos N.one. - Definition two := Pos N.two. - Definition minus_one := Neg N.one. + Definition zero := Pos NN.zero. + Definition one := Pos NN.one. + Definition two := Pos NN.two. + Definition minus_one := Neg NN.one. Definition of_Z x := match x with - | Zpos x => Pos (N.of_N (Npos x)) + | Zpos x => Pos (NN.of_N (Npos x)) | Z0 => zero - | Zneg x => Neg (N.of_N (Npos x)) + | Zneg x => Neg (NN.of_N (Npos x)) end. Definition to_Z x := match x with - | Pos nx => N.to_Z nx - | Neg nx => Zopp (N.to_Z nx) + | Pos nx => NN.to_Z nx + | Neg nx => Z.opp (NN.to_Z nx) end. Theorem spec_of_Z: forall x, to_Z (of_Z x) = x. Proof. intros x; case x; unfold to_Z, of_Z, zero. - exact N.spec_0. - intros; rewrite N.spec_of_N; auto. - intros; rewrite N.spec_of_N; auto. + exact NN.spec_0. + intros; rewrite NN.spec_of_N; auto. + intros; rewrite NN.spec_of_N; auto. Qed. Definition eq x y := (to_Z x = to_Z y). Theorem spec_0: to_Z zero = 0. - exact N.spec_0. + exact NN.spec_0. Qed. Theorem spec_1: to_Z one = 1. - exact N.spec_1. + exact NN.spec_1. Qed. Theorem spec_2: to_Z two = 2. - exact N.spec_2. + exact NN.spec_2. Qed. Theorem spec_m1: to_Z minus_one = -1. - simpl; rewrite N.spec_1; auto. + simpl; rewrite NN.spec_1; auto. Qed. Definition compare x y := match x, y with - | Pos nx, Pos ny => N.compare nx ny + | Pos nx, Pos ny => NN.compare nx ny | Pos nx, Neg ny => - match N.compare nx N.zero with + match NN.compare nx NN.zero with | Gt => Gt - | _ => N.compare ny N.zero + | _ => NN.compare ny NN.zero end | Neg nx, Pos ny => - match N.compare N.zero nx with + match NN.compare NN.zero nx with | Lt => Lt - | _ => N.compare N.zero ny + | _ => NN.compare NN.zero ny end - | Neg nx, Neg ny => N.compare ny nx + | Neg nx, Neg ny => NN.compare ny nx end. Theorem spec_compare : - forall x y, compare x y = Zcompare (to_Z x) (to_Z y). + forall x y, compare x y = Z.compare (to_Z x) (to_Z y). Proof. unfold compare, to_Z. destruct x as [x|x], y as [y|y]; - rewrite ?N.spec_compare, ?N.spec_0, <-?Zcompare_opp; auto; - assert (Hx:=N.spec_pos x); assert (Hy:=N.spec_pos y); - set (X:=N.to_Z x) in *; set (Y:=N.to_Z y) in *; clearbody X Y. - destruct (Zcompare_spec X 0) as [EQ|LT|GT]. - rewrite EQ. rewrite <- Zopp_0 at 2. apply Zcompare_opp. - exfalso. omega. - symmetry. change (X > -Y). omega. - destruct (Zcompare_spec 0 X) as [EQ|LT|GT]. - rewrite <- EQ. rewrite Zopp_0; auto. - symmetry. change (-X < Y). omega. - exfalso. omega. + rewrite ?NN.spec_compare, ?NN.spec_0, ?Z.compare_opp; auto; + assert (Hx:=NN.spec_pos x); assert (Hy:=NN.spec_pos y); + set (X:=NN.to_Z x) in *; set (Y:=NN.to_Z y) in *; clearbody X Y. + - destruct (Z.compare_spec X 0) as [EQ|LT|GT]. + + rewrite <- Z.opp_0 in EQ. now rewrite EQ, Z.compare_opp. + + exfalso. omega. + + symmetry. change (X > -Y). omega. + - destruct (Z.compare_spec 0 X) as [EQ|LT|GT]. + + rewrite <- EQ, Z.opp_0; auto. + + symmetry. change (-X < Y). omega. + + exfalso. omega. Qed. Definition eqb x y := @@ -155,14 +155,14 @@ Module Make (N:NType) <: ZType. Definition min n m := match compare n m with Gt => m | _ => n end. Definition max n m := match compare n m with Lt => m | _ => n end. - Theorem spec_min : forall n m, to_Z (min n m) = Zmin (to_Z n) (to_Z m). + Theorem spec_min : forall n m, to_Z (min n m) = Z.min (to_Z n) (to_Z m). Proof. - unfold min, Zmin. intros. rewrite spec_compare. destruct Zcompare; auto. + unfold min, Z.min. intros. rewrite spec_compare. destruct Z.compare; auto. Qed. - Theorem spec_max : forall n m, to_Z (max n m) = Zmax (to_Z n) (to_Z m). + Theorem spec_max : forall n m, to_Z (max n m) = Z.max (to_Z n) (to_Z m). Proof. - unfold max, Zmax. intros. rewrite spec_compare. destruct Zcompare; auto. + unfold max, Z.max. intros. rewrite spec_compare. destruct Z.compare; auto. Qed. Definition to_N x := @@ -173,11 +173,11 @@ Module Make (N:NType) <: ZType. Definition abs x := Pos (to_N x). - Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z x). + Theorem spec_abs: forall x, to_Z (abs x) = Z.abs (to_Z x). Proof. - intros x; case x; clear x; intros x; assert (F:=N.spec_pos x). - simpl; rewrite Zabs_eq; auto. - simpl; rewrite Zabs_non_eq; simpl; auto with zarith. + intros x; case x; clear x; intros x; assert (F:=NN.spec_pos x). + simpl; rewrite Z.abs_eq; auto. + simpl; rewrite Z.abs_neq; simpl; auto with zarith. Qed. Definition opp x := @@ -193,10 +193,10 @@ Module Make (N:NType) <: ZType. Definition succ x := match x with - | Pos n => Pos (N.succ n) + | Pos n => Pos (NN.succ n) | Neg n => - match N.compare N.zero n with - | Lt => Neg (N.pred n) + match NN.compare NN.zero n with + | Lt => Neg (NN.pred n) | _ => one end end. @@ -204,134 +204,134 @@ Module Make (N:NType) <: ZType. Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1. Proof. intros x; case x; clear x; intros x. - exact (N.spec_succ x). - simpl. rewrite N.spec_compare. case Zcompare_spec; rewrite ?N.spec_0; simpl. - intros HH; rewrite <- HH; rewrite N.spec_1; ring. - intros HH; rewrite N.spec_pred, Zmax_r; auto with zarith. - generalize (N.spec_pos x); auto with zarith. + exact (NN.spec_succ x). + simpl. rewrite NN.spec_compare. case Z.compare_spec; rewrite ?NN.spec_0; simpl. + intros HH; rewrite <- HH; rewrite NN.spec_1; ring. + intros HH; rewrite NN.spec_pred, Z.max_r; auto with zarith. + generalize (NN.spec_pos x); auto with zarith. Qed. Definition add x y := match x, y with - | Pos nx, Pos ny => Pos (N.add nx ny) + | Pos nx, Pos ny => Pos (NN.add nx ny) | Pos nx, Neg ny => - match N.compare nx ny with - | Gt => Pos (N.sub nx ny) + match NN.compare nx ny with + | Gt => Pos (NN.sub nx ny) | Eq => zero - | Lt => Neg (N.sub ny nx) + | Lt => Neg (NN.sub ny nx) end | Neg nx, Pos ny => - match N.compare nx ny with - | Gt => Neg (N.sub nx ny) + match NN.compare nx ny with + | Gt => Neg (NN.sub nx ny) | Eq => zero - | Lt => Pos (N.sub ny nx) + | Lt => Pos (NN.sub ny nx) end - | Neg nx, Neg ny => Neg (N.add nx ny) + | Neg nx, Neg ny => Neg (NN.add nx ny) end. Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. Proof. unfold add, to_Z; intros [x | x] [y | y]; - try (rewrite N.spec_add; auto with zarith); - rewrite N.spec_compare; case Zcompare_spec; - unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *. + try (rewrite NN.spec_add; auto with zarith); + rewrite NN.spec_compare; case Z.compare_spec; + unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. Qed. Definition pred x := match x with | Pos nx => - match N.compare N.zero nx with - | Lt => Pos (N.pred nx) + match NN.compare NN.zero nx with + | Lt => Pos (NN.pred nx) | _ => minus_one end - | Neg nx => Neg (N.succ nx) + | Neg nx => Neg (NN.succ nx) end. Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. Proof. unfold pred, to_Z, minus_one; intros [x | x]; - try (rewrite N.spec_succ; ring). - rewrite N.spec_compare; case Zcompare_spec; - rewrite ?N.spec_0, ?N.spec_1, ?N.spec_pred; - generalize (N.spec_pos x); omega with *. + try (rewrite NN.spec_succ; ring). + rewrite NN.spec_compare; case Z.compare_spec; + rewrite ?NN.spec_0, ?NN.spec_1, ?NN.spec_pred; + generalize (NN.spec_pos x); omega with *. Qed. Definition sub x y := match x, y with | Pos nx, Pos ny => - match N.compare nx ny with - | Gt => Pos (N.sub nx ny) + match NN.compare nx ny with + | Gt => Pos (NN.sub nx ny) | Eq => zero - | Lt => Neg (N.sub ny nx) + | Lt => Neg (NN.sub ny nx) end - | Pos nx, Neg ny => Pos (N.add nx ny) - | Neg nx, Pos ny => Neg (N.add nx ny) + | Pos nx, Neg ny => Pos (NN.add nx ny) + | Neg nx, Pos ny => Neg (NN.add nx ny) | Neg nx, Neg ny => - match N.compare nx ny with - | Gt => Neg (N.sub nx ny) + match NN.compare nx ny with + | Gt => Neg (NN.sub nx ny) | Eq => zero - | Lt => Pos (N.sub ny nx) + | Lt => Pos (NN.sub ny nx) end end. Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. Proof. unfold sub, to_Z; intros [x | x] [y | y]; - try (rewrite N.spec_add; auto with zarith); - rewrite N.spec_compare; case Zcompare_spec; - unfold zero; rewrite ?N.spec_0, ?N.spec_sub; omega with *. + try (rewrite NN.spec_add; auto with zarith); + rewrite NN.spec_compare; case Z.compare_spec; + unfold zero; rewrite ?NN.spec_0, ?NN.spec_sub; omega with *. Qed. Definition mul x y := match x, y with - | Pos nx, Pos ny => Pos (N.mul nx ny) - | Pos nx, Neg ny => Neg (N.mul nx ny) - | Neg nx, Pos ny => Neg (N.mul nx ny) - | Neg nx, Neg ny => Pos (N.mul nx ny) + | Pos nx, Pos ny => Pos (NN.mul nx ny) + | Pos nx, Neg ny => Neg (NN.mul nx ny) + | Neg nx, Pos ny => Neg (NN.mul nx ny) + | Neg nx, Neg ny => Pos (NN.mul nx ny) end. Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. Proof. - unfold mul, to_Z; intros [x | x] [y | y]; rewrite N.spec_mul; ring. + unfold mul, to_Z; intros [x | x] [y | y]; rewrite NN.spec_mul; ring. Qed. Definition square x := match x with - | Pos nx => Pos (N.square nx) - | Neg nx => Pos (N.square nx) + | Pos nx => Pos (NN.square nx) + | Neg nx => Pos (NN.square nx) end. Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. Proof. - unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring. + unfold square, to_Z; intros [x | x]; rewrite NN.spec_square; ring. Qed. Definition pow_pos x p := match x with - | Pos nx => Pos (N.pow_pos nx p) + | Pos nx => Pos (NN.pow_pos nx p) | Neg nx => match p with | xH => x - | xO _ => Pos (N.pow_pos nx p) - | xI _ => Neg (N.pow_pos nx p) + | xO _ => Pos (NN.pow_pos nx p) + | xI _ => Neg (NN.pow_pos nx p) end end. Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n. Proof. assert (F0: forall x, (-x)^2 = x^2). - intros x; rewrite Zpower_2; ring. + intros x; rewrite Z.pow_2_r; ring. unfold pow_pos, to_Z; intros [x | x] [p | p |]; - try rewrite N.spec_pow_pos; try ring. + try rewrite NN.spec_pow_pos; try ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. - rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Zpower_mult; auto with zarith. + rewrite Pos2Z.inj_xI; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Z.pow_mul_r; auto with zarith. rewrite F0; ring. assert (F: 0 <= 2 * Zpos p). assert (0 <= Zpos p); auto with zarith. - rewrite Zpos_xO; repeat rewrite Zpower_exp; auto with zarith. - repeat rewrite Zpower_mult; auto with zarith. + rewrite Pos2Z.inj_xO; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Z.pow_mul_r; auto with zarith. rewrite F0; ring. Qed. @@ -341,9 +341,9 @@ Module Make (N:NType) <: ZType. | Npos p => pow_pos x p end. - Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z_of_N n. + Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z.of_N n. Proof. - destruct n; simpl. apply N.spec_1. + destruct n; simpl. apply NN.spec_1. apply spec_pow_pos. Qed. @@ -357,38 +357,38 @@ Module Make (N:NType) <: ZType. Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y. Proof. intros. unfold pow. destruct (to_Z y); simpl. - apply N.spec_1. + apply NN.spec_1. apply spec_pow_pos. - apply N.spec_0. + apply NN.spec_0. Qed. Definition log2 x := match x with - | Pos nx => Pos (N.log2 nx) + | Pos nx => Pos (NN.log2 nx) | Neg nx => zero end. Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x). Proof. - intros. destruct x as [p|p]; simpl. apply N.spec_log2. - rewrite N.spec_0. - destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ]. + intros. destruct x as [p|p]; simpl. apply NN.spec_log2. + rewrite NN.spec_0. + destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. rewrite Z.log2_nonpos; auto with zarith. now rewrite <- EQ. Qed. Definition sqrt x := match x with - | Pos nx => Pos (N.sqrt nx) - | Neg nx => Neg N.zero + | Pos nx => Pos (NN.sqrt nx) + | Neg nx => Neg NN.zero end. Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x). Proof. destruct x as [p|p]; simpl. - apply N.spec_sqrt. - rewrite N.spec_0. - destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ]. + apply NN.spec_sqrt. + rewrite NN.spec_0. + destruct (Z_le_lt_eq_dec _ _ (NN.spec_pos p)) as [LT|EQ]. rewrite Z.sqrt_neg; auto with zarith. now rewrite <- EQ. Qed. @@ -396,68 +396,68 @@ Module Make (N:NType) <: ZType. Definition div_eucl x y := match x, y with | Pos nx, Pos ny => - let (q, r) := N.div_eucl nx ny in + let (q, r) := NN.div_eucl nx ny in (Pos q, Pos r) | Pos nx, Neg ny => - let (q, r) := N.div_eucl nx ny in - if N.eqb N.zero r + let (q, r) := NN.div_eucl nx ny in + if NN.eqb NN.zero r then (Neg q, zero) - else (Neg (N.succ q), Neg (N.sub ny r)) + else (Neg (NN.succ q), Neg (NN.sub ny r)) | Neg nx, Pos ny => - let (q, r) := N.div_eucl nx ny in - if N.eqb N.zero r + let (q, r) := NN.div_eucl nx ny in + if NN.eqb NN.zero r then (Neg q, zero) - else (Neg (N.succ q), Pos (N.sub ny r)) + else (Neg (NN.succ q), Pos (NN.sub ny r)) | Neg nx, Neg ny => - let (q, r) := N.div_eucl nx ny in + let (q, r) := NN.div_eucl nx ny in (Pos q, Neg r) end. Ltac break_nonneg x px EQx := let H := fresh "H" in - assert (H:=N.spec_pos x); - destruct (N.to_Z x) as [|px|px]_eqn:EQx; + assert (H:=NN.spec_pos x); + destruct (NN.to_Z x) as [|px|px] eqn:EQx; [clear H|clear H|elim H; reflexivity]. Theorem spec_div_eucl: forall x y, let (q,r) := div_eucl x y in - (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). + (to_Z q, to_Z r) = Z.div_eucl (to_Z x) (to_Z y). Proof. unfold div_eucl, to_Z. intros [x | x] [y | y]. (* Pos Pos *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y); auto. + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y); auto. (* Pos Neg *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr; - simpl; rewrite Hq, N.spec_0; auto). + try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos py) with (Zneg py). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). intros (EQ,MOD). injection 1. intros Hr' Hq'. - rewrite N.spec_eqb, N.spec_0, Hr'. + rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. - subst; simpl. rewrite N.spec_0; auto. + subst; simpl. rewrite NN.spec_0; auto. subst. lazy iota beta delta [Z.eqb]. - rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. (* Neg Pos *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite N.spec_eqb, N.spec_0, Hr; - simpl; rewrite Hq, N.spec_0; auto). + try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos px) with (Zneg px). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). - unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). intros (EQ,MOD). injection 1. intros Hr' Hq'. - rewrite N.spec_eqb, N.spec_0, Hr'. + rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. - subst; simpl. rewrite N.spec_0; auto. + subst; simpl. rewrite NN.spec_0; auto. subst. lazy iota beta delta [Z.eqb]. - rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + rewrite NN.spec_sub, NN.spec_succ, EQy, EQr. f_equal. omega with *. (* Neg Neg *) - generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto). simpl. intros <-; auto. @@ -468,8 +468,8 @@ Module Make (N:NType) <: ZType. Definition spec_div: forall x y, to_Z (div x y) = to_Z x / to_Z y. Proof. - intros x y; generalize (spec_div_eucl x y); unfold div, Zdiv. - case div_eucl; case Zdiv_eucl; simpl; auto. + intros x y; generalize (spec_div_eucl x y); unfold div, Z.div. + case div_eucl; case Z.div_eucl; simpl; auto. intros q r q11 r1 H; injection H; auto. Qed. @@ -478,38 +478,38 @@ Module Make (N:NType) <: ZType. Theorem spec_modulo: forall x y, to_Z (modulo x y) = to_Z x mod to_Z y. Proof. - intros x y; generalize (spec_div_eucl x y); unfold modulo, Zmod. - case div_eucl; case Zdiv_eucl; simpl; auto. + intros x y; generalize (spec_div_eucl x y); unfold modulo, Z.modulo. + case div_eucl; case Z.div_eucl; simpl; auto. intros q r q11 r1 H; injection H; auto. Qed. Definition quot x y := match x, y with - | Pos nx, Pos ny => Pos (N.div nx ny) - | Pos nx, Neg ny => Neg (N.div nx ny) - | Neg nx, Pos ny => Neg (N.div nx ny) - | Neg nx, Neg ny => Pos (N.div nx ny) + | Pos nx, Pos ny => Pos (NN.div nx ny) + | Pos nx, Neg ny => Neg (NN.div nx ny) + | Neg nx, Pos ny => Neg (NN.div nx ny) + | Neg nx, Neg ny => Pos (NN.div nx ny) end. Definition rem x y := if eqb y zero then x else match x, y with - | Pos nx, Pos ny => Pos (N.modulo nx ny) - | Pos nx, Neg ny => Pos (N.modulo nx ny) - | Neg nx, Pos ny => Neg (N.modulo nx ny) - | Neg nx, Neg ny => Neg (N.modulo nx ny) + | Pos nx, Pos ny => Pos (NN.modulo nx ny) + | Pos nx, Neg ny => Pos (NN.modulo nx ny) + | Neg nx, Pos ny => Neg (NN.modulo nx ny) + | Neg nx, Neg ny => Neg (NN.modulo nx ny) end. Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y). Proof. - intros [x|x] [y|y]; simpl; symmetry; rewrite N.spec_div; + intros [x|x] [y|y]; simpl; symmetry; rewrite NN.spec_div; (* Nota: we rely here on [forall a b, a ÷ 0 = b / 0] *) - destruct (Z.eq_dec (N.to_Z y) 0) as [EQ|NEQ]; - try (rewrite EQ; now destruct (N.to_Z x)); + destruct (Z.eq_dec (NN.to_Z y) 0) as [EQ|NEQ]; + try (rewrite EQ; now destruct (NN.to_Z x)); rewrite ?Z.quot_opp_r, ?Z.quot_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; trivial; apply Z.quot_div_nonneg; - generalize (N.spec_pos x) (N.spec_pos y); Z.order. + generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. Qed. Lemma spec_rem : forall x y, @@ -521,26 +521,26 @@ Module Make (N:NType) <: ZType. rewrite Hy. now destruct (to_Z x). destruct x as [x|x], y as [y|y]; simpl in *; symmetry; rewrite ?Z.eq_opp_l, ?Z.opp_0 in Hy; - rewrite N.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive, + rewrite NN.spec_modulo, ?Z.rem_opp_r, ?Z.rem_opp_l, ?Z.opp_involutive, ?Z.opp_inj_wd; trivial; apply Z.rem_mod_nonneg; - generalize (N.spec_pos x) (N.spec_pos y); Z.order. + generalize (NN.spec_pos x) (NN.spec_pos y); Z.order. Qed. Definition gcd x y := match x, y with - | Pos nx, Pos ny => Pos (N.gcd nx ny) - | Pos nx, Neg ny => Pos (N.gcd nx ny) - | Neg nx, Pos ny => Pos (N.gcd nx ny) - | Neg nx, Neg ny => Pos (N.gcd nx ny) + | Pos nx, Pos ny => Pos (NN.gcd nx ny) + | Pos nx, Neg ny => Pos (NN.gcd nx ny) + | Neg nx, Pos ny => Pos (NN.gcd nx ny) + | Neg nx, Neg ny => Pos (NN.gcd nx ny) end. - Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b). + Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b). Proof. - unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd; - auto; case N.to_Z; simpl; auto with zarith; - try rewrite Zabs_Zopp; auto; - case N.to_Z; simpl; auto with zarith. + unfold gcd, Z.gcd, to_Z; intros [x | x] [y | y]; rewrite NN.spec_gcd; unfold Z.gcd; + auto; case NN.to_Z; simpl; auto with zarith; + try rewrite Z.abs_opp; auto; + case NN.to_Z; simpl; auto with zarith. Qed. Definition sgn x := @@ -550,124 +550,124 @@ Module Make (N:NType) <: ZType. | Gt => minus_one end. - Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x). + Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x). Proof. - intros. unfold sgn. rewrite spec_compare. case Zcompare_spec. + intros. unfold sgn. rewrite spec_compare. case Z.compare_spec. rewrite spec_0. intros <-; auto. - rewrite spec_0, spec_1. symmetry. rewrite Zsgn_pos; auto. - rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith. + rewrite spec_0, spec_1. symmetry. rewrite Z.sgn_pos_iff; auto. + rewrite spec_0, spec_m1. symmetry. rewrite Z.sgn_neg_iff; auto with zarith. Qed. Definition even z := match z with - | Pos n => N.even n - | Neg n => N.even n + | Pos n => NN.even n + | Neg n => NN.even n end. Definition odd z := match z with - | Pos n => N.odd n - | Neg n => N.odd n + | Pos n => NN.odd n + | Neg n => NN.odd n end. - Lemma spec_even : forall z, even z = Zeven_bool (to_Z z). + Lemma spec_even : forall z, even z = Z.even (to_Z z). Proof. - intros [n|n]; simpl; rewrite N.spec_even; trivial. - destruct (N.to_Z n) as [|p|p]; now try destruct p. + intros [n|n]; simpl; rewrite NN.spec_even; trivial. + destruct (NN.to_Z n) as [|p|p]; now try destruct p. Qed. - Lemma spec_odd : forall z, odd z = Zodd_bool (to_Z z). + Lemma spec_odd : forall z, odd z = Z.odd (to_Z z). Proof. - intros [n|n]; simpl; rewrite N.spec_odd; trivial. - destruct (N.to_Z n) as [|p|p]; now try destruct p. + intros [n|n]; simpl; rewrite NN.spec_odd; trivial. + destruct (NN.to_Z n) as [|p|p]; now try destruct p. Qed. Definition norm_pos z := match z with | Pos _ => z - | Neg n => if N.eqb n N.zero then Pos n else z + | Neg n => if NN.eqb n NN.zero then Pos n else z end. Definition testbit a n := match norm_pos n, norm_pos a with - | Pos p, Pos a => N.testbit a p - | Pos p, Neg a => negb (N.testbit (N.pred a) p) + | Pos p, Pos a => NN.testbit a p + | Pos p, Neg a => negb (NN.testbit (NN.pred a) p) | Neg p, _ => false end. Definition shiftl a n := match norm_pos a, n with - | Pos a, Pos n => Pos (N.shiftl a n) - | Pos a, Neg n => Pos (N.shiftr a n) - | Neg a, Pos n => Neg (N.shiftl a n) - | Neg a, Neg n => Neg (N.succ (N.shiftr (N.pred a) n)) + | Pos a, Pos n => Pos (NN.shiftl a n) + | Pos a, Neg n => Pos (NN.shiftr a n) + | Neg a, Pos n => Neg (NN.shiftl a n) + | Neg a, Neg n => Neg (NN.succ (NN.shiftr (NN.pred a) n)) end. Definition shiftr a n := shiftl a (opp n). Definition lor a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.lor a b) - | Neg a, Pos b => Neg (N.succ (N.ldiff (N.pred a) b)) - | Pos a, Neg b => Neg (N.succ (N.ldiff (N.pred b) a)) - | Neg a, Neg b => Neg (N.succ (N.land (N.pred a) (N.pred b))) + | Pos a, Pos b => Pos (NN.lor a b) + | Neg a, Pos b => Neg (NN.succ (NN.ldiff (NN.pred a) b)) + | Pos a, Neg b => Neg (NN.succ (NN.ldiff (NN.pred b) a)) + | Neg a, Neg b => Neg (NN.succ (NN.land (NN.pred a) (NN.pred b))) end. Definition land a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.land a b) - | Neg a, Pos b => Pos (N.ldiff b (N.pred a)) - | Pos a, Neg b => Pos (N.ldiff a (N.pred b)) - | Neg a, Neg b => Neg (N.succ (N.lor (N.pred a) (N.pred b))) + | Pos a, Pos b => Pos (NN.land a b) + | Neg a, Pos b => Pos (NN.ldiff b (NN.pred a)) + | Pos a, Neg b => Pos (NN.ldiff a (NN.pred b)) + | Neg a, Neg b => Neg (NN.succ (NN.lor (NN.pred a) (NN.pred b))) end. Definition ldiff a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.ldiff a b) - | Neg a, Pos b => Neg (N.succ (N.lor (N.pred a) b)) - | Pos a, Neg b => Pos (N.land a (N.pred b)) - | Neg a, Neg b => Pos (N.ldiff (N.pred b) (N.pred a)) + | Pos a, Pos b => Pos (NN.ldiff a b) + | Neg a, Pos b => Neg (NN.succ (NN.lor (NN.pred a) b)) + | Pos a, Neg b => Pos (NN.land a (NN.pred b)) + | Neg a, Neg b => Pos (NN.ldiff (NN.pred b) (NN.pred a)) end. Definition lxor a b := match norm_pos a, norm_pos b with - | Pos a, Pos b => Pos (N.lxor a b) - | Neg a, Pos b => Neg (N.succ (N.lxor (N.pred a) b)) - | Pos a, Neg b => Neg (N.succ (N.lxor a (N.pred b))) - | Neg a, Neg b => Pos (N.lxor (N.pred a) (N.pred b)) + | Pos a, Pos b => Pos (NN.lxor a b) + | Neg a, Pos b => Neg (NN.succ (NN.lxor (NN.pred a) b)) + | Pos a, Neg b => Neg (NN.succ (NN.lxor a (NN.pred b))) + | Neg a, Neg b => Pos (NN.lxor (NN.pred a) (NN.pred b)) end. Definition div2 x := shiftr x one. Lemma Zlnot_alt1 : forall x, -(x+1) = Z.lnot x. Proof. - unfold Z.lnot, Zpred; auto with zarith. + unfold Z.lnot, Z.pred; auto with zarith. Qed. Lemma Zlnot_alt2 : forall x, Z.lnot (x-1) = -x. Proof. - unfold Z.lnot, Zpred; auto with zarith. + unfold Z.lnot, Z.pred; auto with zarith. Qed. Lemma Zlnot_alt3 : forall x, Z.lnot (-x) = x-1. Proof. - unfold Z.lnot, Zpred; auto with zarith. + unfold Z.lnot, Z.pred; auto with zarith. Qed. Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x. Proof. intros [x|x]; simpl; trivial. - rewrite N.spec_eqb, N.spec_0. + rewrite NN.spec_eqb, NN.spec_0. case Z.eqb_spec; simpl; auto with zarith. Qed. Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y -> - 0 < N.to_Z y. + 0 < NN.to_Z y. Proof. intros [x|x] y; simpl; try easy. - rewrite N.spec_eqb, N.spec_0. + rewrite NN.spec_eqb, NN.spec_0. case Z.eqb_spec; simpl; try easy. - inversion 2. subst. generalize (N.spec_pos y); auto with zarith. + inversion 2. subst. generalize (NN.spec_pos y); auto with zarith. Qed. Ltac destr_norm_pos x := @@ -682,9 +682,9 @@ Module Make (N:NType) <: ZType. Proof. intros x p. unfold testbit. destr_norm_pos p; simpl. destr_norm_pos x; simpl. - apply N.spec_testbit. - rewrite N.spec_testbit, N.spec_pred, Zmax_r by auto with zarith. - symmetry. apply Z.bits_opp. apply N.spec_pos. + apply NN.spec_testbit. + rewrite NN.spec_testbit, NN.spec_pred, Z.max_r by auto with zarith. + symmetry. apply Z.bits_opp. apply NN.spec_pos. symmetry. apply Z.testbit_neg_r; auto with zarith. Qed. @@ -692,13 +692,13 @@ Module Make (N:NType) <: ZType. Proof. intros x p. unfold shiftl. destr_norm_pos x; destruct p as [p|p]; simpl; - assert (Hp := N.spec_pos p). - apply N.spec_shiftl. - rewrite Z.shiftl_opp_r. apply N.spec_shiftr. - rewrite !N.spec_shiftl. - rewrite !Z.shiftl_mul_pow2 by apply N.spec_pos. - apply Zopp_mult_distr_l. - rewrite Z.shiftl_opp_r, N.spec_succ, N.spec_shiftr, N.spec_pred, Zmax_r + assert (Hp := NN.spec_pos p). + apply NN.spec_shiftl. + rewrite Z.shiftl_opp_r. apply NN.spec_shiftr. + rewrite !NN.spec_shiftl. + rewrite !Z.shiftl_mul_pow2 by apply NN.spec_pos. + symmetry. apply Z.mul_opp_l. + rewrite Z.shiftl_opp_r, NN.spec_succ, NN.spec_shiftr, NN.spec_pred, Z.max_r by auto with zarith. now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2. Qed. @@ -713,8 +713,8 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold land. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor, - ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith. + rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, + ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite Z.ldiff_land, Zlnot_alt2. now rewrite Z.ldiff_land, Z.land_comm, Zlnot_alt2. now rewrite Z.lnot_lor, !Zlnot_alt2. @@ -724,8 +724,8 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold lor. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor, - ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith. + rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, + ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite Z.lnot_ldiff, Z.lor_comm, Zlnot_alt2. now rewrite Z.lnot_ldiff, Zlnot_alt2. now rewrite Z.lnot_land, !Zlnot_alt2. @@ -735,8 +735,8 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold ldiff. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_land, ?N.spec_ldiff, ?N.spec_lor, - ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; auto with zarith. + rewrite ?NN.spec_succ, ?NN.spec_land, ?NN.spec_ldiff, ?NN.spec_lor, + ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite Z.ldiff_land, Zlnot_alt3. now rewrite Z.lnot_lor, Z.ldiff_land, <- Zlnot_alt2. now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3. @@ -746,7 +746,7 @@ Module Make (N:NType) <: ZType. Proof. intros x y. unfold lxor. destr_norm_pos x; destr_norm_pos y; simpl; - rewrite ?N.spec_succ, ?N.spec_lxor, ?N.spec_pred, ?Zmax_r, ?Zlnot_alt1; + rewrite ?NN.spec_succ, ?NN.spec_lxor, ?NN.spec_pred, ?Z.max_r, ?Zlnot_alt1; auto with zarith. now rewrite !Z.lnot_lxor_r, Zlnot_alt2. now rewrite !Z.lnot_lxor_l, Zlnot_alt2. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index d7c0abd8..fc600eae 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* eq==>eq) modulo. Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -intros a b. zify. intros. apply Z_div_mod_eq_full; auto. +intros a b. zify. intros. apply Z.div_mod; auto. Qed. Theorem mod_pos_bound : -- cgit v1.2.3