diff options
-rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 37 | ||||
-rw-r--r-- | theories/QArith/Qcanon.v | 120 |
2 files changed, 83 insertions, 74 deletions
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 4ac36425b..b9fed9d56 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -1050,13 +1050,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_of_Qc: forall q, [[of_Qc q]] = q. Proof. intros; apply Qc_decomp; simpl; intros. - rewrite strong_spec_of_Qc; auto. + rewrite strong_spec_of_Qc. apply canon. Qed. Theorem spec_oppc: forall q, [[opp q]] = -[[q]]. Proof. intros q; unfold Qcopp, to_Qc, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. rewrite spec_opp, <- Qred_opp, Qred_correct. apply Qeq_refl. @@ -1085,10 +1085,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] + [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_add; auto. unfold Qcplus, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qplus_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1099,10 +1099,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] + [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_add_norm; auto. unfold Qcplus, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qplus_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1147,10 +1147,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] * [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_mul; auto. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1161,10 +1161,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] * [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_mul_norm; auto. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1185,10 +1185,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc (/[x])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_inv; auto. unfold Qcinv, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1199,10 +1199,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc (/[x])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_inv_norm; auto. unfold Qcinv, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1247,13 +1247,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x]^2)). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_square; auto. simpl Qcpower. replace (Q2Qc [x] * 1) with (Q2Qc [x]); try ring. simpl. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1264,14 +1264,14 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x]^Zpos p)). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_power_pos; auto. induction p using Pos.peano_ind. simpl; ring. rewrite Pos2Nat.inj_succ; simpl Qcpower. rewrite <- IHp; clear IHp. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. setoid_replace ([x] ^ ' Pos.succ p)%Q with ([x] * [x] ^ ' p)%Q. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. @@ -1281,4 +1281,3 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Qed. End Make. - diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index d966b050c..86be28d7b 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -21,37 +21,30 @@ Bind Scope Qc_scope with Qc. Arguments Qcmake this%Q _. Open Scope Qc_scope. +(** An alternative statement of [Qred q = q] via [Z.gcd] *) + Lemma Qred_identity : forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. Proof. - unfold Qred; intros (a,b); simpl. - generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)). - intros. - rewrite H1 in H; clear H1. - destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. - destruct H0. - rewrite Z.mul_1_l in H, H0. - subst; simpl; auto. + intros (a,b) H; simpl in *. + rewrite <- Z.ggcd_gcd in H. + generalize (Z.ggcd_correct_divisors a ('b)). + destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst. + rewrite !Z.mul_1_l. now intros (<-,<-). Qed. Lemma Qred_identity2 : forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z. Proof. - unfold Qred; intros (a,b); simpl. - generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)) (Z.gcd_nonneg a ('b)). - intros. - rewrite <- H; rewrite <- H in H1; clear H. - destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. - injection H2; intros; clear H2. - destruct H0. - clear H0 H3. - destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate. - f_equal. - apply Pos.mul_reg_r with bb. - injection H2; intros. - rewrite <- H0. - rewrite H; simpl; auto. - elim H1; auto. + intros (a,b) H; simpl in *. + generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + rewrite <- Z.ggcd_gcd. + destruct Z.ggcd as (g,(aa,bb)); simpl in *. + injection H as <- <-. intros H (_,H'). + destruct g as [|g|g]; [ discriminate | | now elim H ]. + destruct bb as [|b|b]; simpl in *; try discriminate. + injection H' as H'. f_equal. + apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l. Qed. Lemma Qred_iff : forall q:Q, Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1%Z. @@ -61,6 +54,23 @@ Proof. apply Qred_identity; auto. Qed. +(** Coercion from [Qc] to [Q] and equality *) + +Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. +Proof. + intros (q,hq) (q',hq') H. simpl in *. + assert (H' := Qred_complete _ _ H). + rewrite hq, hq' in H'. subst q'. f_equal. + apply eq_proofs_unicity. intros. repeat decide equality. +Qed. +Hint Resolve Qc_is_canon. + +Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'. +Proof. + intros. apply Qc_is_canon. now rewrite H. +Qed. + +(** [Q2Qc] : a conversion from [Q] to [Qc]. *) Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q. Proof. @@ -71,20 +81,20 @@ Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). Arguments Q2Qc q%Q. -Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. +Lemma Qred_eq_iff (q q' : Q) : Qred q = Qred q' <-> q == q'. Proof. - intros (q,proof_q) (q',proof_q'). - simpl. - intros H. - assert (H0:=Qred_complete _ _ H). - assert (q = q') by congruence. - subst q'. - assert (proof_q = proof_q'). - apply eq_proofs_unicity; auto; intros. - repeat decide equality. - congruence. + split. + - intros E. rewrite <- (Qred_correct q), <- (Qred_correct q'). + now rewrite E. + - apply Qred_complete. +Qed. + +Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'. +Proof. + split; intro H. + - injection H. apply Qred_eq_iff. + - apply Qc_is_canon. simpl. now rewrite H. Qed. -Hint Resolve Qc_is_canon. Notation " 0 " := (Q2Qc 0) : Qc_scope. Notation " 1 " := (Q2Qc 1) : Qc_scope. @@ -107,8 +117,7 @@ Lemma Qceq_alt : forall p q, (p = q) <-> (p ?= q) = Eq. Proof. unfold Qccompare. intros; rewrite <- Qeq_alt. - split; auto. - intro H; rewrite H; auto with qarith. + split; auto. now intros <-. Qed. Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt). @@ -166,7 +175,7 @@ Qed. Ltac qc := match goal with | q:Qc |- _ => destruct q; qc - | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct + | _ => apply Qc_is_canon; simpl; rewrite !Qred_correct end. Opaque Qred. @@ -216,6 +225,18 @@ Proof. intros; qc; apply Qmult_assoc. Qed. +(** [0] is absorbing for multiplication: *) + +Lemma Qcmult_0_l : forall n, 0*n = 0. +Proof. + intros; qc; split. +Qed. + +Theorem Qcmult_0_r : forall n, n*0=0. +Proof. + intros; qc; rewrite Qmult_comm; split. +Qed. + (** [1] is a neutral element for multiplication: *) Lemma Qcmult_1_l : forall n, 1*n = n. @@ -303,7 +324,7 @@ Proof. apply Qcmult_1_l. Qed. -(** Properties of order upon Q. *) +(** Properties of order upon Qc. *) Lemma Qcle_refl : forall x, x<=x. Proof. @@ -372,9 +393,11 @@ Proof. unfold Qcle, Qclt; intros; apply Qle_not_lt; auto. Qed. -Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y. +Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x=y. Proof. - unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto. + unfold Qcle, Qclt; intros x y H. + destruct (Qle_lt_or_eq _ _ H); [left|right]; trivial. + now apply Qc_is_canon. Qed. (** Some decidability results about orders. *) @@ -459,7 +482,7 @@ Proof. induction n; simpl; auto with qarith. rewrite IHn; auto with qarith. Qed. -Transparent Qred. + Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0. Proof. destruct n; simpl. @@ -525,16 +548,3 @@ intros. field. auto. Qed. - - -Theorem Qc_decomp: forall x y: Qc, - (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y. -Proof. - intros (q, Hq) (q', Hq'); simpl; intros H. - assert (H1 := H Hq Hq'). - subst q'. - assert (Hq = Hq'). - apply Eqdep_dec.eq_proofs_unicity; auto; intros. - repeat decide equality. - congruence. -Qed. |