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 --- theories/Numbers/Rational/BigQ/BigQ.v | 26 ++++++++++++++------------ theories/Numbers/Rational/BigQ/QMake.v | 9 --------- 2 files changed, 14 insertions(+), 21 deletions(-) (limited to 'theories/Numbers/Rational') 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). -- cgit v1.2.3