diff options
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith_base.v | 535 | ||||
| -rw-r--r-- | theories/QArith/Qcanon.v | 344 | ||||
| -rw-r--r-- | theories/QArith/Qreals.v | 26 | ||||
| -rw-r--r-- | theories/QArith/Qreduction.v | 169 | ||||
| -rw-r--r-- | theories/QArith/Qring.v | 81 |
5 files changed, 602 insertions, 553 deletions
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 335466a6..66d16cfe 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 8989 2006-06-25 22:17:49Z letouzey $ i*) +(*i $Id: QArith_base.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export ZArith. Require Export ZArithRing. @@ -87,7 +87,7 @@ Qed. Hint Unfold Qeq Qlt Qle: qarith. Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith. -(** Properties of equality. *) +(** * Properties of equality. *) Theorem Qeq_refl : forall x, x == x. Proof. @@ -104,8 +104,10 @@ Proof. unfold Qeq in |- *; intros. apply Zmult_reg_l with (QDen y). auto with qarith. -ring; rewrite H; ring. -rewrite Zmult_assoc; rewrite H0; ring. +transitivity (Qnum x * QDen y * QDen z)%Z; try ring. +rewrite H. +transitivity (Qnum y * QDen z * QDen x)%Z; try ring. +rewrite H0; ring. Qed. (** Furthermore, this equality is decidable: *) @@ -128,6 +130,9 @@ Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith. Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith. Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith. + +(** * Addition, multiplication and opposite *) + (** The addition, multiplication and opposite are defined in the straightforward way: *) @@ -160,133 +165,138 @@ Infix "/" := Qdiv : Q_scope. Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope. -(** Setoid compatibility results *) + +(** * Setoid compatibility results *) Add Morphism Qplus : Qplus_comp. Proof. -unfold Qeq, Qplus; simpl. -Open Scope Z_scope. -intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. -simpl_mult; ring. -replace (p1 * ('s2 * 'q2)) with (p1 * 'q2 * 's2) by ring. -rewrite H. -replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring. -rewrite H0. -ring. -Open Scope Q_scope. + unfold Qeq, Qplus; simpl. + Open Scope Z_scope. + intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. + simpl_mult; ring_simplify. + replace (p1 * 'r2 * 'q2) with (p1 * 'q2 * 'r2) by ring. + rewrite H. + replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring. + rewrite H0. + ring. + Close Scope Z_scope. Qed. Add Morphism Qopp : Qopp_comp. Proof. -unfold Qeq, Qopp; simpl. -intros; ring; rewrite H; ring. + unfold Qeq, Qopp; simpl. + Open Scope Z_scope. + intros. + replace (- Qnum x1 * ' Qden x2) with (- (Qnum x1 * ' Qden x2)) by ring. + rewrite H in |- *; ring. + Close Scope Z_scope. Qed. Add Morphism Qminus : Qminus_comp. Proof. -intros. -unfold Qminus. -rewrite H; rewrite H0; auto with qarith. + intros. + unfold Qminus. + rewrite H; rewrite H0; auto with qarith. Qed. Add Morphism Qmult : Qmult_comp. Proof. -unfold Qeq; simpl. -Open Scope Z_scope. -intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. -intros; simpl_mult; ring. -replace ('p2 * (q1 * s1)) with (q1 * 'p2 * s1) by ring. -rewrite <- H. -replace ('s2 * ('q2 * r1)) with (r1 * 's2 * 'q2) by ring. -rewrite H0. -ring. -Open Scope Q_scope. + unfold Qeq; simpl. + Open Scope Z_scope. + intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; simpl in *. + intros; simpl_mult; ring_simplify. + replace (q1 * s1 * 'p2) with (q1 * 'p2 * s1) by ring. + rewrite <- H. + replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring. + rewrite H0. + ring. + Close Scope Z_scope. Qed. Add Morphism Qinv : Qinv_comp. Proof. -unfold Qeq, Qinv; simpl. -Open Scope Z_scope. -intros (p1, p2) (q1, q2); simpl. -case p1; simpl. -intros. -assert (q1 = 0). - elim (Zmult_integral q1 ('p2)); auto with zarith. - intros; discriminate. -subst; auto. -case q1; simpl; intros; try discriminate. -rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto. -case q1; simpl; intros; try discriminate. -rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto. -Open Scope Q_scope. + unfold Qeq, Qinv; simpl. + Open Scope Z_scope. + intros (p1, p2) (q1, q2); simpl. + case p1; simpl. + intros. + assert (q1 = 0). + elim (Zmult_integral q1 ('p2)); auto with zarith. + intros; discriminate. + subst; auto. + case q1; simpl; intros; try discriminate. + rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto. + case q1; simpl; intros; try discriminate. + rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto. + Close Scope Z_scope. Qed. Add Morphism Qdiv : Qdiv_comp. Proof. -intros; unfold Qdiv. -rewrite H; rewrite H0; auto with qarith. + intros; unfold Qdiv. + rewrite H; rewrite H0; auto with qarith. Qed. Add Morphism Qle with signature Qeq ==> Qeq ==> iff as Qle_comp. Proof. -cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<=x3 -> x2<=x4). -split; apply H; assumption || (apply Qeq_sym ; assumption). - -unfold Qeq, Qle; simpl. -Open Scope Z_scope. -intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *. -apply Zmult_le_reg_r with ('p2). -unfold Zgt; auto. -replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring. -rewrite <- H. -apply Zmult_le_reg_r with ('r2). -unfold Zgt; auto. -replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring. -rewrite <- H0. -replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. -replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. -auto with zarith. -Open Scope Q_scope. + cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<=x3 -> x2<=x4). + split; apply H; assumption || (apply Qeq_sym ; assumption). + + unfold Qeq, Qle; simpl. + Open Scope Z_scope. + intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *. + apply Zmult_le_reg_r with ('p2). + unfold Zgt; auto. + replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring. + rewrite <- H. + apply Zmult_le_reg_r with ('r2). + unfold Zgt; auto. + replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring. + rewrite <- H0. + replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. + replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. + auto with zarith. + Close Scope Z_scope. Qed. Add Morphism Qlt with signature Qeq ==> Qeq ==> iff as Qlt_comp. Proof. -cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<x3 -> x2<x4). -split; apply H; assumption || (apply Qeq_sym ; assumption). - -unfold Qeq, Qlt; simpl. -Open Scope Z_scope. -intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *. -apply Zgt_lt. -generalize (Zlt_gt _ _ H1); clear H1; intro H1. -apply Zmult_gt_reg_r with ('p2); auto with zarith. -replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring. -rewrite <- H. -apply Zmult_gt_reg_r with ('r2); auto with zarith. -replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring. -rewrite <- H0. -replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. -replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. -apply Zlt_gt. -apply Zmult_gt_0_lt_compat_l; auto with zarith. -Open Scope Q_scope. + cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<x3 -> x2<x4). + split; apply H; assumption || (apply Qeq_sym ; assumption). + + unfold Qeq, Qlt; simpl. + Open Scope Z_scope. + intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *. + apply Zgt_lt. + generalize (Zlt_gt _ _ H1); clear H1; intro H1. + apply Zmult_gt_reg_r with ('p2); auto with zarith. + replace (q1 * 's2 * 'p2) with (q1 * 'p2 * 's2) by ring. + rewrite <- H. + apply Zmult_gt_reg_r with ('r2); auto with zarith. + replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring. + rewrite <- H0. + replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring. + replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. + apply Zlt_gt. + apply Zmult_gt_0_lt_compat_l; auto with zarith. + Close Scope Z_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)). + (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. + 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. + intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto. Qed. @@ -294,382 +304,387 @@ Qed. Lemma Q_apart_0_1 : ~ 1 == 0. Proof. - unfold Qeq; auto with qarith. + unfold Qeq; auto with qarith. Qed. +(** * Properties of [Qadd] *) + (** Addition is associative: *) Theorem Qplus_assoc : forall x y z, x+(y+z)==(x+y)+z. Proof. - intros (x1, x2) (y1, y2) (z1, z2). - unfold Qeq, Qplus; simpl; simpl_mult; ring. + intros (x1, x2) (y1, y2) (z1, z2). + unfold Qeq, Qplus; simpl; simpl_mult; ring. Qed. (** [0] is a neutral element for addition: *) Lemma Qplus_0_l : forall x, 0+x == x. Proof. - intros (x1, x2); unfold Qeq, Qplus; simpl; ring. + intros (x1, x2); unfold Qeq, Qplus; simpl; ring. Qed. Lemma Qplus_0_r : forall x, x+0 == x. Proof. - intros (x1, x2); unfold Qeq, Qplus; simpl. - rewrite Pmult_comm; simpl; ring. + intros (x1, x2); unfold Qeq, Qplus; simpl. + rewrite Pmult_comm; simpl; ring. Qed. (** Commutativity of addition: *) Theorem Qplus_comm : forall x y, x+y == y+x. Proof. - intros (x1, x2); unfold Qeq, Qplus; simpl. - intros; rewrite Pmult_comm; ring. + intros (x1, x2); unfold Qeq, Qplus; simpl. + intros; rewrite Pmult_comm; ring. Qed. -(** Properties of [Qopp] *) + +(** * Properties of [Qopp] *) Lemma Qopp_involutive : forall q, - -q == q. Proof. - red; simpl; intros; ring. + red; simpl; intros; ring. Qed. Theorem Qplus_opp_r : forall q, q+(-q) == 0. Proof. - red; simpl; intro; ring. + red; simpl; intro; ring. Qed. + +(** * Properties of [Qmult] *) + (** Multiplication is associative: *) Theorem Qmult_assoc : forall n m p, n*(m*p)==(n*m)*p. Proof. - intros; red; simpl; rewrite Pmult_assoc; ring. + intros; red; simpl; rewrite Pmult_assoc; ring. Qed. (** [1] is a neutral element for multiplication: *) Lemma Qmult_1_l : forall n, 1*n == n. Proof. - intro; red; simpl; destruct (Qnum n); auto. + intro; red; simpl; destruct (Qnum n); auto. Qed. Theorem Qmult_1_r : forall n, n*1==n. Proof. - intro; red; simpl. - rewrite Zmult_1_r with (n := Qnum n). - rewrite Pmult_comm; simpl; trivial. + intro; red; simpl. + rewrite Zmult_1_r with (n := Qnum n). + rewrite Pmult_comm; simpl; trivial. Qed. (** Commutativity of multiplication *) Theorem Qmult_comm : forall x y, x*y==y*x. Proof. - intros; red; simpl; rewrite Pmult_comm; ring. + intros; red; simpl; rewrite Pmult_comm; ring. Qed. -(** Distributivity *) +(** Distributivity over [Qadd] *) Theorem Qmult_plus_distr_r : forall x y z, x*(y+z)==(x*y)+(x*z). Proof. -intros (x1, x2) (y1, y2) (z1, z2). -unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring. + intros (x1, x2) (y1, y2) (z1, z2). + unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring. Qed. Theorem Qmult_plus_distr_l : forall x y z, (x+y)*z==(x*z)+(y*z). Proof. -intros (x1, x2) (y1, y2) (z1, z2). -unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring. + intros (x1, x2) (y1, y2) (z1, z2). + unfold Qeq, Qmult, Qplus; simpl; simpl_mult; ring. Qed. (** Integrality *) Theorem Qmult_integral : forall x y, x*y==0 -> x==0 \/ y==0. Proof. - intros (x1,x2) (y1,y2). - unfold Qeq, Qmult; simpl; intros. - destruct (Zmult_integral (x1*1)%Z (y1*1)%Z); auto. - rewrite <- H; ring. + intros (x1,x2) (y1,y2). + unfold Qeq, Qmult; simpl; intros. + destruct (Zmult_integral (x1*1)%Z (y1*1)%Z); auto. + rewrite <- H; ring. Qed. Theorem Qmult_integral_l : forall x y, ~ x == 0 -> x*y == 0 -> y == 0. Proof. - intros (x1, x2) (y1, y2). - unfold Qeq, Qmult; simpl; intros. - apply Zmult_integral_l with x1; auto with zarith. - rewrite <- H0; ring. + intros (x1, x2) (y1, y2). + unfold Qeq, Qmult; simpl; intros. + apply Zmult_integral_l with x1; auto with zarith. + rewrite <- H0; ring. Qed. -(** Inverse and division. *) +(** * Inverse and division. *) Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1. Proof. - intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; - intros; simpl_mult; try ring. - elim H; auto. + intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; + intros; simpl_mult; try ring. + elim H; auto. Qed. Lemma Qinv_mult_distr : forall p q, / (p * q) == /p * /q. Proof. -intros (x1,x2) (y1,y2); unfold Qeq, Qinv, Qmult; simpl. -destruct x1; simpl; auto; - destruct y1; simpl; auto. + intros (x1,x2) (y1,y2); unfold Qeq, Qinv, Qmult; simpl. + destruct x1; simpl; auto; + destruct y1; simpl; auto. Qed. Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x. Proof. - intros; unfold Qdiv. - rewrite <- (Qmult_assoc x y (Qinv y)). - rewrite (Qmult_inv_r y H). - apply Qmult_1_r. + intros; unfold Qdiv. + rewrite <- (Qmult_assoc x y (Qinv y)). + rewrite (Qmult_inv_r y H). + apply Qmult_1_r. Qed. Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x. Proof. - intros; unfold Qdiv. - rewrite (Qmult_assoc y x (Qinv y)). - rewrite (Qmult_comm y x). - fold (Qdiv (Qmult x y) y). - apply Qdiv_mult_l; auto. + intros; unfold Qdiv. + rewrite (Qmult_assoc y x (Qinv y)). + rewrite (Qmult_comm y x). + fold (Qdiv (Qmult x y) y). + apply Qdiv_mult_l; auto. Qed. -(** Properties of order upon Q. *) +(** * Properties of order upon Q. *) Lemma Qle_refl : forall x, x<=x. Proof. -unfold Qle; auto with zarith. + unfold Qle; auto with zarith. Qed. Lemma Qle_antisym : forall x y, x<=y -> y<=x -> x==y. Proof. -unfold Qle, Qeq; auto with zarith. + unfold Qle, Qeq; auto with zarith. Qed. Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. -unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. -Open Scope Z_scope. -apply Zmult_le_reg_r with ('y2). -red; trivial. -apply Zle_trans with (y1 * 'x2 * 'z2). -replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. -apply Zmult_le_compat_r; auto with zarith. -replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. -replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. -apply Zmult_le_compat_r; auto with zarith. -Open Scope Q_scope. + unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. + Open Scope Z_scope. + apply Zmult_le_reg_r with ('y2). + red; trivial. + apply Zle_trans with (y1 * 'x2 * 'z2). + replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. + apply Zmult_le_compat_r; auto with zarith. + replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. + replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. + apply Zmult_le_compat_r; auto with zarith. + Close Scope Z_scope. Qed. Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y. Proof. -unfold Qlt, Qeq; auto with zarith. + unfold Qlt, Qeq; auto with zarith. Qed. (** Large = strict or equal *) Lemma Qlt_le_weak : forall x y, x<y -> x<=y. Proof. -unfold Qle, Qlt; auto with zarith. + unfold Qle, Qlt; auto with zarith. Qed. Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z. Proof. -unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. -Open Scope Z_scope. -apply Zgt_lt. -apply Zmult_gt_reg_r with ('y2). -red; trivial. -apply Zgt_le_trans with (y1 * 'x2 * 'z2). -replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. -replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. -apply Zmult_gt_compat_r; auto with zarith. -replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. -apply Zmult_le_compat_r; auto with zarith. -Open Scope Q_scope. + unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. + Open Scope Z_scope. + apply Zgt_lt. + apply Zmult_gt_reg_r with ('y2). + red; trivial. + apply Zgt_le_trans with (y1 * 'x2 * 'z2). + replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. + replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. + apply Zmult_gt_compat_r; auto with zarith. + replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. + apply Zmult_le_compat_r; auto with zarith. + Close Scope Z_scope. Qed. Lemma Qlt_le_trans : forall x y z, x<y -> y<=z -> x<z. Proof. -unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. -Open Scope Z_scope. -apply Zgt_lt. -apply Zmult_gt_reg_r with ('y2). -red; trivial. -apply Zle_gt_trans with (y1 * 'x2 * 'z2). -replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. -replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. -apply Zmult_le_compat_r; auto with zarith. -replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. -apply Zmult_gt_compat_r; auto with zarith. -Open Scope Q_scope. + unfold Qle, Qlt; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. + Open Scope Z_scope. + apply Zgt_lt. + apply Zmult_gt_reg_r with ('y2). + red; trivial. + apply Zle_gt_trans with (y1 * 'x2 * 'z2). + replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. + replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. + apply Zmult_le_compat_r; auto with zarith. + replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. + apply Zmult_gt_compat_r; auto with zarith. + Close Scope Z_scope. Qed. Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z. Proof. -intros. -apply Qle_lt_trans with y; auto. -apply Qlt_le_weak; auto. + intros. + apply Qle_lt_trans with y; auto. + apply Qlt_le_weak; auto. Qed. (** [x<y] iff [~(y<=x)] *) Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x. Proof. -unfold Qle, Qlt; auto with zarith. + unfold Qle, Qlt; auto with zarith. Qed. Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x. Proof. -unfold Qle, Qlt; auto with zarith. + unfold Qle, Qlt; auto with zarith. Qed. Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x. Proof. -unfold Qle, Qlt; auto with zarith. + unfold Qle, Qlt; auto with zarith. Qed. Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x. Proof. -unfold Qle, Qlt; auto with zarith. + unfold Qle, Qlt; auto with zarith. Qed. Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y. Proof. -unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto. + unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto. Qed. (** Some decidability results about orders. *) Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}. Proof. -unfold Qlt, Qle, Qeq; intros. -exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)). + unfold Qlt, Qle, Qeq; intros. + exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)). Defined. Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}. Proof. -unfold Qlt, Qle; intros. -exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)). + unfold Qlt, Qle; intros. + exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)). Defined. (** Compatibility of operations with respect to order. *) Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p. Proof. -intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. -do 2 rewrite <- Zopp_mult_distr_l; omega. + intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. + do 2 rewrite <- Zopp_mult_distr_l; omega. Qed. Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. Proof. -intros (x1,x2) (y1,y2); unfold Qle; simpl. -rewrite <- Zopp_mult_distr_l. -split; omega. + intros (x1,x2) (y1,y2); unfold Qle; simpl. + rewrite <- Zopp_mult_distr_l. + split; omega. Qed. Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p. Proof. -intros (x1,x2) (y1,y2); unfold Qlt; simpl. -rewrite <- Zopp_mult_distr_l. -split; omega. + intros (x1,x2) (y1,y2); unfold Qlt; simpl. + rewrite <- Zopp_mult_distr_l. + split; omega. Qed. Lemma Qplus_le_compat : - forall x y z t, x<=y -> z<=t -> x+z <= y+t. -Proof. -unfold Qplus, Qle; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2); - simpl; simpl_mult. -Open Scope Z_scope. -intros. -match goal with |- ?a <= ?b => ring a; ring b end. -apply Zplus_le_compat. -replace ('t2 * ('y2 * (z1 * 'x2))) with (z1 * 't2 * ('y2 * 'x2)) by ring. -replace ('z2 * ('x2 * (t1 * 'y2))) with (t1 * 'z2 * ('y2 * 'x2)) by ring. -apply Zmult_le_compat_r; auto with zarith. -replace ('t2 * ('y2 * ('z2 * x1))) with (x1 * 'y2 * ('z2 * 't2)) by ring. -replace ('z2 * ('x2 * ('t2 * y1))) with (y1 * 'x2 * ('z2 * 't2)) by ring. -apply Zmult_le_compat_r; auto with zarith. -Open Scope Q_scope. + forall x y z t, x<=y -> z<=t -> x+z <= y+t. +Proof. + unfold Qplus, Qle; intros (x1, x2) (y1, y2) (z1, z2) (t1, t2); + simpl; simpl_mult. + Open Scope Z_scope. + intros. + match goal with |- ?a <= ?b => ring_simplify a b end. + rewrite Zplus_comm. + apply Zplus_le_compat. + match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end. + auto with zarith. + match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end. + auto with zarith. + Close Scope Z_scope. Qed. Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. Proof. -intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. -Open Scope Z_scope. -intros; simpl_mult. -replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. -replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. -apply Zmult_le_compat_r; auto with zarith. -Open Scope Q_scope. + intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. + Open Scope Z_scope. + intros; simpl_mult. + replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. + replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. + apply Zmult_le_compat_r; auto with zarith. + Close Scope Z_scope. Qed. Lemma Qmult_lt_0_le_reg_r : forall x y z, 0 < z -> x*z <= y*z -> x <= y. Proof. -intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. -Open Scope Z_scope. -simpl_mult. -replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. -replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. -intros; apply Zmult_le_reg_r with (c1*'c2); auto with zarith. -Open Scope Q_scope. + intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. + Open Scope Z_scope. + simpl_mult. + replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. + replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. + intros; apply Zmult_le_reg_r with (c1*'c2); auto with zarith. + Close Scope Z_scope. Qed. Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. Proof. -intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. -Open Scope Z_scope. -intros; simpl_mult. -replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. -replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. -apply Zmult_lt_compat_r; auto with zarith. -apply Zmult_lt_0_compat. -omega. -compute; auto. -Open Scope Q_scope. + intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. + Open Scope Z_scope. + intros; simpl_mult. + replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring. + replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring. + apply Zmult_lt_compat_r; auto with zarith. + apply Zmult_lt_0_compat. + omega. + compute; auto. + Close Scope Z_scope. Qed. -(** Rational to the n-th power *) +(** * Rational to the n-th power *) Fixpoint Qpower (q:Q)(n:nat) { struct n } : Q := - match n with - | O => 1 - | S n => q * (Qpower q n) - end. + match n with + | O => 1 + | S n => q * (Qpower q n) + end. Notation " q ^ n " := (Qpower q n) : Q_scope. Lemma Qpower_1 : forall n, 1^n == 1. Proof. -induction n; simpl; auto with qarith. -rewrite IHn; auto with qarith. + induction n; simpl; auto with qarith. + rewrite IHn; auto with qarith. Qed. Lemma Qpower_0 : forall n, n<>O -> 0^n == 0. Proof. -destruct n; simpl. -destruct 1; auto. -intros. -compute; auto. + destruct n; simpl. + destruct 1; auto. + intros. + 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 Qle_trans with (0*(p^n)). -compute; intro; discriminate. -apply Qmult_le_compat_r; auto. + induction n; simpl; auto with qarith. + intros; compute; intro; discriminate. + intros. + apply Qle_trans with (0*(p^n)). + compute; intro; discriminate. + apply Qmult_le_compat_r; auto. Qed. Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n. Proof. -induction n. -compute; auto. -simpl. -intros; rewrite IHn; clear IHn. -unfold Qdiv; rewrite Qinv_mult_distr. -setoid_replace (1#p) with (/ inject_Z ('p)). -apply Qeq_refl. -compute; auto. + induction n. + compute; auto. + simpl. + intros; rewrite IHn; clear IHn. + unfold Qdiv; rewrite Qinv_mult_distr. + setoid_replace (1#p) with (/ inject_Z ('p)). + apply Qeq_refl. + compute; auto. Qed. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 9cbd400d..98c5ff9e 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -6,9 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qcanon.v 8989 2006-06-25 22:17:49Z letouzey $ i*) +(*i $Id: Qcanon.v 9245 2006-10-17 12:53:34Z notin $ i*) +Require Import Field. Require Import QArith. +Require Import Znumtheory. Require Import Eqdep_dec. (** [Qc] : A canonical representation of rational numbers. @@ -22,50 +24,50 @@ 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. + 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. + 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. + 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. + 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. + intros; apply Qred_complete. + apply Qred_correct. Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). @@ -74,16 +76,16 @@ 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. + 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. @@ -105,39 +107,39 @@ 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. + 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). + 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). + 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). + 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). + 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. + 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 @@ -160,8 +162,8 @@ Infix "/" := Qcdiv : Qc_scope. Lemma Q_apart_0_1 : 1 <> 0. Proof. - unfold Q2Qc. - intros H; discriminate H. + unfold Q2Qc. + intros H; discriminate H. Qed. Ltac qc := match goal with @@ -175,309 +177,309 @@ Opaque Qred. Theorem Qcplus_assoc : forall x y z, x+(y+z)=(x+y)+z. Proof. - intros; qc; apply Qplus_assoc. + 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. + intros; qc; apply Qplus_0_l. Qed. Lemma Qcplus_0_r : forall x, x+0 = x. Proof. - intros; qc; apply Qplus_0_r. + 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. + intros; qc; apply Qplus_comm. Qed. (** Properties of [Qopp] *) Lemma Qcopp_involutive : forall q, - -q = q. Proof. - intros; qc; apply Qopp_involutive. + intros; qc; apply Qopp_involutive. Qed. Theorem Qcplus_opp_r : forall q, q+(-q) = 0. Proof. - intros; qc; apply Qplus_opp_r. + 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. + 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. + intros; qc; apply Qmult_1_l. Qed. Theorem Qcmult_1_r : forall n, n*1=n. Proof. - intros; qc; apply Qmult_1_r. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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. + 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: *) @@ -488,10 +490,12 @@ 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. +Proof. + 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. @@ -506,17 +510,37 @@ 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 ]. +*) +Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)). +Proof. + constructor. + exact Qcplus_0_l. + exact Qcplus_comm. + exact Qcplus_assoc. + exact Qcmult_1_l. + exact Qcmult_comm. + exact Qcmult_assoc. + exact Qcmult_plus_distr_l. + reflexivity. + exact Qcplus_opp_r. +Qed. -(** A field tactic for rational numbers *) +Definition Qcft : + field_theory 0%Qc 1%Qc Qcplus Qcmult Qcminus Qcopp Qcdiv Qcinv (eq(A:=Qc)). +Proof. + constructor. + exact Qcrt. + exact Q_apart_0_1. + reflexivity. + exact Qcmult_inv_l. +Qed. -Require Import Field. +Add Field Qcfield : Qcft. -Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l - with div:=Qcdiv. +(** A field tactic for rational numbers *) -Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x. +Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc. intros. field. auto. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5b7480c1..6bd161f3 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreals.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: Qreals.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Rbase. Require Export QArith_base. -(** * A field tactic for rational numbers. *) +(** A field tactic for rational numbers. *) (** Since field cannot operate on setoid datatypes (yet?), we translate Q goals into reals before applying field. *) @@ -52,8 +52,9 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R). unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. apply IZR_eq; auto. clear H. -field; auto. -rewrite <- H0; field; auto. +field_simplify_eq; auto. +ring_simplify X1 Y2 (Y2 * X1)%R. +rewrite H0 in |- *; ring. Qed. Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y. @@ -176,16 +177,11 @@ unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *. case x1. simpl in |- *; intros; elim H; trivial. intros; field; auto. -apply Rmult_integral_contrapositive; split; auto. -apply Rmult_integral_contrapositive; split; auto. -apply Rinv_neq_0_compat; auto. -intros; field; auto. -do 2 rewrite <- mult_IZR. -simpl in |- *; rewrite Pmult_comm; auto. -apply Rmult_integral_contrapositive; split; auto. -apply Rmult_integral_contrapositive; split; auto. -apply not_O_IZR; auto with qarith. -apply Rinv_neq_0_compat; auto. +intros; + change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *; + change (IZR (Zneg p)) with (- IZR (' p))%R in |- *; + field; (*auto 8 with real.*) + repeat split; auto; auto with real. Qed. Lemma Q2R_div : @@ -210,4 +206,4 @@ Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x. intros; QField. intro; apply H; apply eqR_Qeq. rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real. -Abort.
\ No newline at end of file +Abort. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index c503daad..340cac83 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreduction.v 8989 2006-06-25 22:17:49Z letouzey $ i*) +(*i $Id: Qreduction.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** * Normalisation functions for rational numbers. *) +(** Normalisation functions for rational numbers. *) Require Export QArith_base. -Require Export Znumtheory. +Require Import Znumtheory. (** First, a function that (tries to) build a positive back from a Z. *) @@ -42,104 +42,105 @@ Definition Qred (q:Q) := Lemma Qred_correct : forall q, (Qred q) == q. Proof. -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. -Open Scope Z_scope. -intuition. -rewrite <- H in H0,H1; clear H. -rewrite H3; rewrite H4. -assert (0 <> g). + 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. + Open Scope Z_scope. + intuition. + rewrite <- H in H0,H1; clear H. + rewrite H3; rewrite H4. + assert (0 <> g). intro; subst g; discriminate. - -assert (0 < dd). + + assert (0 < dd). apply Zmult_gt_0_lt_0_reg_r with g. omega. rewrite Zmult_comm. rewrite <- H4; compute; auto. -rewrite Z2P_correct; auto. -ring. + rewrite Z2P_correct; auto. + ring. + Close Scope Z_scope. Qed. Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q. Proof. -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)). -destruct (Zggcd a (Zpos b)) as (g,(aa,bb)). -generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) - (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)). -destruct (Zggcd c (Zpos d)) as (g',(cc,dd)). -simpl. -intro H; rewrite <- H; clear H. -intros Hg'1 Hg'2 (Hg'3,Hg'4). -intro H; rewrite <- H; clear H. -intros Hg1 Hg2 (Hg3,Hg4). -intros. -assert (g <> 0). + 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)). + destruct (Zggcd a (Zpos b)) as (g,(aa,bb)). + generalize (Zggcd_gcd c ('d)) (Zgcd_is_gcd c ('d)) + (Zgcd_is_pos c ('d)) (Zggcd_correct_divisors c ('d)). + destruct (Zggcd c (Zpos d)) as (g',(cc,dd)). + simpl. + intro H; rewrite <- H; clear H. + intros Hg'1 Hg'2 (Hg'3,Hg'4). + intro H; rewrite <- H; clear H. + intros Hg1 Hg2 (Hg3,Hg4). + intros. + assert (g <> 0). intro; subst g; discriminate. -assert (g' <> 0). + assert (g' <> 0). intro; subst g'; discriminate. -elim (rel_prime_cross_prod aa bb cc dd). -congruence. -unfold rel_prime in |- *. -(*rel_prime*) -constructor. -exists aa; auto with zarith. -exists bb; auto with zarith. -intros. -inversion Hg1. -destruct (H6 (g*x)). -rewrite Hg3. -destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring. -rewrite Hg4. -destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring. -exists q. -apply Zmult_reg_l with g; auto. -pattern g at 1; rewrite H7; ring. -(* /rel_prime *) -unfold rel_prime in |- *. -(* rel_prime *) -constructor. -exists cc; auto with zarith. -exists dd; auto with zarith. -intros. -inversion Hg'1. -destruct (H6 (g'*x)). -rewrite Hg'3. -destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring. -rewrite Hg'4. -destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring. -exists q. -apply Zmult_reg_l with g'; auto. -pattern g' at 1; rewrite H7; ring. -(* /rel_prime *) -assert (0<bb); [|auto with zarith]. + elim (rel_prime_cross_prod aa bb cc dd). + congruence. + unfold rel_prime in |- *. + (*rel_prime*) + constructor. + exists aa; auto with zarith. + exists bb; auto with zarith. + intros. + inversion Hg1. + destruct (H6 (g*x)). + rewrite Hg3. + destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring. + rewrite Hg4. + destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring. + exists q. + apply Zmult_reg_l with g; auto. + pattern g at 1; rewrite H7; ring. + (* /rel_prime *) + unfold rel_prime in |- *. + (* rel_prime *) + constructor. + exists cc; auto with zarith. + exists dd; auto with zarith. + intros. + inversion Hg'1. + destruct (H6 (g'*x)). + rewrite Hg'3. + destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring. + rewrite Hg'4. + destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring. + exists q. + apply Zmult_reg_l with g'; auto. + pattern g' at 1; rewrite H7; ring. + (* /rel_prime *) + assert (0<bb); [|auto with zarith]. apply Zmult_gt_0_lt_0_reg_r with g. omega. rewrite Zmult_comm. rewrite <- Hg4; compute; auto. -assert (0<dd); [|auto with zarith]. + assert (0<dd); [|auto with zarith]. apply Zmult_gt_0_lt_0_reg_r with g'. omega. rewrite Zmult_comm. rewrite <- Hg'4; compute; auto. -apply Zmult_reg_l with (g'*g). -intro H2; elim (Zmult_integral _ _ H2); auto. -replace (g'*g*(aa*dd)) with ((g*aa)*(g'*dd)); [|ring]. -replace (g'*g*(bb*cc)) with ((g'*cc)*(g*bb)); [|ring]. -rewrite <- Hg3; rewrite <- Hg4; rewrite <- Hg'3; rewrite <- Hg'4; auto. -Open Scope Q_scope. + apply Zmult_reg_l with (g'*g). + intro H2; elim (Zmult_integral _ _ H2); auto. + replace (g'*g*(aa*dd)) with ((g*aa)*(g'*dd)); [|ring]. + replace (g'*g*(bb*cc)) with ((g'*cc)*(g*bb)); [|ring]. + rewrite <- Hg3; rewrite <- Hg4; rewrite <- Hg'3; rewrite <- Hg'4; auto. + Close Scope Z_scope. Qed. Add Morphism Qred : Qred_comp. Proof. -intros q q' H. -rewrite (Qred_correct q); auto. -rewrite (Qred_correct q'); auto. + intros q q' H. + rewrite (Qred_correct q); auto. + rewrite (Qred_correct q'); auto. Qed. Definition Qplus' (p q : Q) := Qred (Qplus p q). @@ -147,22 +148,22 @@ Definition Qmult' (p q : Q) := Qred (Qmult p q). Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q). Proof. -intros; unfold Qplus' in |- *; apply Qred_correct; auto. + intros; unfold Qplus' in |- *; apply Qred_correct; auto. Qed. Lemma Qmult'_correct : forall p q : Q, (Qmult' p q)==(Qmult p q). Proof. -intros; unfold Qmult' in |- *; apply Qred_correct; auto. + intros; unfold Qmult' in |- *; apply Qred_correct; auto. Qed. Add Morphism Qplus' : Qplus'_comp. Proof. -intros; unfold Qplus' in |- *. -rewrite H; rewrite H0; auto with qarith. + intros; unfold Qplus' in |- *. + rewrite H; rewrite H0; auto with qarith. Qed. Add Morphism Qmult' : Qmult'_comp. -intros; unfold Qmult' in |- *. -rewrite H; rewrite H0; auto with qarith. + intros; unfold Qmult' in |- *. + rewrite H; rewrite H0; auto with qarith. Qed. diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 774b20f4..9d294805 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -6,10 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qring.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: Qring.v 9245 2006-10-17 12:53:34Z notin $ i*) -Require Import Ring. -Require Export Setoid_ring. +Require Export Ring. Require Export QArith_base. (** * A ring tactic for rational numbers *) @@ -18,74 +17,88 @@ Definition Qeq_bool (x y : Q) := if Qeq_dec x y then true else false. Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y. -intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. -intros _ H; inversion H. +Proof. + intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. + intros _ H; inversion H. Qed. -Definition Qsrt : Setoid_Ring_Theory Qeq Qplus Qmult 1 0 Qopp Qeq_bool. +Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. Proof. -constructor. -exact Qplus_comm. -exact Qplus_assoc. -exact Qmult_comm. -exact Qmult_assoc. -exact Qplus_0_l. -exact Qmult_1_l. -exact Qplus_opp_r. -exact Qmult_plus_distr_l. -unfold Is_true; intros x y; generalize (Qeq_bool_correct x y); - case (Qeq_bool x y); auto. + constructor. + exact Qplus_0_l. + exact Qplus_comm. + exact Qplus_assoc. + exact Qmult_1_l. + exact Qmult_comm. + exact Qmult_assoc. + exact Qmult_plus_distr_l. + reflexivity. + exact Qplus_opp_r. Qed. -Add Setoid Ring Q Qeq Q_Setoid Qplus Qmult 1 0 Qopp Qeq_bool - Qplus_comp Qmult_comp Qopp_comp Qsrt - [ Qmake (*inject_Z*) Zpos 0%Z Zneg xI xO 1%positive ]. - +Ltac isQcst t := + let t := eval hnf in t in + match t with + Qmake ?n ?d => + match isZcst n with + true => isZcst d + | _ => false + end + | _ => false + end. + +Ltac Qcst t := + match isQcst t with + true => t + | _ => NotConstant + end. + +Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]). (** Exemple of use: *) Section Examples. Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). -intros. -ring. + intros. + ring. Qed. Let ex2 : forall x y : Q, x+y == y+x. -intros. -ring. + intros. + ring. Qed. Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z). -intros. -ring. + intros. + ring. Qed. Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2). -ring. + ring. Qed. Let ex5 : 1+1 == 2#1. -ring. + ring. Qed. Let ex6 : (1#1)+(1#1) == 2#1. -ring. + ring. Qed. Let ex7 : forall x : Q, x-x== 0#1. -intro. -ring. + intro. + ring. Qed. End Examples. Lemma Qopp_plus : forall a b, -(a+b) == -a + -b. Proof. -intros; ring. + intros; ring. Qed. Lemma Qopp_opp : forall q, - -q==q. Proof. -intros; ring. + intros; ring. Qed. |