diff options
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/QArith.v | 2 | ||||
| -rw-r--r-- | theories/QArith/QArith_base.v | 183 | ||||
| -rw-r--r-- | theories/QArith/Qabs.v | 124 | ||||
| -rw-r--r-- | theories/QArith/Qcanon.v | 38 | ||||
| -rw-r--r-- | theories/QArith/Qfield.v | 153 | ||||
| -rw-r--r-- | theories/QArith/Qpower.v | 239 | ||||
| -rw-r--r-- | theories/QArith/Qreals.v | 32 | ||||
| -rw-r--r-- | theories/QArith/Qreduction.v | 26 | ||||
| -rw-r--r-- | theories/QArith/Qring.v | 97 | ||||
| -rw-r--r-- | theories/QArith/Qround.v | 139 |
10 files changed, 864 insertions, 169 deletions
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v index 03935e2b..2af65320 100644 --- a/theories/QArith/QArith.v +++ b/theories/QArith/QArith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: QArith.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: QArith.v 10739 2008-04-01 14:45:20Z herbelin $ i*) Require Export QArith_base. Require Export Qring. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index fc92c678..304fbf77 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 9932 2007-07-02 14:31:33Z notin $ i*) +(*i $Id: QArith_base.v 10765 2008-04-08 16:15:23Z msozeau $ i*) Require Export ZArith. Require Export ZArithRing. @@ -79,9 +79,9 @@ Qed. Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). Proof. unfold Qle, Qcompare, Zle. -split; intros; swap H. +split; intros; contradict H. rewrite Zcompare_Gt_Lt_antisym; auto. -rewrite Zcompare_Gt_Lt_antisym in H0; auto. +rewrite Zcompare_Gt_Lt_antisym in H; auto. Qed. Hint Unfold Qeq Qlt Qle: qarith. @@ -121,7 +121,7 @@ Defined. Definition Q_Setoid : Setoid_Theory Q Qeq. Proof. - split; unfold Qeq in |- *; auto; apply Qeq_trans. + split; red; unfold Qeq in |- *; auto; apply Qeq_trans. Qed. Add Setoid Q Qeq Q_Setoid as Qsetoid. @@ -130,6 +130,12 @@ 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. +Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. +Proof. + auto with qarith. +Qed. + +Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) @@ -165,6 +171,13 @@ Infix "/" := Qdiv : Q_scope. Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope. +Lemma Qmake_Qdiv : forall a b, a#b==inject_Z a/inject_Z ('b). +Proof. +intros a b. +unfold Qeq. +simpl. +ring. +Qed. (** * Setoid compatibility results *) @@ -187,7 +200,7 @@ Proof. unfold Qeq, Qopp; simpl. Open Scope Z_scope. intros. - replace (- Qnum x1 * ' Qden x2) with (- (Qnum x1 * ' Qden x2)) by ring. + replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring. rewrite H in |- *; ring. Close Scope Z_scope. Qed. @@ -416,6 +429,11 @@ Qed. (** * Inverse and division. *) +Lemma Qinv_involutive : forall q, (/ / q) == q. +Proof. +intros [[|n|n] d]; red; simpl; reflexivity. +Qed. + Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1. Proof. intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; @@ -474,6 +492,8 @@ Proof. Close Scope Z_scope. Qed. +Hint Resolve Qle_trans : qarith. + Lemma Qlt_not_eq : forall x y, x<y -> ~ x==y. Proof. unfold Qlt, Qeq; auto with zarith. @@ -552,6 +572,9 @@ Proof. unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto. Qed. +Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le + Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih. + (** Some decidability results about orders. *) Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}. @@ -574,6 +597,8 @@ Proof. do 2 rewrite <- Zopp_mult_distr_l; omega. Qed. +Hint Resolve Qopp_le_compat : qarith. + Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. Proof. intros (x1,x2) (y1,y2); unfold Qle; simpl. @@ -641,50 +666,136 @@ Proof. Close Scope Z_scope. Qed. -(** * Rational to the n-th power *) +Lemma Qmult_le_0_compat : forall a b, 0 <= a -> 0 <= b -> 0 <= a*b. +Proof. +intros a b Ha Hb. +unfold Qle in *. +simpl in *. +auto with *. +Qed. -Fixpoint Qpower (q:Q)(n:nat) { struct n } : Q := - match n with - | O => 1 - | S n => q * (Qpower q n) - end. +Lemma Qinv_le_0_compat : forall a, 0 <= a -> 0 <= /a. +Proof. +intros [[|n|n] d] Ha; assumption. +Qed. -Notation " q ^ n " := (Qpower q n) : Q_scope. +Lemma Qle_shift_div_l : forall a b c, + 0 < c -> a*c <= b -> a <= b/c. +Proof. +intros a b c Hc H. +apply Qmult_lt_0_le_reg_r with (c). + assumption. +setoid_replace (b/c*c) with (c*(b/c)) by apply Qmult_comm. +rewrite Qmult_div_r; try assumption. +auto with *. +Qed. -Lemma Qpower_1 : forall n, 1^n == 1. +Lemma Qle_shift_inv_l : forall a c, + 0 < c -> a*c <= 1 -> a <= /c. Proof. - induction n; simpl; auto with qarith. - rewrite IHn; auto with qarith. +intros a c Hc H. +setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l). +change (a <= 1/c). +apply Qle_shift_div_l; assumption. Qed. -Lemma Qpower_0 : forall n, n<>O -> 0^n == 0. +Lemma Qle_shift_div_r : forall a b c, + 0 < b -> a <= c*b -> a/b <= c. Proof. - destruct n; simpl. - destruct 1; auto. - intros. - compute; auto. +intros a b c Hc H. +apply Qmult_lt_0_le_reg_r with b. + assumption. +setoid_replace (a/b*b) with (b*(a/b)) by apply Qmult_comm. +rewrite Qmult_div_r; try assumption. +auto with *. Qed. -Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n. +Lemma Qle_shift_inv_r : forall b c, + 0 < b -> 1 <= c*b -> /b <= c. 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. +intros b c Hc H. +setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l). +change (1/b <= c). +apply Qle_shift_div_r; assumption. Qed. -Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n. +Lemma Qinv_lt_0_compat : forall a, 0 < a -> 0 < /a. 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. +intros [[|n|n] d] Ha; assumption. +Qed. + +Lemma Qlt_shift_div_l : forall a b c, + 0 < c -> a*c < b -> a < b/c. +Proof. +intros a b c Hc H. +apply Qnot_le_lt. +intros H0. +apply (Qlt_not_le _ _ H). +apply Qmult_lt_0_le_reg_r with (/c). + apply Qinv_lt_0_compat. + assumption. +setoid_replace (a*c/c) with (a) by (apply Qdiv_mult_l; auto with *). +assumption. +Qed. + +Lemma Qlt_shift_inv_l : forall a c, + 0 < c -> a*c < 1 -> a < /c. +Proof. +intros a c Hc H. +setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l). +change (a < 1/c). +apply Qlt_shift_div_l; assumption. +Qed. + +Lemma Qlt_shift_div_r : forall a b c, + 0 < b -> a < c*b -> a/b < c. +Proof. +intros a b c Hc H. +apply Qnot_le_lt. +intros H0. +apply (Qlt_not_le _ _ H). +apply Qmult_lt_0_le_reg_r with (/b). + apply Qinv_lt_0_compat. + assumption. +setoid_replace (c*b/b) with (c) by (apply Qdiv_mult_l; auto with *). +assumption. +Qed. + +Lemma Qlt_shift_inv_r : forall b c, + 0 < b -> 1 < c*b -> /b < c. +Proof. +intros b c Hc H. +setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l). +change (1/b < c). +apply Qlt_shift_div_r; assumption. Qed. +(** * Rational to the n-th power *) + +Definition Qpower_positive (q:Q)(p:positive) : Q := + pow_pos Qmult q p. +Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp. +Proof. +intros x1 x2 Hx y. +unfold Qpower_positive. +induction y; simpl; +try rewrite IHy; +try rewrite Hx; +reflexivity. +Qed. + +Definition Qpower (q:Q) (z:Z) := + match z with + | Zpos p => Qpower_positive q p + | Z0 => 1 + | Zneg p => /Qpower_positive q p + end. + +Notation " q ^ z " := (Qpower q z) : Q_scope. + +Add Morphism Qpower with signature Qeq ==> @eq _ ==> Qeq as Qpower_comp. +Proof. +intros x1 x2 Hx [|y|y]; try reflexivity; +simpl; rewrite Hx; reflexivity. +Qed. diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v new file mode 100644 index 00000000..e672016e --- /dev/null +++ b/theories/QArith/Qabs.v @@ -0,0 +1,124 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +Require Export QArith. +Require Export Qreduction. + +Hint Resolve Qlt_le_weak : qarith. + +Definition Qabs (x:Q) := let (n,d):=x in (Zabs n#d). + +Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x). +Proof. +intros x P H1 H2. +destruct x as [[|xn|xn] xd]; +[apply H1|apply H1|apply H2]; +abstract (compute; discriminate). +Defined. + +Add Morphism Qabs with signature Qeq ==> Qeq as Qabs_wd. +intros [xn xd] [yn yd] H. +simpl. +unfold Qeq in *. +simpl in *. +change (' yd)%Z with (Zabs (' yd)). +change (' xd)%Z with (Zabs (' xd)). +repeat rewrite <- Zabs_Zmult. +congruence. +Qed. + +Lemma Qabs_pos : forall x, 0 <= x -> Qabs x == x. +Proof. +intros x H. +apply Qabs_case. +reflexivity. +intros H0. +setoid_replace x with 0. +reflexivity. +apply Qle_antisym; assumption. +Qed. + +Lemma Qabs_neg : forall x, x <= 0 -> Qabs x == - x. +Proof. +intros x H. +apply Qabs_case. +intros H0. +setoid_replace x with 0. +reflexivity. +apply Qle_antisym; assumption. +reflexivity. +Qed. + +Lemma Qabs_nonneg : forall x, 0 <= (Qabs x). +intros x. +apply Qabs_case. +auto. +apply (Qopp_le_compat x 0). +Qed. + +Lemma Zabs_Qabs : forall n d, (Zabs n#d)==Qabs (n#d). +Proof. +intros [|n|n]; reflexivity. +Qed. + +Lemma Qabs_opp : forall x, Qabs (-x) == Qabs x. +Proof. +intros x. +do 2 apply Qabs_case; try (intros; ring); +(intros H0 H1; +setoid_replace x with 0;[reflexivity|]; +apply Qle_antisym);try assumption; +rewrite Qle_minus_iff in *; +ring_simplify; +ring_simplify in H1; +assumption. +Qed. + +Lemma Qabs_triangle : forall x y, Qabs (x+y) <= Qabs x + Qabs y. +Proof. +intros [xn xd] [yn yd]. +unfold Qplus. +unfold Qle. +simpl. +apply Zmult_le_compat_r;auto with *. +change (' yd)%Z with (Zabs (' yd)). +change (' xd)%Z with (Zabs (' xd)). +repeat rewrite <- Zabs_Zmult. +apply Zabs_triangle. +Qed. + +Lemma Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b). +Proof. +intros [an ad] [bn bd]. +simpl. +rewrite Zabs_Zmult. +reflexivity. +Qed. + +Lemma Qle_Qabs : forall a, a <= Qabs a. +Proof. +intros a. +apply Qabs_case; auto with *. +intros H. +apply Qle_trans with 0; try assumption. +change 0 with (-0). +apply Qopp_le_compat. +assumption. +Qed. + +Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y). +Proof. +intros x y. +rewrite Qle_minus_iff. +setoid_replace (Qabs (x - y) + - (Qabs x - Qabs y)) with ((Qabs (x - y) + Qabs y) + - Qabs x) by ring. +rewrite <- Qle_minus_iff. +setoid_replace (Qabs x) with (Qabs (x-y+y)). +apply Qabs_triangle. +apply Qabs_wd. +ring. +Qed. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 98c5ff9e..42522468 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qcanon.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Qcanon.v 10739 2008-04-01 14:45:20Z herbelin $ i*) Require Import Field. Require Import QArith. @@ -101,6 +101,7 @@ Infix "<=" := Qcle : Qc_scope. Infix ">" := Qcgt : Qc_scope. Infix ">=" := Qcge : Qc_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : 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. @@ -139,7 +140,7 @@ 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. + right; contradict H; subst; auto with qarith. Defined. (** The addition, multiplication and opposite are defined @@ -347,7 +348,7 @@ Proof. unfold Qcle, Qclt; intros; eapply Qlt_le_trans; eauto. Qed. -Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z. +Lemma Qclt_trans : forall x y z, x<y -> y<z -> x<z. Proof. unfold Qclt; intros; eapply Qlt_trans; eauto. Qed. @@ -472,7 +473,7 @@ Proof. compute; auto. Qed. -Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n. +Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n. Proof. induction n; simpl; auto with qarith. intros; compute; intro; discriminate. @@ -495,23 +496,6 @@ Proof. 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 ]. -*) Definition Qcrt : ring_theory 0 1 Qcplus Qcmult Qcminus Qcopp (eq(A:=Qc)). Proof. constructor. @@ -547,4 +531,14 @@ 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. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v new file mode 100644 index 00000000..5d548aea --- /dev/null +++ b/theories/QArith/Qfield.v @@ -0,0 +1,153 @@ +(************************************************************************) +(* 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: Qfield.v 10739 2008-04-01 14:45:20Z herbelin $ i*) + +Require Export Field. +Require Export QArith_base. +Require Import NArithRing. + +(** * field and ring tactics for rational numbers *) + +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. +Proof. + intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. + intros _ H; inversion H. +Qed. + +Lemma Qeq_bool_complete : forall x y : Q, x==y -> Qeq_bool x y = true. +Proof. + intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. +Qed. + +Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq. +Proof. + constructor. + 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. + discriminate. + reflexivity. + intros p Hp. + rewrite Qmult_comm. + apply Qmult_inv_r. + exact Hp. +Qed. + +Lemma Qpower_theory : power_theory 1 Qmult Qeq Z_of_N Qpower. +Proof. +constructor. +intros r [|n]; +reflexivity. +Qed. + +Ltac isQcst t := + match t with + | inject_Z ?z => isZcst z + | Qmake ?n ?d => + match isZcst n with + true => isPcst d + | _ => false + end + | _ => false + end. + +Ltac Qcst t := + match isQcst t with + true => t + | _ => NotConstant + end. + +Ltac Qpow_tac t := + match t with + | Z0 => N0 + | Zpos ?n => Ncst (Npos n) + | Z_of_N ?n => Ncst n + | NtoZ ?n => Ncst n + | _ => NotConstant + end. + +Add Field Qfield : Qsft + (decidable Qeq_bool_correct, + completeness Qeq_bool_complete, + constants [Qcst], + power_tac Qpower_theory [Qpow_tac]). + +(** Exemple of use: *) + +Section Examples. + +Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). + intros. + ring. +Qed. + +Let ex2 : forall x y : Q, x+y == y+x. + intros. + ring. +Qed. + +Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z). + intros. + ring. +Qed. + +Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2). + ring. +Qed. + +Let ex5 : 1+1 == 2#1. + ring. +Qed. + +Let ex6 : (1#1)+(1#1) == 2#1. + ring. +Qed. + +Let ex7 : forall x : Q, x-x== 0. + intro. + ring. +Qed. + +Let ex8 : forall x : Q, x^1 == x. + intro. + ring. +Qed. + +Let ex9 : forall x : Q, x^0 == 1. + intro. + ring. +Qed. + +Let ex10 : forall x y : Q, ~(y==0) -> (x/y)*y == x. +intros. +field. +auto. +Qed. + +End Examples. + +Lemma Qopp_plus : forall a b, -(a+b) == -a + -b. +Proof. + intros; ring. +Qed. + +Lemma Qopp_opp : forall q, - -q==q. +Proof. + intros; ring. +Qed. diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v new file mode 100644 index 00000000..8672592d --- /dev/null +++ b/theories/QArith/Qpower.v @@ -0,0 +1,239 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +Require Import Zpow_facts Qfield Qreduction. + +Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1. +Proof. +induction n; +simpl; try rewrite IHn; reflexivity. +Qed. + +Lemma Qpower_1 : forall n, 1^n == 1. +Proof. + intros [|n|n]; simpl; try rewrite Qpower_positive_1; reflexivity. +Qed. + +Lemma Qpower_positive_0 : forall n, Qpower_positive 0 n == 0. +Proof. +induction n; +simpl; try rewrite IHn; reflexivity. +Qed. + +Lemma Qpower_0 : forall n, (n<>0)%Z -> 0^n == 0. +Proof. + intros [|n|n] Hn; try (elim Hn; reflexivity); simpl; + rewrite Qpower_positive_0; reflexivity. +Qed. + +Lemma Qpower_not_0_positive : forall a n, ~a==0 -> ~Qpower_positive a n == 0. +Proof. +intros a n X H. +apply X; clear X. +induction n; simpl in *; try assumption; +destruct (Qmult_integral _ _ H); +try destruct (Qmult_integral _ _ H0); auto. +Qed. + +Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n. +intros p n Hp. +induction n; simpl; repeat apply Qmult_le_0_compat;assumption. +Qed. + +Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n. +Proof. + intros p [|n|n] Hp; simpl; try discriminate; + try apply Qinv_le_0_compat; apply Qpower_pos_positive; assumption. +Qed. + +Lemma Qmult_power_positive : forall a b n, Qpower_positive (a*b) n == (Qpower_positive a n)*(Qpower_positive b n). +Proof. +induction n; +simpl; repeat rewrite IHn; ring. +Qed. + +Lemma Qmult_power : forall a b n, (a*b)^n == a^n*b^n. +Proof. + intros a b [|n|n]; simpl; + try rewrite Qmult_power_positive; + try rewrite Qinv_mult_distr; + reflexivity. +Qed. + +Lemma Qinv_power_positive : forall a n, Qpower_positive (/a) n == /(Qpower_positive a n). +Proof. +induction n; +simpl; repeat (rewrite IHn || rewrite Qinv_mult_distr); reflexivity. +Qed. + +Lemma Qinv_power : forall a n, (/a)^n == /a^n. +Proof. + intros a [|n|n]; simpl; + try rewrite Qinv_power_positive; + reflexivity. +Qed. + +Lemma Qdiv_power : forall a b n, (a/b)^n == (a^n/b^n). +Proof. +unfold Qdiv. +intros a b n. +rewrite Qmult_power. +rewrite Qinv_power. +reflexivity. +Qed. + +Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n. +Proof. +intros n p. +rewrite Qmake_Qdiv. +rewrite Qdiv_power. +rewrite Qpower_1. +unfold Qdiv. +ring. +Qed. + +Lemma Qpower_plus_positive : forall a n m, Qpower_positive a (n+m) == (Qpower_positive a n)*(Qpower_positive a m). +Proof. +intros a n m. +unfold Qpower_positive. +apply pow_pos_Pplus. +apply Q_Setoid. +apply Qmult_comp. +apply Qmult_comm. +apply Qmult_assoc. +Qed. + +Lemma Qpower_opp : forall a n, a^(-n) == /a^n. +Proof. +intros a [|n|n]; simpl; try reflexivity. +symmetry; apply Qinv_involutive. +Qed. + +Lemma Qpower_minus_positive : forall a (n m:positive), (Pcompare n m Eq=Gt)%positive -> Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m). +Proof. +intros a n m H. +destruct (Qeq_dec a 0). + rewrite q. + repeat rewrite Qpower_positive_0. + reflexivity. +rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by + (apply Qpower_not_0_positive; assumption). +apply Qdiv_comp;[|reflexivity]. +rewrite Qmult_comm. +rewrite <- Qpower_plus_positive. +rewrite Pplus_minus. +reflexivity. +assumption. +Qed. + +Lemma Qpower_plus : forall a n m, ~a==0 -> a^(n+m) == a^n*a^m. +Proof. +intros a [|n|n] [|m|m] H; simpl; try ring; +try rewrite Qpower_plus_positive; +try apply Qinv_mult_distr; try reflexivity; +case_eq ((n ?= m)%positive Eq); intros H0; simpl; + try rewrite Qpower_minus_positive; + try rewrite (Pcompare_Eq_eq _ _ H0); + try (field; try split; apply Qpower_not_0_positive); + try assumption; + apply ZC2; + assumption. +Qed. + +Lemma Qpower_plus' : forall a n m, (n+m <> 0)%Z -> a^(n+m) == a^n*a^m. +Proof. +intros a n m H. +destruct (Qeq_dec a 0)as [X|X]. +rewrite X. +rewrite Qpower_0 by assumption. +destruct n; destruct m; try (elim H; reflexivity); + simpl; repeat rewrite Qpower_positive_0; ring_simplify; + reflexivity. +apply Qpower_plus. +assumption. +Qed. + +Lemma Qpower_mult_positive : forall a n m, Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m. +Proof. +intros a n m. +induction n using Pind. + reflexivity. +rewrite Pmult_Sn_m. +rewrite Pplus_one_succ_l. +do 2 rewrite Qpower_plus_positive. +rewrite IHn. +rewrite Qmult_power_positive. +reflexivity. +Qed. + +Lemma Qpower_mult : forall a n m, a^(n*m) == (a^n)^m. +Proof. +intros a [|n|n] [|m|m]; simpl; + try rewrite Qpower_positive_1; + try rewrite Qpower_mult_positive; + try rewrite Qinv_power_positive; + try rewrite Qinv_involutive; + try reflexivity. +Qed. + +Lemma Zpower_Qpower : forall (a n:Z), (0<=n)%Z -> inject_Z (a^n) == (inject_Z a)^n. +Proof. +intros a [|n|n] H;[reflexivity| |elim H; reflexivity]. +induction n using Pind. + replace (a^1)%Z with a by ring. + ring. +rewrite Zpos_succ_morphism. +unfold Zsucc. +rewrite Zpower_exp; auto with *; try discriminate. +rewrite Qpower_plus' by discriminate. +rewrite <- IHn by discriminate. +replace (a^'n*a^1)%Z with (a^'n*a)%Z by ring. +ring_simplify. +reflexivity. +Qed. + +Lemma Qsqr_nonneg : forall a, 0 <= a^2. +Proof. +intros a. +destruct (Qlt_le_dec 0 a) as [A|A]. +apply (Qmult_le_0_compat a a); + (apply Qlt_le_weak; assumption). +setoid_replace (a^2) with ((-a)*(-a)) by ring. +rewrite Qle_minus_iff in A. +setoid_replace (0+ - a) with (-a) in A by ring. +apply Qmult_le_0_compat; assumption. +Qed. + +Theorem Qpower_decomp: forall p x y, + Qpower_positive (x #y) p == x ^ Zpos p # (Z2P ((Zpos y) ^ Zpos p)). +Proof. +induction p; intros; unfold Qmult; simpl. +(* xI *) +rewrite IHp, xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l. +repeat rewrite Zpower_pos_is_exp. +red; unfold Qmult, Qnum, Qden, Zpower. +repeat rewrite Zpos_mult_morphism. +repeat rewrite Z2P_correct. +repeat rewrite Zpower_pos_1_r; ring. +apply Zpower_pos_pos; red; auto. +repeat apply Zmult_lt_0_compat; auto; + apply Zpower_pos_pos; red; auto. +(* xO *) +rewrite IHp, <-Pplus_diag. +repeat rewrite Zpower_pos_is_exp. +red; unfold Qmult, Qnum, Qden, Zpower. +repeat rewrite Zpos_mult_morphism. +repeat rewrite Z2P_correct; try ring. +apply Zpower_pos_pos; red; auto. +repeat apply Zmult_lt_0_compat; auto; + apply Zpower_pos_pos; red; auto. +(* xO *) +unfold Qmult; simpl. +red; simpl; rewrite Zpower_pos_1_r; + rewrite Zpos_mult_morphism; ring. +Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 6bd161f3..c98cef3f 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -6,24 +6,20 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qreals.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Qreals.v 10739 2008-04-01 14:45:20Z herbelin $ i*) Require Export Rbase. Require Export QArith_base. -(** A field tactic for rational numbers. *) +(** Injection of rational numbers into real numbers. *) -(** Since field cannot operate on setoid datatypes (yet?), - we translate Q goals into reals before applying field. *) +Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R. Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R. intros; apply not_O_IZR; auto with qarith. Qed. -Hint Immediate IZR_nz. -Hint Resolve Rmult_integral_contrapositive. - -Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R. +Hint Resolve IZR_nz Rmult_integral_contrapositive. Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. Proof. @@ -171,7 +167,7 @@ Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R. unfold Qminus in |- *; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto. Qed. -Lemma Q2R_inv : forall x : Q, ~ x==0#1 -> Q2R (/x) = (/ Q2R x)%R. +Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R. Proof. unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *. case x1. @@ -185,7 +181,7 @@ intros; Qed. Lemma Q2R_div : - forall x y : Q, ~ y==0#1 -> Q2R (x/y) = (Q2R x / Q2R y)%R. + forall x y : Q, ~ y==0 -> Q2R (x/y) = (Q2R x / Q2R y)%R. Proof. unfold Qdiv, Rdiv in |- *. intros; rewrite Q2R_mult. @@ -194,16 +190,24 @@ Qed. Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. +Section LegacyQField. + +(** In the past, the field tactic was not able to deal with setoid datatypes, + so translating from Q to R and applying field on reals was a workaround. + See now Qfield for a direct field tactic on Q. *) + Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto. (** Examples of use: *) -Goal forall x y z : Q, (x+y)*z == (x*z)+(y*z). +Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). intros; QField. -Abort. +Qed. -Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x. +Let ex2 : forall x y : Q, ~ y==0 -> (x/y)*y == x. intros; QField. intro; apply H; apply eqR_Qeq. rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real. -Abort. +Qed. + +End LegacyQField.
\ No newline at end of file diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 340cac83..9c522f09 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 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Qreduction.v 10739 2008-04-01 14:45:20Z herbelin $ i*) (** Normalisation functions for rational numbers. *) @@ -145,6 +145,7 @@ Qed. Definition Qplus' (p q : Q) := Qred (Qplus p q). Definition Qmult' (p q : Q) := Qred (Qmult p q). +Definition Qminus' x y := Qred (Qminus x y). Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q). Proof. @@ -156,6 +157,11 @@ Proof. intros; unfold Qmult' in |- *; apply Qred_correct; auto. Qed. +Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q). +Proof. + intros; unfold Qminus' in |- *; apply Qred_correct; auto. +Qed. + Add Morphism Qplus' : Qplus'_comp. Proof. intros; unfold Qplus' in |- *. @@ -167,3 +173,21 @@ Add Morphism Qmult' : Qmult'_comp. rewrite H; rewrite H0; auto with qarith. Qed. +Add Morphism Qminus' : Qminus'_comp. + intros; unfold Qminus' in |- *. + rewrite H; rewrite H0; auto with qarith. +Qed. + +Lemma Qred_opp: forall q, Qred (-q) = - (Qred q). +Proof. + intros (x, y); unfold Qred; simpl. + rewrite Zggcd_opp; case Zggcd; intros p1 (p2, p3); simpl. + unfold Qopp; auto. +Qed. + +Theorem Qred_compare: forall x y, + Qcompare x y = Qcompare (Qred x) (Qred y). +Proof. + intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. +Qed. + diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index f9aa3e50..2d45d537 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -6,99 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Qring.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) - -Require Export Ring. -Require Export QArith_base. - -(** * A ring tactic for rational numbers *) - -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. -Proof. - intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. - intros _ H; inversion H. -Qed. - -Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. -Proof. - 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. - -Ltac isQcst t := - match t with - | inject_Z ?z => isZcst z - | Qmake ?n ?d => - match isZcst n with - true => isPcst 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. -Qed. - -Let ex2 : forall x y : Q, x+y == y+x. - intros. - ring. -Qed. - -Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z). - intros. - ring. -Qed. - -Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2). - ring. -Qed. - -Let ex5 : 1+1 == 2#1. - ring. -Qed. - -Let ex6 : (1#1)+(1#1) == 2#1. - ring. -Qed. - -Let ex7 : forall x : Q, x-x== 0#1. - intro. - ring. -Qed. - -End Examples. - -Lemma Qopp_plus : forall a b, -(a+b) == -a + -b. -Proof. - intros; ring. -Qed. - -Lemma Qopp_opp : forall q, - -q==q. -Proof. - intros; ring. -Qed. +(*i $Id: Qring.v 10739 2008-04-01 14:45:20Z herbelin $ i*) +Require Export Qfield. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v new file mode 100644 index 00000000..3f191c75 --- /dev/null +++ b/theories/QArith/Qround.v @@ -0,0 +1,139 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +Require Import QArith. + +Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p. +Proof. +intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. +do 2 rewrite <- Zopp_mult_distr_l; omega. +Qed. + +Hint Resolve Qopp_lt_compat : qarith. + +(************) + +Coercion Local inject_Z : Z >-> Q. + +Definition Qfloor (x:Q) := let (n,d) := x in Zdiv n (Zpos d). +Definition Qceiling (x:Q) := (-(Qfloor (-x)))%Z. + +Lemma Qfloor_Z : forall z:Z, Qfloor z = z. +Proof. +intros z. +simpl. +auto with *. +Qed. + +Lemma Qceiling_Z : forall z:Z, Qceiling z = z. +Proof. +intros z. +unfold Qceiling. +simpl. +rewrite Zdiv_1_r. +auto with *. +Qed. + +Lemma Qfloor_le : forall x, Qfloor x <= x. +Proof. +intros [n d]. +simpl. +unfold Qle. +simpl. +replace (n*1)%Z with n by ring. +rewrite Zmult_comm. +apply Z_mult_div_ge. +auto with *. +Qed. + +Hint Resolve Qfloor_le : qarith. + +Lemma Qle_ceiling : forall x, x <= Qceiling x. +Proof. +intros x. +apply Qle_trans with (- - x). + rewrite Qopp_involutive. + auto with *. +change (Qceiling x:Q) with (-(Qfloor(-x))). +auto with *. +Qed. + +Hint Resolve Qle_ceiling : qarith. + +Lemma Qle_floor_ceiling : forall x, Qfloor x <= Qceiling x. +Proof. +eauto with qarith. +Qed. + +Lemma Qlt_floor : forall x, x < (Qfloor x+1)%Z. +Proof. +intros [n d]. +simpl. +unfold Qlt. +simpl. +replace (n*1)%Z with n by ring. +ring_simplify. +replace (n / ' d * ' d + ' d)%Z with + (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring. +rewrite <- Z_div_mod_eq; auto with*. +rewrite <- Zlt_plus_swap. +destruct (Z_mod_lt n ('d)); auto with *. +Qed. + +Hint Resolve Qlt_floor : qarith. + +Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x. +Proof. +intros x. +unfold Qceiling. +replace (- Qfloor (- x) - 1)%Z with (-(Qfloor (-x) + 1))%Z by ring. +change ((- (Qfloor (- x) + 1))%Z:Q) with (-(Qfloor (- x) + 1)%Z). +apply Qlt_le_trans with (- - x); auto with *. +rewrite Qopp_involutive. +auto with *. +Qed. + +Hint Resolve Qceiling_lt : qarith. + +Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z. +Proof. +intros [xn xd] [yn yd] Hxy. +unfold Qle in *. +simpl in *. +rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *. +rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *. +rewrite (Zmult_comm ('yd) ('xd)). +apply Z_div_le; auto with *. +Qed. + +Hint Resolve Qfloor_resp_le : qarith. + +Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z. +Proof. +intros x y Hxy. +unfold Qceiling. +cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *. +Qed. + +Hint Resolve Qceiling_resp_le : qarith. + +Add Morphism Qfloor with signature Qeq ==> @eq _ as Qfloor_comp. +Proof. +intros x y H. +apply Zle_antisym. + auto with *. +symmetry in H; auto with *. +Qed. + +Add Morphism Qceiling with signature Qeq ==> @eq _ as Qceiling_comp. +Proof. +intros x y H. +apply Zle_antisym. + auto with *. +symmetry in H; auto with *. +Qed.
\ No newline at end of file |