From 9d7a9ab7c8182dff99d5afd078747f5d6b1247f0 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 16 Oct 2009 17:28:27 +0000 Subject: OrderedType2 : trivial lemmas are turned into tests for order. In particular we remove them from the hint db, a few autos become calls to order. Moreover, lt_antirefl --> lt_irrefl for uniformity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12398 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/MSets/MSetProperties.v | 34 ++++++++++++---------------------- 1 file changed, 12 insertions(+), 22 deletions(-) (limited to 'theories/MSets/MSetProperties.v') diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 24e889eee..ab9c69afb 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -934,32 +934,24 @@ Module OrdProperties (M:Sets). Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x. Proof. - intros; unfold gtb; ME.elim_compare x y; intuition; try discriminate; ME.order. + intros; rewrite <- ME.compare_gt_iff. unfold gtb. + destruct E.compare; intuition; try discriminate. Qed. Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x. Proof. - intros; unfold leb, gtb; ME.elim_compare x y; intuition; try discriminate; ME.order. + intros; rewrite <- ME.compare_gt_iff. unfold leb, gtb. + destruct E.compare; intuition; try discriminate. Qed. - Lemma gtb_compat : forall x, Proper (E.eq==>Logic.eq) (gtb x). + Instance gtb_compat x : Proper (E.eq==>Logic.eq) (gtb x). Proof. - red; intros x a b H. - generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto. - intros. - symmetry; rewrite H1. - apply ME.eq_lt with a; auto. - rewrite <- H0; auto. - intros. - rewrite H0. - apply ME.eq_lt with b; auto. - rewrite <- H1; auto. + intros x a b H. unfold gtb. rewrite H; auto. Qed. - Lemma leb_compat : forall x, Proper (E.eq==>Logic.eq) (leb x). + Instance leb_compat x : Proper (E.eq==>Logic.eq) (leb x). Proof. - red; intros x a b H; unfold leb. - f_equal; apply gtb_compat; auto. + intros x a b H; unfold leb. rewrite H; auto. Qed. Hint Resolve gtb_compat leb_compat. @@ -1021,10 +1013,9 @@ Module OrdProperties (M:Sets). apply sort_equivlistA_eqlistA; auto with set. apply (@SortA_app _ E.eq); auto with *. intros. - inversion_clear H2. + invlist InA. rewrite <- elements_iff in H1. - apply ME.lt_eq with x; auto. - inversion H3. + setoid_replace y with x; auto. red; intros a. rewrite InA_app_iff, InA_cons, InA_nil, <-!elements_iff, (H0 a) by (auto with *). @@ -1040,10 +1031,9 @@ Module OrdProperties (M:Sets). change (sort E.lt ((x::nil) ++ elements s)). apply (@SortA_app _ E.eq); auto with *. intros. - inversion_clear H1. + invlist InA. rewrite <- elements_iff in H2. - apply ME.eq_lt with x; auto. - inversion H3. + setoid_replace x0 with x; auto. red; intros a. rewrite InA_cons, <- !elements_iff, (H0 a); intuition. Qed. -- cgit v1.2.3