diff options
Diffstat (limited to 'theories/QArith')
-rw-r--r-- | theories/QArith/QArith.v | 2 | ||||
-rw-r--r-- | theories/QArith/QArith_base.v | 6 | ||||
-rw-r--r-- | theories/QArith/QOrderedType.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qabs.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qcanon.v | 24 | ||||
-rw-r--r-- | theories/QArith/Qfield.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qminmax.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qpower.v | 3 | ||||
-rw-r--r-- | theories/QArith/Qreals.v | 33 | ||||
-rw-r--r-- | theories/QArith/Qreduction.v | 4 | ||||
-rw-r--r-- | theories/QArith/Qring.v | 2 | ||||
-rw-r--r-- | theories/QArith/Qround.v | 2 |
12 files changed, 33 insertions, 51 deletions
diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v index 1a76d7e1..c32fb950 100644 --- a/theories/QArith/QArith.v +++ b/theories/QArith/QArith.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 080d00d4..7f19b4ce 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -925,8 +925,8 @@ Qed. (** * Rational to the n-th power *) -Definition Qpower_positive (q:Q)(p:positive) : Q := - pow_pos Qmult q p. +Definition Qpower_positive : Q -> positive -> Q := + pow_pos Qmult. Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive. Proof. diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v index dc820e75..fa0b9209 100644 --- a/theories/QArith/QOrderedType.v +++ b/theories/QArith/QOrderedType.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 9b607f1b..f77f409e 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index a865a6cf..f7f83bf0 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -70,7 +70,6 @@ Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). Arguments Q2Qc q%Q. -Notation " !! " := Q2Qc : Qc_scope. Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. Proof. @@ -87,8 +86,8 @@ Proof. Qed. Hint Resolve Qc_is_canon. -Notation " 0 " := (!!0) : Qc_scope. -Notation " 1 " := (!!1) : Qc_scope. +Notation " 0 " := (Q2Qc 0) : Qc_scope. +Notation " 1 " := (Q2Qc 1) : Qc_scope. Definition Qcle (x y : Qc) := (x <= y)%Q. Definition Qclt (x y : Qc) := (x < y)%Q. @@ -144,15 +143,15 @@ Defined. (** The addition, multiplication and opposite are defined in the straightforward way: *) -Definition Qcplus (x y : Qc) := !!(x+y). +Definition Qcplus (x y : Qc) := Q2Qc (x+y). Infix "+" := Qcplus : Qc_scope. -Definition Qcmult (x y : Qc) := !!(x*y). +Definition Qcmult (x y : Qc) := Q2Qc (x*y). Infix "*" := Qcmult : Qc_scope. -Definition Qcopp (x : Qc) := !!(-x). +Definition Qcopp (x : Qc) := Q2Qc (-x). Notation "- x" := (Qcopp x) : Qc_scope. Definition Qcminus (x y : Qc) := x+-y. Infix "-" := Qcminus : Qc_scope. -Definition Qcinv (x : Qc) := !!(/x). +Definition Qcinv (x : Qc) := Q2Qc (/x). Notation "/ x" := (Qcinv x) : Qc_scope. Definition Qcdiv (x y : Qc) := x*/y. Infix "/" := Qcdiv : Qc_scope. @@ -434,14 +433,14 @@ 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 * |-. + 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 *. + rewrite !Qred_correct in *. eapply Qmult_lt_compat_r; eauto. Qed. @@ -460,13 +459,13 @@ Proof. induction n; simpl; auto with qarith. rewrite IHn; auto with qarith. Qed. - +Transparent Qred. Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0. Proof. destruct n; simpl. destruct 1; auto. intros. - now apply Qc_is_canon. + now apply Qc_is_canon. Qed. Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n. @@ -521,6 +520,7 @@ Add Field Qcfield : Qcft. (** A field tactic for rational numbers *) Example test_field : (forall x y : Qc, y<>0 -> (x/y)*y = x)%Qc. +Proof. intros. field. auto. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index a1028ad9..083e40ae 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v index 9a5a1cb1..0fd05325 100644 --- a/theories/QArith/Qminmax.v +++ b/theories/QArith/Qminmax.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 112b3738..8bd643aa 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -41,6 +41,7 @@ try destruct (Qmult_integral _ _ H0); auto. Qed. Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n. +Proof. intros p n Hp. induction n; simpl; repeat apply Qmult_le_0_compat;assumption. Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 029ae8e3..add43b96 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,6 +14,7 @@ Require Export QArith_base. Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R. Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R. +Proof. intros; apply not_O_IZR; auto with qarith. Qed. @@ -162,19 +163,19 @@ field; auto. Qed. Lemma Q2R_minus : forall x y : Q, Q2R (x-y) = (Q2R x - Q2R y)%R. +Proof. unfold Qminus; intros; rewrite Q2R_plus; rewrite Q2R_opp; auto. Qed. Lemma Q2R_inv : forall x : Q, ~ x==0 -> Q2R (/x) = (/ Q2R x)%R. Proof. -unfold Qinv, Q2R, Qeq; intros (x1, x2); unfold Qden, Qnum. -case x1. +unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden. simpl; intros; elim H; trivial. -intros; field; auto. +intros; field; auto. intros; change (IZR (Zneg x2)) with (- IZR (' x2))%R; change (IZR (Zneg p)) with (- IZR (' p))%R; - field; (*auto 8 with real.*) + simpl; field; (*auto 8 with real.*) repeat split; auto; auto with real. Qed. @@ -187,25 +188,3 @@ rewrite Q2R_inv; auto. 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: *) - -Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). -intros; QField. -Qed. - -Let ex2 : forall x y : Q, ~ y==0 -> (x/y)*y == x. -intros; QField. -intro; apply H; apply eqR_Qeq. -rewrite H0; unfold Q2R; simpl; field; auto with real. -Qed. - -End LegacyQField. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index e8ccdee0..1d304964 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -126,11 +126,13 @@ Proof. Qed. Add Morphism Qmult' : Qmult'_comp. +Proof. intros; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qminus' : Qminus'_comp. +Proof. intros; unfold Qminus'. rewrite H, H0; auto with qarith. Qed. diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 9a76bed7..78c464ae 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index ed3d38b1..964a4bae 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |