diff options
Diffstat (limited to 'theories/MSets/MSetList.v')
-rw-r--r-- | theories/MSets/MSetList.v | 899 |
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. |