From 2b4c3fff22d7e9c55289c2fe770e744b7a5f613c Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 4 Jul 2008 16:02:24 +0000 Subject: Fix bug #1899: no more strange notations for Qge and Qgt In fact, Qge and Ggt disappear, and we only leave notations for > and >= that map directly to Qlt and Qle. We also adopt the same approach for BigN, BigZ, BigQ. By the way, various clean-up concerning Zeq_bool, Zle_bool and similar functions for Q. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/micromega/QMicromega.v | 72 ++--------------- contrib/micromega/RMicromega.v | 4 +- contrib/micromega/ZMicromega.v | 11 +-- contrib/setoid_ring/InitialRing.v | 10 +-- contrib/setoid_ring/ZArithRing.v | 2 +- theories/Numbers/Integer/BigZ/BigZ.v | 14 ++-- theories/Numbers/Natural/BigN/BigN.v | 4 +- theories/Numbers/Rational/BigQ/BigQ.v | 26 +++--- theories/Numbers/Rational/BigQ/QMake.v | 9 --- theories/QArith/QArith_base.v | 139 +++++++++++++++++++++++---------- theories/QArith/Qfield.v | 27 +++---- theories/ZArith/Zbool.v | 87 +++++++++++++-------- theories/ZArith/Zcompare.v | 9 +++ 13 files changed, 208 insertions(+), 206 deletions(-) diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v index 9e95f6c49..c054f218a 100644 --- a/contrib/micromega/QMicromega.v +++ b/contrib/micromega/QMicromega.v @@ -16,38 +16,11 @@ Require Import OrderedRing. Require Import RingMicromega. Require Import Refl. Require Import QArith. -Require Import Qring. - -(* Qsrt has been removed from the library ? *) -Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. -Proof. - constructor. - exact Qplus_0_l. - exact Qplus_comm. - exact Qplus_assoc. - exact Qmult_1_l. - exact Qmult_comm. - exact Qmult_assoc. - exact Qmult_plus_distr_l. - reflexivity. - exact Qplus_opp_r. -Qed. - - -Add Ring Qring : Qsrt. - -Lemma Qmult_neutral : forall x , 0 * x == 0. -Proof. - intros. - compute. - reflexivity. -Qed. - -(* Is there any qarith database ? *) +Require Import Qfield. Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt. Proof. - constructor; intros ; subst ; try (intuition (subst; auto with qarith)). + constructor; intros ; subst ; try (intuition (subst; auto with qarith)). apply Q_Setoid. rewrite H ; rewrite H0 ; reflexivity. rewrite H ; rewrite H0 ; reflexivity. @@ -67,45 +40,12 @@ Proof. destruct(Q_dec n m) as [[H1 |H1] | H1 ] ; tauto. apply (Qplus_le_compat p p n m (Qle_refl p) H). generalize (Qmult_lt_compat_r 0 n m H0 H). - rewrite Qmult_neutral. + rewrite Qmult_0_l. auto. compute in H. discriminate. Qed. -Definition Qeq_bool (p q : Q) : bool := Zeq_bool (Qnum p * ' Qden q)%Z (Qnum q * ' Qden p)%Z. - -Definition Qle_bool (x y : Q) : bool := Zle_bool (Qnum x * ' Qden y)%Z (Qnum y * ' Qden x)%Z. - -Require ZMicromega. - -Lemma Qeq_bool_ok : forall x y, Qeq_bool x y = true -> x == y. -Proof. - intros. - unfold Qeq_bool in H. - unfold Qeq. - apply (Zeqb_ok _ _ H). -Qed. - - -Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y. -Proof. - unfold Qeq_bool,Qeq. - red ; intros ; subst. - rewrite H0 in H. - apply (ZMicromega.Zeq_bool_neq _ _ H). - reflexivity. -Qed. - -Lemma Qle_bool_imp_le : forall x y : Q, Qle_bool x y = true -> x <= y. -Proof. - unfold Qle_bool, Qle. - intros. - apply Zle_bool_imp_le ; auto. -Qed. - - - Lemma QSORaddon : SORaddon 0 1 Qplus Qmult Qminus Qopp Qeq Qle (* ring elements *) @@ -115,7 +55,7 @@ Lemma QSORaddon : Proof. constructor. constructor ; intros ; try reflexivity. - apply Qeq_bool_ok ; auto. + apply Qeq_bool_eq; auto. constructor. reflexivity. intros x y. @@ -173,9 +113,9 @@ match o with | OpEq => Qeq | OpNEq => fun x y => ~ x == y | OpLe => Qle -| OpGe => Qge +| OpGe => fun x y => Qle y x | OpLt => Qlt -| OpGt => Qgt +| OpGt => fun x y => Qlt y x end. Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) := diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v index d98c6d422..7c6969c2f 100644 --- a/contrib/micromega/RMicromega.v +++ b/contrib/micromega/RMicromega.v @@ -76,12 +76,12 @@ Proof. apply mult_IZR. apply Ropp_Ropp_IZR. apply IZR_eq. - apply Zeqb_ok ; auto. + apply Zeq_bool_eq ; auto. apply R_power_theory. intros x y. intro. apply IZR_neq. - apply ZMicromega.Zeq_bool_neq ; auto. + apply Zeq_bool_neq ; auto. intros. apply IZR_le. apply Zle_bool_imp_le. auto. Qed. diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v index 94c83f73d..0855925a3 100644 --- a/contrib/micromega/ZMicromega.v +++ b/contrib/micromega/ZMicromega.v @@ -39,15 +39,6 @@ Proof. apply Zmult_lt_0_compat ; auto. Qed. -Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y. -Proof. - red ; intros. - subst. - unfold Zeq_bool in H. - rewrite Zcompare_refl in H. - discriminate. -Qed. - Lemma ZSORaddon : SORaddon 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle (* ring elements *) 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) @@ -56,7 +47,7 @@ Lemma ZSORaddon : Proof. constructor. constructor ; intros ; try reflexivity. - apply Zeqb_ok ; auto. + apply Zeq_bool_eq ; auto. constructor. reflexivity. intros x y. diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index c1fa963f2..e664b3b76 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -38,14 +38,6 @@ Proof. exact Zmult_plus_distr_l. trivial. exact Zminus_diag. Qed. - Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y. - Proof. - intros x y. - assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool; - destruct (Zcompare x y);intros H1;auto;discriminate H1. - Qed. - - (** Two generic morphisms from Z to (abrbitrary) rings, *) (**second one is more convenient for proofs but they are ext. equal*) Section ZMORPHISM. @@ -174,7 +166,7 @@ Section ZMORPHISM. Zeq_bool x y = true -> [x] == [y]. Proof. intros x y H. - assert (H1 := Zeqb_ok x y H);unfold IDphi in H1. + assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. rewrite H1;rrefl. Qed. diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 4a5b623b4..942915abf 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -50,7 +50,7 @@ Ltac Zpower_neg := end. Add Ring Zr : Zth - (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], + (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], power_tac Zpower_theory [Zpow_tac], (* The two following option are not needed, it is the default chose when the set of coefficiant is usual ring Z *) diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index bb2c01437..5189a33ef 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -42,25 +42,27 @@ Infix "?=" := BigZ.compare : bigZ_scope. Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope. Infix "<" := BigZ.lt : bigZ_scope. Infix "<=" := BigZ.le : bigZ_scope. +Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope. +Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope. Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. Open Scope bigZ_scope. (** Some additional results about [BigZ] *) -Theorem spec_to_Z: forall n:bigZ, +Theorem spec_to_Z: forall n:bigZ, BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z. Proof. -intros n; case n; simpl; intros p; +intros n; case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. intros p1 H1; case H1; auto. intros p1 H1; case H1; auto. Qed. -Theorem spec_to_N n: +Theorem spec_to_N n: ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z. Proof. -intros n; case n; simpl; intros p; +intros n; case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. intros p1 H1; case H1; auto. intros p1 H1; case H1; auto. @@ -69,7 +71,7 @@ Qed. Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z -> BigN.to_Z (BigZ.to_N n) = [n]. Proof. -intros n; case n; simpl; intros p; +intros n; case n; simpl; intros p; generalize (BigN.spec_pos p); case (BigN.to_Z p); auto. intros p1 _ H1; case H1; auto. intros p1 H1; case H1; auto. @@ -87,7 +89,7 @@ Qed. (** [BigZ] is a ring *) -Lemma BigZring : +Lemma BigZring : ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq. Proof. constructor. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 1e0b45cd2..653170e34 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -47,6 +47,8 @@ Infix "?=" := BigN.compare : bigN_scope. Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope. Infix "<" := BigN.lt : bigN_scope. Infix "<=" := BigN.le : bigN_scope. +Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. +Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. Open Scope bigN_scope. @@ -62,7 +64,7 @@ Qed. (** [BigN] is a semi-ring *) -Lemma BigNring : +Lemma BigNring : semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq. Proof. constructor. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 11c945f4e..4177fc202 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -54,7 +54,9 @@ Infix "?=" := BigQ.compare : bigQ_scope. Infix "==" := BigQ.eq : bigQ_scope. Infix "<" := BigQ.lt : bigQ_scope. Infix "<=" := BigQ.le : bigQ_scope. -Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. +Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope. +Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope. +Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. Open Scope bigQ_scope. @@ -97,16 +99,16 @@ Proof. Qed. (* TODO : fix this. For the moment it's useless (horribly slow) -Hint Rewrite +Hint Rewrite BigQ.spec_0 BigQ.spec_1 BigQ.spec_m1 BigQ.spec_compare - BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp + BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp BigQ.spec_mul BigQ.spec_inv BigQ.spec_div BigQ.spec_power_pos BigQ.spec_square : bigq. *) (** [BigQ] is a field *) -Lemma BigQfieldth : +Lemma BigQfieldth : field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq. Proof. constructor. @@ -128,7 +130,7 @@ rewrite BigQ.spec_mul, BigQ.spec_inv, BigQ.spec_1; field. rewrite <- BigQ.spec_0; auto. Qed. -Lemma BigQpowerth : +Lemma BigQpowerth : power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power. Proof. constructor. @@ -141,13 +143,13 @@ induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl. destruct n; reflexivity. Qed. -Lemma BigQ_eq_bool_correct : +Lemma BigQ_eq_bool_correct : forall x y, BigQ.eq_bool x y = true -> x==y. Proof. intros; generalize (BigQ.spec_eq_bool x y); rewrite H; auto. Qed. -Lemma BigQ_eq_bool_complete : +Lemma BigQ_eq_bool_complete : forall x y, x==y -> BigQ.eq_bool x y = true. Proof. intros; generalize (BigQ.spec_eq_bool x y). @@ -156,16 +158,16 @@ Qed. (* TODO : improve later the detection of constants ... *) -Ltac BigQcst t := - match t with +Ltac BigQcst t := + match t with | BigQ.zero => BigQ.zero | BigQ.one => BigQ.one | BigQ.minus_one => BigQ.minus_one - | _ => NotConstant + | _ => NotConstant end. -Add Field BigQfield : BigQfieldth - (decidable BigQ_eq_bool_correct, +Add Field BigQfield : BigQfieldth + (decidable BigQ_eq_bool_correct, completeness BigQ_eq_bool_complete, constants [BigQcst], power_tac BigQpowerth [Qpow_tac]). diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index bfed32f9d..82d65dafb 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -155,15 +155,6 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. generalize (Z.spec_eq_bool x y); case Z.eq_bool end). - Ltac destr_zcompare := - match goal with |- context [Zcompare ?x ?y] => - let H := fresh "H" in - case_eq (Zcompare x y); intro H; - [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H | - change (xy)%Z in H ] - end. - Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega). Tactic Notation "simpl_ndiv" "in" "*" := rewrite N.spec_div in * by (nzsimpl; romega). diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 2265715b7..9ebfa19cb 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -10,7 +10,7 @@ Require Export ZArith. Require Export ZArithRing. -Require Export Setoid. +Require Export Setoid Bool. (** * Definition of [Q] and basic properties *) @@ -28,7 +28,7 @@ Ltac simpl_mult := repeat rewrite Zpos_mult_morphism. Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope. -Definition inject_Z (x : Z) := Qmake x 1. +Definition inject_Z (x : Z) := Qmake x 1. Arguments Scope inject_Z [Z_scope]. Notation " 'QDen' p " := (Zpos (Qden p)) (at level 20, no associativity) : Q_scope. @@ -38,14 +38,12 @@ Notation " 1 " := (1#1) : Q_scope. Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z. Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z. Definition Qlt (x y : Q) := (Qnum x * QDen y < Qnum y * QDen x)%Z. -Notation Qgt := (fun a b : Q => Qlt b a). -Notation Qge := (fun a b : Q => Qle b a). -Infix "==" := Qeq (at level 70, no associativity) : Q_scope. +Infix "==" := Qeq (at level 70, no associativity) : Q_scope. Infix "<" := Qlt : Q_scope. -Infix ">" := Qgt : Q_scope. Infix "<=" := Qle : Q_scope. -Infix ">=" := Qge : Q_scope. +Notation "x > y" := (Qlt y x)(only parsing) : Q_scope. +Notation "x >= y" := (Qle y x)(only parsing) : Q_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. (** Another approach : using Qcompare for defining order relations. *) @@ -84,7 +82,7 @@ rewrite Zcompare_Gt_Lt_antisym; auto. rewrite Zcompare_Gt_Lt_antisym in H; auto. Qed. -Hint Unfold Qeq Qlt Qle: qarith. +Hint Unfold Qeq Qlt Qle : qarith. Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith. (** * Properties of equality. *) @@ -94,7 +92,7 @@ Proof. auto with qarith. Qed. -Theorem Qeq_sym : forall x y, x == y -> y == x. +Theorem Qeq_sym : forall x y, x == y -> y == x. Proof. auto with qarith. Qed. @@ -102,7 +100,7 @@ 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). +apply Zmult_reg_l with (QDen y). auto with qarith. transitivity (Qnum x * QDen y * QDen z)%Z; try ring. rewrite H. @@ -117,6 +115,44 @@ Proof. intros; case (Z_eq_dec (Qnum x * QDen y) (Qnum y * QDen x)); auto. Defined. +Definition Qeq_bool x y := + (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z. + +Definition Qle_bool x y := + (Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z. + +Lemma Qeq_bool_iff : forall x y, Qeq_bool x y = true <-> x == y. +Proof. + unfold Qeq_bool, Qeq; intros. + symmetry; apply Zeq_is_eq_bool. +Qed. + +Lemma Qeq_bool_eq : forall x y, Qeq_bool x y = true -> x == y. +Proof. + intros; rewrite <- Qeq_bool_iff; auto. +Qed. + +Lemma Qeq_eq_bool : forall x y, x == y -> Qeq_bool x y = true. +Proof. + intros; rewrite Qeq_bool_iff; auto. +Qed. + +Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y. +Proof. + intros x y H; rewrite <- Qeq_bool_iff, H; discriminate. +Qed. + +Lemma Qle_bool_iff : forall x y, Qle_bool x y = true <-> x <= y. +Proof. + unfold Qle_bool, Qle; intros. + symmetry; apply Zle_is_le_bool. +Qed. + +Lemma Qle_bool_imp_le : forall x y, Qle_bool x y = true -> x <= y. +Proof. + intros; rewrite <- Qle_bool_iff; auto. +Qed. + (** We now consider [Q] seen as a setoid. *) Definition Q_Setoid : Setoid_Theory Q Qeq. @@ -130,7 +166,7 @@ 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. -Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. +Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. Proof. auto with qarith. Qed. @@ -139,13 +175,13 @@ Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) -(** The addition, multiplication and opposite are defined +(** 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 Qmult (x y : Q) := (Qnum x * Qnum y) # (Qden x * Qden y). Definition Qopp (x : Q) := (- Qnum x) # (Qden x). @@ -164,8 +200,8 @@ 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. +Notation "/ x" := (Qinv x) : Q_scope. +Infix "/" := Qdiv : Q_scope. (** A light notation for [Zpos] *) @@ -181,7 +217,7 @@ Qed. (** * Setoid compatibility results *) -Add Morphism Qplus : Qplus_comp. +Add Morphism Qplus : Qplus_comp. Proof. unfold Qeq, Qplus; simpl. Open Scope Z_scope. @@ -208,7 +244,7 @@ Qed. Add Morphism Qminus : Qminus_comp. Proof. intros. - unfold Qminus. + unfold Qminus. rewrite H; rewrite H0; auto with qarith. Qed. @@ -232,11 +268,11 @@ Proof. Open Scope Z_scope. intros (p1, p2) (q1, q2); simpl. case p1; simpl. - intros. + intros. assert (q1 = 0). elim (Zmult_integral q1 ('p2)); auto with zarith. intros; discriminate. - subst; auto. + 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. @@ -254,7 +290,7 @@ 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 *. @@ -289,14 +325,26 @@ Proof. 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. + replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. apply Zlt_gt. apply Zmult_gt_0_lt_compat_l; auto with zarith. Close Scope Z_scope. Qed. +Add Morphism Qeq_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qeqb_comp. +Proof. + intros; apply eq_true_iff_eq. + rewrite 2 Qeq_bool_iff, H, H0; split; auto with qarith. +Qed. + +Add Morphism Qle_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qleb_comp. +Proof. + intros; apply eq_true_iff_eq. + rewrite 2 Qle_bool_iff, H, H0. + split; auto with qarith. +Qed. -Lemma Qcompare_egal_dec: forall n m p q : Q, +Lemma Qcompare_egal_dec: forall n m p q : Q, (n p (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)). Proof. intros. @@ -306,7 +354,6 @@ Proof. omega. Qed. - Add Morphism Qcompare : Qcompare_comp. Proof. intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto. @@ -341,7 +388,7 @@ Lemma Qplus_0_r : forall x, x+0 == x. Proof. intros (x1, x2); unfold Qeq, Qplus; simpl. rewrite Pmult_comm; simpl; ring. -Qed. +Qed. (** Commutativity of addition: *) @@ -374,6 +421,18 @@ Proof. intros; red; simpl; rewrite Pmult_assoc; ring. Qed. +(** multiplication and zero *) + +Lemma Qmult_0_l : forall x , 0*x == 0. +Proof. + intros; compute; reflexivity. +Qed. + +Lemma Qmult_0_r : forall x , x*0 == 0. +Proof. + intros; red; simpl; ring. +Qed. + (** [1] is a neutral element for multiplication: *) Lemma Qmult_1_l : forall n, 1*n == n. @@ -385,7 +444,7 @@ Theorem Qmult_1_r : forall n, n*1==n. Proof. intro; red; simpl. rewrite Zmult_1_r with (n := Qnum n). - rewrite Pmult_comm; simpl; trivial. + rewrite Pmult_comm; simpl; trivial. Qed. (** Commutativity of multiplication *) @@ -427,7 +486,7 @@ Proof. rewrite <- H0; ring. Qed. -(** * Inverse and division. *) +(** * Inverse and division. *) Lemma Qinv_involutive : forall q, (/ / q) == q. Proof. @@ -438,13 +497,13 @@ 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. + 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 x1; simpl; auto; destruct y1; simpl; auto. Qed. @@ -485,10 +544,10 @@ Proof. 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. + 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. + apply Zmult_le_compat_r; auto with zarith. Close Scope Z_scope. Qed. @@ -516,9 +575,9 @@ Proof. apply Zgt_le_trans with (y1 * 'x2 * 'z2). replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring. replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring. - apply Zmult_gt_compat_r; auto with zarith. + apply Zmult_gt_compat_r; auto with zarith. replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. - apply Zmult_le_compat_r; auto with zarith. + apply Zmult_le_compat_r; auto with zarith. Close Scope Z_scope. Qed. @@ -532,9 +591,9 @@ Proof. apply Zle_gt_trans with (y1 * 'x2 * 'z2). 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. + apply Zmult_le_compat_r; auto with zarith. replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring. - apply Zmult_gt_compat_r; auto with zarith. + apply Zmult_gt_compat_r; auto with zarith. Close Scope Z_scope. Qed. @@ -572,7 +631,7 @@ Proof. unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto. Qed. -Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le +Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih. (** Some decidability results about orders. *) @@ -679,7 +738,7 @@ Proof. intros [[|n|n] d] Ha; assumption. Qed. -Lemma Qle_shift_div_l : forall a b c, +Lemma Qle_shift_div_l : forall a b c, 0 < c -> a*c <= b -> a <= b/c. Proof. intros a b c Hc H. @@ -690,7 +749,7 @@ rewrite Qmult_div_r; try assumption. auto with *. Qed. -Lemma Qle_shift_inv_l : forall a c, +Lemma Qle_shift_inv_l : forall a c, 0 < c -> a*c <= 1 -> a <= /c. Proof. intros a c Hc H. @@ -699,7 +758,7 @@ change (a <= 1/c). apply Qle_shift_div_l; assumption. Qed. -Lemma Qle_shift_div_r : forall a b c, +Lemma Qle_shift_div_r : forall a b c, 0 < b -> a <= c*b -> a/b <= c. Proof. intros a b c Hc H. @@ -710,7 +769,7 @@ rewrite Qmult_div_r; try assumption. auto with *. Qed. -Lemma Qle_shift_inv_r : forall b c, +Lemma Qle_shift_inv_r : forall b c, 0 < b -> 1 <= c*b -> /b <= c. Proof. intros b c Hc H. @@ -772,7 +831,7 @@ Qed. (** * Rational to the n-th power *) -Definition Qpower_positive (q:Q)(p:positive) : Q := +Definition Qpower_positive (q:Q)(p:positive) : Q := pow_pos Qmult q p. Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index 2e51ef973..5373c1db3 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -14,23 +14,8 @@ Require Import NArithRing. (** * field and ring tactics for rational numbers *) -Definition Qeq_bool (x y : Q) := - if Qeq_dec x y then true else false. - -Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y. -Proof. - intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. - intros _ H; inversion H. -Qed. - -Lemma Qeq_bool_complete : forall x y : Q, x==y -> Qeq_bool x y = true. -Proof. - intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto. -Qed. - -Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq. +Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. Proof. - constructor. constructor. exact Qplus_0_l. exact Qplus_comm. @@ -41,6 +26,12 @@ Proof. exact Qmult_plus_distr_l. reflexivity. exact Qplus_opp_r. +Qed. + +Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq. +Proof. + constructor. + exact Qsrt. discriminate. reflexivity. intros p Hp. @@ -83,8 +74,8 @@ Ltac Qpow_tac t := end. Add Field Qfield : Qsft - (decidable Qeq_bool_correct, - completeness Qeq_bool_complete, + (decidable Qeq_bool_eq, + completeness Qeq_eq_bool, constants [Qcst], power_tac Qpower_theory [Qpow_tac]). diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index c47f59385..cce0438fa 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -16,7 +16,7 @@ Require Import ZArith_dec. Require Import Sumbool. Unset Boxed Definitions. - +Open Local Scope Z_scope. (** * Boolean operations from decidabilty of order *) (** The decidability of equality and order relations over @@ -37,80 +37,82 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x). (** * Boolean comparisons of binary integers *) Definition Zle_bool (x y:Z) := - match (x ?= y)%Z with + match x ?= y with | Gt => false | _ => true end. Definition Zge_bool (x y:Z) := - match (x ?= y)%Z with + match x ?= y with | Lt => false | _ => true end. Definition Zlt_bool (x y:Z) := - match (x ?= y)%Z with + match x ?= y with | Lt => true | _ => false end. Definition Zgt_bool (x y:Z) := - match (x ?= y)%Z with + match x ?= y with | Gt => true | _ => false end. Definition Zeq_bool (x y:Z) := - match (x ?= y)%Z with + match x ?= y with | Eq => true | _ => false end. Definition Zneq_bool (x y:Z) := - match (x ?= y)%Z with + match x ?= y with | Eq => false | _ => true end. +(** Properties in term of [if ... then ... else ...] *) + Lemma Zle_cases : - forall n m:Z, if Zle_bool n m then (n <= m)%Z else (n > m)%Z. + forall n m:Z, if Zle_bool n m then (n <= m) else (n > m). Proof. intros x y; unfold Zle_bool, Zle, Zgt in |- *. - case (x ?= y)%Z; auto; discriminate. + case (x ?= y); auto; discriminate. Qed. Lemma Zlt_cases : - forall n m:Z, if Zlt_bool n m then (n < m)%Z else (n >= m)%Z. + forall n m:Z, if Zlt_bool n m then (n < m) else (n >= m). Proof. intros x y; unfold Zlt_bool, Zlt, Zge in |- *. - case (x ?= y)%Z; auto; discriminate. + case (x ?= y); auto; discriminate. Qed. Lemma Zge_cases : - forall n m:Z, if Zge_bool n m then (n >= m)%Z else (n < m)%Z. + forall n m:Z, if Zge_bool n m then (n >= m) else (n < m). Proof. intros x y; unfold Zge_bool, Zge, Zlt in |- *. - case (x ?= y)%Z; auto; discriminate. + case (x ?= y); auto; discriminate. Qed. Lemma Zgt_cases : - forall n m:Z, if Zgt_bool n m then (n > m)%Z else (n <= m)%Z. + forall n m:Z, if Zgt_bool n m then (n > m) else (n <= m). Proof. intros x y; unfold Zgt_bool, Zgt, Zle in |- *. - case (x ?= y)%Z; auto; discriminate. + case (x ?= y); auto; discriminate. Qed. (** Lemmas on [Zle_bool] used in contrib/graphs *) -Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m)%Z. +Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m). Proof. unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *. - case (x ?= y)%Z; intros; discriminate. + case (x ?= y); intros; discriminate. Qed. -Lemma Zle_imp_le_bool : forall n m:Z, (n <= m)%Z -> Zle_bool n m = true. +Lemma Zle_imp_le_bool : forall n m:Z, (n <= m) -> Zle_bool n m = true. Proof. - unfold Zle, Zle_bool in |- *. intros x y. case (x ?= y)%Z; trivial. intro. elim (H (refl_equal _)). + unfold Zle, Zle_bool in |- *. intros x y. case (x ?= y); trivial. intro. elim (H (refl_equal _)). Qed. Lemma Zle_bool_refl : forall n:Z, Zle_bool n n = true. @@ -136,8 +138,8 @@ Qed. Definition Zle_bool_total : forall x y:Z, {Zle_bool x y = true} + {Zle_bool y x = true}. Proof. - intros x y; intros. unfold Zle_bool in |- *. cut ((x ?= y)%Z = Gt <-> (y ?= x)%Z = Lt). - case (x ?= y)%Z. left. reflexivity. + intros x y; intros. unfold Zle_bool in |- *. cut ((x ?= y) = Gt <-> (y ?= x) = Lt). + case (x ?= y). left. reflexivity. left. reflexivity. right. rewrite (proj1 H (refl_equal _)). reflexivity. apply Zcompare_Gt_Lt_antisym. @@ -159,39 +161,40 @@ Qed. Lemma Zone_min_pos : forall n:Z, Zle_bool n 0 = false -> Zle_bool 1 n = true. Proof. - intros x; intros. apply Zle_imp_le_bool. change (Zsucc 0 <= x)%Z in |- *. apply Zgt_le_succ. generalize H. - unfold Zle_bool, Zgt in |- *. case (x ?= 0)%Z. intro H0. discriminate H0. + intros x; intros. apply Zle_imp_le_bool. change (Zsucc 0 <= x) in |- *. apply Zgt_le_succ. generalize H. + unfold Zle_bool, Zgt in |- *. case (x ?= 0). intro H0. discriminate H0. intro H0. discriminate H0. reflexivity. Qed. +(** Properties in term of [iff] *) -Lemma Zle_is_le_bool : forall n m:Z, (n <= m)%Z <-> Zle_bool n m = true. +Lemma Zle_is_le_bool : forall n m:Z, (n <= m) <-> Zle_bool n m = true. Proof. intros. split. intro. apply Zle_imp_le_bool. assumption. intro. apply Zle_bool_imp_le. assumption. Qed. -Lemma Zge_is_le_bool : forall n m:Z, (n >= m)%Z <-> Zle_bool m n = true. +Lemma Zge_is_le_bool : forall n m:Z, (n >= m) <-> Zle_bool m n = true. Proof. intros. split. intro. apply Zle_imp_le_bool. apply Zge_le. assumption. intro. apply Zle_ge. apply Zle_bool_imp_le. assumption. Qed. -Lemma Zlt_is_lt_bool : forall n m:Z, (n < m)%Z <-> Zlt_bool n m = true. +Lemma Zlt_is_lt_bool : forall n m:Z, (n < m) <-> Zlt_bool n m = true. Proof. intros n m; unfold Zlt_bool, Zlt. -destruct (n ?= m)%Z; simpl; split; now intro. +destruct (n ?= m); simpl; split; now intro. Qed. -Lemma Zgt_is_gt_bool : forall n m:Z, (n > m)%Z <-> Zgt_bool n m = true. +Lemma Zgt_is_gt_bool : forall n m:Z, (n > m) <-> Zgt_bool n m = true. Proof. intros n m; unfold Zgt_bool, Zgt. -destruct (n ?= m)%Z; simpl; split; now intro. +destruct (n ?= m); simpl; split; now intro. Qed. Lemma Zlt_is_le_bool : - forall n m:Z, (n < m)%Z <-> Zle_bool n (m - 1) = true. + forall n m:Z, (n < m) <-> Zle_bool n (m - 1) = true. Proof. intros x y. split. intro. apply Zle_imp_le_bool. apply Zlt_succ_le. rewrite (Zsucc_pred y) in H. assumption. @@ -199,9 +202,29 @@ Proof. Qed. Lemma Zgt_is_le_bool : - forall n m:Z, (n > m)%Z <-> Zle_bool m (n - 1) = true. + forall n m:Z, (n > m) <-> Zle_bool m (n - 1) = true. Proof. - intros x y. apply iff_trans with (y < x)%Z. split. exact (Zgt_lt x y). + intros x y. apply iff_trans with (y < x). split. exact (Zgt_lt x y). exact (Zlt_gt y x). exact (Zlt_is_le_bool y x). Qed. + +Lemma Zeq_is_eq_bool : forall x y, x = y <-> Zeq_bool x y = true. +Proof. + intros; unfold Zeq_bool. + generalize (Zcompare_Eq_iff_eq x y); destruct Zcompare; intuition; + try discriminate. +Qed. + +Lemma Zeq_bool_eq : forall x y, Zeq_bool x y = true -> x = y. +Proof. + intros x y H; apply <- Zeq_is_eq_bool; auto. +Qed. + +Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y. +Proof. + unfold Zeq_bool; red ; intros; subst. + rewrite Zcompare_refl in H. + discriminate. +Qed. + diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 6c5b07d24..8244d4ceb 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -40,6 +40,15 @@ Proof. | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ]. Qed. +Ltac destr_zcompare := + match goal with |- context [Zcompare ?x ?y] => + let H := fresh "H" in + case_eq (Zcompare x y); intro H; + [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H | + change (xy)%Z in H ] + end. + Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m. Proof. intros x y; split; intro E; -- cgit v1.2.3