From ea05377f19404e0627a105b07c10ce72fb010af9 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 26 Feb 2016 16:12:33 +0100 Subject: Qcanon : implement some old suggestions by C. Auger --- theories/QArith/Qcanon.v | 120 +++++++++++++++++++++++++---------------------- 1 file changed, 65 insertions(+), 55 deletions(-) (limited to 'theories/QArith') 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 (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 xO -> 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. -- cgit v1.2.3