summaryrefslogtreecommitdiff
path: root/theories/QArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/QArith')
-rw-r--r--theories/QArith/QArith.v2
-rw-r--r--theories/QArith/QArith_base.v6
-rw-r--r--theories/QArith/QOrderedType.v2
-rw-r--r--theories/QArith/Qabs.v2
-rw-r--r--theories/QArith/Qcanon.v24
-rw-r--r--theories/QArith/Qfield.v2
-rw-r--r--theories/QArith/Qminmax.v2
-rw-r--r--theories/QArith/Qpower.v3
-rw-r--r--theories/QArith/Qreals.v33
-rw-r--r--theories/QArith/Qreduction.v4
-rw-r--r--theories/QArith/Qring.v2
-rw-r--r--theories/QArith/Qround.v2
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 17:06:17 +0000