diff options
| author | letouzey | 2010-01-17 13:31:24 +0000 |
|---|---|---|
| committer | letouzey | 2010-01-17 13:31:24 +0000 |
| commit | cd4f47d6aa9654b163a2494e462aa43001b55fda (patch) | |
| tree | 524cf2c4138b9c973379915ed7558005db8ecdab | |
| parent | 0768a9c968dfc205334dabdd3e86d2a91bb7a33a (diff) | |
BigN, BigZ, BigQ: presentation via unique module with both ops and props
We use the <+ operation to regroup all known facts about BigN
(resp BigZ, ...) in a unique module. This uses also the new ! feature
for controling inlining. By the way, we also make sure that these
new BigN and BigZ modules implements OrderedTypeFull and TotalOrder,
and also contains facts about min and max (cf. GenericMinMax).
Side effects:
- In NSig and ZSig, specification of compare and eq_bool is now
done with respect to Zcompare and Zeq_bool, as for other ops.
The order <= and < are also defined via Zle and Zlt, instead
of using compare. Min and max are axiomatized instead of being
macros.
- Some proofs rework in QMake
- QOrderedType and Qminmax were in fact not compiled by make world
Still todo: OrderedType + MinMax for BigQ, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |