summaryrefslogtreecommitdiff
path: root/theories/MSets/MSetWeakList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets/MSetWeakList.v')
-rw-r--r--theories/MSets/MSetWeakList.v533
1 files changed, 533 insertions, 0 deletions
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
new file mode 100644
index 00000000..945cb2dd
--- /dev/null
+++ b/theories/MSets/MSetWeakList.v
@@ -0,0 +1,533 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(** * Finite sets library *)
+
+(** This file proposes an implementation of the non-dependant
+ interface [MSetWeakInterface.S] using lists without redundancy. *)
+
+Require Import MSetInterface.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Functions over lists
+
+ First, we provide sets as lists which are (morally) without redundancy.
+ The specs are proved under the additional condition of no redundancy.
+ And the functions returning sets are proved to preserve this invariant. *)
+
+
+(** ** The set operations. *)
+
+Module Ops (X: DecidableType) <: WOps X.
+
+ Definition elt := X.t.
+ Definition t := list elt.
+
+ Definition empty : t := nil.
+
+ Definition is_empty (l : t) : bool := if l then true else false.
+
+ Fixpoint mem (x : elt) (s : t) : bool :=
+ match s with
+ | nil => false
+ | y :: l =>
+ if X.eq_dec x y then true else mem x l
+ end.
+
+ Fixpoint add (x : elt) (s : t) : t :=
+ match s with
+ | nil => x :: nil
+ | y :: l =>
+ if X.eq_dec x y then s else y :: add x l
+ end.
+
+ Definition singleton (x : elt) : t := x :: nil.
+
+ Fixpoint remove (x : elt) (s : t) : t :=
+ match s with
+ | nil => nil
+ | y :: l =>
+ if X.eq_dec x y then l else y :: remove x l
+ end.
+
+ Definition fold (B : Type) (f : elt -> B -> B) (s : t) (i : B) : B :=
+ fold_left (flip f) s i.
+
+ Definition union (s : t) : t -> t := fold add s.
+
+ Definition diff (s s' : t) : t := fold remove s' s.
+
+ Definition inter (s s': t) : t :=
+ fold (fun x s => if mem x s' then add x s else s) s nil.
+
+ Definition subset (s s' : t) : bool := is_empty (diff s s').
+
+ Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s).
+
+ Fixpoint filter (f : elt -> bool) (s : t) : t :=
+ match s with
+ | nil => nil
+ | x :: l => if f x then x :: filter f l else filter f l
+ end.
+
+ Fixpoint for_all (f : elt -> bool) (s : t) : bool :=
+ match s with
+ | nil => true
+ | x :: l => if f x then for_all f l else false
+ end.
+
+ Fixpoint exists_ (f : elt -> bool) (s : t) : bool :=
+ match s with
+ | nil => false
+ | x :: l => if f x then true else exists_ f l
+ end.
+
+ Fixpoint partition (f : elt -> bool) (s : t) : t * t :=
+ match s with
+ | nil => (nil, nil)
+ | x :: l =>
+ let (s1, s2) := partition f l in
+ if f x then (x :: s1, s2) else (s1, x :: s2)
+ end.
+
+ Definition cardinal (s : t) : nat := length s.
+
+ Definition elements (s : t) : list elt := s.
+
+ Definition choose (s : t) : option elt :=
+ match s with
+ | nil => None
+ | x::_ => Some x
+ end.
+
+End Ops.
+
+(** ** Proofs of set operation specifications. *)
+
+Module MakeRaw (X:DecidableType) <: WRawSets X.
+ Include Ops X.
+
+ Section ForNotations.
+ Notation NoDup := (NoDupA X.eq).
+ Notation In := (InA X.eq).
+
+ (* TODO: modify proofs in order to avoid these hints *)
+ Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
+ Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
+ Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+
+ Definition IsOk := NoDup.
+
+ Class Ok (s:t) : Prop := ok : NoDup s.
+
+ Hint Unfold Ok.
+ Hint Resolve @ok.
+
+ Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
+
+ Ltac inv_ok := match goal with
+ | H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok
+ | H:Ok nil |- _ => clear H; inv_ok
+ | H:NoDup ?l |- _ => change (Ok l) in H; inv_ok
+ | _ => idtac
+ end.
+
+ Ltac inv := invlist InA; inv_ok.
+ Ltac constructors := repeat constructor.
+
+ Fixpoint isok l := match l with
+ | nil => true
+ | a::l => negb (mem a l) && isok l
+ end.
+
+ Definition Equal s s' := forall a : elt, In a s <-> In a s'.
+ Definition Subset s s' := forall a : elt, In a s -> In a s'.
+ Definition Empty s := forall a : elt, ~ In a s.
+ Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+ Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+
+ Lemma In_compat : Proper (X.eq==>eq==>iff) In.
+ Proof.
+ repeat red; intros. subst. rewrite H; auto.
+ Qed.
+
+ Lemma mem_spec : forall s x `{Ok s},
+ mem x s = true <-> In x s.
+ Proof.
+ induction s; intros.
+ split; intros; inv. discriminate.
+ simpl; destruct (X.eq_dec x a); split; intros; inv; auto.
+ right; rewrite <- IHs; auto.
+ rewrite IHs; auto.
+ Qed.
+
+ Lemma isok_iff : forall l, Ok l <-> isok l = true.
+ Proof.
+ induction l.
+ intuition.
+ simpl.
+ rewrite andb_true_iff.
+ rewrite negb_true_iff.
+ rewrite <- IHl.
+ split; intros H. inv.
+ split; auto.
+ apply not_true_is_false. rewrite mem_spec; auto.
+ destruct H; constructors; auto.
+ rewrite <- mem_spec; auto; congruence.
+ Qed.
+
+ Global Instance isok_Ok l : isok l = true -> Ok l | 10.
+ Proof.
+ intros. apply <- isok_iff; auto.
+ Qed.
+
+ Lemma add_spec :
+ forall (s : t) (x y : elt) {Hs : Ok s},
+ In y (add x s) <-> X.eq y x \/ In y s.
+ Proof.
+ induction s; simpl; intros.
+ intuition; inv; auto.
+ destruct X.eq_dec; inv; rewrite InA_cons, ?IHs; intuition.
+ left; eauto.
+ inv; auto.
+ Qed.
+
+ Global Instance add_ok s x `(Ok s) : Ok (add x s).
+ Proof.
+ induction s.
+ simpl; intuition.
+ intros; inv. simpl.
+ destruct X.eq_dec; auto.
+ constructors; auto.
+ intro; inv; auto.
+ rewrite add_spec in *; intuition.
+ Qed.
+
+ Lemma remove_spec :
+ forall (s : t) (x y : elt) {Hs : Ok s},
+ In y (remove x s) <-> In y s /\ ~X.eq y x.
+ Proof.
+ induction s; simpl; intros.
+ intuition; inv; auto.
+ destruct X.eq_dec; inv; rewrite !InA_cons, ?IHs; intuition.
+ elim H. setoid_replace a with y; eauto.
+ elim H3. setoid_replace x with y; eauto.
+ elim n. eauto.
+ Qed.
+
+ Global Instance remove_ok s x `(Ok s) : Ok (remove x s).
+ Proof.
+ induction s; simpl; intros.
+ auto.
+ destruct X.eq_dec; inv; auto.
+ constructors; auto.
+ rewrite remove_spec; intuition.
+ Qed.
+
+ Lemma singleton_ok : forall x : elt, Ok (singleton x).
+ Proof.
+ unfold singleton; simpl; constructors; auto. intro; inv.
+ Qed.
+
+ Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.
+ Proof.
+ unfold singleton; simpl; split; intros. inv; auto. left; auto.
+ Qed.
+
+ Lemma empty_ok : Ok empty.
+ Proof.
+ unfold empty; constructors.
+ Qed.
+
+ Lemma empty_spec : Empty empty.
+ Proof.
+ unfold Empty, empty; red; intros; inv.
+ Qed.
+
+ Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.
+ Proof.
+ unfold Empty; destruct s; simpl; split; intros; auto.
+ intro; inv.
+ discriminate.
+ elim (H e); auto.
+ Qed.
+
+ Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.
+ Proof.
+ unfold elements; intuition.
+ Qed.
+
+ Lemma elements_spec2w : forall (s : t) {Hs : Ok s}, NoDup (elements s).
+ Proof.
+ unfold elements; auto.
+ Qed.
+
+ Lemma fold_spec :
+ forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
+ fold f s i = fold_left (flip f) (elements s) i.
+ Proof.
+ reflexivity.
+ Qed.
+
+ Global Instance union_ok : forall s s' `(Ok s, Ok s'), Ok (union s s').
+ Proof.
+ induction s; simpl; auto; intros; inv; unfold flip; auto with *.
+ Qed.
+
+ Lemma union_spec :
+ forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
+ In x (union s s') <-> In x s \/ In x s'.
+ Proof.
+ induction s; simpl in *; unfold flip; intros; auto; inv.
+ intuition; inv.
+ rewrite IHs, add_spec, InA_cons; intuition.
+ Qed.
+
+ Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
+ Proof.
+ unfold inter, fold, flip.
+ set (acc := nil (A:=elt)).
+ assert (Hacc : Ok acc) by constructors.
+ clearbody acc; revert acc Hacc.
+ induction s; simpl; auto; intros. inv.
+ apply IHs; auto.
+ destruct (mem a s'); auto with *.
+ Qed.
+
+ Lemma inter_spec :
+ forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
+ In x (inter s s') <-> In x s /\ In x s'.
+ Proof.
+ unfold inter, fold, flip; intros.
+ set (acc := nil (A:=elt)) in *.
+ assert (Hacc : Ok acc) by constructors.
+ assert (IFF : (In x s /\ In x s') <-> (In x s /\ In x s') \/ In x acc).
+ intuition; unfold acc in *; inv.
+ rewrite IFF; clear IFF. clearbody acc.
+ revert acc Hacc x s' Hs Hs'.
+ induction s; simpl; intros.
+ intuition; inv.
+ inv.
+ case_eq (mem a s'); intros Hm.
+ rewrite IHs, add_spec, InA_cons; intuition.
+ rewrite mem_spec in Hm; auto.
+ left; split; auto. rewrite H1; auto.
+ rewrite IHs, InA_cons; intuition.
+ rewrite H2, <- mem_spec in H3; auto. congruence.
+ Qed.
+
+ Global Instance diff_ok : forall s s' `(Ok s, Ok s'), Ok (diff s s').
+ Proof.
+ unfold diff; intros s s'; revert s.
+ induction s'; simpl; unfold flip; auto; intros. inv; auto with *.
+ Qed.
+
+ Lemma diff_spec :
+ forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'},
+ In x (diff s s') <-> In x s /\ ~In x s'.
+ Proof.
+ unfold diff; intros s s'; revert s.
+ induction s'; simpl; unfold flip.
+ intuition; inv.
+ intros. inv.
+ rewrite IHs', remove_spec, InA_cons; intuition.
+ Qed.
+
+ Lemma subset_spec :
+ forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
+ subset s s' = true <-> Subset s s'.
+ Proof.
+ unfold subset, Subset; intros.
+ rewrite is_empty_spec.
+ unfold Empty; intros.
+ intuition.
+ specialize (H a). rewrite diff_spec in H; intuition.
+ rewrite <- (mem_spec a) in H |- *. destruct (mem a s'); intuition.
+ rewrite diff_spec in H0; intuition.
+ Qed.
+
+ Lemma equal_spec :
+ forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
+ equal s s' = true <-> Equal s s'.
+ Proof.
+ unfold Equal, equal; intros.
+ rewrite andb_true_iff, !subset_spec.
+ unfold Subset; intuition. rewrite <- H; auto. rewrite H; auto.
+ Qed.
+
+ Definition choose_spec1 :
+ forall (s : t) (x : elt), choose s = Some x -> In x s.
+ Proof.
+ destruct s; simpl; intros; inversion H; auto.
+ Qed.
+
+ Definition choose_spec2 : forall s : t, choose s = None -> Empty s.
+ Proof.
+ destruct s; simpl; intros.
+ intros x H0; inversion H0.
+ inversion H.
+ Qed.
+
+ Lemma cardinal_spec :
+ forall (s : t) {Hs : Ok s}, cardinal s = length (elements s).
+ Proof.
+ auto.
+ Qed.
+
+ Lemma filter_spec' : forall s x f,
+ In x (filter f s) -> In x s.
+ Proof.
+ induction s; simpl.
+ intuition; inv.
+ intros; destruct (f a); inv; intuition; right; eauto.
+ Qed.
+
+ Lemma filter_spec :
+ forall (s : t) (x : elt) (f : elt -> bool),
+ Proper (X.eq==>eq) f ->
+ (In x (filter f s) <-> In x s /\ f x = true).
+ Proof.
+ induction s; simpl.
+ intuition; inv.
+ intros.
+ destruct (f a) as [ ]_eqn:E; rewrite ?InA_cons, IHs; intuition.
+ setoid_replace x with a; auto.
+ setoid_replace a with x in E; auto. congruence.
+ Qed.
+
+ Global Instance filter_ok s f `(Ok s) : Ok (filter f s).
+ Proof.
+ induction s; simpl.
+ auto.
+ intros; inv.
+ case (f a); auto.
+ constructors; auto.
+ contradict H0.
+ eapply filter_spec'; eauto.
+ Qed.
+
+ Lemma for_all_spec :
+ forall (s : t) (f : elt -> bool),
+ Proper (X.eq==>eq) f ->
+ (for_all f s = true <-> For_all (fun x => f x = true) s).
+ Proof.
+ unfold For_all; induction s; simpl.
+ intuition. inv.
+ intros; inv.
+ destruct (f a) as [ ]_eqn:F.
+ rewrite IHs; intuition. inv; auto.
+ setoid_replace x with a; auto.
+ split; intros H'; try discriminate.
+ intros.
+ rewrite <- F, <- (H' a); auto.
+ Qed.
+
+ Lemma exists_spec :
+ forall (s : t) (f : elt -> bool),
+ Proper (X.eq==>eq) f ->
+ (exists_ f s = true <-> Exists (fun x => f x = true) s).
+ Proof.
+ unfold Exists; induction s; simpl.
+ split; [discriminate| intros (x & Hx & _); inv].
+ intros.
+ destruct (f a) as [ ]_eqn:F.
+ split; auto.
+ exists a; auto.
+ rewrite IHs; firstorder.
+ inv.
+ setoid_replace a with x in F; auto; congruence.
+ exists x; auto.
+ Qed.
+
+ Lemma partition_spec1 :
+ forall (s : t) (f : elt -> bool),
+ Proper (X.eq==>eq) f ->
+ Equal (fst (partition f s)) (filter f s).
+ Proof.
+ simple induction s; simpl; auto; unfold Equal.
+ firstorder.
+ intros x l Hrec f Hf.
+ generalize (Hrec f Hf); clear Hrec.
+ case (partition f l); intros s1 s2; simpl; intros.
+ case (f x); simpl; firstorder; inversion H0; intros; firstorder.
+ Qed.
+
+ Lemma partition_spec2 :
+ forall (s : t) (f : elt -> bool),
+ Proper (X.eq==>eq) f ->
+ Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+ Proof.
+ simple induction s; simpl; auto; unfold Equal.
+ firstorder.
+ intros x l Hrec f Hf.
+ generalize (Hrec f Hf); clear Hrec.
+ case (partition f l); intros s1 s2; simpl; intros.
+ case (f x); simpl; firstorder; inversion H0; intros; firstorder.
+ Qed.
+
+ Lemma partition_ok1' :
+ forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
+ In x (fst (partition f s)) -> In x s.
+ Proof.
+ induction s; simpl; auto; intros. inv.
+ generalize (IHs H1 f x).
+ destruct (f a); destruct (partition f s); simpl in *; auto.
+ inversion_clear H; auto.
+ Qed.
+
+ Lemma partition_ok2' :
+ forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
+ In x (snd (partition f s)) -> In x s.
+ Proof.
+ induction s; simpl; auto; intros. inv.
+ generalize (IHs H1 f x).
+ destruct (f a); destruct (partition f s); simpl in *; auto.
+ inversion_clear H; auto.
+ Qed.
+
+ Global Instance partition_ok1 : forall s f `(Ok s), Ok (fst (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec f Hs; inv.
+ generalize (@partition_ok1' _ _ f x).
+ generalize (Hrec f H0).
+ case (f x); case (partition f l); simpl; constructors; auto.
+ Qed.
+
+ Global Instance partition_ok2 : forall s f `(Ok s), Ok (snd (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec f Hs; inv.
+ generalize (@partition_ok2' _ _ f x).
+ generalize (Hrec f H0).
+ case (f x); case (partition f l); simpl; constructors; auto.
+ Qed.
+
+ End ForNotations.
+
+ Definition In := InA X.eq.
+ Definition eq := Equal.
+ Instance eq_equiv : Equivalence eq.
+
+End MakeRaw.
+
+(** * Encapsulation
+
+ Now, in order to really provide a functor implementing [S], we
+ need to encapsulate everything into a type of lists without redundancy. *)
+
+Module Make (X: DecidableType) <: WSets with Module E := X.
+ Module Raw := MakeRaw X.
+ Include WRaw2Sets X Raw.
+End Make.
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:46:00 +0000