From 1d12b302120fbde8cbd7f8a3c36bf144a3e1e531 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 31 May 2006 21:56:37 +0000 Subject: ajout de QArith dans les theories standards git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8883 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend.coq | 11 +- Makefile | 12 +- theories/QArith/QArith.v | 13 + theories/QArith/QArith_base.v | 621 ++++++++++++++++++++++++++++++++++++++++++ theories/QArith/Qreals.v | 213 +++++++++++++++ theories/QArith/Qreduction.v | 265 ++++++++++++++++++ theories/QArith/Qring.v | 91 +++++++ theories/ZArith/BinInt.v | 10 +- 8 files changed, 1229 insertions(+), 7 deletions(-) create mode 100644 theories/QArith/QArith.v create mode 100644 theories/QArith/QArith_base.v create mode 100644 theories/QArith/Qreals.v create mode 100644 theories/QArith/Qreduction.v create mode 100644 theories/QArith/Qring.v diff --git a/.depend.coq b/.depend.coq index d6babae105..caa85a2c69 100644 --- a/.depend.coq +++ b/.depend.coq @@ -280,6 +280,11 @@ theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relatio theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/PermutSetoid.vo: theories/Sorting/PermutSetoid.v contrib/omega/Omega.vo theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Lists/SetoidList.vo theories/Sorting/PermutEq.vo: theories/Sorting/PermutEq.v contrib/omega/Omega.vo theories/Relations/Relations.vo theories/Setoids/Setoid.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo +theories/QArith/QArith_base.vo: theories/QArith/QArith_base.v theories/ZArith/ZArith.vo contrib/ring/ZArithRing.vo theories/Setoids/Setoid.vo +theories/QArith/Qreduction.vo: theories/QArith/Qreduction.v theories/QArith/QArith_base.vo theories/ZArith/Znumtheory.vo +theories/QArith/Qring.vo: theories/QArith/Qring.v contrib/ring/Ring.vo contrib/ring/Setoid_ring.vo theories/QArith/QArith_base.vo +theories/QArith/Qreals.vo: theories/QArith/Qreals.v theories/Reals/Rbase.vo theories/QArith/QArith_base.vo +theories/QArith/QArith.vo: theories/QArith/QArith.v theories/QArith/QArith_base.vo theories/QArith/Qring.vo theories/QArith/Qreduction.vo contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/Logic/Decidable.vo @@ -295,9 +300,9 @@ contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/Setoid_ring_normalize.vo: contrib/ring/Setoid_ring_normalize.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring.vo: contrib/ring/Setoid_ring.v contrib/ring/Setoid_ring_theory.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo contrib/ring/Setoid_ring_theory.vo: contrib/ring/Setoid_ring_theory.v theories/Bool/Bool.vo theories/Setoids/Setoid.vo -contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v -contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo -contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo +contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v theories/Lists/List.vo +contrib/field/Field_Theory.vo: contrib/field/Field_Theory.v theories/Lists/List.vo theories/Arith/Peano_dec.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo +contrib/field/Field_Tactic.vo: contrib/field/Field_Tactic.v theories/Lists/List.vo contrib/ring/Ring.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/Field.vo theories/Reals/DiscrR.vo diff --git a/Makefile b/Makefile index fe8d729084..526fdf1e53 100644 --- a/Makefile +++ b/Makefile @@ -869,6 +869,11 @@ ZARITHVO=\ theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \ theories/ZArith/Znumtheory.vo +QARITHVO=\ + theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \ + theories/QArith/Qring.vo theories/QArith/Qreals.vo \ + theories/QArith/QArith.vo + LISTSVO=\ theories/Lists/MonoList.vo \ theories/Lists/ListSet.vo theories/Lists/Streams.vo \ @@ -989,7 +994,7 @@ SETOIDSVO=theories/Setoids/Setoid.vo THEORIESVO =\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(INTMAPVO) \ - $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) + $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) THEORIESLIGHTVO = $(INITVO) $(LOGICVO) $(ARITHVO) @@ -1001,6 +1006,7 @@ arith: $(ARITHVO) bool: $(BOOLVO) narith: $(NARITHVO) zarith: $(ZARITHVO) +qarith: $(QARITHVO) lists: $(LISTSVO) strings: $(STRINGSVO) sets: $(SETSVO) @@ -1015,8 +1021,8 @@ allreals: $(ALLREALS) setoids: $(SETOIDSVO) sorting: $(SORTINGVO) -noreal: logic arith bool zarith lists sets fsets intmap relations wellfounded \ - setoids sorting +noreal: logic arith bool zarith qarith lists sets fsets intmap relations \ + wellfounded setoids sorting ########################################################################### # contribs (interface not included) diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v new file mode 100644 index 0000000000..f7a28598ee --- /dev/null +++ b/theories/QArith/QArith.v @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Qlt y x). +Notation Qge := (fun x y : Q => Qle y x). + +Infix "==" := Qeq (at level 70, no associativity) : Q_scope. +Infix "<" := Qlt : Q_scope. +Infix "<=" := Qle : Q_scope. +Infix ">" := Qgt : Q_scope. +Infix ">=" := Qge : Q_scope. +Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. + +Hint Unfold Qeq Qle Qlt: qarith. +Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith. + +(** Properties of equality. *) + +Theorem Qeq_refl : forall x, x == x. +Proof. + auto with qarith. +Qed. + +Theorem Qeq_sym : forall x y, x == y -> y == x. +Proof. + auto with qarith. +Qed. + +Theorem Qeq_trans : forall x y z, x == y -> y == z -> x == z. +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. +Qed. + +(** Furthermore, this equality is decidable: *) + +Theorem Qeq_dec : forall x y, {x==y} + {~ x==y}. +Proof. + intros; case (Z_eq_dec (Qnum x * QDen y) (Qnum y * QDen x)); auto. +Defined. + +(** We now consider [Q] seen as a setoid. *) + +Definition Q_Setoid : Setoid_Theory Q Qeq. +Proof. + split; unfold Qeq in |- *; auto; apply Qeq_trans. +Qed. + +Add Setoid Q Qeq Q_Setoid as Qsetoid. + +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. + +(** The addition, multiplication and opposite are defined + in the straightforward way: *) + +Definition Qplus (x y : Q) := + (Qnum x * QDen y + Qnum y * QDen x) # (Qden x * Qden y). + +Definition Qmult (x y : Q) := (Qnum x * Qnum y) # (Qden x * Qden y). + +Definition Qopp (x : Q) := (- Qnum x) # (Qden x). + +Definition Qminus (x y : Q) := Qplus x (Qopp y). + +Definition Qinv (x : Q) := + match Qnum x with + | Z0 => 0 + | Zpos p => (QDen x)#p + | Zneg p => (Zneg (Qden x))#p + end. + +Definition Qdiv (x y : Q) := Qmult x (Qinv y). + +Infix "+" := Qplus : Q_scope. +Notation "- x" := (Qopp x) : Q_scope. +Infix "-" := Qminus : Q_scope. +Infix "*" := Qmult : Q_scope. +Notation "/ x" := (Qinv x) : Q_scope. +Infix "/" := Qdiv : Q_scope. + +(** A light notation for [Zpos] *) + +Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope. + +(** 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. +Qed. + +Add Morphism Qopp : Qopp_comp. +Proof. +unfold Qeq, Qopp; simpl. +intros; ring; rewrite H; ring. +Qed. + +Add Morphism Qminus : Qminus_comp. +Proof. +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. +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. +Qed. + +Add Morphism Qdiv : Qdiv_comp. +Proof. +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. +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 x2 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. +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. +Qed. + +(** 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. +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. +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. +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. +Qed. + +(** Properties of order upon Q. *) + +Lemma Qle_refl : forall x, x<=x. +Proof. +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. +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. +Qed. + +Lemma Qlt_not_eq : forall x y, x ~ x==y. +Proof. +unfold Qlt, Qeq; auto with zarith. +Qed. + +(** Large = strict or equal *) + +Lemma Qlt_le_weak : forall x y, x x<=y. +Proof. +unfold Qle, Qlt; auto with zarith. +Qed. + +Lemma Qle_lt_trans : forall x y z, x<=y -> y x y<=z -> x y x y<=x. +Proof. +unfold Qle, Qlt; auto with zarith. +Qed. + +Lemma Qnot_le_lt : forall x y, ~ x<=y -> y ~ y<=x. +Proof. +unfold Qle, Qlt; auto with zarith. +Qed. + +Lemma Qle_not_lt : forall x y, x<=y -> ~ y x -q <= -p. +Proof. +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. +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. +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. +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. +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. +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. +Qed. + +(** 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. + +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. +Qed. + +Lemma Qpower_0 : forall n, n<>O -> 0^n == 0. +Proof. +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. +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. +Qed. + + diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v new file mode 100644 index 0000000000..e4b22dd565 --- /dev/null +++ b/theories/QArith/Qreals.v @@ -0,0 +1,213 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. + +Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. +Proof. +unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; + intros. +apply eq_IZR. +do 2 rewrite mult_IZR. +set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); + set (X2 := IZR (Zpos x2)) in *. +set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); + set (Y2 := IZR (Zpos y2)) in *. +assert ((X2 * X1 * / X2)%R = (X2 * (Y1 * / Y2))%R). +rewrite <- H; field; auto. +rewrite Rinv_r_simpl_m in H0; auto; rewrite H0; field; auto. +Qed. + +Lemma Qeq_eqR : forall x y : Q, x==y -> Q2R x = Q2R y. +Proof. +unfold Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; + intros. +set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); + set (X2 := IZR (Zpos x2)) in *. +set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); + set (Y2 := IZR (Zpos y2)) in *. +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. +Qed. + +Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y. +Proof. +unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; + intros. +apply le_IZR. +do 2 rewrite mult_IZR. +set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); + set (X2 := IZR (Zpos x2)) in *. +set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); + set (Y2 := IZR (Zpos y2)) in *. +replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). +replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). +apply Rmult_le_compat_r; auto. +apply Rmult_le_pos. +unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le; + auto with zarith. +unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_le; + auto with zarith. +Qed. + +Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R. +Proof. +unfold Qle, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; + intros. +set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); + set (X2 := IZR (Zpos x2)) in *. +set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); + set (Y2 := IZR (Zpos y2)) in *. +assert (X1 * Y2 <= Y1 * X2)%R. + unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + apply IZR_le; auto. +clear H. +replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). +replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). +apply Rmult_le_compat_r; auto. +apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat. +unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; + auto with zarith. +unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; + auto with zarith. +Qed. + +Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x (Q2R x < Q2R y)%R. +Proof. +unfold Qlt, Q2R in |- *; intros (x1, x2) (y1, y2); unfold Qnum, Qden in |- *; + intros. +set (X1 := IZR x1) in *; assert (X2nz := IZR_nz x2); + set (X2 := IZR (Zpos x2)) in *. +set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); + set (Y2 := IZR (Zpos y2)) in *. +assert (X1 * Y2 < Y1 * X2)%R. + unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR. + apply IZR_lt; auto. +clear H. +replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). +replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). +apply Rmult_lt_compat_r; auto. +apply Rmult_lt_0_compat; apply Rinv_0_lt_compat. +unfold X2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; + auto with zarith. +unfold Y2 in |- *; replace 0%R with (IZR 0); auto; apply IZR_lt; red in |- *; + auto with zarith. +Qed. + +Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R. +Proof. +unfold Qplus, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); + unfold Qden, Qnum in |- *. +simpl_mult. +rewrite plus_IZR. +do 3 rewrite mult_IZR. +field; auto. +Qed. + +Lemma Q2R_mult : forall x y : Q, Q2R (x*y) = (Q2R x * Q2R y)%R. +Proof. +unfold Qmult, Qeq, Q2R in |- *; intros (x1, x2) (y1, y2); + unfold Qden, Qnum in |- *. +simpl_mult. +do 2 rewrite mult_IZR. +field; auto. +Qed. + +Lemma Q2R_opp : forall x : Q, Q2R (- x) = (- Q2R x)%R. +Proof. +unfold Qopp, Qeq, Q2R in |- *; intros (x1, x2); unfold Qden, Qnum in |- *. +rewrite Ropp_Ropp_IZR. +field; auto. +Qed. + +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. +Proof. +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. +Qed. + +Lemma Q2R_div : + forall x y : Q, ~ y==0#1 -> Q2R (x/y) = (Q2R x / Q2R y)%R. +Proof. +unfold Qdiv, Rdiv in |- *. +intros; rewrite Q2R_mult. +rewrite Q2R_inv; auto. +Qed. + +Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. + +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). +intros; QField. +Abort. + +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 diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v new file mode 100644 index 0000000000..b818f744ff --- /dev/null +++ b/theories/QArith/Qreduction.v @@ -0,0 +1,265 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 1%positive + | Zpos p => p + | Zneg p => p + end. + +Lemma Z2P_correct : forall z : Z, (0 < z)%Z -> Zpos (Z2P z) = z. +Proof. + simple destruct z; simpl in |- *; auto; intros; discriminate. +Qed. + +Lemma Z2P_correct2 : forall z : Z, 0%Z <> z -> Zpos (Z2P z) = Zabs z. +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). + +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. +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). + apply Zmult_gt_0_lt_0_reg_r with g. + omega. + rewrite Zmult_comm. + rewrite <- H4; compute; auto. +rewrite Z2P_correct; auto. +ring. +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 *. +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). + 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 (00). + 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). + +Lemma Qplus'_correct : forall p q : Q, (Qplus' p q)==(Qplus p q). +Proof. +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. +Qed. + +Add Morphism Qplus' : Qplus'_comp. +Proof. +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. +Qed. + diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v new file mode 100644 index 0000000000..84a9684752 --- /dev/null +++ b/theories/QArith/Qring.v @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* x==y. +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. +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. +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 ]. + +(** 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. + diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 16e2ff3256..9cf3944683 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -9,7 +9,7 @@ (*i $Id$ i*) (***********************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (***********************************************************) Require Export BinPos. @@ -703,6 +703,12 @@ Qed. (**********************************************************************) (** Properties of multiplication on binary integer numbers *) +Theorem Zpos_mult_morphism : + forall p q:positive, Zpos (p*q) = Zpos p * Zpos q. +Proof. +auto. +Qed. + (** One is neutral for multiplication *) Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n. @@ -935,6 +941,8 @@ Proof. intros; symmetry in |- *; apply Zmult_succ_l. Qed. + + (** Misc redundant properties *) Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0. -- cgit v1.2.3