From c251e659c18859d0d8522781ff9d95723b253c11 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 20 Jun 2011 17:18:44 +0000 Subject: Zcompare.destr_zcompare subsumed by case Z.compare_spec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14229 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Rational/BigQ/QMake.v | 12 +++--------- theories/ZArith/Zcompare.v | 9 --------- 2 files changed, 3 insertions(+), 18 deletions(-) diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index d4db2c66d..33267a518 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -68,15 +68,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Proof. intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega. Qed. -(* - Lemma if_fun_commut : forall A B (f:A->B)(b:bool) a a', - f (if b then a else a') = if b then f a else f a'. - Proof. now destruct b. Qed. - - Lemma if_fun_commut' : forall A B C D (f:A->B)(b:{C}+{D}) a a', - f (if b then a else a') = if b then f a else f a'. - Proof. now destruct b. Qed. -*) + + Ltac destr_zcompare := case Z.compare_spec; intros ?H. + Ltac destr_eqb := match goal with | |- context [Z.eqb ?x ?y] => diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 49ab619bc..25925a25c 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -19,15 +19,6 @@ Local Open Scope Z_scope. (***************************) (** * Comparison on integers *) -Ltac destr_zcompare := - match goal with |- context [Z.compare ?x ?y] => - let H := fresh "H" in - case_eq (Z.compare x y); intro H; - [generalize (Z.compare_eq _ _ H); clear H; intro H | - change (xy)%Z in H ] - end. - Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt. Proof Z.gt_lt_iff. -- cgit v1.2.3