aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 11:00:20 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 11:00:20 +0100
commit16f93d201cf7e379d5acf533be20fed30bbc212c (patch)
treea4d1e8ee095c3892f98e80860010f118ab9e8558
parenta4f37da927bc267de505da12f5e5d626af219f90 (diff)
parentf4e46fdf6072727cbfdef42a6db77d5be05d027a (diff)
Merge PR #6155: Get rid of ' notation for Zpos in QArith
-rw-r--r--test-suite/micromega/square.v6
-rw-r--r--theories/QArith/QArith_base.v46
-rw-r--r--theories/QArith/Qabs.v8
-rw-r--r--theories/QArith/Qcanon.v4
-rw-r--r--theories/QArith/Qpower.v4
-rw-r--r--theories/QArith/Qreals.v4
-rw-r--r--theories/QArith/Qreduction.v14
-rw-r--r--theories/QArith/Qround.v12
8 files changed, 48 insertions, 50 deletions
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index abf8be72e..d163dfbcd 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -40,7 +40,7 @@ Proof.
Qed.
-Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z.
+Lemma QdenZpower : forall x : Q, Zpos (Qden (x ^ 2)%Q) = (Zpos (Qden x) ^ 2) %Z.
Proof.
intros.
destruct x.
@@ -54,9 +54,9 @@ Qed.
Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
Proof.
unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq.
- assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
+ assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by
(rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
assert (Hnx : (Qnum x <> 0)%Z)
by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
- apply integer_statement; exists (Qnum x); exists (' Qden x); auto.
+ apply integer_statement; exists (Qnum x); exists (Zpos (Qden x)); auto.
Qed.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 467f263be..35706e7fa 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -227,9 +227,7 @@ Infix "/" := Qdiv : Q_scope.
(** A light notation for [Zpos] *)
-Notation " ' x " := (Zpos x) (at level 20, no associativity) : Z_scope.
-
-Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z ('b).
+Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b).
Proof.
unfold Qeq. simpl. ring.
Qed.
@@ -242,9 +240,9 @@ Proof.
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.
+ replace (p1 * Zpos r2 * Zpos q2) with (p1 * Zpos q2 * Zpos r2) by ring.
rewrite H.
- replace (r1 * 'p2 * 'q2 * 's2) with (r1 * 's2 * 'p2 * 'q2) by ring.
+ replace (r1 * Zpos p2 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * Zpos p2 * Zpos q2) by ring.
rewrite H0.
ring.
Close Scope Z_scope.
@@ -255,7 +253,7 @@ Proof.
unfold Qeq, Qopp; simpl.
Open Scope Z_scope.
intros x y H; simpl.
- replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring.
+ replace (- Qnum x * Zpos (Qden y)) with (- (Qnum x * Zpos (Qden y))) by ring.
rewrite H; ring.
Close Scope Z_scope.
Qed.
@@ -272,9 +270,9 @@ Proof.
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.
+ replace (q1 * s1 * Zpos p2) with (q1 * Zpos p2 * s1) by ring.
rewrite <- H.
- replace (p1 * r1 * 'q2 * 's2) with (r1 * 's2 * p1 * 'q2) by ring.
+ replace (p1 * r1 * Zpos q2 * Zpos s2) with (r1 * Zpos s2 * p1 * Zpos q2) by ring.
rewrite H0.
ring.
Close Scope Z_scope.
@@ -305,13 +303,13 @@ Proof.
unfold Qeq, Qcompare.
Open Scope Z_scope.
intros (p1,p2) (q1,q2) H (r1,r2) (s1,s2) H'; simpl in *.
- rewrite <- (Zcompare_mult_compat (q2*s2) (p1*'r2)).
- rewrite <- (Zcompare_mult_compat (p2*r2) (q1*'s2)).
- change ('(q2*s2)) with ('q2 * 's2).
- change ('(p2*r2)) with ('p2 * 'r2).
- replace ('q2 * 's2 * (p1*'r2)) with ((p1*'q2)*'r2*'s2) by ring.
+ rewrite <- (Zcompare_mult_compat (q2*s2) (p1*Zpos r2)).
+ rewrite <- (Zcompare_mult_compat (p2*r2) (q1*Zpos s2)).
+ change (Zpos (q2*s2)) with (Zpos q2 * Zpos s2).
+ change (Zpos (p2*r2)) with (Zpos p2 * Zpos r2).
+ replace (Zpos q2 * Zpos s2 * (p1*Zpos r2)) with ((p1*Zpos q2)*Zpos r2*Zpos s2) by ring.
rewrite H.
- replace ('q2 * 's2 * (r1*'p2)) with ((r1*'s2)*'q2*'p2) by ring.
+ replace (Zpos q2 * Zpos s2 * (r1*Zpos p2)) with ((r1*Zpos s2)*Zpos q2*Zpos p2) by ring.
rewrite H'.
f_equal; ring.
Close Scope Z_scope.
@@ -572,8 +570,8 @@ 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 Z.mul_le_mono_pos_r with ('y2); [easy|].
- apply Z.le_trans with (y1 * 'x2 * 'z2).
+ apply Z.mul_le_mono_pos_r with (Zpos y2); [easy|].
+ apply Z.le_trans with (y1 * Zpos x2 * Zpos z2).
- rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
- rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
now apply Z.mul_le_mono_pos_r.
@@ -620,8 +618,8 @@ 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 Z.mul_lt_mono_pos_r with ('y2); [easy|].
- apply Z.le_lt_trans with (y1 * 'x2 * 'z2).
+ apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].
+ apply Z.le_lt_trans with (y1 * Zpos x2 * Zpos z2).
- rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r.
- rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
now apply Z.mul_lt_mono_pos_r.
@@ -632,8 +630,8 @@ 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 Z.mul_lt_mono_pos_r with ('y2); [easy|].
- apply Z.lt_le_trans with (y1 * 'x2 * 'z2).
+ apply Z.mul_lt_mono_pos_r with (Zpos y2); [easy|].
+ apply Z.lt_le_trans with (y1 * Zpos x2 * Zpos z2).
- rewrite Z.mul_shuffle0. now apply Z.mul_lt_mono_pos_r.
- rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1).
now apply Z.mul_le_mono_pos_r.
@@ -723,9 +721,9 @@ Proof.
match goal with |- ?a <= ?b => ring_simplify a b end.
rewrite Z.add_comm.
apply Z.add_le_mono.
- match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+ match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.
auto with zarith.
- match goal with |- ?a <= ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+ match goal with |- ?a <= ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.
auto with zarith.
Close Scope Z_scope.
Qed.
@@ -740,9 +738,9 @@ Proof.
match goal with |- ?a < ?b => ring_simplify a b end.
rewrite Z.add_comm.
apply Z.add_le_lt_mono.
- match goal with |- ?a <= ?b => ring_simplify z1 t1 ('z2) ('t2) a b end.
+ match goal with |- ?a <= ?b => ring_simplify z1 t1 (Zpos z2) (Zpos t2) a b end.
auto with zarith.
- match goal with |- ?a < ?b => ring_simplify x1 y1 ('x2) ('y2) a b end.
+ match goal with |- ?a < ?b => ring_simplify x1 y1 (Zpos x2) (Zpos y2) a b end.
do 2 (apply Z.mul_lt_mono_pos_r;try easy).
Close Scope Z_scope.
Qed.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 48be89417..31eb41bc9 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -28,8 +28,8 @@ intros [xn xd] [yn yd] H.
simpl.
unfold Qeq in *.
simpl in *.
-change (' yd)%Z with (Z.abs (' yd)).
-change (' xd)%Z with (Z.abs (' xd)).
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
repeat rewrite <- Z.abs_mul.
congruence.
Qed.
@@ -88,8 +88,8 @@ unfold Qplus.
unfold Qle.
simpl.
apply Z.mul_le_mono_nonneg_r;auto with *.
-change (' yd)%Z with (Z.abs (' yd)).
-change (' xd)%Z with (Z.abs (' xd)).
+change (Zpos yd)%Z with (Z.abs (Zpos yd)).
+change (Zpos xd)%Z with (Z.abs (Zpos xd)).
repeat rewrite <- Z.abs_mul.
apply Z.abs_triangle.
Qed.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index e25f69c31..1510a7b82 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -30,7 +30,7 @@ Lemma Qred_identity :
Proof.
intros (a,b) H; simpl in *.
rewrite <- Z.ggcd_gcd in H.
- generalize (Z.ggcd_correct_divisors a ('b)).
+ generalize (Z.ggcd_correct_divisors a (Zpos b)).
destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst.
rewrite !Z.mul_1_l. now intros (<-,<-).
Qed.
@@ -39,7 +39,7 @@ Lemma Qred_identity2 :
forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.
Proof.
intros (a,b) H; simpl in *.
- generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+ generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
rewrite <- Z.ggcd_gcd.
destruct Z.ggcd as (g,(aa,bb)); simpl in *.
injection H as <- <-. intros H (_,H').
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 3fd78f092..010782209 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -90,7 +90,7 @@ rewrite Qinv_power.
reflexivity.
Qed.
-Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z ('p))^n.
+Lemma Qinv_power_n : forall n p, (1#p)^n == /(inject_Z (Zpos p))^n.
Proof.
intros n p.
rewrite Qmake_Qdiv.
@@ -190,7 +190,7 @@ unfold Z.succ.
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.
+replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring.
ring_simplify.
reflexivity.
Qed.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 14ab1700e..c83296259 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -167,8 +167,8 @@ unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden.
simpl; intros; elim H; trivial.
intros; field; auto.
intros;
- change (IZR (Zneg x2)) with (- IZR (' x2))%R;
- change (IZR (Zneg p)) with (- IZR (' p))%R;
+ change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R;
+ change (IZR (Zneg p)) with (- IZR (Zpos p))%R;
simpl; field; (*auto 8 with real.*)
repeat split; auto; auto with real.
Qed.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 7b08515d2..17307c827 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -21,14 +21,14 @@ Notation Z2P_correct := Z2Pos.id (only parsing).
Definition Qred (q:Q) :=
let (q1,q2) := q in
- let (r1,r2) := snd (Z.ggcd q1 ('q2))
+ let (r1,r2) := snd (Z.ggcd q1 (Zpos q2))
in r1#(Z.to_pos r2).
Lemma Qred_correct : forall q, (Qred q) == q.
Proof.
unfold Qred, Qeq; intros (n,d); simpl.
- generalize (Z.ggcd_gcd n ('d)) (Z.gcd_nonneg n ('d))
- (Z.ggcd_correct_divisors n ('d)).
+ generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d))
+ (Z.ggcd_correct_divisors n (Zpos d)).
destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl.
Open Scope Z_scope.
intros Hg LE (Hn,Hd). rewrite Hd, Hn.
@@ -45,13 +45,13 @@ Proof.
unfold Qred, Qeq in *; simpl in *.
Open Scope Z_scope.
intros H.
- generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
- (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+ generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b))
+ (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)).
simpl. intros <- Hg1 Hg2 (Hg3,Hg4).
assert (Hg0 : g <> 0) by (intro; now subst g).
- generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
- (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)).
+ generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d))
+ (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)).
destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)).
simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4).
assert (Hg'0 : g' <> 0) by (intro; now subst g').
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index e4e974972..7c5ddbb6a 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -80,11 +80,11 @@ 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.
+replace (n / Zpos d * Zpos d + Zpos d)%Z with
+ ((Zpos d * (n / Zpos d) + n mod Zpos d) + Zpos d - n mod Zpos d)%Z by ring.
rewrite <- Z_div_mod_eq; auto with*.
rewrite <- Z.lt_add_lt_sub_r.
-destruct (Z_mod_lt n ('d)); auto with *.
+destruct (Z_mod_lt n (Zpos d)); auto with *.
Qed.
Hint Resolve Qlt_floor : qarith.
@@ -107,9 +107,9 @@ 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 (Z.mul_comm ('yd) ('xd)).
+rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *.
+rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *.
+rewrite (Z.mul_comm (Zpos yd) (Zpos xd)).
apply Z_div_le; auto with *.
Qed.