diff options
Diffstat (limited to 'theories/Numbers/Rational')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/BigQ.v | 207 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 721 | ||||
| -rw-r--r-- | theories/Numbers/Rational/SpecViaQ/QSig.v | 202 |
3 files changed, 597 insertions, 533 deletions
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index f01cbbc5..0bc71166 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -5,12 +5,13 @@ (* // * 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: BigQ.v 12509 2009-11-12 15:52:50Z letouzey $ i*) +(** * BigQ: an efficient implementation of rational numbers *) + +(** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) -Require Import Field Qfield BigN BigZ QSig QMake. +Require Export BigZ. +Require Import Field Qfield QSig QMake Orders GenericMinMax. (** We choose for BigQ an implemention with multiple representation of 0: 0, 1/0, 2/0 etc. @@ -34,7 +35,9 @@ End BigN_BigZ. (** This allows to build [BigQ] out of [BigN] and [BigQ] via [QMake] *) -Module BigQ <: QSig.QType := QMake.Make BigN BigZ BigN_BigZ. +Module BigQ <: QType <: OrderedTypeFull <: TotalOrder := + QMake.Make BigN BigZ BigN_BigZ <+ !QProperties <+ HasEqBool2Dec + <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties. (** Notations about [BigQ] *) @@ -43,12 +46,40 @@ Notation bigQ := BigQ.t. Delimit Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with bigQ. Bind Scope bigQ_scope with BigQ.t. - -(* Allow nice printing of rational numerals, either as (Qz 1234) - or as (Qq 1234 5678) *) +Bind Scope bigQ_scope with BigQ.t_. +(* Bind Scope has no retroactive effect, let's declare scopes by hand. *) Arguments Scope BigQ.Qz [bigZ_scope]. -Arguments Scope BigQ.Qq [bigZ_scope bigN_scope]. - +Arguments Scope BigQ.Qq [bigZ_scope bigN_scope]. +Arguments Scope BigQ.to_Q [bigQ_scope]. +Arguments Scope BigQ.red [bigQ_scope]. +Arguments Scope BigQ.opp [bigQ_scope]. +Arguments Scope BigQ.inv [bigQ_scope]. +Arguments Scope BigQ.square [bigQ_scope]. +Arguments Scope BigQ.add [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.sub [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.mul [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.div [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.eq [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.lt [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.le [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.eq [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.compare [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.min [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.max [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.eq_bool [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.power_pos [bigQ_scope positive_scope]. +Arguments Scope BigQ.power [bigQ_scope Z_scope]. +Arguments Scope BigQ.inv_norm [bigQ_scope]. +Arguments Scope BigQ.add_norm [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.sub_norm [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.mul_norm [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.div_norm [bigQ_scope bigQ_scope]. +Arguments Scope BigQ.power_norm [bigQ_scope bigQ_scope]. + +(** As in QArith, we use [#] to denote fractions *) +Notation "p # q" := (BigQ.Qq p q) (at level 55, no associativity) : bigQ_scope. +Local Notation "0" := BigQ.zero : bigQ_scope. +Local Notation "1" := BigQ.one : bigQ_scope. Infix "+" := BigQ.add : bigQ_scope. Infix "-" := BigQ.sub : bigQ_scope. Notation "- x" := (BigQ.opp x) : bigQ_scope. @@ -57,142 +88,102 @@ Infix "/" := BigQ.div : bigQ_scope. Infix "^" := BigQ.power : bigQ_scope. Infix "?=" := BigQ.compare : bigQ_scope. Infix "==" := BigQ.eq : bigQ_scope. +Notation "x != y" := (~x==y)%bigQ (at level 70, no associativity) : bigQ_scope. Infix "<" := BigQ.lt : bigQ_scope. Infix "<=" := BigQ.le : bigQ_scope. Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope. Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope. +Notation "x < y < z" := (x<y /\ y<z)%bigQ : bigQ_scope. +Notation "x < y <= z" := (x<y /\ y<=z)%bigQ : bigQ_scope. +Notation "x <= y < z" := (x<=y /\ y<z)%bigQ : bigQ_scope. +Notation "x <= y <= z" := (x<=y /\ y<=z)%bigQ : bigQ_scope. Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. -Open Scope bigQ_scope. - -(** [BigQ] is a setoid *) - -Add Relation BigQ.t BigQ.eq - reflexivity proved by (fun x => Qeq_refl [x]) - symmetry proved by (fun x y => Qeq_sym [x] [y]) - transitivity proved by (fun x y z => Qeq_trans [x] [y] [z]) -as BigQeq_rel. - -Add Morphism BigQ.add with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQadd_wd. -Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_add; rewrite H, H0; apply Qeq_refl. -Qed. - -Add Morphism BigQ.opp with signature BigQ.eq ==> BigQ.eq as BigQopp_wd. -Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_opp; rewrite H; apply Qeq_refl. -Qed. - -Add Morphism BigQ.sub with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQsub_wd. -Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_sub; rewrite H, H0; apply Qeq_refl. -Qed. - -Add Morphism BigQ.mul with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQmul_wd. -Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_mul; rewrite H, H0; apply Qeq_refl. -Qed. - -Add Morphism BigQ.inv with signature BigQ.eq ==> BigQ.eq as BigQinv_wd. -Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_inv; rewrite H; apply Qeq_refl. -Qed. - -Add Morphism BigQ.div with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQdiv_wd. -Proof. - unfold BigQ.eq; intros; rewrite !BigQ.spec_div; rewrite H, H0; apply Qeq_refl. -Qed. - -(* TODO : fix this. For the moment it's useless (horribly slow) -Hint Rewrite - BigQ.spec_0 BigQ.spec_1 BigQ.spec_m1 BigQ.spec_compare - BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp - BigQ.spec_mul BigQ.spec_inv BigQ.spec_div BigQ.spec_power_pos - BigQ.spec_square : bigq. *) - +Local Open Scope bigQ_scope. (** [BigQ] is a field *) Lemma BigQfieldth : - field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq. + field_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp + BigQ.div BigQ.inv BigQ.eq. Proof. constructor. -constructor; intros; red. -rewrite BigQ.spec_add, BigQ.spec_0; ring. -rewrite ! BigQ.spec_add; ring. -rewrite ! BigQ.spec_add; ring. -rewrite BigQ.spec_mul, BigQ.spec_1; ring. -rewrite ! BigQ.spec_mul; ring. -rewrite ! BigQ.spec_mul; ring. -rewrite BigQ.spec_add, ! BigQ.spec_mul, BigQ.spec_add; ring. -unfold BigQ.sub; apply Qeq_refl. -rewrite BigQ.spec_add, BigQ.spec_0, BigQ.spec_opp; ring. -compute; discriminate. -intros; red. -unfold BigQ.div; apply Qeq_refl. -intros; red. -rewrite BigQ.spec_mul, BigQ.spec_inv, BigQ.spec_1; field. -rewrite <- BigQ.spec_0; auto. -Qed. - -Lemma BigQpowerth : - power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power. -Proof. constructor. -intros; red. -rewrite BigQ.spec_power. -replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q. -destruct n. -simpl; compute; auto. -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. -Proof. -intros; generalize (BigQ.spec_eq_bool x y); rewrite H; auto. +exact BigQ.add_0_l. exact BigQ.add_comm. exact BigQ.add_assoc. +exact BigQ.mul_1_l. exact BigQ.mul_comm. exact BigQ.mul_assoc. +exact BigQ.mul_add_distr_r. exact BigQ.sub_add_opp. +exact BigQ.add_opp_diag_r. exact BigQ.neq_1_0. +exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l. Qed. -Lemma BigQ_eq_bool_complete : - forall x y, x==y -> BigQ.eq_bool x y = true. +Lemma BigQpowerth : + power_theory 1 BigQ.mul BigQ.eq Z_of_N BigQ.power. Proof. -intros; generalize (BigQ.spec_eq_bool x y). -destruct BigQ.eq_bool; auto. +constructor. intros. BigQ.qify. +replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q by (now destruct n). +destruct n. reflexivity. +induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity. Qed. -(* TODO : improve later the detection of constants ... *) +Ltac isBigQcst t := + match t with + | BigQ.Qz ?t => isBigZcst t + | BigQ.Qq ?n ?d => match isBigZcst n with + | true => isBigNcst d + | false => constr:false + end + | BigQ.zero => constr:true + | BigQ.one => constr:true + | BigQ.minus_one => constr:true + | _ => constr:false + end. Ltac BigQcst t := - match t with - | BigQ.zero => BigQ.zero - | BigQ.one => BigQ.one - | BigQ.minus_one => BigQ.minus_one - | _ => NotConstant + match isBigQcst t with + | true => constr:t + | false => constr:NotConstant end. Add Field BigQfield : BigQfieldth - (decidable BigQ_eq_bool_correct, - completeness BigQ_eq_bool_complete, + (decidable BigQ.eqb_correct, + completeness BigQ.eqb_complete, constants [BigQcst], power_tac BigQpowerth [Qpow_tac]). -Section Examples. +Section TestField. Let ex1 : forall x y z, (x+y)*z == (x*z)+(y*z). intros. ring. Qed. -Let ex8 : forall x, x ^ 1 == x. +Let ex8 : forall x, x ^ 2 == x*x. intro. ring. Qed. -Let ex10 : forall x y, ~(y==BigQ.zero) -> (x/y)*y == x. +Let ex10 : forall x y, y!=0 -> (x/y)*y == x. intros. field. auto. Qed. -End Examples.
\ No newline at end of file +End TestField. + +(** [BigQ] can also benefit from an "order" tactic *) + +Module BigQ_Order := !OrdersTac.MakeOrderTac BigQ. +Ltac bigQ_order := BigQ_Order.order. + +Section TestOrder. +Let test : forall x y : bigQ, x<=y -> y<=x -> x==y. +Proof. bigQ_order. Qed. +End TestOrder. + +(** We can also reason by switching to QArith thanks to tactic + BigQ.qify. *) + +Section TestQify. +Let test : forall x : bigQ, 0+x == 1*x. +Proof. intro x. BigQ.qify. ring. Qed. +End TestQify. diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 494420bd..407f7b90 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: QMake.v 11208 2008-07-04 16:57:46Z letouzey $ 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. @@ -28,27 +33,27 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. number y interpreted as x/y. The pairs (x,0) and (0,y) are all interpreted as 0. *) - Inductive t_ := + Inductive t_ := | Qz : Z.t -> t_ | Qq : Z.t -> N.t -> t_. Definition t := t_. - (** Specification with respect to [QArith] *) + (** Specification with respect to [QArith] *) - Open Local Scope Q_scope. + Local Open Scope Q_scope. Definition of_Z x: t := Qz (Z.of_Z x). - Definition of_Q (q:Q) : t := - let (x,y) := q in - match y with + Definition of_Q (q:Q) : t := + let (x,y) := q in + match y with | 1%positive => Qz (Z.of_Z x) | _ => Qq (Z.of_Z x) (N.of_N (Npos y)) end. - Definition to_Q (q: t) := - match q with + Definition to_Q (q: t) := + match q with | Qz x => Z.to_Z x # 1 | Qq x y => if N.eq_bool y N.zero then 0 else Z.to_Z x # Z2P (N.to_Z y) @@ -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; intros; 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; intros; 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,131 +126,96 @@ 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) := match x, y with | Qz zx, Qz zy => Z.compare zx zy - | Qz zx, Qq ny dy => + | Qz zx, Qq ny dy => if N.eq_bool dy N.zero then Z.compare zx Z.zero else Z.compare (Z.mul zx (Z_of_N dy)) ny - | Qq nx dx, Qz zy => - if N.eq_bool dx N.zero then Z.compare Z.zero zy + | Qq nx dx, Qz zy => + if N.eq_bool dx N.zero then Z.compare Z.zero zy else Z.compare nx (Z.mul zy (Z_of_N dx)) | Qq nx dx, Qq ny dy => match N.eq_bool dx N.zero, N.eq_bool dy N.zero with | true, true => Eq | true, false => Z.compare Z.zero ny | false, true => Z.compare nx Z.zero - | false, false => Z.compare (Z.mul nx (Z_of_N dy)) + | false, false => Z.compare (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) 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. + + 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 spec_min : forall n m, [min n m] == Qmin [n] [m]. Proof. - intros; generalize (N.spec_compare n n'); destruct N.compare; auto. - intro H; rewrite H; symmetry; apply Zcompare_refl. + unfold min, Qmin, GenericMinMax.gmin. intros. + rewrite spec_compare; destruct Qcompare; auto with qarith. Qed. - Lemma N_to_Z2P : forall n, N.to_Z n <> 0%Z -> - Zpos (Z2P (N.to_Z n)) = N.to_Z n. + Lemma spec_max : forall n m, [max n m] == Qmax [n] [m]. Proof. - intros; apply Z2P_correct. - generalize (N.spec_pos n); romega. + unfold max, Qmax, GenericMinMax.gmax. 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 - 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. + Definition eq_bool n m := + match compare n m with Eq => true | _ => false end. - Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]). + Theorem spec_eq_bool: forall x y, eq_bool x y = Qeq_bool [x] [y]. Proof. - intros [z1 | x1 y1] [z2 | x2 y2]; - unfold Qcompare, compare; qsimpl; rewrite ! N_to_Z2P; auto. + intros. unfold eq_bool. rewrite spec_compare. reflexivity. 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. + (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *) - Definition eq_bool n m := - match compare n m with Eq => true | _ => false end. + Definition check_int n d := + match N.compare N.one d with + | Lt => Qq n d + | Eq => Qz n + | Gt => zero (* n/0 encodes 0 *) + end. - Theorem spec_eq_bool: forall x y, - if eq_bool x y then [x] == [y] else ~([x] == [y]). + Theorem strong_spec_check_int : forall n d, [check_int n d] = [Qq n d]. 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 check_int. + nzsimpl. + destr_zcompare. + simpl. rewrite <- H; qsimpl. congruence. + reflexivity. + qsimpl. exfalso; romega. Qed. (** Normalisation function *) Definition norm n d : t := - let gcd := N.gcd (Zabs_N n) d in + let gcd := N.gcd (Zabs_N n) d in match N.compare N.one gcd with - | Lt => - let n := Z.div n (Z_of_N gcd) in - let d := N.div d gcd in - match N.compare d N.one with - | Gt => Qq n d - | Eq => Qz n - | Lt => zero - end - | Eq => Qq n d + | Lt => check_int (Z.div n (Z_of_N gcd)) (N.div d gcd) + | Eq => check_int n d | Gt => zero (* gcd = 0 => both numbers are 0 *) end. @@ -217,29 +226,16 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. assert (Hq := N.spec_pos q). nzsimpl. destr_zcompare. + (* Eq *) + rewrite strong_spec_check_int; reflexivity. + (* Lt *) + rewrite strong_spec_check_int. qsimpl. - - simpl_ndiv. - destr_zcompare. - qsimpl. - rewrite H1 in *; rewrite Zdiv_0_l in H0; discriminate. - rewrite N_to_Z2P; auto. - simpl_zdiv; nzsimpl. - rewrite Zgcd_div_swap0, H0; romega. - - qsimpl. - assert (0 < N.to_Z q / Zgcd (Z.to_Z p) (N.to_Z q))%Z. - apply Zgcd_div_pos; romega. - romega. - - qsimpl. - simpl_ndiv in *; nzsimpl; romega. - simpl_ndiv in *. - rewrite H1, Zdiv_0_l in H2; elim H2; 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. assert (H' : Zgcd (Z.to_Z p) (N.to_Z q) = 0%Z). generalize (Zgcd_is_pos (Z.to_Z p) (N.to_Z q)); romega. @@ -249,48 +245,37 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q]. Proof. intros. - replace (Qred [Qq p q]) with (Qred [norm p q]) by + replace (Qred [Qq p q]) with (Qred [norm p q]) by (apply Qred_complete; apply spec_norm). symmetry; apply Qred_identity. unfold norm. assert (Hp := N.spec_pos (Zabs_N p)). assert (Hq := N.spec_pos q). nzsimpl. - destr_zcompare. + destr_zcompare; rewrite ?strong_spec_check_int. (* Eq *) - simpl. - destr_neq_bool; nzsimpl; simpl; auto. - intros. - rewrite N_to_Z2P; auto. - (* Lt *) - simpl_ndiv. - destr_zcompare. - qsimpl; auto. qsimpl. + (* Lt *) qsimpl. - simpl_zdiv; nzsimpl. - rewrite N_to_Z2P; auto. - clear H1. - simpl_ndiv; 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. - rewrite Zdiv_0_l in H0; discriminate. + rewrite Zdiv_0_l in *; romega. (* Gt *) - simpl; auto. + simpl; auto with zarith. Qed. - (** Reduction function : producing irreducible fractions *) + (** Reduction function : producing irreducible fractions *) - Definition red (x : t) : t := - match x with + Definition red (x : t) : t := + match x with | Qz z => x | 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. @@ -304,21 +289,21 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Proof. intros [ z | n d ]. unfold red. - symmetry; apply Qred_identity; simpl; auto. + symmetry; apply Qred_identity; simpl; auto with zarith. unfold red; apply strong_spec_norm. Qed. - + Definition add (x y: t): t := match x with | Qz zx => match y with | Qz zy => Qz (Z.add zx zy) - | Qq ny dy => - if N.eq_bool dy N.zero then x + | Qq ny dy => + if N.eq_bool dy N.zero then x else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy end | Qq nx dx => - if N.eq_bool dx N.zero then y + if N.eq_bool dx N.zero then y else match y with | Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx | Qq ny dy => @@ -332,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 := @@ -352,12 +330,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. | Qz zx => match y with | Qz zy => Qz (Z.add zx zy) - | Qq ny dy => - if N.eq_bool dy N.zero then x + | Qq ny dy => + if N.eq_bool dy N.zero then x else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy end | Qq nx dx => - if N.eq_bool dx N.zero then y + if N.eq_bool dx N.zero then y else match y with | Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx | Qq ny dy => @@ -372,26 +350,20 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y]. Proof. intros x y; rewrite <- spec_add. - destruct x; destruct y; unfold add_norm, add; - destr_neq_bool; auto using Qeq_refl, spec_norm. + destruct x; destruct y; unfold add_norm, add; + 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 <- (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 := @@ -404,7 +376,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Proof. intros [z | x y]; simpl. rewrite Z.spec_opp; auto. - match goal with |- context[N.eq_bool ?X ?Y] => + match goal with |- context[N.eq_bool ?X ?Y] => generalize (N.spec_eq_bool X Y); case N.eq_bool end; auto; rewrite N.spec_0. rewrite Z.spec_opp; auto. @@ -415,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. @@ -438,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. @@ -458,35 +430,34 @@ 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 := + Definition irred n d := let gcd := N.gcd (Zabs_N n) d in - match N.compare gcd N.one with + match N.compare gcd N.one with | Gt => (Z.div n (Z_of_N gcd), N.div d gcd) | _ => (n, d) end. - Lemma spec_irred : forall n d, exists g, - let (n',d') := irred n d in + Lemma spec_irred : forall n d, exists g, + let (n',d') := irred n d in (Z.to_Z n' * g = Z.to_Z n)%Z /\ (N.to_Z d' * g = N.to_Z d)%Z. Proof. intros. @@ -503,15 +474,15 @@ 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. - Lemma spec_irred_zero : forall n d, + Lemma spec_irred_zero : forall n d, (N.to_Z d = 0)%Z <-> (N.to_Z (snd (irred n d)) = 0)%Z. Proof. intros. @@ -520,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. @@ -535,8 +506,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. compute in H1; elim H1; auto. Qed. - Lemma strong_spec_irred : forall n d, - (N.to_Z d <> 0%Z) -> + Lemma strong_spec_irred : forall n d, + (N.to_Z d <> 0%Z) -> let (n',d') := irred n d in Zgcd (Z.to_Z n') (N.to_Z d') = 1%Z. Proof. unfold irred; intros. @@ -546,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. @@ -554,89 +525,81 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. apply Zgcd_is_gcd; auto. Qed. - Definition mul_norm_Qz_Qq z n d := - if Z.eq_bool z Z.zero then zero + Definition mul_norm_Qz_Qq z n d := + if Z.eq_bool z Z.zero then zero else let gcd := N.gcd (Zabs_N z) d in match N.compare gcd N.one with - | Gt => + | 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. - Definition mul_norm (x y: t): t := + Definition mul_norm (x y: t): t := match x, y with | Qz zx, Qz zy => Qz (Z.mul zx zy) | Qz zx, Qq ny dy => mul_norm_Qz_Qq zx ny dy | Qq nx dx, Qz zy => mul_norm_Qz_Qq zy nx dx - | 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 + | Qq nx dx, Qq ny dy => + let (nx, dy) := irred nx dy in + let (ny, dx) := irred ny dx in + norm_denum (Z.mul ny nx) (N.mul dx dy) end. - Lemma spec_mul_norm_Qz_Qq : forall z n d, + 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 : + forall `(Reduced (Qq n d)), Reduced (mul_norm_Qz_Qq z n d). Proof. - unfold Reduced; intros z n d. + unfold Reduced. 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; intros; 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. @@ -652,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]. @@ -670,37 +630,31 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destruct (spec_irred ny dx) as (g' & Hg'). assert (Hz := spec_irred_zero nx dy). assert (Hz':= spec_irred_zero ny dx). - destruct irred as (n1,d1); destruct irred as (n2,d2). + 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 : + forall `(Reduced x, Reduced y), Reduced (mul_norm x y). Proof. unfold Reduced; intros. rewrite strong_spec_red, Qred_iff. destruct x as [zx|nx dx]; destruct y as [zy|ny dy]. - simpl in *; auto. + simpl in *; auto with zarith. simpl. rewrite <- Qred_iff, <- strong_spec_red, strong_spec_mul_norm_Qz_Qq; auto. simpl. @@ -712,26 +666,27 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. assert (Hz':= spec_irred_zero ny dx). assert (Hgc := strong_spec_irred nx dy). assert (Hgc' := strong_spec_irred ny dx). - destruct irred as (n1,d1); destruct irred as (n2,d2). + 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. - apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1. - 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. + destr_eqb; simpl; nzsimpl; try romega; intros. + rewrite Z2P_correct in *; auto. - rewrite N_to_Z2P in *; auto. - rewrite Z2P_correct. + apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; + apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto. - apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; - apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; auto. - rewrite Zgcd_1_rel_prime in *. apply bezout_rel_prime. destruct (rel_prime_bezout _ _ H4) as [u v Huv]. @@ -743,21 +698,17 @@ 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 := + Definition inv (x: t): t := match x with - | Qz z => - match Z.compare Z.zero z with + | Qz z => + match Z.compare Z.zero z with | Eq => zero | Lt => Qq Z.one (Zabs_N z) | Gt => Qq Z.minus_one (Zabs_N z) end - | Qq n d => + | Qq n d => match Z.compare Z.zero n with | Eq => zero | Lt => Qq (Z_of_N d) (Zabs_N n) @@ -770,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. @@ -784,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. @@ -792,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. @@ -811,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. @@ -826,28 +777,28 @@ 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 := + Definition inv_norm (x: t): t := match x with - | Qz z => - match Z.compare Z.zero z with + | Qz z => + match Z.compare Z.zero z with | Eq => zero | Lt => Qq Z.one (Zabs_N z) | Gt => Qq Z.minus_one (Zabs_N z) end - | Qq n d => - if N.eq_bool d N.zero then zero else - match Z.compare Z.zero n with + | Qq n d => + if N.eq_bool d N.zero then zero else + match Z.compare Z.zero n with | Eq => zero - | Lt => - match Z.compare n Z.one with + | Lt => + match Z.compare n Z.one with | Gt => Qq (Z_of_N d) (Zabs_N n) | _ => Qz (Z_of_N d) end - | Gt => - match Z.compare n Z.minus_one with + | Gt => + match Z.compare n Z.minus_one with | Lt => Qq (Z.opp (Z_of_N d)) (Zabs_N n) | _ => Qz (Z.opp (Z_of_N d)) end @@ -861,74 +812,72 @@ 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. + unfold Reduced. intros. destruct x as [ z | n d ]. (* Qz *) 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 Zgcd_sym; auto. + 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_sym, Zgcd_Zabs, Zgcd_sym. + rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm. apply Zis_gcd_gcd; auto with zarith. apply Zis_gcd_minus. rewrite Zopp_involutive, <- H1; apply Zgcd_is_gcd. @@ -939,7 +888,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_div x y: [div x y] == [x] / [y]. Proof. - intros x y; unfold div; rewrite spec_mul; auto. + unfold div; rewrite spec_mul; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. @@ -949,14 +898,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_div_norm x y: [div_norm x y] == [x] / [y]. Proof. - intros x y; unfold div_norm; rewrite spec_mul_norm; auto. + unfold div_norm; rewrite spec_mul_norm; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. 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. @@ -974,15 +923,13 @@ 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 Z.spec_square, N.spec_square. + rewrite H in H0; romega. + rewrite Z.spec_square, N.spec_square. red; simpl. rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto. apply Zmult_lt_0_compat; auto. @@ -993,7 +940,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. | Qz zx => Qz (Z.power_pos zx p) | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p) end. - + Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p. Proof. intros [ z | n d ] p; unfold power_pos. @@ -1006,44 +953,42 @@ 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. Qed. - Definition power (x : t) (z : Z) : t := - match z with + Definition power (x : t) (z : Z) : t := + match z with | Z0 => one | Zpos p => power_pos x p | Zneg p => inv (power_pos x p) @@ -1058,8 +1003,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite spec_inv, spec_power_pos; apply Qeq_refl. Qed. - Definition power_norm (x : t) (z : Z) : t := - match z with + Definition power_norm (x : t) (z : Z) : t := + match z with | Z0 => one | Zpos p => power_pos x p | Zneg p => inv_norm (power_pos x p) @@ -1074,7 +1019,7 @@ 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, + Instance strong_spec_power_norm x z : Reduced x -> Reduced (power_norm x z). Proof. destruct z; simpl. @@ -1087,7 +1032,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (** Interaction with [Qcanon.Qc] *) - + Open Scope Qc_scope. Definition of_Qc q := of_Q (this q). @@ -1102,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. @@ -1143,7 +1088,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_addc x y: [[add x y]] = [[x]] + [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] + [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1157,7 +1102,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_add_normc x y: [[add_norm x y]] = [[x]] + [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] + [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1168,7 +1113,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. apply Qplus_comp; apply Qeq_sym; apply Qred_correct. Qed. - Theorem spec_add_normc_bis : forall x y : Qc, + Theorem spec_add_normc_bis : forall x y : Qc, [add_norm (of_Qc x) (of_Qc y)] = x+y. Proof. intros. @@ -1180,18 +1125,18 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_subc x y: [[sub x y]] = [[x]] - [[y]]. Proof. - intros x y; unfold sub; rewrite spec_addc; auto. + unfold sub; rewrite spec_addc; auto. rewrite spec_oppc; ring. Qed. Theorem spec_sub_normc x y: [[sub_norm x y]] = [[x]] - [[y]]. Proof. - intros x y; unfold sub_norm; rewrite spec_add_normc; auto. + unfold sub_norm; rewrite spec_add_normc; auto. rewrite spec_oppc; ring. Qed. - Theorem spec_sub_normc_bis : forall x y : Qc, + Theorem spec_sub_normc_bis : forall x y : Qc, [sub_norm (of_Qc x) (of_Qc y)] = x-y. Proof. intros. @@ -1199,13 +1144,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite strong_spec_red. symmetry; apply (Qred_complete (x+(-y)%Qc)%Q). rewrite spec_sub_norm, ! strong_spec_of_Qc. - unfold Qcopp, Q2Qc; rewrite Qred_correct; auto with qarith. + unfold Qcopp, Q2Qc, this. rewrite Qred_correct ; auto with qarith. Qed. Theorem spec_mulc x y: [[mul x y]] = [[x]] * [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] * [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1219,7 +1164,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_mul_normc x y: [[mul_norm x y]] = [[x]] * [[y]]. Proof. - intros x y; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x] * [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1230,7 +1175,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. - Theorem spec_mul_normc_bis : forall x y : Qc, + Theorem spec_mul_normc_bis : forall x y : Qc, [mul_norm (of_Qc x) (of_Qc y)] = x*y. Proof. intros. @@ -1243,7 +1188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_invc x: [[inv x]] = /[[x]]. Proof. - intros x; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! (/[x])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1257,7 +1202,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_inv_normc x: [[inv_norm x]] = /[[x]]. Proof. - intros x; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! (/[x])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1268,7 +1213,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed. - Theorem spec_inv_normc_bis : forall x : Qc, + Theorem spec_inv_normc_bis : forall x : Qc, [inv_norm (of_Qc x)] = /x. Proof. intros. @@ -1280,19 +1225,19 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]]. Proof. - intros x y; unfold div; rewrite spec_mulc; auto. + unfold div; rewrite spec_mulc; auto. unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. - apply spec_invc; auto. + apply spec_invc; auto. Qed. Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]]. Proof. - intros x y; unfold div_norm; rewrite spec_mul_normc; auto. + unfold div_norm; rewrite spec_mul_normc; auto. unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. apply spec_inv_normc; auto. Qed. - Theorem spec_div_normc_bis : forall x y : Qc, + Theorem spec_div_normc_bis : forall x y : Qc, [div_norm (of_Qc x) (of_Qc y)] = x/y. Proof. intros. @@ -1300,12 +1245,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. rewrite strong_spec_red. symmetry; apply (Qred_complete (x*(/y)%Qc)%Q). rewrite spec_div_norm, ! strong_spec_of_Qc. - unfold Qcinv, Q2Qc; rewrite Qred_correct; auto with qarith. + 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. + unfold to_Qc. apply trans_equal with (!! ([x]^2)). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. @@ -1322,7 +1267,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_power_posc x p: [[power_pos x p]] = [[x]] ^ nat_of_P p. Proof. - intros x p; unfold to_Qc. + unfold to_Qc. apply trans_equal with (!! ([x]^Zpos p)). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index be9b2d4e..10d0189a 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: QSig.v 11207 2008-07-04 16:50:32Z letouzey $ i*) +(*i $Id$ i*) -Require Import QArith Qpower. +Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax. Open Scope Q_scope. @@ -23,75 +23,203 @@ Module Type QType. Parameter t : Type. Parameter to_Q : t -> Q. - Notation "[ x ]" := (to_Q x). + Local 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 spec_add: forall x y, [add x y] == [x] + [y]. + Parameter spec_sub: forall x y, [sub x y] == [x] - [y]. + Parameter spec_opp: forall x, [opp x] == - [x]. + Parameter spec_mul: forall x y, [mul x y] == [x] * [y]. + Parameter spec_square: forall x, [square x] == [x] ^ 2. + Parameter spec_inv : forall x, [inv x] == / [x]. + Parameter spec_div: forall x y, [div x y] == [x] / [y]. + Parameter spec_power: forall x z, [power x z] == [x] ^ z. - Parameter compare : t -> t -> comparison. +End QType. - Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]). +(** NB: several of the above functions come with [..._norm] variants + that expect reduced arguments and return reduced results. *) - 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. +(** TODO : also speak of specifications via Qcanon ... *) - Parameter eq_bool : t -> t -> bool. - - Parameter spec_eq_bool : forall x y, - if eq_bool x y then [x]==[y] else ~([x]==[y]). +Module Type QType_Notation (Import Q : QType). + Notation "[ x ]" := (to_Q x). + Infix "==" := eq (at level 70). + Notation "x != y" := (~x==y) (at level 70). + Infix "<=" := le. + Infix "<" := lt. + Notation "0" := zero. + Notation "1" := one. + Infix "+" := add. + Infix "-" := sub. + Infix "*" := mul. + Notation "- x" := (opp x). + Infix "/" := div. + Notation "/ x" := (inv x). + Infix "^" := power. +End QType_Notation. - Parameter red : t -> t. - - Parameter spec_red : forall x, [red x] == [x]. - Parameter strong_spec_red : forall x, [red x] = Qred [x]. +Module Type QType' := QType <+ QType_Notation. - Parameter add : t -> t -> t. - Parameter spec_add: forall x y, [add x y] == [x] + [y]. +Module QProperties (Import Q : QType'). - Parameter sub : t -> t -> t. +(** Conversion to Q *) - Parameter spec_sub: forall x y, [sub x y] == [x] - [y]. +Hint Rewrite + spec_red spec_compare spec_eq_bool spec_min spec_max + spec_add spec_sub spec_opp spec_mul spec_square spec_inv spec_div + spec_power : qsimpl. +Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl; + try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *. - Parameter opp : t -> t. +(** NB: do not add [spec_0] in the autorewrite database. Otherwise, + after instanciation in BigQ, this lemma become convertible to 0=0, + and autorewrite loops. Idem for [spec_1] and [spec_m1] *) - Parameter spec_opp: forall x, [opp x] == - [x]. +(** Morphisms *) - Parameter mul : t -> t -> t. +Ltac solve_wd1 := intros x x' Hx; qify; now rewrite Hx. +Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy. - Parameter spec_mul: forall x y, [mul x y] == [x] * [y]. +Local Obligation Tactic := solve_wd2 || solve_wd1. - Parameter square : t -> t. +Instance : Measure to_Q. +Instance eq_equiv : Equivalence eq. - Parameter spec_square: forall x, [square x] == [x] ^ 2. +Program Instance lt_wd : Proper (eq==>eq==>iff) lt. +Program Instance le_wd : Proper (eq==>eq==>iff) le. +Program Instance red_wd : Proper (eq==>eq) red. +Program Instance compare_wd : Proper (eq==>eq==>Logic.eq) compare. +Program Instance eq_bool_wd : Proper (eq==>eq==>Logic.eq) eq_bool. +Program Instance min_wd : Proper (eq==>eq==>eq) min. +Program Instance max_wd : Proper (eq==>eq==>eq) max. +Program Instance add_wd : Proper (eq==>eq==>eq) add. +Program Instance sub_wd : Proper (eq==>eq==>eq) sub. +Program Instance opp_wd : Proper (eq==>eq) opp. +Program Instance mul_wd : Proper (eq==>eq==>eq) mul. +Program Instance square_wd : Proper (eq==>eq) square. +Program Instance inv_wd : Proper (eq==>eq) inv. +Program Instance div_wd : Proper (eq==>eq==>eq) div. +Program Instance power_wd : Proper (eq==>Logic.eq==>eq) power. - Parameter inv : t -> t. +(** Let's implement [HasCompare] *) - Parameter spec_inv : forall x, [inv x] == / [x]. +Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). +Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed. - Parameter div : t -> t -> t. +(** Let's implement [TotalOrder] *) - Parameter spec_div: forall x y, [div x y] == [x] / [y]. +Definition lt_compat := lt_wd. +Instance lt_strorder : StrictOrder lt. - Parameter power : t -> Z -> t. +Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y. +Proof. intros. qify. apply Qle_lteq. Qed. - Parameter spec_power: forall x z, [power x z] == [x] ^ z. +Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. +Proof. intros. destruct (compare_spec x y); auto. Qed. -End QType. +(** Let's implement [HasEqBool] *) -(** NB: several of the above functions come with [..._norm] variants - that expect reduced arguments and return reduced results. *) +Definition eqb := eq_bool. -(** TODO : also speak of specifications via Qcanon ... *) +Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y. +Proof. intros. qify. apply Qeq_bool_iff. Qed. + +Lemma eqb_correct : forall x y, eq_bool x y = true -> x == y. +Proof. now apply eqb_eq. Qed. + +Lemma eqb_complete : forall x y, x == y -> eq_bool x y = true. +Proof. now apply eqb_eq. Qed. + +(** Let's implement [HasMinMax] *) + +Lemma max_l : forall x y, y<=x -> max x y == x. +Proof. intros x y. qify. apply Qminmax.Q.max_l. Qed. + +Lemma max_r : forall x y, x<=y -> max x y == y. +Proof. intros x y. qify. apply Qminmax.Q.max_r. Qed. + +Lemma min_l : forall x y, x<=y -> min x y == x. +Proof. intros x y. qify. apply Qminmax.Q.min_l. Qed. + +Lemma min_r : forall x y, y<=x -> min x y == y. +Proof. intros x y. qify. apply Qminmax.Q.min_r. Qed. + +(** Q is a ring *) + +Lemma add_0_l : forall x, 0+x == x. +Proof. intros. qify. apply Qplus_0_l. Qed. + +Lemma add_comm : forall x y, x+y == y+x. +Proof. intros. qify. apply Qplus_comm. Qed. + +Lemma add_assoc : forall x y z, x+(y+z) == x+y+z. +Proof. intros. qify. apply Qplus_assoc. Qed. + +Lemma mul_1_l : forall x, 1*x == x. +Proof. intros. qify. apply Qmult_1_l. Qed. + +Lemma mul_comm : forall x y, x*y == y*x. +Proof. intros. qify. apply Qmult_comm. Qed. + +Lemma mul_assoc : forall x y z, x*(y*z) == x*y*z. +Proof. intros. qify. apply Qmult_assoc. Qed. + +Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z. +Proof. intros. qify. apply Qmult_plus_distr_l. Qed. + +Lemma sub_add_opp : forall x y, x-y == x+(-y). +Proof. intros. qify. now unfold Qminus. Qed. + +Lemma add_opp_diag_r : forall x, x+(-x) == 0. +Proof. intros. qify. apply Qplus_opp_r. Qed. + +(** Q is a field *) + +Lemma neq_1_0 : 1!=0. +Proof. intros. qify. apply Q_apart_0_1. Qed. + +Lemma div_mul_inv : forall x y, x/y == x*(/y). +Proof. intros. qify. now unfold Qdiv. Qed. + +Lemma mul_inv_diag_l : forall x, x!=0 -> /x * x == 1. +Proof. intros x. qify. rewrite Qmult_comm. apply Qmult_inv_r. Qed. + +End QProperties. + +Module QTypeExt (Q : QType) + <: QType <: TotalOrder <: HasCompare Q <: HasMinMax Q <: HasEqBool Q + := Q <+ QProperties.
\ No newline at end of file |