diff options
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith_base.v | 62 | ||||
| -rw-r--r-- | theories/QArith/Qcanon.v | 526 | ||||
| -rw-r--r-- | theories/QArith/Qreduction.v | 111 |
3 files changed, 591 insertions, 108 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 1d56b747..335466a6 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: QArith_base.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: QArith_base.v 8989 2006-06-25 22:17:49Z letouzey $ i*) Require Export ZArith. Require Export ZArithRing. @@ -43,12 +43,48 @@ Notation Qge := (fun x y : Q => Qle y x). Infix "==" := Qeq (at level 70, no associativity) : Q_scope. Infix "<" := Qlt : Q_scope. +Infix ">" := Qgt : Q_scope. Infix "<=" := Qle : Q_scope. -Infix ">" := Qgt : Q_scope. -Infix ">=" := Qge : Q_scope. +Infix ">=" := Qge : Q_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. -Hint Unfold Qeq Qle Qlt: qarith. +(** Another approach : using Qcompare for defining order relations. *) + +Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z. +Notation "p ?= q" := (Qcompare p q) : Q_scope. + +Lemma Qeq_alt : forall p q, (p == q) <-> (p ?= q) = Eq. +Proof. +unfold Qeq, Qcompare; intros; split; intros. +rewrite H; apply Zcompare_refl. +apply Zcompare_Eq_eq; auto. +Qed. + +Lemma Qlt_alt : forall p q, (p<q) <-> (p?=q = Lt). +Proof. +unfold Qlt, Qcompare, Zlt; split; auto. +Qed. + +Lemma Qgt_alt : forall p q, (p>q) <-> (p?=q = Gt). +Proof. +unfold Qlt, Qcompare, Zlt. +intros; rewrite Zcompare_Gt_Lt_antisym; split; auto. +Qed. + +Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). +Proof. +unfold Qle, Qcompare, Zle; split; auto. +Qed. + +Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). +Proof. +unfold Qle, Qcompare, Zle. +split; intros; swap H. +rewrite Zcompare_Gt_Lt_antisym; auto. +rewrite Zcompare_Gt_Lt_antisym in H0; auto. +Qed. + +Hint Unfold Qeq Qlt Qle: qarith. Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith. (** Properties of equality. *) @@ -236,6 +272,24 @@ apply Zmult_gt_0_lt_compat_l; auto with zarith. Open Scope Q_scope. Qed. + +Lemma Qcompare_egal_dec: forall n m p q : Q, + (n<m -> p<q) -> (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)). +Proof. +intros. +do 2 rewrite Qeq_alt in H0. +unfold Qeq, Qlt, Qcompare in *. +apply Zcompare_egal_dec; auto. +omega. +Qed. + + +Add Morphism Qcompare : Qcompare_comp. +Proof. +intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto. +Qed. + + (** [0] and [1] are apart *) Lemma Q_apart_0_1 : ~ 1 == 0. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v new file mode 100644 index 00000000..9cbd400d --- /dev/null +++ b/theories/QArith/Qcanon.v @@ -0,0 +1,526 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Qcanon.v 8989 2006-06-25 22:17:49Z letouzey $ i*) + +Require Import QArith. +Require Import Eqdep_dec. + +(** [Qc] : A canonical representation of rational numbers. + based on the setoid representation [Q]. *) + +Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }. + +Delimit Scope Qc_scope with Qc. +Bind Scope Qc_scope with Qc. +Arguments Scope Qcmake [Q_scope]. +Open Scope Qc_scope. + +Lemma Qred_identity : + forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. +Proof. +unfold Qred; intros (a,b); simpl. +generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)). +intros. +rewrite H1 in H; clear H1. +destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. +destruct H0. +rewrite Zmult_1_l in H, H0. +subst; simpl; auto. +Qed. + +Lemma Qred_identity2 : + forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z. +Proof. +unfold Qred; intros (a,b); simpl. +generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)). +intros. +rewrite <- H; rewrite <- H in H1; clear H. +destruct (Zggcd 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 Pmult_reg_r with bb. +injection H2; intros. +rewrite <- H0. +rewrite H; simpl; auto. +elim H1; auto. +Qed. + +Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z. +Proof. +split; intros. +apply Qred_identity2; auto. +apply Qred_identity; auto. +Qed. + + +Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q. +Proof. +intros; apply Qred_complete. +apply Qred_correct. +Qed. + +Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). +Arguments Scope Q2Qc [Q_scope]. +Notation " !! " := Q2Qc : Qc_scope. + +Lemma Qc_is_canon : forall q q' : Qc, q == 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. +Qed. +Hint Resolve Qc_is_canon. + +Notation " 0 " := (!!0) : Qc_scope. +Notation " 1 " := (!!1) : Qc_scope. + +Definition Qcle (x y : Qc) := (x <= y)%Q. +Definition Qclt (x y : Qc) := (x < y)%Q. +Notation Qcgt := (fun x y : Qc => Qlt y x). +Notation Qcge := (fun x y : Qc => Qle y x). +Infix "<" := Qclt : Qc_scope. +Infix "<=" := Qcle : Qc_scope. +Infix ">" := Qcgt : Qc_scope. +Infix ">=" := Qcge : Qc_scope. +Notation "x <= y <= z" := (x<=y/\y<=z) : Qc_scope. + +Definition Qccompare (p q : Qc) := (Qcompare p q). +Notation "p ?= q" := (Qccompare p q) : Qc_scope. + +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. +Qed. + +Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt). +Proof. +intros; exact (Qlt_alt p q). +Qed. + +Lemma Qcgt_alt : forall p q, (p>q) <-> (p?=q = Gt). +Proof. +intros; exact (Qgt_alt p q). +Qed. + +Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). +Proof. +intros; exact (Qle_alt p q). +Qed. + +Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). +Proof. +intros; exact (Qge_alt p q). +Qed. + +(** equality on [Qc] is decidable: *) + +Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}. +Proof. + intros. + destruct (Qeq_dec x y) as [H|H]; auto. + right; swap H; subst; auto with qarith. +Defined. + +(** The addition, multiplication and opposite are defined + in the straightforward way: *) + +Definition Qcplus (x y : Qc) := !!(x+y). +Infix "+" := Qcplus : Qc_scope. +Definition Qcmult (x y : Qc) := !!(x*y). +Infix "*" := Qcmult : Qc_scope. +Definition Qcopp (x : Qc) := !!(-x). +Notation "- x" := (Qcopp x) : Qc_scope. +Definition Qcminus (x y : Qc) := x+-y. +Infix "-" := Qcminus : Qc_scope. +Definition Qcinv (x : Qc) := !!(/x). +Notation "/ x" := (Qcinv x) : Qc_scope. +Definition Qcdiv (x y : Qc) := x*/y. +Infix "/" := Qcdiv : Qc_scope. + +(** [0] and [1] are apart *) + +Lemma Q_apart_0_1 : 1 <> 0. +Proof. + unfold Q2Qc. + intros H; discriminate H. +Qed. + +Ltac qc := match goal with + | q:Qc |- _ => destruct q; qc + | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct +end. + +Opaque Qred. + +(** Addition is associative: *) + +Theorem Qcplus_assoc : forall x y z, x+(y+z)=(x+y)+z. +Proof. + intros; qc; apply Qplus_assoc. +Qed. + +(** [0] is a neutral element for addition: *) + +Lemma Qcplus_0_l : forall x, 0+x = x. +Proof. + intros; qc; apply Qplus_0_l. +Qed. + +Lemma Qcplus_0_r : forall x, x+0 = x. +Proof. + intros; qc; apply Qplus_0_r. +Qed. + +(** Commutativity of addition: *) + +Theorem Qcplus_comm : forall x y, x+y = y+x. +Proof. + intros; qc; apply Qplus_comm. +Qed. + +(** Properties of [Qopp] *) + +Lemma Qcopp_involutive : forall q, - -q = q. +Proof. + intros; qc; apply Qopp_involutive. +Qed. + +Theorem Qcplus_opp_r : forall q, q+(-q) = 0. +Proof. + intros; qc; apply Qplus_opp_r. +Qed. + +(** Multiplication is associative: *) + +Theorem Qcmult_assoc : forall n m p, n*(m*p)=(n*m)*p. +Proof. + intros; qc; apply Qmult_assoc. +Qed. + +(** [1] is a neutral element for multiplication: *) + +Lemma Qcmult_1_l : forall n, 1*n = n. +Proof. + intros; qc; apply Qmult_1_l. +Qed. + +Theorem Qcmult_1_r : forall n, n*1=n. +Proof. + intros; qc; apply Qmult_1_r. +Qed. + +(** Commutativity of multiplication *) + +Theorem Qcmult_comm : forall x y, x*y=y*x. +Proof. + intros; qc; apply Qmult_comm. +Qed. + +(** Distributivity *) + +Theorem Qcmult_plus_distr_r : forall x y z, x*(y+z)=(x*y)+(x*z). +Proof. + intros; qc; apply Qmult_plus_distr_r. +Qed. + +Theorem Qcmult_plus_distr_l : forall x y z, (x+y)*z=(x*z)+(y*z). +Proof. + intros; qc; apply Qmult_plus_distr_l. +Qed. + +(** Integrality *) + +Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. +Proof. + intros. + destruct (Qmult_integral x y); try qc; auto. + injection H; clear H; intros. + rewrite <- (Qred_correct (x*y)). + rewrite <- (Qred_correct 0). + rewrite H; auto with qarith. +Qed. + +Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0. +Proof. + intros; destruct (Qcmult_integral _ _ H0); tauto. +Qed. + +(** Inverse and division. *) + +Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1. +Proof. + intros; qc; apply Qmult_inv_r; auto. +Qed. + +Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1. +Proof. + intros. + rewrite Qcmult_comm. + apply Qcmult_inv_r; auto. +Qed. + +Lemma Qcinv_mult_distr : forall p q, / (p * q) = /p * /q. +Proof. + intros; qc; apply Qinv_mult_distr. +Qed. + +Theorem Qcdiv_mult_l : forall x y, y<>0 -> (x*y)/y = x. +Proof. + unfold Qcdiv. + intros. + rewrite <- Qcmult_assoc. + rewrite Qcmult_inv_r; auto. + apply Qcmult_1_r. +Qed. + +Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y*(x/y) = x. +Proof. + unfold Qcdiv. + intros. + rewrite Qcmult_assoc. + rewrite Qcmult_comm. + rewrite Qcmult_assoc. + rewrite Qcmult_inv_l; auto. + apply Qcmult_1_l. +Qed. + +(** Properties of order upon Q. *) + +Lemma Qcle_refl : forall x, x<=x. +Proof. +unfold Qcle; intros; simpl; apply Qle_refl. +Qed. + +Lemma Qcle_antisym : forall x y, x<=y -> y<=x -> x=y. +Proof. +unfold Qcle; intros; simpl in *. +apply Qc_is_canon; apply Qle_antisym; auto. +Qed. + +Lemma Qcle_trans : forall x y z, x<=y -> y<=z -> x<=z. +Proof. +unfold Qcle; intros; eapply Qle_trans; eauto. +Qed. + +Lemma Qclt_not_eq : forall x y, x<y -> x<>y. +Proof. +unfold Qclt; intros; simpl in *. +intro; destruct (Qlt_not_eq _ _ H). +subst; auto with qarith. +Qed. + +(** Large = strict or equal *) + +Lemma Qclt_le_weak : forall x y, x<y -> x<=y. +Proof. +unfold Qcle, Qclt; intros; apply Qlt_le_weak; auto. +Qed. + +Lemma Qcle_lt_trans : forall x y z, x<=y -> y<z -> x<z. +Proof. +unfold Qcle, Qclt; intros; eapply Qle_lt_trans; eauto. +Qed. + +Lemma Qclt_le_trans : forall x y z, x<y -> y<=z -> x<z. +Proof. +unfold Qcle, Qclt; intros; eapply Qlt_le_trans; eauto. +Qed. + +Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z. +Proof. +unfold Qclt; intros; eapply Qlt_trans; eauto. +Qed. + +(** [x<y] iff [~(y<=x)] *) + +Lemma Qcnot_lt_le : forall x y, ~ x<y -> y<=x. +Proof. +unfold Qcle, Qclt; intros; apply Qnot_lt_le; auto. +Qed. + +Lemma Qcnot_le_lt : forall x y, ~ x<=y -> y<x. +Proof. +unfold Qcle, Qclt; intros; apply Qnot_le_lt; auto. +Qed. + +Lemma Qclt_not_le : forall x y, x<y -> ~ y<=x. +Proof. +unfold Qcle, Qclt; intros; apply Qlt_not_le; auto. +Qed. + +Lemma Qcle_not_lt : forall x y, x<=y -> ~ y<x. +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. +Proof. +unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto. +Qed. + +(** Some decidability results about orders. *) + +Lemma Qc_dec : forall x y, {x<y} + {y<x} + {x=y}. +Proof. +unfold Qclt, Qcle; intros. +destruct (Q_dec x y) as [H|H]. +left; auto. +right; apply Qc_is_canon; auto. +Defined. + +Lemma Qclt_le_dec : forall x y, {x<y} + {y<=x}. +Proof. +unfold Qclt, Qcle; intros; apply Qlt_le_dec; auto. +Defined. + +(** Compatibility of operations with respect to order. *) + +Lemma Qcopp_le_compat : forall p q, p<=q -> -q <= -p. +Proof. +unfold Qcle, Qcopp; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qopp_le_compat; auto. +Qed. + +Lemma Qcle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. +Proof. +unfold Qcle, Qcminus; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qle_minus_iff; auto. +Qed. + +Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q+-p. +Proof. +unfold Qclt, Qcplus, Qcopp; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qlt_minus_iff; auto. +Qed. + +Lemma Qcplus_le_compat : + forall x y z t, x<=y -> z<=t -> x+z <= y+t. +Proof. +unfold Qcplus, Qcle; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qplus_le_compat; auto. +Qed. + +Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. +Proof. +unfold Qcmult, Qcle; intros; simpl in *. +repeat rewrite Qred_correct. +apply Qmult_le_compat_r; auto. +Qed. + +Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y. +Proof. +unfold Qcmult, Qcle, Qclt; intros; simpl in *. +repeat progress rewrite Qred_correct in * |-. +eapply Qmult_lt_0_le_reg_r; eauto. +Qed. + +Lemma Qcmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. +Proof. +unfold Qcmult, Qclt; intros; simpl in *. +repeat progress rewrite Qred_correct in *. +eapply Qmult_lt_compat_r; eauto. +Qed. + +(** Rational to the n-th power *) + +Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := + match n with + | O => 1 + | S n => q * (Qcpower q n) + end. + +Notation " q ^ n " := (Qcpower q n) : Qc_scope. + +Lemma Qcpower_1 : forall n, 1^n = 1. +Proof. +induction n; simpl; auto with qarith. +rewrite IHn; auto with qarith. +Qed. + +Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0. +Proof. +destruct n; simpl. +destruct 1; auto. +intros. +apply Qc_is_canon. +simpl. +compute; auto. +Qed. + +Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n. +Proof. +induction n; simpl; auto with qarith. +intros; compute; intro; discriminate. +intros. +apply Qcle_trans with (0*(p^n)). +compute; intro; discriminate. +apply Qcmult_le_compat_r; auto. +Qed. + +(** And now everything is easier concerning tactics: *) + +(** A ring tactic for rational numbers *) + +Definition Qc_eq_bool (x y : Qc) := + if Qc_eq_dec x y then true else false. + +Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y. +intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto. +intros _ H; inversion H. +Qed. + +Definition Qcrt : Ring_Theory Qcplus Qcmult 1 0 Qcopp Qc_eq_bool. +Proof. +constructor. +exact Qcplus_comm. +exact Qcplus_assoc. +exact Qcmult_comm. +exact Qcmult_assoc. +exact Qcplus_0_l. +exact Qcmult_1_l. +exact Qcplus_opp_r. +exact Qcmult_plus_distr_l. +unfold Is_true; intros x y; generalize (Qc_eq_bool_correct x y); + case (Qc_eq_bool x y); auto. +Qed. + +Add Ring Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcrt [ Qcmake ]. + +(** A field tactic for rational numbers *) + +Require Import Field. + +Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l + with div:=Qcdiv. + +Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x. +intros. +field. +auto. +Qed. + + + diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 049c195a..c503daad 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreduction.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: Qreduction.v 8989 2006-06-25 22:17:49Z letouzey $ i*) (** * Normalisation functions for rational numbers. *) @@ -32,65 +32,17 @@ Proof. simple destruct z; simpl in |- *; auto; intros; elim H; auto. Qed. -(** A simple cancelation by powers of two *) - -Fixpoint Pfactor_twos (p p':positive) {struct p} : (positive*positive) := - match p, p' with - | xO p, xO p' => Pfactor_twos p p' - | _, _ => (p,p') - end. - -Definition Qfactor_twos (q:Q) := - let (p,q) := q in - match p with - | Z0 => 0 - | Zpos p => let (p,q) := Pfactor_twos p q in (Zpos p)#q - | Zneg p => let (p,q) := Pfactor_twos p q in (Zneg p)#q - end. - -Lemma Pfactor_twos_correct : forall p p', - (p*(snd (Pfactor_twos p p')))%positive = - (p'*(fst (Pfactor_twos p p')))%positive. -Proof. -induction p; intros. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -destruct p'. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -simpl; f_equal; auto. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -simpl snd; simpl fst; rewrite Pmult_comm; auto. -Qed. - -Lemma Qfactor_twos_correct : forall q, Qfactor_twos q == q. -Proof. -intros (p,q). -destruct p. -red; simpl; auto. -simpl. -generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q). -red; simpl. -intros; f_equal. -rewrite H; apply Pmult_comm. -simpl. -generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q). -red; simpl. -intros; f_equal. -rewrite H; apply Pmult_comm. -Qed. -Hint Resolve Qfactor_twos_correct. - (** Simplification of fractions using [Zgcd]. This version can compute within Coq. *) Definition Qred (q:Q) := - let (q1,q2) := Qfactor_twos q in - let (r1,r2) := snd (Zggcd q1 (Zpos q2)) in r1#(Z2P r2). + let (q1,q2) := q in + let (r1,r2) := snd (Zggcd q1 ('q2)) + in r1#(Z2P r2). Lemma Qred_correct : forall q, (Qred q) == q. Proof. -intros; apply Qeq_trans with (Qfactor_twos q); auto. -unfold Qred. -destruct (Qfactor_twos q) as (n,d); red; simpl. +unfold Qred, Qeq; intros (n,d); simpl. generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)). destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl. @@ -112,16 +64,8 @@ Qed. Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q. Proof. -intros. -assert (Qfactor_twos p == Qfactor_twos q). - apply Qeq_trans with p; auto. - apply Qeq_trans with q; auto. - symmetry; auto. -clear H. -unfold Qred. -destruct (Qfactor_twos p) as (a,b); -destruct (Qfactor_twos q) as (c,d); clear p q. -unfold Qeq in *; simpl in *. +intros (a,b) (c,d). +unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)). @@ -198,47 +142,6 @@ rewrite (Qred_correct q); auto. rewrite (Qred_correct q'); auto. Qed. -(** Another version, dedicated to extraction *) - -Definition Qred_extr (q : Q) := - let (q1, q2) := Qfactor_twos q in - let (p,_) := Zggcd_spec_pos (Zpos q2) (Zle_0_pos q2) q1 in - let (r2,r1) := snd p in r1#(Z2P r2). - -Lemma Qred_extr_Qred : forall q, Qred_extr q = Qred q. -Proof. -unfold Qred, Qred_extr. -intro q; destruct (Qfactor_twos q) as (n,p); clear q. -Open Scope Z_scope. -destruct (Zggcd_spec_pos (' p) (Zle_0_pos p) n) as ((g,(pp,nn)),H). -generalize (H (Zle_0_pos p)); clear H; intros (Hg1,(Hg2,(Hg4,Hg3))). -simpl. -generalize (Zggcd_gcd n ('p)) (Zgcd_is_gcd n ('p)) - (Zgcd_is_pos n ('p)) (Zggcd_correct_divisors n ('p)). -destruct (Zggcd n (Zpos p)) as (g',(nn',pp')); simpl. -intro H; rewrite <- H; clear H. -intros Hg'1 Hg'2 (Hg'3,Hg'4). -assert (g<>0). - intro; subst g; discriminate. -destruct (Zis_gcd_uniqueness_apart_sign n ('p) g g'); auto. -apply Zis_gcd_sym; auto. -subst g'. -f_equal. -apply Zmult_reg_l with g; auto; congruence. -f_equal. -apply Zmult_reg_l with g; auto; congruence. -elimtype False; omega. -Open Scope Q_scope. -Qed. - -Add Morphism Qred_extr : Qred_extr_comp. -Proof. -intros q q' H. -do 2 rewrite Qred_extr_Qred. -rewrite (Qred_correct q); auto. -rewrite (Qred_correct q'); auto. -Qed. - Definition Qplus' (p q : Q) := Qred (Qplus p q). Definition Qmult' (p q : Q) := Qred (Qmult p q). |