From f02a1fdf03f7cd4c99776957ccfefa0e6db1bc94 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 10 Oct 2019 12:31:44 +0000 Subject: QArith_base: do not use “omega” --- theories/QArith/QArith_base.v | 65 +++++++++++++++++++------------------------ 1 file changed, 29 insertions(+), 36 deletions(-) diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index b60feb9256..54d35cded2 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -79,7 +79,7 @@ Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b. Proof. - unfold Qeq. simpl. omega. + unfold Qeq; simpl; rewrite !Z.mul_1_r; reflexivity. Qed. (** Another approach : using Qcompare for defining order relations. *) @@ -599,9 +599,7 @@ Proof. Qed. Lemma Qle_antisym x y : x<=y -> y<=x -> x==y. -Proof. - unfold Qle, Qeq; auto with zarith. -Qed. +Proof. apply Z.le_antisymm. Qed. Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. @@ -618,14 +616,10 @@ Qed. Hint Resolve Qle_trans : qarith. Lemma Qlt_irrefl x : ~x ~ x==y. -Proof. - unfold Qlt, Qeq; auto with zarith. -Qed. +Proof. apply Z.lt_neq. Qed. Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y). Proof. @@ -647,9 +641,7 @@ Proof. Qed. Lemma Qlt_le_weak x y : x x<=y. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Proof. apply Z.lt_le_incl. Qed. Lemma Qle_lt_trans : forall x y z, x<=y -> y x y<=x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qnot_lt_le x y : ~ x < y -> y <= x. +Proof. apply Z.nlt_ge. Qed. -Lemma Qnot_le_lt : forall x y, ~ x<=y -> y y < x. +Proof. apply Z.nle_gt. Qed. -Lemma Qlt_not_le : forall x y, x ~ y<=x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qlt_not_le x y : x < y -> ~ y <= x. +Proof. apply Z.lt_nge. Qed. -Lemma Qle_not_lt : forall x y, x<=y -> ~ y ~ y < x. +Proof. apply Z.le_ngt. Qed. Lemma Qle_lt_or_eq : forall x y, x<=y -> x -q <= -p. Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. - rewrite !Z.mul_opp_l. omega. + now rewrite !Z.mul_opp_l, <- Z.opp_le_mono. 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. - rewrite Z.mul_opp_l. omega. + rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.le_sub_le_add_r, Z.opp_involutive. + reflexivity. Qed. Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p. Proof. intros (x1,x2) (y1,y2); unfold Qlt; simpl. - rewrite Z.mul_opp_l. omega. + rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.lt_sub_lt_add_r, Z.opp_involutive. + reflexivity. Qed. Lemma Qplus_le_compat : @@ -831,9 +818,11 @@ 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. + rewrite Z.mul_1_r. intros; simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). - apply Z.mul_le_mono_nonneg_r; auto with zarith. + apply Z.mul_le_mono_nonneg_r; auto. + now apply Z.mul_nonneg_nonneg. Close Scope Z_scope. Qed. @@ -843,9 +832,10 @@ Proof. Open Scope Z_scope. simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + rewrite Z.mul_1_r. intros LT LE. apply Z.mul_le_mono_pos_r in LE; trivial. - apply Z.mul_pos_pos; [omega|easy]. + apply Z.mul_pos_pos; easy. Close Scope Z_scope. Qed. @@ -866,10 +856,11 @@ 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. + rewrite Z.mul_1_r. intros; simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). apply Z.mul_lt_mono_pos_r; auto with zarith. - apply Z.mul_pos_pos; [omega|reflexivity]. + apply Z.mul_pos_pos; easy. Close Scope Z_scope. Qed. @@ -880,8 +871,9 @@ Proof. unfold Qle, Qlt; simpl. simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + rewrite Z.mul_1_r. intro LT. rewrite <- Z.mul_lt_mono_pos_r. reflexivity. - apply Z.mul_pos_pos; [omega|reflexivity]. + now apply Z.mul_pos_pos. Close Scope Z_scope. Qed. @@ -896,6 +888,7 @@ Proof. intros a b Ha Hb. unfold Qle in *. simpl in *. +rewrite Z.mul_1_r in *. auto with *. Qed. -- cgit v1.2.3