diff options
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 62 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 326 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 107 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 228 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 19 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 68 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 70 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 96 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 204 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 21 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 471 | ||||
| -rw-r--r-- | theories/Numbers/Rational/SpecViaQ/QSig.v | 66 | ||||
| -rw-r--r-- | theories/QArith/QOrderedType.v | 6 | ||||
| -rw-r--r-- | theories/QArith/Qminmax.v | 6 | ||||
| -rw-r--r-- | theories/QArith/vo.itarget | 2 | ||||
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 14 | ||||
| -rw-r--r-- | theories/Structures/OrdersTac.v | 4 | ||||
| -rw-r--r-- | theories/ZArith/Zbool.v | 5 |
18 files changed, 769 insertions, 1006 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index fc94f693af..73cc5c21b9 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -13,13 +13,26 @@ Require Export BigN. Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. -Module BigZ <: ZType := ZMake.Make BigN. +(** * [BigZ] : arbitrary large efficient integers. -(** Module [BigZ] implements [ZAxiomsSig] *) + The following [BigZ] module regroups both the operations and + all the abstract properties: -Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ. -Module Export BigZPropMod := ZPropFunct BigZAxiomsMod. -Module Export BigZDivPropMod := ZDivPropFunct BigZAxiomsMod BigZPropMod. + - [ZMake.Make BigN] provides the operations and basic specs w.r.t. ZArith + - [ZTypeIsZAxioms] shows (mainly) that these operations implement + the interface [ZAxioms] + - [ZPropSig] adds all generic properties derived from [ZAxioms] + - [ZDivPropFunct] provides generic properties of [div] and [mod] + ("Floor" variant) + - [MinMax*Properties] provides properties of [min] and [max] + +*) + + +Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder := + ZMake.Make BigN <+ ZTypeIsZAxioms + <+ !ZPropSig <+ !ZDivPropFunct <+ HasEqBool2Dec + <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. (** Notations about [BigZ] *) @@ -69,7 +82,7 @@ Infix "<=" := BigZ.le : bigZ_scope. Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope. Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope. Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. -Infix "mod" := modulo (at level 40, no associativity) : bigN_scope. +Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigN_scope. Local Open Scope bigZ_scope. @@ -102,35 +115,34 @@ intros p1 _ H1; case H1; auto. intros p1 H1; case H1; auto. Qed. -Lemma sub_opp : forall x y : bigZ, x - y == x + (- y). -Proof. -red; intros; zsimpl; auto. -Qed. - -Lemma add_opp : forall x : bigZ, x + (- x) == 0. -Proof. -red; intros; zsimpl; auto with zarith. -Qed. - (** [BigZ] is a ring *) Lemma BigZring : ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. Proof. constructor. -exact add_0_l. -exact add_comm. -exact add_assoc. -exact mul_1_l. -exact mul_comm. -exact mul_assoc. -exact mul_add_distr_r. -exact sub_opp. -exact add_opp. +exact BigZ.add_0_l. +exact BigZ.add_comm. +exact BigZ.add_assoc. +exact BigZ.mul_1_l. +exact BigZ.mul_comm. +exact BigZ.mul_assoc. +exact BigZ.mul_add_distr_r. +symmetry. apply BigZ.add_opp_r. +exact BigZ.add_opp_diag_r. Qed. Add Ring BigZr : BigZring. +(** [BigZ] benefits from an "order" tactic *) + +Ltac bigZ_order := BigZ.order. + +Section Test. +Let test : forall x y : bigZ, x<=y -> y<=x -> x==y. +Proof. bigZ_order. Qed. +End Test. + (** Todo: tactic translating from [BigZ] to [Z] + omega *) (** Todo: micromega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 0ab509650a..05c7ee32f3 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -49,6 +49,7 @@ Module Make (N:NType) <: ZType. 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. @@ -85,34 +86,23 @@ Module Make (N:NType) <: ZType. | Neg nx, Neg ny => N.compare ny nx end. - Definition lt n m := compare n m = Lt. - Definition le n m := compare n m <> Gt. - 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_compare: forall x y, - match compare x y with - Eq => to_Z x = to_Z y - | Lt => to_Z x < to_Z y - | Gt => to_Z x > to_Z y - end. - unfold compare, to_Z; intros x y; case x; case y; clear x y; - intros x y; auto; generalize (N.spec_pos x) (N.spec_pos y). - generalize (N.spec_compare y x); case N.compare; auto with zarith. - generalize (N.spec_compare y N.zero); case N.compare; - try rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare x N.zero); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare x N.zero); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare N.zero y); case N.compare; - try rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; auto with zarith. - generalize (N.spec_compare x y); case N.compare; auto with zarith. - Qed. + Theorem spec_compare : + forall x y, compare x y = Zcompare (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. + Qed. Definition eq_bool x y := match compare x y with @@ -120,36 +110,27 @@ Module Make (N:NType) <: ZType. | _ => false end. - Theorem spec_eq_bool: forall x y, - if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y. - intros x y; unfold eq_bool; - generalize (spec_compare x y); case compare; auto with zarith. + Theorem spec_eq_bool: + forall x y, eq_bool x y = Zeq_bool (to_Z x) (to_Z y). + Proof. + unfold eq_bool, Zeq_bool; intros; rewrite spec_compare; reflexivity. Qed. - Definition cmp_sign x y := - match x, y with - | Pos nx, Neg ny => - if N.eq_bool ny N.zero then Eq else Gt - | Neg nx, Pos ny => - if N.eq_bool nx N.zero then Eq else Lt - | _, _ => Eq - end. + Definition lt n m := to_Z n < to_Z m. + Definition le n m := to_Z n <= to_Z m. - Theorem spec_cmp_sign: forall x y, - match cmp_sign x y with - | Gt => 0 <= to_Z x /\ to_Z y < 0 - | Lt => to_Z x < 0 /\ 0 <= to_Z y - | Eq => True - end. - Proof. - intros [x | x] [y | y]; unfold cmp_sign; auto. - generalize (N.spec_eq_bool y N.zero); case N.eq_bool; auto. - rewrite N.spec_0; unfold to_Z. - generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. - generalize (N.spec_eq_bool x N.zero); case N.eq_bool; auto. - rewrite N.spec_0; unfold to_Z. - generalize (N.spec_pos x) (N.spec_pos y); auto with zarith. - Qed. + Definition min n m := match compare n m with Gt => m | _ => n end. + Definition max n m := match compare n m with Lt => m | _ => n end. + + Theorem spec_min : forall n m, to_Z (min n m) = Zmin (to_Z n) (to_Z m). + Proof. + unfold min, Zmin. intros. rewrite spec_compare. destruct Zcompare; auto. + Qed. + + Theorem spec_max : forall n m, to_Z (max n m) = Zmax (to_Z n) (to_Z m). + Proof. + unfold max, Zmax. intros. rewrite spec_compare. destruct Zcompare; auto. + Qed. Definition to_N x := match x with @@ -160,6 +141,7 @@ 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). + 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. @@ -172,6 +154,7 @@ Module Make (N:NType) <: ZType. end. Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x. + Proof. intros x; case x; simpl; auto with zarith. Qed. @@ -186,10 +169,10 @@ Module Make (N:NType) <: ZType. end. 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; generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; simpl. + 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. @@ -214,17 +197,11 @@ Module Make (N:NType) <: ZType. end. Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. - unfold add, to_Z; intros [x | x] [y | y]. - exact (N.spec_add x y). - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. - intros; rewrite N.spec_add; auto with zarith. + 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 *. Qed. Definition pred x := @@ -238,12 +215,12 @@ Module Make (N:NType) <: ZType. end. Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. - unfold pred, to_Z, minus_one; intros [x | x]. - generalize (N.spec_compare N.zero x); case N.compare; - rewrite N.spec_0; try rewrite N.spec_1; auto with zarith. - intros H; rewrite N.spec_pred, Zmax_r; auto with zarith. - generalize (N.spec_pos x); auto with zarith. - rewrite N.spec_succ; ring. + 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 *. Qed. Definition sub x y := @@ -265,17 +242,11 @@ Module Make (N:NType) <: ZType. end. Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. - unfold sub, to_Z; intros [x | x] [y | y]. - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. - rewrite N.spec_add; auto with zarith. - rewrite N.spec_add; auto with zarith. - unfold zero; generalize (N.spec_compare x y); case N.compare. - rewrite N.spec_0; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. - intros; rewrite N.spec_sub, Zmax_r; auto with zarith. + 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 *. Qed. Definition mul x y := @@ -286,8 +257,8 @@ Module Make (N:NType) <: ZType. | Neg nx, Neg ny => Pos (N.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. Qed. @@ -298,6 +269,7 @@ Module Make (N:NType) <: ZType. 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. Qed. @@ -313,6 +285,7 @@ Module Make (N:NType) <: ZType. end. Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. + Proof. assert (F0: forall x, (-x)^2 = x^2). intros x; rewrite Zpower_2; ring. unfold power_pos, to_Z; intros [x | x] [p | p |]; @@ -335,9 +308,9 @@ Module Make (N:NType) <: ZType. | Neg nx => Neg N.zero end. - Theorem spec_sqrt: forall x, 0 <= to_Z x -> to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. + Proof. unfold to_Z, sqrt; intros [x | x] H. exact (N.spec_sqrt x). replace (N.to_Z x) with 0. @@ -353,144 +326,74 @@ Module Make (N:NType) <: ZType. (Pos q, Pos r) | Pos nx, Neg ny => let (q, r) := N.div_eucl nx ny in - match N.compare N.zero r with - | Eq => (Neg q, zero) - | _ => (Neg (N.succ q), Neg (N.sub ny r)) - end + if N.eq_bool N.zero r + then (Neg q, zero) + else (Neg (N.succ q), Neg (N.sub ny r)) | Neg nx, Pos ny => let (q, r) := N.div_eucl nx ny in - match N.compare N.zero r with - | Eq => (Neg q, zero) - | _ => (Neg (N.succ q), Pos (N.sub ny r)) - end + if N.eq_bool N.zero r + then (Neg q, zero) + else (Neg (N.succ q), Pos (N.sub ny r)) | Neg nx, Neg ny => let (q, r) := N.div_eucl nx ny in (Pos q, Neg r) end. - - Theorem spec_div_eucl_nz: forall x y, - to_Z y <> 0 -> - let (q,r) := div_eucl x y in - (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). - unfold div_eucl, to_Z; intros [x | x] [y | y] H. - assert (H1: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y); case N.div_eucl; auto. - assert (HH: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y); case N.div_eucl; auto. - intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; - case_eq (N.to_Z x); case_eq (N.to_Z y); - try (intros; apply False_ind; auto with zarith; fail). - intros p He1 He2 _ _ H1; injection H1; intros H2 H3. - generalize (N.spec_compare N.zero r); case N.compare; - unfold zero; rewrite N.spec_0; try rewrite H3; auto. - rewrite H2; intros; apply False_ind; auto with zarith. - rewrite H2; intros; apply False_ind; auto with zarith. - intros p _ _ _ H1; discriminate H1. - intros p He p1 He1 H1 _. - generalize (N.spec_compare N.zero r); case N.compare. - change (- Zpos p) with (Zneg p). - unfold zero; lazy zeta. - rewrite N.spec_0; intros H2; rewrite <- H2. - intros H3; rewrite <- H3; auto. - rewrite N.spec_0; intros H2. - change (- Zpos p) with (Zneg p); lazy iota beta. - intros H3; rewrite <- H3; auto. - rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r. - generalize H2; case (N.to_Z r). - intros; apply False_ind; auto with zarith. - intros p2 _; rewrite He; auto with zarith. - change (Zneg p) with (- (Zpos p)); apply f_equal2 with (f := @pair Z Z); ring. - intros p2 H4; discriminate H4. - assert (N.to_Z r = (Zpos p1 mod (Zpos p))). - unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. - case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. - rewrite N.spec_0; intros H2; generalize (N.spec_pos r); - intros; apply False_ind; auto with zarith. - assert (HH: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y); case N.div_eucl; auto. - intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; - case_eq (N.to_Z x); case_eq (N.to_Z y); - try (intros; apply False_ind; auto with zarith; fail). - intros p He1 He2 _ _ H1; injection H1; intros H2 H3. - generalize (N.spec_compare N.zero r); case N.compare; - unfold zero; rewrite N.spec_0; try rewrite H3; auto. - rewrite H2; intros; apply False_ind; auto with zarith. - rewrite H2; intros; apply False_ind; auto with zarith. - intros p _ _ _ H1; discriminate H1. - intros p He p1 He1 H1 _. - generalize (N.spec_compare N.zero r); case N.compare. - change (- Zpos p1) with (Zneg p1). - unfold zero; lazy zeta. - rewrite N.spec_0; intros H2; rewrite <- H2. - intros H3; rewrite <- H3; auto. - rewrite N.spec_0; intros H2. - change (- Zpos p1) with (Zneg p1); lazy iota beta. - intros H3; rewrite <- H3; auto. - rewrite N.spec_succ; rewrite N.spec_sub, Zmax_r. - generalize H2; case (N.to_Z r). - intros; apply False_ind; auto with zarith. - intros p2 _; rewrite He; auto with zarith. - intros p2 H4; discriminate H4. - assert (N.to_Z r = (Zpos p1 mod (Zpos p))). - unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. - case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. - rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith. - assert (H1: 0 < N.to_Z y). - generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y); case N.div_eucl; auto. - intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl; - case_eq (N.to_Z x); case_eq (N.to_Z y); - try (intros; apply False_ind; auto with zarith; fail). - change (-0) with 0; lazy iota beta; auto. - intros p _ _ _ _ H2; injection H2. - intros H3 H4; rewrite H3; rewrite H4; auto. - intros p _ _ _ H2; discriminate H2. - intros p He p1 He1 _ _ H2. - change (- Zpos p1) with (Zneg p1); lazy iota beta. - change (- Zpos p) with (Zneg p); lazy iota beta. - rewrite <- H2; auto. - Qed. - - Lemma Zdiv_eucl_0 : forall a, Zdiv_eucl a 0 = (0,0). - Proof. destruct a; auto. Qed. + 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; + [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). + let (q,r) := div_eucl x y in + (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). Proof. - intros. destruct (Z_eq_dec (to_Z y) 0) as [EQ|NEQ]; - [|apply spec_div_eucl_nz; auto]. - unfold div_eucl. - destruct x; destruct y; simpl in *. - generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. - generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. - assert (EQ' : N.to_Z t1 = 0) by auto with zarith. - rewrite EQ'. simpl. rewrite Zdiv_eucl_0. injection 1; intros. - generalize (N.spec_compare N.zero t3); destruct N.compare. - simpl. intros. f_equal; auto with zarith. - rewrite N.spec_0; intro; exfalso; auto with zarith. - rewrite N.spec_0; intro; exfalso; auto with zarith. - generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. - assert (EQ' : N.to_Z t1 = 0) by auto with zarith. - rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros. - generalize (N.spec_compare N.zero t3); destruct N.compare. - simpl. intros. f_equal; auto with zarith. - rewrite N.spec_0; intro; exfalso; auto with zarith. - rewrite N.spec_0; intro; exfalso; auto with zarith. - generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. - assert (EQ' : N.to_Z t1 = 0) by auto with zarith. - rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros. - f_equal; auto with zarith. + 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. + (* Pos Neg *) + generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + break_nonneg x px EQx; break_nonneg y py EQy; + try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr; + simpl; rewrite Hq, N.spec_0; auto). + change (- Zpos py) with (Zneg py). + assert (GT : Zpos py > 0) by (compute; auto). + generalize (Z_div_mod (Zpos px) (Zpos py) GT). + unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + intros (EQ,MOD). injection 1. intros Hr' Hq'. + rewrite N.spec_eq_bool, N.spec_0, Hr'. + break_nonneg r pr EQr. + subst; simpl. rewrite N.spec_0; auto. + subst. lazy iota beta delta [Zeq_bool Zcompare]. + rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + (* Neg Pos *) + generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + break_nonneg x px EQx; break_nonneg y py EQy; + try (injection 1; intros Hr Hq; rewrite N.spec_eq_bool, N.spec_0, Hr; + simpl; rewrite Hq, N.spec_0; auto). + change (- Zpos px) with (Zneg px). + assert (GT : Zpos py > 0) by (compute; auto). + generalize (Z_div_mod (Zpos px) (Zpos py) GT). + unfold Zdiv_eucl. destruct (Zdiv_eucl_POS px (Zpos py)) as (q',r'). + intros (EQ,MOD). injection 1. intros Hr' Hq'. + rewrite N.spec_eq_bool, N.spec_0, Hr'. + break_nonneg r pr EQr. + subst; simpl. rewrite N.spec_0; auto. + subst. lazy iota beta delta [Zeq_bool Zcompare]. + rewrite N.spec_sub, N.spec_succ, EQy, EQr. f_equal. omega with *. + (* Neg Neg *) + generalize (N.spec_div_eucl x y); destruct (N.div_eucl x y) as (q,r). + break_nonneg x px EQx; break_nonneg y py EQy; + try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto). + simpl. intros <-; auto. Qed. Definition div x y := fst (div_eucl x y). 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 q r q11 r1 H; injection H; auto. @@ -500,6 +403,7 @@ 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 q r q11 r1 H; injection H; auto. @@ -514,6 +418,7 @@ Module Make (N:NType) <: ZType. end. Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (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; @@ -529,8 +434,7 @@ Module Make (N:NType) <: ZType. Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x). Proof. - intros. unfold sgn. generalize (spec_compare zero x). - destruct compare. + intros. unfold sgn. rewrite spec_compare. case Zcompare_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. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index a7c5473aa3..a9945e848c 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -25,100 +25,75 @@ Module Type ZType. Parameter t : Type. Parameter to_Z : t -> Z. - Notation "[ x ]" := (to_Z x). + Local Notation "[ x ]" := (to_Z x). - Definition eq x y := ([x] = [y]). + Definition eq x y := [x] = [y]. + Definition lt x y := [x] < [y]. + Definition le x y := [x] <= [y]. Parameter of_Z : Z -> t. Parameter spec_of_Z: forall x, to_Z (of_Z x) = x. + Parameter compare : t -> t -> comparison. + Parameter eq_bool : t -> t -> bool. + Parameter min : t -> t -> t. + Parameter max : t -> t -> t. Parameter zero : t. Parameter one : t. Parameter minus_one : t. + Parameter succ : t -> t. + Parameter add : t -> t -> t. + Parameter pred : t -> t. + Parameter sub : t -> t -> t. + Parameter opp : t -> t. + Parameter mul : t -> t -> t. + Parameter square : t -> t. + Parameter power_pos : t -> positive -> t. + Parameter sqrt : t -> t. + Parameter div_eucl : t -> t -> t * t. + Parameter div : t -> t -> t. + Parameter modulo : t -> t -> t. + Parameter gcd : t -> t -> t. + Parameter sgn : t -> t. + Parameter abs : t -> t. + Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y]. + Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y]. + Parameter spec_min : forall x y, [min x y] = Zmin [x] [y]. + Parameter spec_max : forall x y, [max x y] = Zmax [x] [y]. Parameter spec_0: [zero] = 0. Parameter spec_1: [one] = 1. Parameter spec_m1: [minus_one] = -1. - - Parameter compare : t -> t -> comparison. - - Parameter spec_compare: forall x y, - match compare x y with - | Eq => [x] = [y] - | Lt => [x] < [y] - | Gt => [x] > [y] - end. - - Definition lt n m := compare n m = Lt. - Definition le n m := compare n m <> Gt. - 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. - - Parameter eq_bool : t -> t -> bool. - - Parameter spec_eq_bool: forall x y, - if eq_bool x y then [x] = [y] else [x] <> [y]. - - Parameter succ : t -> t. - Parameter spec_succ: forall n, [succ n] = [n] + 1. - - Parameter add : t -> t -> t. - Parameter spec_add: forall x y, [add x y] = [x] + [y]. - - Parameter pred : t -> t. - Parameter spec_pred: forall x, [pred x] = [x] - 1. - - Parameter sub : t -> t -> t. - Parameter spec_sub: forall x y, [sub x y] = [x] - [y]. - - Parameter opp : t -> t. - Parameter spec_opp: forall x, [opp x] = - [x]. - - Parameter mul : t -> t -> t. - Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. - - Parameter square : t -> t. - Parameter spec_square: forall x, [square x] = [x] * [x]. - - Parameter power_pos : t -> positive -> t. - Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. - - Parameter sqrt : t -> t. - Parameter spec_sqrt: forall x, 0 <= [x] -> [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. - - Parameter div_eucl : t -> t -> t * t. - Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. - - Parameter div : t -> t -> t. - Parameter spec_div: forall x y, [div x y] = [x] / [y]. - - Parameter modulo : t -> t -> t. - Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. - - Parameter gcd : t -> t -> t. - Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). - - Parameter sgn : t -> t. - Parameter spec_sgn : forall x, [sgn x] = Zsgn [x]. - - Parameter abs : t -> t. - Parameter spec_abs : forall x, [abs x] = Zabs [x]. End ZType. + +Module Type ZType_Notation (Import Z:ZType). + Notation "[ x ]" := (to_Z x). + Infix "==" := eq (at level 70). + Notation "0" := zero. + Infix "+" := add. + Infix "-" := sub. + Infix "*" := mul. + Notation "- x" := (opp x). + Infix "<=" := le. + Infix "<" := lt. +End ZType_Notation. + +Module Type ZType' := ZType <+ ZType_Notation.
\ No newline at end of file diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index a94e1a318f..3d53707eb8 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -16,71 +16,64 @@ Require Import ZArith ZAxioms ZDivFloor ZSig. *) -Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig <: ZDivSig. - -Local Notation "[ x ]" := (Z.to_Z x). -Local Infix "==" := Z.eq (at level 70). -Local Notation "0" := Z.zero. -Local Infix "+" := Z.add. -Local Infix "-" := Z.sub. -Local Infix "*" := Z.mul. -Local Notation "- x" := (Z.opp x). -Local Infix "<=" := Z.le. -Local Infix "<" := Z.lt. +Module ZTypeIsZAxioms (Import Z : ZType'). Hint Rewrite - Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ - Z.spec_mul Z.spec_opp Z.spec_of_Z Z.spec_div Z.spec_modulo: zspec. + spec_0 spec_1 spec_add spec_sub spec_pred spec_succ + spec_mul spec_opp spec_of_Z spec_div spec_modulo + spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn + : zsimpl. -Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec. +Ltac zsimpl := autorewrite with zsimpl. Ltac zcongruence := repeat red; intros; zsimpl; congruence. +Ltac zify := unfold eq, lt, le in *; zsimpl. -Instance eq_equiv : Equivalence Z.eq. -Proof. unfold Z.eq. firstorder. Qed. +Instance eq_equiv : Equivalence eq. +Proof. unfold eq. firstorder. Qed. Local Obligation Tactic := zcongruence. -Program Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ. -Program Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred. -Program Instance add_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add. -Program Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub. -Program Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul. +Program Instance succ_wd : Proper (eq ==> eq) succ. +Program Instance pred_wd : Proper (eq ==> eq) pred. +Program Instance add_wd : Proper (eq ==> eq ==> eq) add. +Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub. +Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul. -Theorem pred_succ : forall n, Z.pred (Z.succ n) == n. +Theorem pred_succ : forall n, pred (succ n) == n. Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. Section Induction. Variable A : Z.t -> Prop. -Hypothesis A_wd : Proper (Z.eq==>iff) A. +Hypothesis A_wd : Proper (eq==>iff) A. Hypothesis A0 : A 0. -Hypothesis AS : forall n, A n <-> A (Z.succ n). +Hypothesis AS : forall n, A n <-> A (succ n). -Let B (z : Z) := A (Z.of_Z z). +Let B (z : Z) := A (of_Z z). Lemma B0 : B 0. Proof. unfold B; simpl. rewrite <- (A_wd 0); auto. -zsimpl; auto. +zify. auto. Qed. Lemma BS : forall z : Z, B z -> B (z + 1). Proof. intros z H. unfold B in *. apply -> AS in H. -setoid_replace (Z.of_Z (z + 1)) with (Z.succ (Z.of_Z z)); auto. -zsimpl; auto. +setoid_replace (of_Z (z + 1)) with (succ (of_Z z)); auto. +zify. auto. Qed. Lemma BP : forall z : Z, B z -> B (z - 1). Proof. intros z H. unfold B in *. rewrite AS. -setoid_replace (Z.succ (Z.of_Z (z - 1))) with (Z.of_Z z); auto. -zsimpl; auto with zarith. +setoid_replace (succ (of_Z (z - 1))) with (of_Z z); auto. +zify. auto with zarith. Qed. Lemma B_holds : forall z : Z, B z. @@ -99,213 +92,168 @@ Qed. Theorem bi_induction : forall n, A n. Proof. -intro n. setoid_replace n with (Z.of_Z (Z.to_Z n)). +intro n. setoid_replace n with (of_Z (to_Z n)). apply B_holds. -zsimpl; auto. +zify. auto. Qed. End Induction. Theorem add_0_l : forall n, 0 + n == n. Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem add_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). +Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m). Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. Theorem sub_0_r : forall n, n - 0 == n. Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem sub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). +Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m). Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m. +Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m. Proof. -intros; zsimpl; ring. +intros. zify. ring. Qed. (** Order *) -Lemma spec_compare_alt : forall x y, Z.compare x y = ([x] ?= [y])%Z. +Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. - intros; generalize (Z.spec_compare x y). - destruct (Z.compare x y); auto. - intros H; rewrite H; symmetry; apply Zcompare_refl. + intros. zify. destruct (Zcompare_spec [x] [y]); auto. Qed. -Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. -Proof. - intros; unfold Z.lt, Zlt; rewrite spec_compare_alt; intuition. -Qed. - -Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. -Proof. - intros; unfold Z.le, Zle; rewrite spec_compare_alt; intuition. -Qed. - -Lemma spec_min : forall x y, [Z.min x y] = Zmin [x] [y]. -Proof. - intros; unfold Z.min, Zmin. - rewrite spec_compare_alt; destruct Zcompare; auto. -Qed. +Definition eqb := eq_bool. -Lemma spec_max : forall x y, [Z.max x y] = Zmax [x] [y]. +Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y. Proof. - intros; unfold Z.max, Zmax. - rewrite spec_compare_alt; destruct Zcompare; auto. + intros. zify. symmetry. apply Zeq_is_eq_bool. Qed. -Instance compare_wd : Proper (Z.eq ==> Z.eq ==> eq) Z.compare. +Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. Proof. -intros x x' Hx y y' Hy. -rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition. +intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition. Qed. -Instance lt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt. +Instance lt_wd : Proper (eq ==> eq ==> iff) lt. Proof. -intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition. +intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition. Qed. Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. Proof. -intros. -unfold Z.eq; rewrite spec_lt, spec_le; omega. +intros. zify. omega. Qed. Theorem lt_irrefl : forall n, ~ n < n. Proof. -intros; rewrite spec_lt; auto with zarith. +intros. zify. omega. Qed. -Theorem lt_succ_r : forall n m, n < (Z.succ m) <-> n <= m. +Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m. Proof. -intros; rewrite spec_lt, spec_le, Z.spec_succ; omega. +intros. zify. omega. Qed. -Theorem min_l : forall n m, n <= m -> Z.min n m == n. +Theorem min_l : forall n m, n <= m -> min n m == n. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_min. -generalize (Zmin_spec [n] [m]); omega. +intros n m. zify. omega with *. Qed. -Theorem min_r : forall n m, m <= n -> Z.min n m == m. +Theorem min_r : forall n m, m <= n -> min n m == m. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_min. -generalize (Zmin_spec [n] [m]); omega. +intros n m. zify. omega with *. Qed. -Theorem max_l : forall n m, m <= n -> Z.max n m == n. +Theorem max_l : forall n m, m <= n -> max n m == n. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_max. -generalize (Zmax_spec [n] [m]); omega. +intros n m. zify. omega with *. Qed. -Theorem max_r : forall n m, n <= m -> Z.max n m == m. +Theorem max_r : forall n m, n <= m -> max n m == m. Proof. -intros n m; unfold Z.eq; rewrite spec_le, spec_max. -generalize (Zmax_spec [n] [m]); omega. +intros n m. zify. omega with *. Qed. (** Part specific to integers, not natural numbers *) -Program Instance opp_wd : Proper (Z.eq ==> Z.eq) Z.opp. +Program Instance opp_wd : Proper (eq ==> eq) opp. -Theorem succ_pred : forall n, Z.succ (Z.pred n) == n. +Theorem succ_pred : forall n, succ (pred n) == n. Proof. -red; intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. Theorem opp_0 : - 0 == 0. Proof. -red; intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem opp_succ : forall n, - (Z.succ n) == Z.pred (- n). +Theorem opp_succ : forall n, - (succ n) == pred (- n). Proof. -intros; zsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem abs_eq : forall n, 0 <= n -> Z.abs n == n. +Theorem abs_eq : forall n, 0 <= n -> abs n == n. Proof. -intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs. apply Zabs_eq. +intros n. zify. omega with *. Qed. -Theorem abs_neq : forall n, n <= 0 -> Z.abs n == -n. +Theorem abs_neq : forall n, n <= 0 -> abs n == -n. Proof. -intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs, Z.spec_opp. - apply Zabs_non_eq. +intros n. zify. omega with *. Qed. -Theorem sgn_null : forall n, n==0 -> Z.sgn n == 0. +Theorem sgn_null : forall n, n==0 -> sgn n == 0. Proof. -intros n. unfold Z.eq. rewrite Z.spec_sgn, Z.spec_0. rewrite Zsgn_null; auto. +intros n. zify. omega with *. Qed. -Theorem sgn_pos : forall n, 0<n -> Z.sgn n == Z.succ 0. +Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0. Proof. -intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_pos; auto. +intros n. zify. omega with *. Qed. -Theorem sgn_neg : forall n, n<0 -> Z.sgn n == Z.opp (Z.succ 0). +Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0). Proof. -intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_neg; auto. +intros n. zify. omega with *. Qed. -Program Instance div_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.div. -Program Instance mod_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.modulo. +Program Instance div_wd : Proper (eq==>eq==>eq) div. +Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. -Theorem div_mod : forall a b, ~b==0 -> a == b*(Z.div a b) + (Z.modulo a b). +Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -intros a b. unfold Z.eq; zsimpl. intros. -apply Z_div_mod_eq_full; auto. +intros a b. zify. intros. apply Z_div_mod_eq_full; auto. Qed. Theorem mod_pos_bound : - forall a b, 0 < b -> 0 <= Z.modulo a b /\ Z.modulo a b < b. + forall a b, 0 < b -> 0 <= modulo a b /\ modulo a b < b. Proof. -intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros. -rewrite Z.spec_modulo; auto with zarith. -apply Z_mod_lt; auto with zarith. +intros a b. zify. intros. apply Z_mod_lt; auto with zarith. Qed. Theorem mod_neg_bound : - forall a b, b < 0 -> b < Z.modulo a b /\ Z.modulo a b <= 0. -Proof. -intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros. -rewrite Z.spec_modulo; auto with zarith. -apply Z_mod_neg; auto with zarith. -Qed. - -(** Aliases *) - -Definition t := Z.t. -Definition eq := Z.eq. -Definition zero := Z.zero. -Definition succ := Z.succ. -Definition pred := Z.pred. -Definition add := Z.add. -Definition sub := Z.sub. -Definition mul := Z.mul. -Definition opp := Z.opp. -Definition lt := Z.lt. -Definition le := Z.le. -Definition min := Z.min. -Definition max := Z.max. -Definition abs := Z.abs. -Definition sgn := Z.sgn. -Definition div := Z.div. -Definition modulo := Z.modulo. - -End ZSig_ZAxioms. + forall a b, b < 0 -> b < modulo a b /\ modulo a b <= 0. +Proof. +intros a b. zify. intros. apply Z_mod_neg; auto with zarith. +Qed. + +End ZTypeIsZAxioms. + +Module ZType_ZAxioms (Z : ZType) + <: ZAxiomsSig <: ZDivSig <: HasCompare Z <: HasEqBool Z + := Z <+ ZTypeIsZAxioms. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 734ebe95be..14fa0bfde1 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -144,6 +144,10 @@ Qed. (** We know enough now to benefit from the generic [order] tactic. *) +Definition lt_compat := lt_wd. +Definition lt_total := lt_trichotomy. +Definition le_lteq := lt_eq_cases. + Module OrderElts <: TotalOrder. Definition t := t. Definition eq := eq. @@ -151,9 +155,9 @@ Module OrderElts <: TotalOrder. Definition le := le. Definition eq_equiv := eq_equiv. Definition lt_strorder := lt_strorder. - Definition lt_compat := lt_wd. - Definition lt_total := lt_trichotomy. - Definition le_lteq := lt_eq_cases. + Definition lt_compat := lt_compat. + Definition lt_total := lt_total. + Definition le_lteq := le_lteq. End OrderElts. Module OrderTac := !MakeOrderTac OrderElts. Ltac order := OrderTac.order. @@ -635,9 +639,6 @@ Module NZOrderPropFunct (NZ : NZOrdSig) := an [OrderedType] structure. *) Module NZOrderedTypeFunct (NZ : NZDecOrdSig') - <: DecidableTypeFull <: OrderedTypeFull. - Include NZ <+ NZOrderPropFunct. - Definition lt_compat := lt_wd. - Definition le_lteq := lt_eq_cases. - Include Compare2EqBool <+ HasEqBool2Dec. -End NZOrderedTypeFunct. + <: DecidableTypeFull <: OrderedTypeFull := + NZ <+ NZOrderPropFunct <+ Compare2EqBool <+ HasEqBool2Dec. + diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index b87056a634..64d2e58e62 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -6,24 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(** * Efficient arbitrary large natural numbers in base 2^31 *) -(** * Natural numbers in base 2^31 *) - -(** -Author: Arnaud Spiwack -*) +(** Initial Author: Arnaud Spiwack *) Require Export Int31. -Require Import CyclicAxioms Cyclic31 NSig NSigNAxioms NMake NProperties NDiv. +Require Import CyclicAxioms Cyclic31 NSig NSigNAxioms NMake + NProperties NDiv GenericMinMax. + +(** The following [BigN] module regroups both the operations and + all the abstract properties: -Module BigN <: NType := NMake.Make Int31Cyclic. + - [NMake.Make Int31Cyclic] provides the operations and basic specs + w.r.t. ZArith + - [NTypeIsNAxioms] shows (mainly) that these operations implement + the interface [NAxioms] + - [NPropSig] adds all generic properties derived from [NAxioms] + - [NDivPropFunct] provides generic properties of [div] and [mod]. + - [MinMax*Properties] provides properties of [min] and [max]. + +*) -(** Module [BigN] implements [NAxiomsSig] *) +Module BigN <: NType <: OrderedTypeFull <: TotalOrder := + NMake.Make Int31Cyclic <+ NTypeIsNAxioms + <+ !NPropSig <+ !NDivPropFunct <+ HasEqBool2Dec + <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. -Module Export BigNAxiomsMod := NSig_NAxioms BigN. -Module Export BigNPropMod := NPropFunct BigNAxiomsMod. -Module Export BigDivModProp := NDivPropFunct BigNAxiomsMod BigNPropMod. (** Notations about [BigN] *) @@ -69,7 +77,7 @@ Infix "<=" := BigN.le : bigN_scope. Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. -Infix "mod" := modulo (at level 40, no associativity) : bigN_scope. +Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope. Local Open Scope bigN_scope. @@ -78,7 +86,7 @@ Local Open Scope bigN_scope. Theorem succ_pred: forall q : bigN, 0 < q -> BigN.succ (BigN.pred q) == q. Proof. -intros; apply succ_pred. +intros; apply BigN.succ_pred. intro H'; rewrite H' in H; discriminate. Qed. @@ -88,18 +96,32 @@ Lemma BigNring : semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq. Proof. constructor. -exact add_0_l. -exact add_comm. -exact add_assoc. -exact mul_1_l. -exact mul_0_l. -exact mul_comm. -exact mul_assoc. -exact mul_add_distr_r. +exact BigN.add_0_l. +exact BigN.add_comm. +exact BigN.add_assoc. +exact BigN.mul_1_l. +exact BigN.mul_0_l. +exact BigN.mul_comm. +exact BigN.mul_assoc. +exact BigN.mul_add_distr_r. Qed. Add Ring BigNr : BigNring. -(** Todo: tactic translating from [BigN] to [Z] + omega *) +(** We benefit from an "order" tactic *) + +Ltac bigN_order := BigN.order. + +Section TestOrder. +Let test : forall x y : bigN, x<=y -> y<=x -> x==y. +Proof. bigN_order. Qed. +End TestOrder. + +(** We can use at least a bit of (r)omega by translating to [Z]. *) + +Section TestOmega. +Let test : forall x y : bigN, x<=y -> y<=x -> x==y. +Proof. intros x y. BigN.zify. omega. Qed. +End TestOmega. (** Todo: micromega *) diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index b8e879c668..6257e8e630 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1339,12 +1339,6 @@ let _ = pr " comparenm)."; pr ""; - pr " Definition lt n m := compare n m = Lt."; - pr " Definition le n m := compare n m <> Gt."; - pr " Definition min n m := match compare n m with Gt => m | _ => n end."; - pr " Definition max n m := match compare n m with Lt => m | _ => n end."; - pr ""; - for i = 0 to size do pp " Let spec_compare_%i: forall x y," i; pp " match compare_%i x y with " i; @@ -1386,7 +1380,7 @@ let _ = pp ""; - pr " Theorem spec_compare: forall x y,"; + pr " Theorem spec_compare_aux: forall x y,"; pr " match compare x y with "; pr " Eq => [x] = [y]"; pr " | Lt => [x] < [y]"; @@ -1421,6 +1415,15 @@ let _ = pp " Qed."; pr ""; + pr " Theorem spec_compare : forall x y, compare x y = Zcompare [x] [y]."; + pa " Admitted."; + pp " Proof."; + pp " intros x y. generalize (spec_compare_aux x y); destruct compare;"; + pp " intros; symmetry; try rewrite Zcompare_Eq_iff_eq; assumption."; + pp " Qed."; + pr ""; + + pr " Definition eq_bool x y :="; pr " match compare x y with"; pr " | Eq => true"; @@ -1428,17 +1431,42 @@ let _ = pr " end."; pr ""; + pr " Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y]."; + pa " Admitted."; + pp " Proof."; + pp " intros. unfold eq_bool, Zeq_bool. rewrite spec_compare; reflexivity."; + pp " Qed."; + pr ""; - pr " Theorem spec_eq_bool: forall x y,"; + pr " Theorem spec_eq_bool_aux: forall x y,"; pr " if eq_bool x y then [x] = [y] else [x] <> [y]."; pa " Admitted."; pp " Proof."; pp " intros x y; unfold eq_bool."; - pp " generalize (spec_compare x y); case compare; auto with zarith."; - pp " Qed."; + pp " generalize (spec_compare_aux x y); case compare; auto with zarith."; + pp " Qed."; pr ""; + pr " Definition lt n m := [n] < [m]."; + pr " Definition le n m := [n] <= [m]."; + pr ""; + pr " Definition min n m := match compare n m with Gt => m | _ => n end."; + pr " Definition max n m := match compare n m with Lt => m | _ => n end."; + pr ""; + + pr " Theorem spec_max : forall n m, [max n m] = Zmax [n] [m]."; + pa " Admitted."; + pp " Proof."; + pp " intros. unfold max, Zmax. rewrite spec_compare; destruct Zcompare; reflexivity."; + pp " Qed."; + pr ""; + pr " Theorem spec_min : forall n m, [min n m] = Zmin [n] [m]."; + pa " Admitted."; + pp " Proof."; + pp " intros. unfold min, Zmin. rewrite spec_compare; destruct Zcompare; reflexivity."; + pp " Qed."; + pr ""; pr " (***************************************************************)"; pr " (* *)"; @@ -1974,12 +2002,12 @@ let _ = pp " assert (F1: [one] = 1)."; pp " exact (spec_1 w0_spec)."; pp " intros x y. unfold div_eucl."; - pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0."; + pp " generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0."; pp " intro H. rewrite H. destruct [x]; auto."; pp " intro H'."; pp " assert (0 < [y]) by (generalize (spec_pos y); auto with zarith)."; pp " clear H'."; - pp " generalize (spec_compare x y); case compare; try rewrite F0;"; + pp " generalize (spec_compare_aux x y); case compare; try rewrite F0;"; pp " try rewrite F1; intros; auto with zarith."; pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))"; pp " (Z_mod_same [y] (Zlt_gt _ _ H));"; @@ -2121,12 +2149,12 @@ let _ = pp " assert (F1: [one] = 1)."; pp " exact (spec_1 w0_spec)."; pp " intros x y. unfold modulo."; - pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0."; + pp " generalize (spec_eq_bool_aux y zero). destruct eq_bool; rewrite F0."; pp " intro H; rewrite H. destruct [x]; auto."; pp " intro H'."; pp " assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith)."; pp " clear H'."; - pp " generalize (spec_compare x y); case compare; try rewrite F0;"; + pp " generalize (spec_compare_aux x y); case compare; try rewrite F0;"; pp " try rewrite F1; intros; try split; auto with zarith."; pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith."; pp " apply sym_equal; apply Zmod_small; auto with zarith."; @@ -2185,11 +2213,11 @@ let _ = pp " assert (F1: [zero] = 0)."; pp " unfold zero, w_0, to_Z; rewrite (spec_0 w0_spec); auto."; pp " intros a b cont p H2 H3 H4; unfold gcd_gt_body."; - pp " generalize (spec_compare b zero); case compare; try rewrite F1."; + pp " generalize (spec_compare_aux b zero); case compare; try rewrite F1."; pp " intros HH; rewrite HH; apply Zis_gcd_0."; pp " intros HH; absurd (0 <= [b]); auto with zarith."; pp " case (spec_digits b); auto with zarith."; - pp " intros H5; generalize (spec_compare (mod_gt a b) zero); "; + pp " intros H5; generalize (spec_compare_aux (mod_gt a b) zero); "; pp " case compare; try rewrite F1."; pp " intros H6; rewrite <- (Zmult_1_r [b])."; pp " rewrite (Z_div_mod_eq [a] [b]); auto with zarith."; @@ -2322,7 +2350,7 @@ let _ = pp " intros a b."; pp " case (spec_digits a); intros H1 H2."; pp " case (spec_digits b); intros H3 H4."; - pp " unfold gcd; generalize (spec_compare a b); case compare."; + pp " unfold gcd; generalize (spec_compare_aux a b); case compare."; pp " intros HH; rewrite HH; apply sym_equal; apply Zis_gcd_gcd; auto."; pp " apply Zis_gcd_refl."; pp " intros; apply trans_equal with (Zgcd [b] [a])."; @@ -2727,7 +2755,7 @@ let _ = pa " Admitted."; pp " Proof."; pp " intros n x; unfold safe_shiftr;"; - pp " generalize (spec_compare n (Ndigits x)); case compare; intros H."; + pp " generalize (spec_compare_aux n (Ndigits x)); case compare; intros H."; pp " apply trans_equal with (1 := spec_0 w0_spec)."; pp " apply sym_equal; apply Zdiv_small; rewrite H."; pp " rewrite spec_Ndigits; exact (spec_digits x)."; @@ -3063,7 +3091,7 @@ let _ = pa " Admitted."; pp " Proof."; pp " intros n p x cont H1 H2; unfold safe_shiftl_aux_body."; - pp " generalize (spec_compare n (head0 x)); case compare; intros H."; + pp " generalize (spec_compare_aux n (head0 x)); case compare; intros H."; pp " apply spec_shiftl; auto with zarith."; pp " apply spec_shiftl; auto with zarith."; pp " rewrite H2."; @@ -3131,11 +3159,11 @@ let _ = pa " Admitted."; pp " Proof."; pp " intros n x; unfold safe_shiftl, safe_shiftl_aux_body."; - pp " generalize (spec_compare n (head0 x)); case compare; intros H."; + pp " generalize (spec_compare_aux n (head0 x)); case compare; intros H."; pp " apply spec_shiftl; auto with zarith."; pp " apply spec_shiftl; auto with zarith."; pp " rewrite <- (spec_double_size x)."; - pp " generalize (spec_compare n (head0 (double_size x))); case compare; intros H1."; + pp " generalize (spec_compare_aux n (head0 (double_size x))); case compare; intros H1."; pp " apply spec_shiftl; auto with zarith."; pp " apply spec_shiftl; auto with zarith."; pp " rewrite <- (spec_double_size (double_size x))."; diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index ecb49d32dc..586e4992e2 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -25,87 +25,67 @@ Module Type NType. Parameter t : Type. Parameter to_Z : t -> Z. - Notation "[ x ]" := (to_Z x). + Local Notation "[ x ]" := (to_Z x). Parameter spec_pos: forall x, 0 <= [x]. Parameter of_N : N -> t. Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x. Definition to_N n := Zabs_N (to_Z n). - Definition eq n m := ([n] = [m]). + Definition eq n m := [n] = [m]. + Definition lt n m := [n] < [m]. + Definition le n m := [n] <= [m]. + Parameter compare : t -> t -> comparison. + Parameter eq_bool : t -> t -> bool. + Parameter max : t -> t -> t. + Parameter min : t -> t -> t. Parameter zero : t. Parameter one : t. + Parameter succ : t -> t. + Parameter pred : t -> t. + Parameter add : t -> t -> t. + Parameter sub : t -> t -> t. + Parameter mul : t -> t -> t. + Parameter square : t -> t. + Parameter power_pos : t -> positive -> t. + Parameter sqrt : t -> t. + Parameter div_eucl : t -> t -> t * t. + Parameter div : t -> t -> t. + Parameter modulo : t -> t -> t. + Parameter gcd : t -> t -> t. + Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y]. + Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y]. + Parameter spec_max : forall x y, [max x y] = Zmax [x] [y]. + Parameter spec_min : forall x y, [min x y] = Zmin [x] [y]. Parameter spec_0: [zero] = 0. Parameter spec_1: [one] = 1. - - Parameter compare : t -> t -> comparison. - - Parameter spec_compare: forall x y, - match compare x y with - | Eq => [x] = [y] - | Lt => [x] < [y] - | Gt => [x] > [y] - end. - - Definition lt n m := compare n m = Lt. - Definition le n m := compare n m <> Gt. - 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. - - Parameter eq_bool : t -> t -> bool. - - Parameter spec_eq_bool: forall x y, - if eq_bool x y then [x] = [y] else [x] <> [y]. - - Parameter succ : t -> t. - Parameter spec_succ: forall n, [succ n] = [n] + 1. - - Parameter add : t -> t -> t. - Parameter spec_add: forall x y, [add x y] = [x] + [y]. - - Parameter pred : t -> t. - Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1). - - Parameter sub : t -> t -> t. - Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]). - - Parameter mul : t -> t -> t. - Parameter spec_mul: forall x y, [mul x y] = [x] * [y]. - - Parameter square : t -> t. - Parameter spec_square: forall x, [square x] = [x] * [x]. - - Parameter power_pos : t -> positive -> t. - Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n. - - Parameter sqrt : t -> t. - Parameter spec_sqrt: forall x, [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2. - - Parameter div_eucl : t -> t -> t * t. - Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. - - Parameter div : t -> t -> t. - Parameter spec_div: forall x y, [div x y] = [x] / [y]. - - Parameter modulo : t -> t -> t. - Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. - - Parameter gcd : t -> t -> t. - - Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b]. End NType. + +Module Type NType_Notation (Import N:NType). + Notation "[ x ]" := (to_Z x). + Infix "==" := eq (at level 70). + Notation "0" := zero. + Infix "+" := add. + Infix "-" := sub. + Infix "*" := mul. + Infix "<=" := le. + Infix "<" := lt. +End NType_Notation. + +Module Type NType' := NType <+ NType_Notation. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 0e3be25aaf..9e3674a23d 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -12,50 +12,41 @@ Require Import ZArith Nnat NAxioms NDiv NSig. (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *) -Module NSig_NAxioms (N:NType) <: NAxiomsSig <: NDivSig. - -Delimit Scope NumScope with Num. -Bind Scope NumScope with N.t. -Local Open Scope NumScope. -Local Notation "[ x ]" := (N.to_Z x) : NumScope. -Local Infix "==" := N.eq (at level 70) : NumScope. -Local Notation "0" := N.zero : NumScope. -Local Infix "+" := N.add : NumScope. -Local Infix "-" := N.sub : NumScope. -Local Infix "*" := N.mul : NumScope. +Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite - N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub - N.spec_div N.spec_modulo : num. -Ltac nsimpl := autorewrite with num. -Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence. + spec_0 spec_succ spec_add spec_mul spec_pred spec_sub + spec_div spec_modulo spec_gcd spec_compare spec_eq_bool + spec_max spec_min + : nsimpl. +Ltac nsimpl := autorewrite with nsimpl. +Ltac ncongruence := unfold eq; repeat red; intros; nsimpl; congruence. +Ltac zify := unfold eq, lt, le in *; nsimpl. Local Obligation Tactic := ncongruence. -Instance eq_equiv : Equivalence N.eq. -Proof. unfold N.eq. firstorder. Qed. +Instance eq_equiv : Equivalence eq. +Proof. unfold eq. firstorder. Qed. -Program Instance succ_wd : Proper (N.eq==>N.eq) N.succ. -Program Instance pred_wd : Proper (N.eq==>N.eq) N.pred. -Program Instance add_wd : Proper (N.eq==>N.eq==>N.eq) N.add. -Program Instance sub_wd : Proper (N.eq==>N.eq==>N.eq) N.sub. -Program Instance mul_wd : Proper (N.eq==>N.eq==>N.eq) N.mul. +Program Instance succ_wd : Proper (eq==>eq) succ. +Program Instance pred_wd : Proper (eq==>eq) pred. +Program Instance add_wd : Proper (eq==>eq==>eq) add. +Program Instance sub_wd : Proper (eq==>eq==>eq) sub. +Program Instance mul_wd : Proper (eq==>eq==>eq) mul. -Theorem pred_succ : forall n, N.pred (N.succ n) == n. +Theorem pred_succ : forall n, pred (succ n) == n. Proof. -unfold N.eq; repeat red; intros. -rewrite N.spec_pred; rewrite N.spec_succ. -generalize (N.spec_pos n); omega with *. +intros. zify. generalize (spec_pos n); omega with *. Qed. -Definition N_of_Z z := N.of_N (Zabs_N z). +Definition N_of_Z z := of_N (Zabs_N z). Section Induction. Variable A : N.t -> Prop. -Hypothesis A_wd : Proper (N.eq==>iff) A. +Hypothesis A_wd : Proper (eq==>iff) A. Hypothesis A0 : A 0. -Hypothesis AS : forall n, A n <-> A (N.succ n). +Hypothesis AS : forall n, A n <-> A (succ n). Let B (z : Z) := A (N_of_Z z). @@ -63,17 +54,17 @@ Lemma B0 : B 0. Proof. unfold B, N_of_Z; simpl. rewrite <- (A_wd 0); auto. -red; rewrite N.spec_0, N.spec_of_N; auto. +red; rewrite spec_0, spec_of_N; auto. Qed. Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1). Proof. intros z H1 H2. unfold B in *. apply -> AS in H2. -setoid_replace (N_of_Z (z + 1)) with (N.succ (N_of_Z z)); auto. -unfold N.eq. rewrite N.spec_succ. +setoid_replace (N_of_Z (z + 1)) with (succ (N_of_Z z)); auto. +unfold eq. rewrite spec_succ. unfold N_of_Z. -rewrite 2 N.spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith. +rewrite 2 spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith. Qed. Lemma B_holds : forall z : Z, (0 <= z)%Z -> B z. @@ -83,147 +74,124 @@ Qed. Theorem bi_induction : forall n, A n. Proof. -intro n. setoid_replace n with (N_of_Z (N.to_Z n)). -apply B_holds. apply N.spec_pos. +intro n. setoid_replace n with (N_of_Z (to_Z n)). +apply B_holds. apply spec_pos. red; unfold N_of_Z. -rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto. -apply N.spec_pos. +rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto. +apply spec_pos. Qed. End Induction. Theorem add_0_l : forall n, 0 + n == n. Proof. -intros; red; nsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem add_succ_l : forall n m, (N.succ n) + m == N.succ (n + m). +Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m). Proof. -intros; red; nsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. Theorem sub_0_r : forall n, n - 0 == n. Proof. -intros; red; nsimpl. generalize (N.spec_pos n); omega with *. +intros. zify. generalize (spec_pos n); omega with *. Qed. -Theorem sub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m). +Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m). Proof. -intros; red; nsimpl. omega with *. +intros. zify. omega with *. Qed. Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intros; red; nsimpl; auto with zarith. +intros. zify. auto with zarith. Qed. -Theorem mul_succ_l : forall n m, (N.succ n) * m == n * m + m. +Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m. Proof. -intros; red; nsimpl. ring. +intros. zify. ring. Qed. (** Order *) -Infix "<=" := N.le : NumScope. -Infix "<" := N.lt : NumScope. - -Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z. +Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. - intros; generalize (N.spec_compare x y). - destruct (N.compare x y); auto. - intros H; rewrite H; symmetry; apply Zcompare_refl. + intros. zify. destruct (Zcompare_spec [x] [y]); auto. Qed. -Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z. -Proof. - intros; unfold N.lt, Zlt; rewrite spec_compare_alt; intuition. -Qed. +Definition eqb := eq_bool. -Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z. +Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y. Proof. - intros; unfold N.le, Zle; rewrite spec_compare_alt; intuition. + intros. zify. symmetry. apply Zeq_is_eq_bool. Qed. -Lemma spec_min : forall x y, [N.min x y] = Zmin [x] [y]. +Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. Proof. - intros; unfold N.min, Zmin. - rewrite spec_compare_alt; destruct Zcompare; auto. +intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition. Qed. -Lemma spec_max : forall x y, [N.max x y] = Zmax [x] [y]. +Instance lt_wd : Proper (eq ==> eq ==> iff) lt. Proof. - intros; unfold N.max, Zmax. - rewrite spec_compare_alt; destruct Zcompare; auto. -Qed. - -Instance compare_wd : Proper (N.eq ==> N.eq ==> eq) N.compare. -Proof. -intros x x' Hx y y' Hy. -rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition. -Qed. - -Instance lt_wd : Proper (N.eq ==> N.eq ==> iff) N.lt. -Proof. -intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition. +intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition. Qed. Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m. Proof. -intros. -unfold N.eq; rewrite spec_lt, spec_le; omega. +intros. zify. omega. Qed. Theorem lt_irrefl : forall n, ~ n < n. Proof. -intros; rewrite spec_lt; auto with zarith. +intros. zify. omega. Qed. -Theorem lt_succ_r : forall n m, n < (N.succ m) <-> n <= m. +Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m. Proof. -intros; rewrite spec_lt, spec_le, N.spec_succ; omega. +intros. zify. omega. Qed. -Theorem min_l : forall n m, n <= m -> N.min n m == n. +Theorem min_l : forall n m, n <= m -> min n m == n. Proof. -intros n m; red; rewrite spec_le, spec_min; omega with *. +intros n m. zify. omega with *. Qed. -Theorem min_r : forall n m, m <= n -> N.min n m == m. +Theorem min_r : forall n m, m <= n -> min n m == m. Proof. -intros n m; red; rewrite spec_le, spec_min; omega with *. +intros n m. zify. omega with *. Qed. -Theorem max_l : forall n m, m <= n -> N.max n m == n. +Theorem max_l : forall n m, m <= n -> max n m == n. Proof. -intros n m; red; rewrite spec_le, spec_max; omega with *. +intros n m. zify. omega with *. Qed. -Theorem max_r : forall n m, n <= m -> N.max n m == m. +Theorem max_r : forall n m, n <= m -> max n m == m. Proof. -intros n m; red; rewrite spec_le, spec_max; omega with *. +intros n m. zify. omega with *. Qed. (** Properties specific to natural numbers, not integers. *) -Theorem pred_0 : N.pred 0 == 0. +Theorem pred_0 : pred 0 == 0. Proof. -red; nsimpl; auto. +zify. auto. Qed. -Program Instance div_wd : Proper (N.eq==>N.eq==>N.eq) N.div. -Program Instance mod_wd : Proper (N.eq==>N.eq==>N.eq) N.modulo. +Program Instance div_wd : Proper (eq==>eq==>eq) div. +Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. -Theorem div_mod : forall a b, ~b==0 -> a == b*(N.div a b) + (N.modulo a b). +Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b). Proof. -intros a b. unfold N.eq. nsimpl. intros. -apply Z_div_mod_eq_full; auto. +intros a b. zify. intros. apply Z_div_mod_eq_full; auto. Qed. -Theorem mod_upper_bound : forall a b, ~b==0 -> N.modulo a b < b. +Theorem mod_upper_bound : forall a b, ~b==0 -> modulo a b < b. Proof. -intros a b. unfold N.eq. rewrite spec_lt. nsimpl. intros. +intros a b. zify. intros. destruct (Z_mod_lt [a] [b]); auto. -generalize (N.spec_pos b); auto with zarith. +generalize (spec_pos b); auto with zarith. Qed. Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) := @@ -231,9 +199,9 @@ Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) := Implicit Arguments recursion [A]. Instance recursion_wd (A : Type) (Aeq : relation A) : - Proper (Aeq ==> (N.eq==>Aeq==>Aeq) ==> N.eq ==> Aeq) (@recursion A). + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). Proof. -unfold N.eq. +unfold eq. intros A Aeq a a' Eaa' f f' Eff' x x' Exx'. unfold recursion. unfold N.to_N. @@ -255,11 +223,11 @@ Qed. Theorem recursion_succ : forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A), - Aeq a a -> Proper (N.eq==>Aeq==>Aeq) f -> - forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)). + Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> + forall n, Aeq (recursion a f (succ n)) (f n (recursion a f n)). Proof. unfold N.eq, recursion; intros A Aeq a f EAaa f_wd n. -replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)). +replace (N.to_N (succ n)) with (Nsucc (N.to_N n)). rewrite Nrect_step. apply f_wd; auto. unfold N.to_N. @@ -277,26 +245,12 @@ apply Z_of_N_eq_rev. rewrite Z_of_N_succ. rewrite 2 Z_of_N_abs. rewrite 2 Zabs_eq; auto. -generalize (N.spec_pos n); auto with zarith. -apply N.spec_pos; auto. +generalize (spec_pos n); auto with zarith. +apply spec_pos; auto. Qed. -(** The instantiation of operations. - Placing them at the very end avoids having indirections in above lemmas. *) - -Definition t := N.t. -Definition eq := N.eq. -Definition zero := N.zero. -Definition succ := N.succ. -Definition pred := N.pred. -Definition add := N.add. -Definition sub := N.sub. -Definition mul := N.mul. -Definition lt := N.lt. -Definition le := N.le. -Definition min := N.min. -Definition max := N.max. -Definition div := N.div. -Definition modulo := N.modulo. - -End NSig_NAxioms. +End NTypeIsNAxioms. + +Module NType_NAxioms (N : NType) + <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N + := N <+ NTypeIsNAxioms. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index fcfb5d7e75..15abaaa42b 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -5,10 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) -(************************************************************************) -(*i $Id$ i*) +(** * BigQ: an efficient implementation of rational numbers *) + +(** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) Require Export BigZ. Require Import Field Qfield QSig QMake. @@ -178,18 +178,19 @@ induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl. destruct n; reflexivity. Qed. -Lemma BigQ_eq_bool_correct : - forall x y, BigQ.eq_bool x y = true -> x==y. +Lemma BigQ_eq_bool_iff : + forall x y, BigQ.eq_bool x y = true <-> x==y. Proof. -intros; generalize (BigQ.spec_eq_bool x y); rewrite H; auto. +intros. rewrite BigQ.spec_eq_bool. apply Qeq_bool_iff. Qed. +Lemma BigQ_eq_bool_correct : + forall x y, BigQ.eq_bool x y = true -> x==y. +Proof. now apply BigQ_eq_bool_iff. Qed. + Lemma BigQ_eq_bool_complete : forall x y, x==y -> BigQ.eq_bool x y = true. -Proof. -intros; generalize (BigQ.spec_eq_bool x y). -destruct BigQ.eq_bool; auto. -Qed. +Proof. now apply BigQ_eq_bool_iff. Qed. (* TODO : improve later the detection of constants ... *) diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 046dd2dfdd..6513922c4a 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -5,15 +5,20 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) -(************************************************************************) -(*i $Id$ i*) +(** * QMake : a generic efficient implementation of rational numbers *) + +(** Initial authors : Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) Require Import BigNumPrelude ROmega. -Require Import QArith Qcanon Qpower. +Require Import QArith Qcanon Qpower Qminmax. Require Import NSig ZSig QSig. +(** We will build rationals out of an implementation of integers [ZType] + for numerators and an implementation of natural numbers [NType] for + denominators. But first we will need some glue between [NType] and + [ZType]. *) + Module Type NType_ZType (N:NType)(Z:ZType). Parameter Z_of_N : N.t -> Z.t. Parameter spec_Z_of_N : forall n, Z.to_Z (Z_of_N n) = N.to_Z n. @@ -56,17 +61,56 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Notation "[ x ]" := (to_Q x). + Lemma N_to_Z_pos : + forall x, (N.to_Z x <> N.to_Z N.zero)%Z -> (0 < N.to_Z x)%Z. + Proof. + intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega. + Qed. +(* + Lemma if_fun_commut : forall A B (f:A->B)(b:bool) a a', + f (if b then a else a') = if b then f a else f a'. + Proof. now destruct b. Qed. + + Lemma if_fun_commut' : forall A B C D (f:A->B)(b:{C}+{D}) a a', + f (if b then a else a') = if b then f a else f a'. + Proof. now destruct b. Qed. +*) + Ltac destr_eqb := + match goal with + | |- context [Z.eq_bool ?x ?y] => + rewrite (Z.spec_eq_bool x y); + generalize (Zeq_bool_if (Z.to_Z x) (Z.to_Z y)); + case (Zeq_bool (Z.to_Z x) (Z.to_Z y)); + destr_eqb + | |- context [N.eq_bool ?x ?y] => + rewrite (N.spec_eq_bool x y); + generalize (Zeq_bool_if (N.to_Z x) (N.to_Z y)); + case (Zeq_bool (N.to_Z x) (N.to_Z y)); + [ | let H:=fresh "H" in + try (intro H;generalize (N_to_Z_pos _ H); clear H)]; + destr_eqb + | _ => idtac + end. + + Hint Rewrite + Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l + Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp + Z.spec_compare N.spec_compare + Z.spec_add N.spec_add Z.spec_mul N.spec_mul Z.spec_div N.spec_div + Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1 + spec_Z_of_N spec_Zabs_N + : nz. + Ltac nzsimpl := autorewrite with nz in *. + + Ltac qsimpl := try red; unfold to_Q; simpl; intros; + destr_eqb; simpl; nzsimpl; intros; + rewrite ?Z2P_correct by auto; + auto. + Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q. Proof. - intros(x,y); destruct y; simpl; rewrite Z.spec_of_Z; auto. - generalize (N.spec_eq_bool (N.of_N (Npos y~1)) N.zero); - case N.eq_bool; auto; rewrite N.spec_0. - rewrite N.spec_of_N; discriminate. - rewrite N.spec_of_N; auto. - generalize (N.spec_eq_bool (N.of_N (Npos y~0)) N.zero); - case N.eq_bool; auto; rewrite N.spec_0. - rewrite N.spec_of_N; discriminate. - rewrite N.spec_of_N; auto. + intros(x,y); destruct y; simpl; rewrite ?Z.spec_of_Z; auto; + destr_eqb; now rewrite ?N.spec_0, ?N.spec_of_N. Qed. Theorem spec_of_Q: forall q: Q, [of_Q q] == q. @@ -82,17 +126,17 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Lemma spec_0: [zero] == 0. Proof. - simpl; rewrite Z.spec_0; reflexivity. + simpl. nzsimpl. reflexivity. Qed. Lemma spec_1: [one] == 1. Proof. - simpl; rewrite Z.spec_1; reflexivity. + simpl. nzsimpl. reflexivity. Qed. Lemma spec_m1: [minus_one] == -(1). Proof. - simpl; rewrite Z.spec_m1; reflexivity. + simpl. nzsimpl. reflexivity. Qed. Definition compare (x y: t) := @@ -114,83 +158,36 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. end end. - Lemma Zcompare_spec_alt : - forall z z', Z.compare z z' = (Z.to_Z z ?= Z.to_Z z')%Z. + Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]). Proof. - intros; generalize (Z.spec_compare z z'); destruct Z.compare; auto. - intro H; rewrite H; symmetry; apply Zcompare_refl. + intros [z1 | x1 y1] [z2 | x2 y2]; + unfold Qcompare, compare; qsimpl. Qed. - Lemma Ncompare_spec_alt : - forall n n', N.compare n n' = (N.to_Z n ?= N.to_Z n')%Z. - Proof. - intros; generalize (N.spec_compare n n'); destruct N.compare; auto. - intro H; rewrite H; symmetry; apply Zcompare_refl. - Qed. + Definition lt n m := [n] < [m]. + Definition le n m := [n] <= [m]. + + 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. - Lemma N_to_Z2P : forall n, N.to_Z n <> 0%Z -> - Zpos (Z2P (N.to_Z n)) = N.to_Z n. + Lemma spec_min : forall n m, [min n m] == Qmin [n] [m]. Proof. - intros; apply Z2P_correct. - generalize (N.spec_pos n); romega. + unfold min, Qmin, GenericMinMax.gmin. intros. + rewrite spec_compare; destruct Qcompare; auto with qarith. Qed. - Hint Rewrite - Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l - Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp - Zcompare_spec_alt Ncompare_spec_alt - Z.spec_add N.spec_add Z.spec_mul N.spec_mul - Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1 - spec_Z_of_N spec_Zabs_N - : nz. - Ltac nzsimpl := autorewrite with nz in *. - - Ltac destr_neq_bool := repeat - (match goal with |- context [N.eq_bool ?x ?y] => - generalize (N.spec_eq_bool x y); case N.eq_bool - end). - - Ltac destr_zeq_bool := repeat - (match goal with |- context [Z.eq_bool ?x ?y] => - generalize (Z.spec_eq_bool x y); case Z.eq_bool - end). - - Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega). - Tactic Notation "simpl_ndiv" "in" "*" := - rewrite N.spec_div in * by (nzsimpl; romega). - - Ltac simpl_zdiv := rewrite Z.spec_div by (nzsimpl; romega). - Tactic Notation "simpl_zdiv" "in" "*" := - rewrite Z.spec_div in * by (nzsimpl; romega). - - Ltac qsimpl := try red; unfold to_Q; simpl; intros; - destr_neq_bool; destr_zeq_bool; simpl; nzsimpl; auto; intros. - - Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]). + Lemma spec_max : forall n m, [max n m] == Qmax [n] [m]. Proof. - intros [z1 | x1 y1] [z2 | x2 y2]; - unfold Qcompare, compare; qsimpl; rewrite ! N_to_Z2P; auto. + unfold max, Qmax, GenericMinMax.gmax. intros. + rewrite spec_compare; destruct Qcompare; auto with qarith. Qed. - Definition lt n m := compare n m = Lt. - Definition le n m := compare n m <> Gt. - 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. - Definition eq_bool n m := match compare n m with Eq => true | _ => false end. - Theorem spec_eq_bool: forall x y, - if eq_bool x y then [x] == [y] else ~([x] == [y]). + Theorem spec_eq_bool: forall x y, eq_bool x y = Qeq_bool [x] [y]. Proof. - intros. - unfold eq_bool. - rewrite spec_compare. - generalize (Qeq_alt [x] [y]). - destruct Qcompare. - intros H; rewrite H; auto. - intros H H'; rewrite H in H'; discriminate. - intros H H'; rewrite H in H'; discriminate. + intros. unfold eq_bool. rewrite spec_compare. reflexivity. Qed. (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *) @@ -209,7 +206,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destr_zcompare. simpl. rewrite <- H; qsimpl. congruence. reflexivity. - qsimpl. exfalso. generalize (N.spec_pos d); romega. + qsimpl. exfalso; romega. Qed. (** Normalisation function *) @@ -234,12 +231,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (* Lt *) rewrite strong_spec_check_int. qsimpl. - simpl_ndiv in *; nzsimpl. - generalize (Zgcd_div_pos (Z.to_Z p) (N.to_Z q)). omega. - simpl_ndiv in *. - rewrite H0 in *. rewrite Zdiv_0_l in H1; elim H1; auto. - rewrite 2 N_to_Z2P; auto. - simpl_ndiv; simpl_zdiv; nzsimpl. + generalize (Zgcd_div_pos (Z.to_Z p) (N.to_Z q)). romega. + replace (N.to_Z q) with 0%Z in * by assumption. + rewrite Zdiv_0_l in *; auto with zarith. apply Zgcd_div_swap0; romega. (* Gt *) qsimpl. @@ -260,20 +254,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. nzsimpl. destr_zcompare; rewrite ?strong_spec_check_int. (* Eq *) - simpl. - destr_neq_bool; nzsimpl; simpl; auto. - intros. - rewrite N_to_Z2P; auto. + qsimpl. (* Lt *) qsimpl. - rewrite N_to_Z2P; auto. - simpl_zdiv; simpl_ndiv in *; nzsimpl. rewrite Zgcd_1_rel_prime. destruct (Z_lt_le_dec 0 (N.to_Z q)). apply Zis_gcd_rel_prime; auto with zarith. apply Zgcd_is_gcd. replace (N.to_Z q) with 0%Z in * by romega. - simpl in H0; elim H0; auto. + rewrite Zdiv_0_l in *; romega. (* Gt *) simpl; auto with zarith. Qed. @@ -286,7 +275,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. | Qq n d => norm n d end. - Definition Reduced x := [red x] = [x]. + Class Reduced x := is_reduced : [red x] = [x]. Theorem spec_red : forall x, [red x] == [x]. Proof. @@ -328,19 +317,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_add : forall x y, [add x y] == [x] + [y]. Proof. - intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl. - intuition. - rewrite N_to_Z2P; auto. - intuition. - rewrite Pmult_1_r, N_to_Z2P; auto. - intuition. - rewrite Pmult_1_r, N_to_Z2P; auto. - destruct (Zmult_integral _ _ H); intuition. - rewrite Zpos_mult_morphism, 2 N_to_Z2P; auto. - rewrite (Z2P_correct (N.to_Z dx * N.to_Z dy)); auto. - apply Zmult_lt_0_compat. - generalize (N.spec_pos dx); romega. - generalize (N.spec_pos dy); romega. + intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl; + auto with zarith. + rewrite Pmult_1_r, Z2P_correct; auto. + rewrite Pmult_1_r, Z2P_correct; auto. + destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition. + rewrite Zpos_mult_morphism, 2 Z2P_correct; auto. Qed. Definition add_norm (x y: t): t := @@ -369,25 +351,19 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Proof. intros x y; rewrite <- spec_add. destruct x; destruct y; unfold add_norm, add; - destr_neq_bool; auto using Qeq_refl, spec_norm. + destr_eqb; auto using Qeq_refl, spec_norm. Qed. - Theorem strong_spec_add_norm : forall x y : t, - Reduced x -> Reduced y -> Reduced (add_norm x y). + Instance strong_spec_add_norm x y + `(Reduced x, Reduced y) : Reduced (add_norm x y). Proof. unfold Reduced; intros. rewrite strong_spec_red. rewrite <- (Qred_complete [add x y]); [ | rewrite spec_add, spec_add_norm; apply Qeq_refl ]. rewrite <- strong_spec_red. - destruct x as [zx|nx dx]; destruct y as [zy|ny dy]. - simpl in *; auto. - simpl; intros. - destr_neq_bool; nzsimpl; simpl; auto. - simpl; intros. - destr_neq_bool; nzsimpl; simpl; auto. - simpl; intros. - destr_neq_bool; nzsimpl; simpl; auto. + destruct x as [zx|nx dx]; destruct y as [zy|ny dy]; + simpl; destr_eqb; nzsimpl; simpl; auto. Qed. Definition opp (x: t): t := @@ -411,7 +387,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. intros; rewrite strong_spec_opp; red; auto. Qed. - Theorem strong_spec_opp_norm : forall q, Reduced q -> Reduced (opp q). + Instance strong_spec_opp_norm q `(Reduced q) : Reduced (opp q). Proof. unfold Reduced; intros. rewrite strong_spec_opp, <- H, !strong_spec_red, <- Qred_opp. @@ -434,8 +410,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite spec_opp; ring. Qed. - Theorem strong_spec_sub_norm : forall x y, - Reduced x -> Reduced y -> Reduced (sub_norm x y). + Instance strong_spec_sub_norm x y + `(Reduced x, Reduced y) : Reduced (sub_norm x y). Proof. intros. unfold sub_norm. @@ -454,24 +430,23 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_mul : forall x y, [mul x y] == [x] * [y]. Proof. intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl. - rewrite Pmult_1_r, N_to_Z2P; auto. - destruct (Zmult_integral _ _ H1); intuition. - rewrite H0 in H1; elim H1; auto. - rewrite H0 in H1; elim H1; auto. - rewrite H in H1; nzsimpl; elim H1; auto. - rewrite Zpos_mult_morphism, 2 N_to_Z2P; auto. - rewrite (Z2P_correct (N.to_Z dx * N.to_Z dy)); auto. - apply Zmult_lt_0_compat. - generalize (N.spec_pos dx); omega. - generalize (N.spec_pos dy); omega. + rewrite Pmult_1_r, Z2P_correct; auto. + destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition. + rewrite H0 in H1; auto with zarith. + rewrite H0 in H1; auto with zarith. + rewrite H in H1; nzsimpl; auto with zarith. + rewrite Zpos_mult_morphism, 2 Z2P_correct; auto. Qed. - Lemma norm_denum : forall n d, - [if N.eq_bool d N.one then Qz n else Qq n d] == [Qq n d]. + Definition norm_denum n d := + if N.eq_bool d N.one then Qz n else Qq n d. + + Lemma spec_norm_denum : forall n d, + [norm_denum n d] == [Qq n d]. Proof. - intros; simpl; qsimpl. - rewrite H0 in H; discriminate. - rewrite N_to_Z2P, H0; auto with zarith. + unfold norm_denum; intros; simpl; qsimpl. + congruence. + rewrite H0 in *; auto with zarith. Qed. Definition irred n d := @@ -499,10 +474,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. exists (Zgcd (Z.to_Z n) (N.to_Z d)). simpl. split. - simpl_zdiv; nzsimpl. + nzsimpl. destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)). rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. - simpl_ndiv; nzsimpl. + nzsimpl. destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)). rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. Qed. @@ -516,10 +491,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. nzsimpl; intros. destr_zcompare; auto. simpl. - simpl_ndiv; nzsimpl. + nzsimpl. rewrite H, Zdiv_0_l; auto. nzsimpl; destr_zcompare; simpl; auto. - simpl_ndiv; nzsimpl. + nzsimpl. intros. generalize (N.spec_pos d); intros. destruct (N.to_Z d); auto. @@ -542,7 +517,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. apply (Zgcd_inv_0_r (Z.to_Z n)). generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega. - simpl_ndiv; simpl_zdiv; nzsimpl. + nzsimpl. rewrite Zgcd_1_rel_prime. apply Zis_gcd_rel_prime. generalize (N.spec_pos d); romega. @@ -558,7 +533,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. | Gt => let z := Z.div z (Z_of_N gcd) in let d := N.div d gcd in - if N.eq_bool d N.one then Qz (Z.mul z n) else Qq (Z.mul z n) d + norm_denum (Z.mul z n) d | _ => Qq (Z.mul z n) d end. @@ -570,69 +545,61 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. | Qq nx dx, Qq ny dy => let (nx, dy) := irred nx dy in let (ny, dx) := irred ny dx in - let d := N.mul dx dy in - if N.eq_bool d N.one then Qz (Z.mul ny nx) else Qq (Z.mul ny nx) d + norm_denum (Z.mul ny nx) (N.mul dx dy) end. Lemma spec_mul_norm_Qz_Qq : forall z n d, [mul_norm_Qz_Qq z n d] == [Qq (Z.mul z n) d]. Proof. intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. - destr_zeq_bool; intros Hz; nzsimpl. + destr_eqb; nzsimpl; intros Hz. qsimpl; rewrite Hz; auto. - assert (Hd := N.spec_pos d). - destruct Z_le_gt_dec. + destruct Z_le_gt_dec; intros. qsimpl. - rewrite norm_denum. + rewrite spec_norm_denum. qsimpl. - simpl_ndiv in *; nzsimpl. - rewrite (Zdiv_gcd_zero _ _ H0 H) in z0; discriminate. - simpl_ndiv in *; nzsimpl. - rewrite H, Zdiv_0_l in H0; elim H0; auto. - rewrite 2 N_to_Z2P; auto. - simpl_ndiv; simpl_zdiv; nzsimpl. - rewrite (Zmult_comm (Z.to_Z z)), <- 2 Zmult_assoc. - rewrite <- Zgcd_div_swap0; auto with zarith; ring. + rewrite Zdiv_gcd_zero in z0; auto with zarith. + rewrite H in *. rewrite Zdiv_0_l in *; discriminate. + rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc. + rewrite Zgcd_div_swap0; try romega. + ring. Qed. - Lemma strong_spec_mul_norm_Qz_Qq : forall z n d, - Reduced (Qq n d) -> Reduced (mul_norm_Qz_Qq z n d). + Instance strong_spec_mul_norm_Qz_Qq z n d + `(Reduced (Qq n d)) : Reduced (mul_norm_Qz_Qq z n d). Proof. unfold Reduced; intros z n d. rewrite 2 strong_spec_red, 2 Qred_iff. simpl; nzsimpl. - destr_neq_bool; intros Hd H; simpl in *; nzsimpl. + destr_eqb; intros Hd H; simpl in *; nzsimpl. unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. - destr_zeq_bool; intros Hz; simpl; nzsimpl; simpl; auto. + destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto. destruct Z_le_gt_dec. simpl; nzsimpl. - destr_neq_bool; simpl; nzsimpl; auto. - intros H'; elim H'; auto. - destr_neq_bool; simpl; nzsimpl. - simpl_ndiv; nzsimpl; rewrite Hd, Zdiv_0_l; discriminate. + destr_eqb; simpl; nzsimpl; auto with zarith. + unfold norm_denum. destr_eqb; simpl; nzsimpl. + rewrite Hd, Zdiv_0_l; discriminate. intros _. - destr_neq_bool; simpl; nzsimpl; auto. - simpl_ndiv; nzsimpl; rewrite Hd, Zdiv_0_l; intro H'; elim H'; auto. + destr_eqb; simpl; nzsimpl; auto. + nzsimpl; rewrite Hd, Zdiv_0_l; auto with zarith. - rewrite N_to_Z2P in H; auto. + rewrite Z2P_correct in H; auto. unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. - destr_zeq_bool; intros Hz; simpl; nzsimpl; simpl; auto. + destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto. destruct Z_le_gt_dec as [H'|H']. simpl; nzsimpl. - destr_neq_bool; simpl; nzsimpl; auto. + destr_eqb; simpl; nzsimpl; auto. intros. - rewrite N_to_Z2P; auto. + rewrite Z2P_correct; auto. apply Zgcd_mult_rel_prime; auto. generalize (Zgcd_inv_0_l (Z.to_Z z) (N.to_Z d)) (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega. - destr_neq_bool; simpl; nzsimpl; auto. - simpl_ndiv; simpl_zdiv; nzsimpl. - intros. - destr_neq_bool; simpl; nzsimpl; auto. - simpl_ndiv in *; nzsimpl. - intros. - rewrite Z2P_correct. + destr_eqb; simpl; nzsimpl; auto. + unfold norm_denum. + destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto. + intros; nzsimpl. + rewrite Z2P_correct; auto. apply Zgcd_mult_rel_prime. rewrite Zgcd_1_rel_prime. apply Zis_gcd_rel_prime. @@ -648,9 +615,6 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite <- Huv; rewrite Hd0 at 2; ring. rewrite Hd0 at 1. symmetry; apply Z_div_mult_full; auto with zarith. - apply Zgcd_div_pos. - generalize (N.spec_pos d); romega. - generalize (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega. Qed. Theorem spec_mul_norm : forall x y, [mul_norm x y] == [x] * [y]. @@ -668,30 +632,24 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. assert (Hz':= spec_irred_zero ny dx). destruct irred as (n1,d1); destruct irred as (n2,d2). simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. - rewrite norm_denum. + rewrite spec_norm_denum. qsimpl. - elim H; destruct (Zmult_integral _ _ H0) as [Eq|Eq]. - rewrite <- Hz' in Eq; rewrite Eq; simpl; auto. - rewrite <- Hz in Eq; rewrite Eq; nzsimpl; auto. + destruct (Zmult_integral _ _ H0) as [Eq|Eq]. + rewrite Eq in *; simpl in *. + rewrite <- Hg2' in *; auto with zarith. + rewrite Eq in *; simpl in *. + rewrite <- Hg2 in *; auto with zarith. - elim H0; destruct (Zmult_integral _ _ H) as [Eq|Eq]. - rewrite Hz' in Eq; rewrite Eq; simpl; auto. - rewrite Hz in Eq; rewrite Eq; nzsimpl; auto. + destruct (Zmult_integral _ _ H) as [Eq|Eq]. + rewrite Hz' in Eq; rewrite Eq in *; auto with zarith. + rewrite Hz in Eq; rewrite Eq in *; auto with zarith. - rewrite 2 Z2P_correct. rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring. - - assert (0 <= N.to_Z d2 * N.to_Z d1)%Z - by (apply Zmult_le_0_compat; apply N.spec_pos). - romega. - assert (0 <= N.to_Z dx * N.to_Z dy)%Z - by (apply Zmult_le_0_compat; apply N.spec_pos). - romega. Qed. - Theorem strong_spec_mul_norm : forall x y, - Reduced x -> Reduced y -> Reduced (mul_norm x y). + Instance strong_spec_mul_norm x y + `(Reduced x, Reduced y) : Reduced (mul_norm x y). Proof. unfold Reduced; intros. rewrite strong_spec_red, Qred_iff. @@ -710,18 +668,21 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. assert (Hgc' := strong_spec_irred ny dx). destruct irred as (n1,d1); destruct irred as (n2,d2). simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2']. - destr_neq_bool; simpl; nzsimpl; intros; auto. - destr_neq_bool; simpl; nzsimpl; intros; auto. + + unfold norm_denum; qsimpl. + + assert (NEQ : N.to_Z dy <> 0%Z) by + (rewrite Hz; intros EQ; rewrite EQ in *; romega). + specialize (Hgc NEQ). + + assert (NEQ' : N.to_Z dx <> 0%Z) by + (rewrite Hz'; intro EQ; rewrite EQ in *; romega). + specialize (Hgc' NEQ'). revert H H0. rewrite 2 strong_spec_red, 2 Qred_iff; simpl. - destr_neq_bool; simpl; nzsimpl; intros. - rewrite Hz in H; rewrite H in H2; nzsimpl; elim H2; auto. - rewrite Hz' in H0; rewrite H0 in H2; nzsimpl; elim H2; auto. - rewrite Hz in H; rewrite H in H2; nzsimpl; elim H2; auto. - - rewrite N_to_Z2P in *; auto. - rewrite Z2P_correct. + destr_eqb; simpl; nzsimpl; try romega; intros. + rewrite Z2P_correct in *; auto. apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto. @@ -737,10 +698,6 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destruct (rel_prime_bezout _ _ H3) as [u v Huv]. apply Bezout_intro with (u*g)%Z (v*g')%Z. rewrite <- Huv, <- Hg2', <- Hg1. ring. - - assert (0 <= N.to_Z d2 * N.to_Z d1)%Z. - apply Zmult_le_0_compat; apply N.spec_pos. - romega. Qed. Definition inv (x: t): t := @@ -764,13 +721,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destruct x as [ z | n d ]. (* Qz z *) simpl. - rewrite Zcompare_spec_alt; destr_zcompare. + rewrite Z.spec_compare; destr_zcompare. (* 0 = z *) rewrite <- H. simpl; nzsimpl; compute; auto. (* 0 < z *) simpl. - destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ]. set (z':=Z.to_Z z) in *; clearbody z'. red; simpl. rewrite Zabs_eq by romega. @@ -778,7 +735,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. unfold Qinv; simpl; destruct z'; simpl; auto; discriminate. (* 0 > z *) simpl. - destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ]. set (z':=Z.to_Z z) in *; clearbody z'. red; simpl. rewrite Zabs_non_eq by romega. @@ -786,14 +743,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. unfold Qinv; simpl; destruct z'; simpl; auto; discriminate. (* Qq n d *) simpl. - rewrite Zcompare_spec_alt; destr_zcompare. + rewrite Z.spec_compare; destr_zcompare. (* 0 = n *) rewrite <- H. simpl; nzsimpl. - destr_neq_bool; intros; compute; auto. + destr_eqb; intros; compute; auto. (* 0 < n *) simpl. - destr_neq_bool; nzsimpl; intros. + destr_eqb; nzsimpl; intros. intros; rewrite Zabs_eq in *; romega. intros; rewrite Zabs_eq in *; romega. clear H1. @@ -805,10 +762,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. red; simpl. rewrite Z2P_correct by auto. unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate. - rewrite Zpos_mult_morphism, N_to_Z2P; auto. + rewrite Zpos_mult_morphism, Z2P_correct; auto. (* 0 > n *) simpl. - destr_neq_bool; nzsimpl; intros. + destr_eqb; nzsimpl; intros. intros; rewrite Zabs_non_eq in *; romega. intros; rewrite Zabs_non_eq in *; romega. clear H1. @@ -820,7 +777,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite Z2P_correct by romega. unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate. assert (T : forall x, Zneg x = Zopp (Zpos x)) by auto. - rewrite T, Zpos_mult_morphism, N_to_Z2P; auto; ring. + rewrite T, Zpos_mult_morphism, Z2P_correct; auto; ring. Qed. Definition inv_norm (x: t): t := @@ -855,28 +812,28 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destruct x as [ z | n d ]. (* Qz z *) simpl. - rewrite Zcompare_spec_alt; destr_zcompare; auto with qarith. + rewrite Z.spec_compare; destr_zcompare; auto with qarith. (* Qq n d *) - simpl; nzsimpl; destr_neq_bool. + simpl; nzsimpl; destr_eqb. destr_zcompare; simpl; auto with qarith. - destr_neq_bool; nzsimpl; auto with qarith. + destr_eqb; nzsimpl; auto with qarith. intros _ Hd; rewrite Hd; auto with qarith. - destr_neq_bool; nzsimpl; auto with qarith. + destr_eqb; nzsimpl; auto with qarith. intros _ Hd; rewrite Hd; auto with qarith. (* 0 < n *) destr_zcompare; auto with qarith. destr_zcompare; nzsimpl; simpl; auto with qarith; intros. - destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ]. rewrite H0; auto with qarith. romega. (* 0 > n *) destr_zcompare; nzsimpl; simpl; auto with qarith. - destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ]. rewrite H0; auto with qarith. romega. Qed. - Theorem strong_spec_inv_norm : forall x, Reduced x -> Reduced (inv_norm x). + Instance strong_spec_inv_norm x `(Reduced x) : Reduced (inv_norm x). Proof. unfold Reduced. intros. @@ -885,42 +842,40 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. simpl; nzsimpl. rewrite strong_spec_red, Qred_iff. destr_zcompare; simpl; nzsimpl; auto. - destr_neq_bool; nzsimpl; simpl; auto. - destr_neq_bool; nzsimpl; simpl; auto. + destr_eqb; nzsimpl; simpl; auto. + destr_eqb; nzsimpl; simpl; auto. (* Qq n d *) rewrite strong_spec_red, Qred_iff in H; revert H. simpl; nzsimpl. - destr_neq_bool; nzsimpl; auto with qarith. + destr_eqb; nzsimpl; auto with qarith. destr_zcompare; simpl; nzsimpl; auto; intros. (* 0 < n *) destr_zcompare; simpl; nzsimpl; auto. - destr_neq_bool; nzsimpl; simpl; auto. + destr_eqb; nzsimpl; simpl; auto. rewrite Zabs_eq; romega. intros _. rewrite strong_spec_norm; simpl; nzsimpl. - destr_neq_bool; nzsimpl. + destr_eqb; nzsimpl. rewrite Zabs_eq; romega. intros _. rewrite Qred_iff. simpl. rewrite Zabs_eq; auto with zarith. - rewrite N_to_Z2P in *; auto. - rewrite Z2P_correct; auto with zarith. + rewrite Z2P_correct in *; auto. rewrite Zgcd_comm; auto. (* 0 > n *) - destr_neq_bool; nzsimpl; simpl; auto; intros. + destr_eqb; nzsimpl; simpl; auto; intros. destr_zcompare; simpl; nzsimpl; auto. - destr_neq_bool; nzsimpl. + destr_eqb; nzsimpl. rewrite Zabs_non_eq; romega. intros _. rewrite strong_spec_norm; simpl; nzsimpl. - destr_neq_bool; nzsimpl. + destr_eqb; nzsimpl. rewrite Zabs_non_eq; romega. intros _. rewrite Qred_iff. simpl. - rewrite N_to_Z2P in *; auto. - rewrite Z2P_correct; auto with zarith. + rewrite Z2P_correct in *; auto. intros. rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm. apply Zis_gcd_gcd; auto with zarith. @@ -949,8 +904,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. apply spec_inv_norm; auto. Qed. - Theorem strong_spec_div_norm : forall x y, - Reduced x -> Reduced y -> Reduced (div_norm x y). + Instance strong_spec_div_norm x y + `(Reduced x, Reduced y) : Reduced (div_norm x y). Proof. intros; unfold div_norm. apply strong_spec_mul_norm; auto. @@ -968,14 +923,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destruct x as [ z | n d ]. simpl; rewrite Z.spec_square; red; auto. simpl. - destr_neq_bool; nzsimpl; intros. + destr_eqb; nzsimpl; intros. apply Qeq_refl. rewrite N.spec_square in *; nzsimpl. - contradict H; elim (Zmult_integral _ _ H0); auto. + elim (Zmult_integral _ _ H0); romega. rewrite N.spec_square in *; nzsimpl. - rewrite H in H0; simpl in H0; elim H0; auto. - assert (0 < N.to_Z d)%Z by (generalize (N.spec_pos d); romega). - clear H H0. + rewrite H in H0; romega. rewrite Z.spec_square, N.spec_square. red; simpl. rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto. @@ -1000,37 +953,35 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (* Qq *) simpl. rewrite Z.spec_power_pos. - destr_neq_bool; nzsimpl; intros. + destr_eqb; nzsimpl; intros. apply Qeq_sym; apply Qpower_positive_0. rewrite N.spec_power_pos in *. - assert (0 < N.to_Z d ^ ' p)%Z. - apply Zpower_gt_0; auto with zarith. - generalize (N.spec_pos d); romega. + assert (0 < N.to_Z d ^ ' p)%Z by + (apply Zpower_gt_0; auto with zarith). romega. rewrite N.spec_power_pos, H in *. - rewrite Zpower_0_l in H0; [ elim H0; auto | discriminate ]. + rewrite Zpower_0_l in H0; [romega|discriminate]. rewrite Qpower_decomp. red; simpl; do 3 f_equal. rewrite Z2P_correct by (generalize (N.spec_pos d); romega). rewrite N.spec_power_pos. auto. Qed. - Theorem strong_spec_power_pos : forall x p, - Reduced x -> Reduced (power_pos x p). + Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p). Proof. destruct x as [z | n d]; simpl; intros. red; simpl; auto. red; simpl; intros. rewrite strong_spec_norm; simpl. - destr_neq_bool; nzsimpl; intros. + destr_eqb; nzsimpl; intros. simpl; auto. rewrite Qred_iff. revert H. unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl. - destr_neq_bool; nzsimpl; simpl; intros. + destr_eqb; nzsimpl; simpl; intros. rewrite N.spec_power_pos in H0. - elim H0; rewrite H; rewrite Zpower_0_l; auto; discriminate. - rewrite N_to_Z2P in *; auto. + rewrite H, Zpower_0_l in *; [romega|discriminate]. + rewrite Z2P_correct in *; auto. rewrite N.spec_power_pos, Z.spec_power_pos; auto. rewrite Zgcd_1_rel_prime in *. apply rel_prime_Zpower; auto with zarith. @@ -1068,8 +1019,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl. Qed. - Theorem strong_spec_power_norm : forall x z, - Reduced x -> Reduced (power_norm x z). + Instance strong_spec_power_norm x z + `(Reduced x) : Reduced (power_norm x z). Proof. destruct z; simpl. intros _; unfold Reduced; rewrite strong_spec_red. @@ -1096,7 +1047,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. unfold of_Qc; rewrite strong_spec_of_Q; auto. Qed. - Lemma strong_spec_of_Qc_bis : forall q, Reduced (of_Qc q). + Instance strong_spec_of_Qc_bis q : Reduced (of_Qc q). Proof. intros; red; rewrite strong_spec_red, strong_spec_of_Qc. destruct q; simpl; auto. @@ -1297,7 +1248,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. unfold Qcinv, Q2Qc, this; rewrite Qred_correct; auto with qarith. Qed. - Theorem spec_squarec x: [[square x]] = [[x]]^2. + Theorem spec_squarec x: [[square x]] = [[x]]^2. Proof. intros x; unfold to_Qc. apply trans_equal with (!! ([x]^2)). diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index 8be66493e5..1959f4ad69 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Import QArith Qpower. +Require Import QArith Qpower Qminmax. Open Scope Q_scope. @@ -26,67 +26,45 @@ Module Type QType. Notation "[ x ]" := (to_Q x). Definition eq x y := [x] == [y]. + Definition lt x y := [x] < [y]. + Definition le x y := [x] <= [y]. Parameter of_Q : Q -> t. Parameter spec_of_Q: forall x, to_Q (of_Q x) == x. + Parameter red : t -> t. + Parameter compare : t -> t -> comparison. + Parameter eq_bool : t -> t -> bool. + Parameter max : t -> t -> t. + Parameter min : t -> t -> t. Parameter zero : t. Parameter one : t. Parameter minus_one : t. + Parameter add : t -> t -> t. + Parameter sub : t -> t -> t. + Parameter opp : t -> t. + Parameter mul : t -> t -> t. + Parameter square : t -> t. + Parameter inv : t -> t. + Parameter div : t -> t -> t. + Parameter power : t -> Z -> t. + Parameter spec_red : forall x, [red x] == [x]. + Parameter strong_spec_red : forall x, [red x] = Qred [x]. + Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]). + Parameter spec_eq_bool : forall x y, eq_bool x y = Qeq_bool [x] [y]. + Parameter spec_max : forall x y, [max x y] == Qmax [x] [y]. + Parameter spec_min : forall x y, [min x y] == Qmin [x] [y]. Parameter spec_0: [zero] == 0. Parameter spec_1: [one] == 1. Parameter spec_m1: [minus_one] == -(1). - - Parameter compare : t -> t -> comparison. - - Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]). - - Definition lt n m := compare n m = Lt. - Definition le n m := compare n m <> Gt. - 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. - - Parameter eq_bool : t -> t -> bool. - - Parameter spec_eq_bool : forall x y, - if eq_bool x y then [x]==[y] else ~([x]==[y]). - - Parameter red : t -> t. - - Parameter spec_red : forall x, [red x] == [x]. - Parameter strong_spec_red : forall x, [red x] = Qred [x]. - - Parameter add : t -> t -> t. - Parameter spec_add: forall x y, [add x y] == [x] + [y]. - - Parameter sub : t -> t -> t. - Parameter spec_sub: forall x y, [sub x y] == [x] - [y]. - - Parameter opp : t -> t. - Parameter spec_opp: forall x, [opp x] == - [x]. - - Parameter mul : t -> t -> t. - Parameter spec_mul: forall x y, [mul x y] == [x] * [y]. - - Parameter square : t -> t. - Parameter spec_square: forall x, [square x] == [x] ^ 2. - - Parameter inv : t -> t. - Parameter spec_inv : forall x, [inv x] == / [x]. - - Parameter div : t -> t -> t. - Parameter spec_div: forall x y, [div x y] == [x] / [y]. - - Parameter power : t -> Z -> t. - Parameter spec_power: forall x z, [power x z] == [x] ^ z. End QType. diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index 4d92aadb10..692bfd9296 100644 --- a/theories/QArith/QOrderedType.v +++ b/theories/QArith/QOrderedType.v @@ -15,12 +15,12 @@ Local Open Scope Q_scope. Module Q_as_DT <: DecidableTypeFull. Definition t := Q. Definition eq := Qeq. - Definition eq_equiv := Q_setoid. + Definition eq_equiv := Q_Setoid. Definition eqb := Qeq_bool. Definition eqb_eq := Qeq_bool_iff. - Include Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *) - Include Bool2Dec_fun. (** eq_dec *) + Include BackportEq. (** eq_refl, eq_sym, eq_trans *) + Include HasEqBool2Dec. (** eq_dec *) End Q_as_DT. diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v index d20396c86a..d05a85947d 100644 --- a/theories/QArith/Qminmax.v +++ b/theories/QArith/Qminmax.v @@ -21,8 +21,10 @@ Module QHasMinMax <: HasMinMax Q_as_OT. Module QMM := GenericMinMax Q_as_OT. Definition max := Qmax. Definition min := Qmin. - Definition max_spec := QMM.max_spec. - Definition min_spec := QMM.min_spec. + Definition max_l := QMM.max_l. + Definition max_r := QMM.max_r. + Definition min_l := QMM.min_l. + Definition min_r := QMM.min_r. End QHasMinMax. Module Q. diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget index bc13ae2427..b3faef8817 100644 --- a/theories/QArith/vo.itarget +++ b/theories/QArith/vo.itarget @@ -8,3 +8,5 @@ Qreals.vo Qreduction.vo Qring.vo Qround.vo +QOrderedType.vo +Qminmax.vo
\ No newline at end of file diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 01c6134b2a..a62d96aa0f 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -175,9 +175,6 @@ Qed. (** *** Least-upper bound properties of [max] *) -Definition max_l := max_l. -Definition max_r := max_r. - Lemma le_max_l : forall n m, n <= max n m. Proof. intros; destruct (max_spec n m); intuition; order. @@ -329,9 +326,6 @@ Proof. intros. symmetry; apply MPRev.max_assoc. Qed. Lemma min_comm : forall n m, min n m == min m n. Proof. intros. exact (MPRev.max_comm m n). Qed. -Definition min_l := min_l. -Definition min_r := min_r. - Lemma le_min_r : forall n m, min n m <= m. Proof. intros. exact (MPRev.le_max_l m n). Qed. @@ -544,6 +538,10 @@ Module MinMaxProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O). Module OT := OTF_to_TotalOrder O. Include MinMaxLogicalProperties OT M. Include MinMaxDecProperties O M. + Definition max_l := max_l. + Definition max_r := max_r. + Definition min_l := min_l. + Definition min_r := min_r. Notation max_monotone := max_mono. Notation min_monotone := min_mono. Notation max_min_antimonotone := max_min_antimono. @@ -611,6 +609,10 @@ Module UsualMinMaxProperties Module OT := OTF_to_TotalOrder O. Include UsualMinMaxLogicalProperties OT M. Include UsualMinMaxDecProperties O M. + Definition max_l := max_l. + Definition max_r := max_r. + Definition min_l := min_l. + Definition min_r := min_r. End UsualMinMaxProperties. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 64c764d9fc..66a672c920 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -262,11 +262,9 @@ End OTF_to_OrderTac. Module OT_to_OrderTac (OT:OrderedType). Module OTF := OT_to_Full OT. - Include !OTF_to_OrderTac OTF. (* Why a bang here ? *) + Include !OTF_to_OrderTac OTF. End OT_to_OrderTac. - - Module TotalOrderRev (O:TotalOrder) <: TotalOrder. Definition t := O.t. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 5aab73f2e0..8cdd73cc7c 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -228,3 +228,8 @@ Proof. discriminate. Qed. +Lemma Zeq_bool_if : forall x y, if Zeq_bool x y then x=y else x<>y. +Proof. + intros. generalize (Zeq_bool_eq x y)(Zeq_bool_neq x y). + destruct Zeq_bool; auto. +Qed.
\ No newline at end of file |