summaryrefslogtreecommitdiff
path: root/theories/MSets/MSetList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets/MSetList.v')
-rw-r--r--theories/MSets/MSetList.v899
1 files changed, 899 insertions, 0 deletions
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
new file mode 100644
index 00000000..48af7e6a
--- /dev/null
+++ b/theories/MSets/MSetList.v
@@ -0,0 +1,899 @@
+(***********************************************************************)
+(* 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 [MSetInterface.S] using strictly ordered list. *)
+
+Require Export MSetInterface OrdersFacts OrdersLists.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Functions over lists
+
+ First, we provide sets as lists which are not necessarily sorted.
+ The specs are proved under the additional condition of being sorted.
+ And the functions returning sets are proved to preserve this invariant. *)
+
+Module Ops (X:OrderedType) <: WOps X.
+
+ Definition elt := X.t.
+ Definition t := list elt.
+
+ Definition empty : t := nil.
+
+ Definition is_empty (l : t) := if l then true else false.
+
+ (** ** The set operations. *)
+
+ Fixpoint mem x s :=
+ match s with
+ | nil => false
+ | y :: l =>
+ match X.compare x y with
+ | Lt => false
+ | Eq => true
+ | Gt => mem x l
+ end
+ end.
+
+ Fixpoint add x s :=
+ match s with
+ | nil => x :: nil
+ | y :: l =>
+ match X.compare x y with
+ | Lt => x :: s
+ | Eq => s
+ | Gt => y :: add x l
+ end
+ end.
+
+ Definition singleton (x : elt) := x :: nil.
+
+ Fixpoint remove x s :=
+ match s with
+ | nil => nil
+ | y :: l =>
+ match X.compare x y with
+ | Lt => s
+ | Eq => l
+ | Gt => y :: remove x l
+ end
+ end.
+
+ Fixpoint union (s : t) : t -> t :=
+ match s with
+ | nil => fun s' => s'
+ | x :: l =>
+ (fix union_aux (s' : t) : t :=
+ match s' with
+ | nil => s
+ | x' :: l' =>
+ match X.compare x x' with
+ | Lt => x :: union l s'
+ | Eq => x :: union l l'
+ | Gt => x' :: union_aux l'
+ end
+ end)
+ end.
+
+ Fixpoint inter (s : t) : t -> t :=
+ match s with
+ | nil => fun _ => nil
+ | x :: l =>
+ (fix inter_aux (s' : t) : t :=
+ match s' with
+ | nil => nil
+ | x' :: l' =>
+ match X.compare x x' with
+ | Lt => inter l s'
+ | Eq => x :: inter l l'
+ | Gt => inter_aux l'
+ end
+ end)
+ end.
+
+ Fixpoint diff (s : t) : t -> t :=
+ match s with
+ | nil => fun _ => nil
+ | x :: l =>
+ (fix diff_aux (s' : t) : t :=
+ match s' with
+ | nil => s
+ | x' :: l' =>
+ match X.compare x x' with
+ | Lt => x :: diff l s'
+ | Eq => diff l l'
+ | Gt => diff_aux l'
+ end
+ end)
+ end.
+
+ Fixpoint equal (s : t) : t -> bool :=
+ fun s' : t =>
+ match s, s' with
+ | nil, nil => true
+ | x :: l, x' :: l' =>
+ match X.compare x x' with
+ | Eq => equal l l'
+ | _ => false
+ end
+ | _, _ => false
+ end.
+
+ Fixpoint subset s s' :=
+ match s, s' with
+ | nil, _ => true
+ | x :: l, x' :: l' =>
+ match X.compare x x' with
+ | Lt => false
+ | Eq => subset l l'
+ | Gt => subset s l'
+ end
+ | _, _ => false
+ end.
+
+ Definition fold (B : Type) (f : elt -> B -> B) (s : t) (i : B) : B :=
+ fold_left (flip f) s i.
+
+ 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 (x : t) : list elt := x.
+
+ Definition min_elt (s : t) : option elt :=
+ match s with
+ | nil => None
+ | x :: _ => Some x
+ end.
+
+ Fixpoint max_elt (s : t) : option elt :=
+ match s with
+ | nil => None
+ | x :: nil => Some x
+ | _ :: l => max_elt l
+ end.
+
+ Definition choose := min_elt.
+
+ Fixpoint compare s s' :=
+ match s, s' with
+ | nil, nil => Eq
+ | nil, _ => Lt
+ | _, nil => Gt
+ | x::s, x'::s' =>
+ match X.compare x x' with
+ | Eq => compare s s'
+ | Lt => Lt
+ | Gt => Gt
+ end
+ end.
+
+End Ops.
+
+Module MakeRaw (X: OrderedType) <: RawSets X.
+ Module Import MX := OrderedTypeFacts X.
+ Module Import ML := OrderedTypeLists X.
+
+ Include Ops X.
+
+ (** ** Proofs of set operation specifications. *)
+
+ Section ForNotations.
+
+ Definition inf x l :=
+ match l with
+ | nil => true
+ | y::_ => match X.compare x y with Lt => true | _ => false end
+ end.
+
+ Fixpoint isok l :=
+ match l with
+ | nil => true
+ | x::l => inf x l && isok l
+ end.
+
+ Notation Sort l := (isok l = true).
+ Notation Inf := (lelistA X.lt).
+ 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 s := Sort s.
+
+ Class Ok (s:t) : Prop := ok : Sort s.
+
+ Hint Resolve @ok.
+ Hint Unfold Ok.
+
+ Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
+
+ Lemma inf_iff : forall x l, Inf x l <-> inf x l = true.
+ Proof.
+ intros x l; split; intro H.
+ (* -> *)
+ destruct H; simpl in *.
+ reflexivity.
+ rewrite <- compare_lt_iff in H; rewrite H; reflexivity.
+ (* <- *)
+ destruct l as [|y ys]; simpl in *.
+ constructor; fail.
+ revert H; case_eq (X.compare x y); try discriminate; [].
+ intros Ha _.
+ rewrite compare_lt_iff in Ha.
+ constructor; assumption.
+ Qed.
+
+ Lemma isok_iff : forall l, sort X.lt l <-> Ok l.
+ Proof.
+ intro l; split; intro H.
+ (* -> *)
+ elim H.
+ constructor; fail.
+ intros y ys Ha Hb Hc.
+ change (inf y ys && isok ys = true).
+ rewrite inf_iff in Hc.
+ rewrite andb_true_iff; tauto.
+ (* <- *)
+ induction l as [|x xs].
+ constructor.
+ change (inf x xs && isok xs = true) in H.
+ rewrite andb_true_iff, <- inf_iff in H.
+ destruct H; constructor; tauto.
+ Qed.
+
+ Hint Extern 1 (Ok _) => rewrite <- isok_iff.
+
+ Ltac inv_ok := match goal with
+ | H:sort X.lt (_ :: _) |- _ => inversion_clear H; inv_ok
+ | H:sort X.lt nil |- _ => clear H; inv_ok
+ | H:sort X.lt ?l |- _ => change (Ok l) in H; inv_ok
+ | H:Ok _ |- _ => rewrite <- isok_iff in H; inv_ok
+ | |- Ok _ => rewrite <- isok_iff
+ | _ => idtac
+ end.
+
+ Ltac inv := invlist InA; inv_ok; invlist lelistA.
+ Ltac constructors := repeat constructor.
+
+ Ltac sort_inf_in := match goal with
+ | H:Inf ?x ?l, H':In ?y ?l |- _ =>
+ cut (X.lt x y); [ intro | apply Sort_Inf_In with l; auto]
+ | _ => fail
+ end.
+
+ Global Instance isok_Ok s `(isok s = true) : Ok s | 10.
+ Proof.
+ intros. assumption.
+ Qed.
+
+ 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 : t) := exists x, In x s /\ P x.
+
+ Lemma mem_spec :
+ forall (s : t) (x : elt) (Hs : Ok s), mem x s = true <-> In x s.
+ Proof.
+ induction s; intros x Hs; inv; simpl.
+ intuition. discriminate. inv.
+ elim_compare x a; rewrite InA_cons; intuition; try order.
+ discriminate.
+ sort_inf_in. order.
+ rewrite <- IHs; auto.
+ rewrite IHs; auto.
+ Qed.
+
+ Lemma add_inf :
+ forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s).
+ Proof.
+ simple induction s; simpl.
+ intuition.
+ intros; elim_compare x a; inv; intuition.
+ Qed.
+ Hint Resolve add_inf.
+
+ Global Instance add_ok s x : forall `(Ok s), Ok (add x s).
+ Proof.
+ repeat rewrite <- isok_iff; revert s x.
+ simple induction s; simpl.
+ intuition.
+ intros; elim_compare x a; inv; 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.
+ elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
+ left; order.
+ Qed.
+
+ Lemma remove_inf :
+ forall (s : t) (x a : elt) (Hs : Ok s), Inf a s -> Inf a (remove x s).
+ Proof.
+ induction s; simpl.
+ intuition.
+ intros; elim_compare x a; inv; auto.
+ apply Inf_lt with a; auto.
+ Qed.
+ Hint Resolve remove_inf.
+
+ Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).
+ Proof.
+ repeat rewrite <- isok_iff; revert s x.
+ induction s; simpl.
+ intuition.
+ intros; elim_compare x a; inv; auto.
+ 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.
+ elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition;
+ try sort_inf_in; try order.
+ Qed.
+
+ Global Instance singleton_ok x : Ok (singleton x).
+ Proof.
+ unfold singleton; simpl; auto.
+ Qed.
+
+ Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.
+ Proof.
+ unfold singleton; simpl; split; intros; inv; auto.
+ Qed.
+
+ Ltac induction2 :=
+ simple induction s;
+ [ simpl; auto; try solve [ intros; inv ]
+ | intros x l Hrec; simple induction s';
+ [ simpl; auto; try solve [ intros; inv ]
+ | intros x' l' Hrec'; simpl; elim_compare x x'; intros; inv; auto ]].
+
+ Lemma union_inf :
+ forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'),
+ Inf a s -> Inf a s' -> Inf a (union s s').
+ Proof.
+ induction2.
+ Qed.
+ Hint Resolve union_inf.
+
+ Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
+ Proof.
+ repeat rewrite <- isok_iff; revert s s'.
+ induction2; constructors; try apply @ok; auto.
+ apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
+ change (Inf x' (union (x :: l) l')); auto.
+ 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.
+ induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
+ left; order.
+ Qed.
+
+ Lemma inter_inf :
+ forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'),
+ Inf a s -> Inf a s' -> Inf a (inter s s').
+ Proof.
+ induction2.
+ apply Inf_lt with x; auto.
+ apply Hrec'; auto.
+ apply Inf_lt with x'; auto.
+ Qed.
+ Hint Resolve inter_inf.
+
+ Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').
+ Proof.
+ repeat rewrite <- isok_iff; revert s s'.
+ induction2.
+ constructors; auto.
+ apply Inf_eq with x'; auto; apply inter_inf; auto; apply Inf_eq with x; auto.
+ 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.
+ induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
+ try sort_inf_in; try order.
+ left; order.
+ Qed.
+
+ Lemma diff_inf :
+ forall (s s' : t) (Hs : Ok s) (Hs' : Ok s') (a : elt),
+ Inf a s -> Inf a s' -> Inf a (diff s s').
+ Proof.
+ intros s s'; repeat rewrite <- isok_iff; revert s s'.
+ induction2.
+ apply Hrec; trivial.
+ apply Inf_lt with x; auto.
+ apply Inf_lt with x'; auto.
+ apply Hrec'; auto.
+ apply Inf_lt with x'; auto.
+ Qed.
+ Hint Resolve diff_inf.
+
+ Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').
+ Proof.
+ repeat rewrite <- isok_iff; revert s s'.
+ induction2.
+ 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.
+ induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
+ try sort_inf_in; try order.
+ right; intuition; inv; auto.
+ Qed.
+
+ Lemma equal_spec :
+ forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
+ equal s s' = true <-> Equal s s'.
+ Proof.
+ induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl.
+ intuition.
+ split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv.
+ split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv.
+ inv.
+ elim_compare x x' as C; try discriminate.
+ (* x=x' *)
+ rewrite IH; auto.
+ split; intros E y; specialize (E y).
+ rewrite !InA_cons, E, C; intuition.
+ rewrite !InA_cons, C in E. intuition; try sort_inf_in; order.
+ (* x<x' *)
+ split; intros E. discriminate.
+ assert (In x (x'::s')) by (rewrite <- E; auto).
+ inv; try sort_inf_in; order.
+ (* x>x' *)
+ split; intros E. discriminate.
+ assert (In x' (x::s)) by (rewrite E; auto).
+ inv; try sort_inf_in; order.
+ Qed.
+
+ Lemma subset_spec :
+ forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
+ subset s s' = true <-> Subset s s'.
+ Proof.
+ intros s s'; revert s.
+ induction s' as [ | x' s' IH]; intros [ | x s] Hs Hs'; simpl; auto.
+ split; try red; intros; auto.
+ split; intros H. discriminate. assert (In x nil) by (apply H; auto). inv.
+ split; try red; intros; auto. inv.
+ inv. elim_compare x x' as C.
+ (* x=x' *)
+ rewrite IH; auto.
+ split; intros S y; specialize (S y).
+ rewrite !InA_cons, C. intuition.
+ rewrite !InA_cons, C in S. intuition; try sort_inf_in; order.
+ (* x<x' *)
+ split; intros S. discriminate.
+ assert (In x (x'::s')) by (apply S; auto).
+ inv; try sort_inf_in; order.
+ (* x>x' *)
+ rewrite IH; auto.
+ split; intros S y; specialize (S y).
+ rewrite !InA_cons. intuition.
+ rewrite !InA_cons in S. rewrite !InA_cons. intuition; try sort_inf_in; order.
+ Qed.
+
+ Global Instance empty_ok : Ok empty.
+ Proof.
+ constructors.
+ Qed.
+
+ Lemma empty_spec : Empty empty.
+ Proof.
+ unfold Empty, empty; intuition; inv.
+ Qed.
+
+ Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.
+ Proof.
+ intros [ | x s]; simpl.
+ split; auto. intros _ x H. inv.
+ split. discriminate. intros H. elim (H x); auto.
+ Qed.
+
+ Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.
+ Proof.
+ intuition.
+ Qed.
+
+ Lemma elements_spec2 : forall (s : t) (Hs : Ok s), sort X.lt (elements s).
+ Proof.
+ intro s; repeat rewrite <- isok_iff; auto.
+ Qed.
+
+ Lemma elements_spec2w : forall (s : t) (Hs : Ok s), NoDupA X.eq (elements s).
+ Proof.
+ intro s; repeat rewrite <- isok_iff; auto.
+ Qed.
+
+ Lemma min_elt_spec1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.
+ Proof.
+ destruct s; simpl; inversion 1; auto.
+ Qed.
+
+ Lemma min_elt_spec2 :
+ forall (s : t) (x y : elt) (Hs : Ok s),
+ min_elt s = Some x -> In y s -> ~ X.lt y x.
+ Proof.
+ induction s as [ | x s IH]; simpl; inversion 2; subst.
+ intros; inv; try sort_inf_in; order.
+ Qed.
+
+ Lemma min_elt_spec3 : forall s : t, min_elt s = None -> Empty s.
+ Proof.
+ destruct s; simpl; red; intuition. inv. discriminate.
+ Qed.
+
+ Lemma max_elt_spec1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.
+ Proof.
+ induction s as [ | x s IH]. inversion 1.
+ destruct s as [ | y s]. simpl. inversion 1; subst; auto.
+ right; apply IH; auto.
+ Qed.
+
+ Lemma max_elt_spec2 :
+ forall (s : t) (x y : elt) (Hs : Ok s),
+ max_elt s = Some x -> In y s -> ~ X.lt x y.
+ Proof.
+ induction s as [ | a s IH]. inversion 2.
+ destruct s as [ | b s]. inversion 2; subst. intros; inv; order.
+ intros. inv; auto.
+ assert (~X.lt x b) by (apply IH; auto).
+ assert (X.lt a b) by auto.
+ order.
+ Qed.
+
+ Lemma max_elt_spec3 : forall s : t, max_elt s = None -> Empty s.
+ Proof.
+ induction s as [ | a s IH]. red; intuition; inv.
+ destruct s as [ | b s]. inversion 1.
+ intros; elim IH with b; auto.
+ Qed.
+
+ Definition choose_spec1 :
+ forall (s : t) (x : elt), choose s = Some x -> In x s := min_elt_spec1.
+
+ Definition choose_spec2 :
+ forall s : t, choose s = None -> Empty s := min_elt_spec3.
+
+ Lemma choose_spec3: forall s s' x x', Ok s -> Ok s' ->
+ choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'.
+ Proof.
+ unfold choose; intros s s' x x' Hs Hs' Hx Hx' H.
+ assert (~X.lt x x').
+ apply min_elt_spec2 with s'; auto.
+ rewrite <-H; auto using min_elt_spec1.
+ assert (~X.lt x' x).
+ apply min_elt_spec2 with s; auto.
+ rewrite H; auto using min_elt_spec1.
+ order.
+ 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.
+
+ Lemma cardinal_spec :
+ forall (s : t) (Hs : Ok s),
+ cardinal s = length (elements s).
+ Proof.
+ auto.
+ Qed.
+
+ Lemma filter_inf :
+ forall (s : t) (x : elt) (f : elt -> bool) (Hs : Ok s),
+ Inf x s -> Inf x (filter f s).
+ Proof.
+ simple induction s; simpl.
+ intuition.
+ intros x l Hrec a f Hs Ha; inv.
+ case (f x); auto.
+ apply Hrec; auto.
+ apply Inf_lt with x; auto.
+ Qed.
+
+ Global Instance filter_ok s f : forall `(Ok s), Ok (filter f s).
+ Proof.
+ repeat rewrite <- isok_iff; revert s f.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec f Hs; inv.
+ case (f x); auto.
+ constructors; auto.
+ apply filter_inf; auto.
+ 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; intros.
+ split; intuition; inv.
+ destruct (f a) as [ ]_eqn:F; rewrite !InA_cons, ?IHs; intuition.
+ setoid_replace x with a; auto.
+ setoid_replace a with x in F; auto; congruence.
+ 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; intros.
+ split; intros; auto. inv.
+ destruct (f a) as [ ]_eqn:F.
+ rewrite IHs; auto. firstorder. inv; auto.
+ setoid_replace x with a; auto.
+ split; intros H'. discriminate.
+ rewrite H' in F; 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; intros.
+ firstorder. discriminate. inv.
+ destruct (f a) as [ ]_eqn:F.
+ firstorder.
+ rewrite IHs; auto.
+ firstorder.
+ inv.
+ setoid_replace a with x in F; auto; congruence.
+ exists x; auto.
+ Qed.
+
+ Lemma partition_inf1 :
+ forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
+ Inf x s -> Inf x (fst (partition f s)).
+ Proof.
+ intros s f x; repeat rewrite <- isok_iff; revert s f x.
+ simple induction s; simpl.
+ intuition.
+ intros x l Hrec f a Hs Ha; inv.
+ generalize (Hrec f a H).
+ case (f x); case (partition f l); simpl.
+ auto.
+ intros; apply H2; apply Inf_lt with x; auto.
+ Qed.
+
+ Lemma partition_inf2 :
+ forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
+ Inf x s -> Inf x (snd (partition f s)).
+ Proof.
+ intros s f x; repeat rewrite <- isok_iff; revert s f x.
+ simple induction s; simpl.
+ intuition.
+ intros x l Hrec f a Hs Ha; inv.
+ generalize (Hrec f a H).
+ case (f x); case (partition f l); simpl.
+ intros; apply H2; apply Inf_lt with x; auto.
+ auto.
+ Qed.
+
+ Global Instance partition_ok1 s f : forall `(Ok s), Ok (fst (partition f s)).
+ Proof.
+ repeat rewrite <- isok_iff; revert s f.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec f Hs; inv.
+ generalize (Hrec f H); generalize (@partition_inf1 l f x).
+ case (f x); case (partition f l); simpl; auto.
+ Qed.
+
+ Global Instance partition_ok2 s f : forall `(Ok s), Ok (snd (partition f s)).
+ Proof.
+ repeat rewrite <- isok_iff; revert s f.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec f Hs; inv.
+ generalize (Hrec f H); generalize (@partition_inf2 l f x).
+ case (f x); case (partition f l); simpl; 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.
+ split; auto.
+ intros x l Hrec f Hf.
+ generalize (Hrec f Hf); clear Hrec.
+ destruct (partition f l) as [s1 s2]; simpl; intros.
+ case (f x); simpl; auto.
+ split; inversion_clear 1; auto.
+ constructor 2; rewrite <- H; auto.
+ constructor 2; rewrite H; auto.
+ 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.
+ split; auto.
+ intros x l Hrec f Hf.
+ generalize (Hrec f Hf); clear Hrec.
+ destruct (partition f l) as [s1 s2]; simpl; intros.
+ case (f x); simpl; auto.
+ split; inversion_clear 1; auto.
+ constructor 2; rewrite <- H; auto.
+ constructor 2; rewrite H; auto.
+ Qed.
+
+ End ForNotations.
+
+ Definition In := InA X.eq.
+ Instance In_compat : Proper (X.eq==>eq==> iff) In.
+ Proof. repeat red; intros; rewrite H, H0; auto. Qed.
+
+ Module L := MakeListOrdering X.
+ Definition eq := L.eq.
+ Definition eq_equiv := L.eq_equiv.
+ Definition lt l1 l2 :=
+ exists l1', exists l2', Ok l1' /\ Ok l2' /\
+ eq l1 l1' /\ eq l2 l2' /\ L.lt l1' l2'.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+ split.
+ intros s (s1 & s2 & B1 & B2 & E1 & E2 & L).
+ repeat rewrite <- isok_iff in *.
+ assert (eqlistA X.eq s1 s2).
+ apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto using @ok with *.
+ transitivity s; auto. symmetry; auto.
+ rewrite H in L.
+ apply (StrictOrder_Irreflexive s2); auto.
+ intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
+ (s2'' & s3' & B2' & B3 & E2' & E3 & L23).
+ exists s1', s3'.
+ repeat rewrite <- isok_iff in *.
+ do 4 (split; trivial).
+ assert (eqlistA X.eq s2' s2'').
+ apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto using @ok with *.
+ transitivity s2; auto. symmetry; auto.
+ transitivity s2'; auto.
+ rewrite H; auto.
+ Qed.
+
+ Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Proof.
+ intros s1 s2 E12 s3 s4 E34. split.
+ intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
+ exists s1', s3'; do 2 (split; trivial).
+ split. transitivity s1; auto. symmetry; auto.
+ split; auto. transitivity s3; auto. symmetry; auto.
+ intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
+ exists s1', s3'; do 2 (split; trivial).
+ split. transitivity s2; auto.
+ split; auto. transitivity s4; auto.
+ Qed.
+
+ Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
+ Proof.
+ induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
+ elim_compare x x'; auto.
+ Qed.
+
+ Lemma compare_spec : forall s s', Ok s -> Ok s' ->
+ CompSpec eq lt s s' (compare s s').
+ Proof.
+ intros s s' Hs Hs'.
+ destruct (compare_spec_aux s s'); constructor; auto.
+ exists s, s'; repeat split; auto using @ok.
+ exists s', s; repeat split; auto using @ok.
+ Qed.
+
+End MakeRaw.
+
+(** * Encapsulation
+
+ Now, in order to really provide a functor implementing [S], we
+ need to encapsulate everything into a type of strictly ordered lists. *)
+
+Module Make (X: OrderedType) <: S with Module E := X.
+ Module Raw := MakeRaw X.
+ Include Raw2Sets X Raw.
+End Make.
+
+(** For this specific implementation, eq coincides with Leibniz equality *)
+
+Require Eqdep_dec.
+
+Module Type OrderedTypeWithLeibniz.
+ Include OrderedType.
+ Parameter eq_leibniz : forall x y, eq x y -> x = y.
+End OrderedTypeWithLeibniz.
+
+Module Type SWithLeibniz.
+ Declare Module E : OrderedTypeWithLeibniz.
+ Include SetsOn E.
+ Parameter eq_leibniz : forall x y, eq x y -> x = y.
+End SWithLeibniz.
+
+Module MakeWithLeibniz (X: OrderedTypeWithLeibniz) <: SWithLeibniz with Module E := X.
+ Module E := X.
+ Module Raw := MakeRaw X.
+ Include Raw2SetsOn X Raw.
+
+ Lemma eq_leibniz_list : forall xs ys, eqlistA X.eq xs ys -> xs = ys.
+ Proof.
+ induction xs as [|x xs]; intros [|y ys] H; inversion H; [ | ].
+ reflexivity.
+ f_equal.
+ apply X.eq_leibniz; congruence.
+ apply IHxs; subst; assumption.
+ Qed.
+
+ Lemma eq_leibniz : forall s s', eq s s' -> s = s'.
+ Proof.
+ intros [xs Hxs] [ys Hys] Heq.
+ change (equivlistA X.eq xs ys) in Heq.
+ assert (H : eqlistA X.eq xs ys).
+ rewrite <- Raw.isok_iff in Hxs, Hys.
+ apply SortA_equivlistA_eqlistA with X.lt; auto with *.
+ apply eq_leibniz_list in H.
+ subst ys.
+ f_equal.
+ apply Eqdep_dec.eq_proofs_unicity.
+ intros x y; destruct (bool_dec x y); tauto.
+ Qed.
+
+End MakeWithLeibniz.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 03:14:46 +0000