diff options
Diffstat (limited to 'theories/Lists/ListSet.v')
-rw-r--r-- | theories/Lists/ListSet.v | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 37d051a3..0a0bf0de 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -1,16 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** A Library for finite sets, implemented as lists *) +(** A library for finite sets, implemented as lists *) -(** List is loaded, but not exported. - This allow to "hide" the definitions, functions and theorems of List - and to see only the ones of ListSet *) +(** This is a light implementation of finite sets as lists; for a more + extensive library, you might rather consider MSetWeakList.v. In + addition, if your domain is totally ordered, you might also + consider implementations of finite sets with access in logarithmic + time (e.g. MSetRBT.v which is based on red-black trees). *) Require Import List. @@ -116,7 +118,7 @@ Section first_definitions. simple induction x; simpl; intros. apply H0; red; trivial. case (Aeq_dec a a0); auto with datatypes. - intro; apply H; intros; auto. + intro Hneg; apply H; intros; auto. apply H1; red; intro. case H3; auto. Qed. @@ -147,8 +149,8 @@ Section first_definitions. simple induction x; simpl. tauto. intros a0 l; elim (Aeq_dec a a0). - intros; discriminate H0. - unfold not; intros; elim H1; auto with datatypes. + intros _ _ [=]. + unfold not; intros H H0 H1 [|]; auto with datatypes. Qed. Lemma set_mem_complete2 : @@ -157,7 +159,7 @@ Section first_definitions. simple induction x; simpl. tauto. intros a0 l; elim (Aeq_dec a a0). - intros; elim H0; auto with datatypes. + intros H H0 []; auto with datatypes. tauto. Qed. @@ -204,7 +206,7 @@ Section first_definitions. simpl; do 3 intro. elim (Aeq_dec b a0). simpl; tauto. - simpl; intros; elim H0. + simpl; intros H0 [|]. trivial with datatypes. tauto. tauto. |