summaryrefslogtreecommitdiff
path: root/theories/FSets/FSetList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetList.v')
-rw-r--r--theories/FSets/FSetList.v1163
1 files changed, 1163 insertions, 0 deletions
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
new file mode 100644
index 00000000..ca86ffcc
--- /dev/null
+++ b/theories/FSets/FSetList.v
@@ -0,0 +1,1163 @@
+(***********************************************************************)
+(* 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: FSetList.v 8667 2006-03-28 11:59:44Z letouzey $ *)
+
+(** * Finite sets library *)
+
+(** This file proposes an implementation of the non-dependant
+ interface [FSetInterface.S] using strictly ordered list. *)
+
+Require Export FSetInterface.
+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 Raw (X: OrderedType).
+
+ Module E := X.
+ Module MX := OrderedTypeFacts X.
+ Import MX.
+
+ Definition elt := X.t.
+ Definition t := list elt.
+
+ Definition empty : t := nil.
+
+ Definition is_empty (l : t) : bool := if l then true else false.
+
+ (** ** The set operations. *)
+
+ Fixpoint mem (x : elt) (s : t) {struct s} : bool :=
+ 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 : elt) (s : t) {struct s} : t :=
+ 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) : t := x :: nil.
+
+ Fixpoint remove (x : elt) (s : t) {struct s} : t :=
+ 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' : t) {struct s'} : bool :=
+ 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.
+
+ Fixpoint fold (B : Set) (f : elt -> B -> B) (s : t) {struct s} :
+ B -> B := fun i => match s with
+ | nil => i
+ | x :: l => fold f l (f x i)
+ end.
+
+ Fixpoint filter (f : elt -> bool) (s : t) {struct s} : 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) {struct s} : 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) {struct s} : 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) {struct s} :
+ 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.
+
+ (** ** Proofs of set operation specifications. *)
+
+ Notation Sort := (sort X.lt).
+ Notation Inf := (lelistA X.lt).
+ Notation In := (InA X.eq).
+
+ 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_1 :
+ forall (s : t) (Hs : Sort s) (x : elt), In x s -> mem x s = true.
+ Proof.
+ simple induction s; intros.
+ inversion H.
+ inversion_clear Hs.
+ inversion_clear H0.
+ simpl; elim_comp; trivial.
+ simpl; elim_comp_gt x a; auto.
+ apply Sort_Inf_In with l; trivial.
+ Qed.
+
+ Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s.
+ Proof.
+ simple induction s.
+ intros; inversion H.
+ intros a l Hrec x.
+ simpl.
+ case (X.compare x a); intros; try discriminate; 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.
+ simpl; intros; case (X.compare x a); intuition; inversion H0;
+ intuition.
+ Qed.
+ Hint Resolve add_Inf.
+
+ Lemma add_sort : forall (s : t) (Hs : Sort s) (x : elt), Sort (add x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.compare x a); intuition; inversion_clear Hs;
+ auto.
+ Qed.
+
+ Lemma add_1 :
+ forall (s : t) (Hs : Sort s) (x y : elt), X.eq x y -> In y (add x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.compare x a); inversion_clear Hs; auto.
+ constructor; apply X.eq_trans with x; auto.
+ Qed.
+
+ Lemma add_2 :
+ forall (s : t) (Hs : Sort s) (x y : elt), In y s -> In y (add x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.compare x a); intuition.
+ inversion_clear Hs; inversion_clear H0; auto.
+ Qed.
+
+ Lemma add_3 :
+ forall (s : t) (Hs : Sort s) (x y : elt),
+ ~ X.eq x y -> In y (add x s) -> In y s.
+ Proof.
+ simple induction s.
+ simpl; inversion_clear 3; auto; order.
+ simpl; intros a l Hrec Hs x y; case (X.compare x a); intros;
+ inversion_clear H0; inversion_clear Hs; auto.
+ order.
+ constructor 2; apply Hrec with x; auto.
+ Qed.
+
+ Lemma remove_Inf :
+ forall (s : t) (Hs : Sort s) (x a : elt), Inf a s -> Inf a (remove x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.compare x a); intuition; inversion_clear H0; auto.
+ inversion_clear Hs; apply Inf_lt with a; auto.
+ Qed.
+ Hint Resolve remove_Inf.
+
+ Lemma remove_sort :
+ forall (s : t) (Hs : Sort s) (x : elt), Sort (remove x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.compare x a); intuition; inversion_clear Hs; auto.
+ Qed.
+
+ Lemma remove_1 :
+ forall (s : t) (Hs : Sort s) (x y : elt), X.eq x y -> ~ In y (remove x s).
+ Proof.
+ simple induction s.
+ simpl; red; intros; inversion H0.
+ simpl; intros; case (X.compare x a); intuition; inversion_clear Hs.
+ inversion_clear H1.
+ order.
+ generalize (Sort_Inf_In H2 H3 H4); order.
+ generalize (Sort_Inf_In H2 H3 H1); order.
+ inversion_clear H1.
+ order.
+ apply (H H2 _ _ H0 H4).
+ Qed.
+
+ Lemma remove_2 :
+ forall (s : t) (Hs : Sort s) (x y : elt),
+ ~ X.eq x y -> In y s -> In y (remove x s).
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros; case (X.compare x a); intuition; inversion_clear Hs;
+ inversion_clear H1; auto.
+ destruct H0; apply X.eq_trans with a; auto.
+ Qed.
+
+ Lemma remove_3 :
+ forall (s : t) (Hs : Sort s) (x y : elt), In y (remove x s) -> In y s.
+ Proof.
+ simple induction s.
+ simpl; intuition.
+ simpl; intros a l Hrec Hs x y; case (X.compare x a); intuition.
+ inversion_clear Hs; inversion_clear H; auto.
+ constructor 2; apply Hrec with x; auto.
+ Qed.
+
+ Lemma singleton_sort : forall x : elt, Sort (singleton x).
+ Proof.
+ unfold singleton; simpl; auto.
+ Qed.
+
+ Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y.
+ Proof.
+ unfold singleton; simpl; intuition.
+ inversion_clear H; auto; inversion H0.
+ Qed.
+
+ Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x).
+ Proof.
+ unfold singleton; simpl; auto.
+ Qed.
+
+ Ltac DoubleInd :=
+ simple induction s;
+ [ simpl; auto; try solve [ intros; inversion H ]
+ | intros x l Hrec; simple induction s';
+ [ simpl; auto; try solve [ intros; inversion H ]
+ | intros x' l' Hrec' Hs Hs'; inversion Hs; inversion Hs'; subst;
+ simpl ] ].
+
+ Lemma union_Inf :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt),
+ Inf a s -> Inf a s' -> Inf a (union s s').
+ Proof.
+ DoubleInd.
+ intros i His His'; inversion_clear His; inversion_clear His'.
+ case (X.compare x x'); auto.
+ Qed.
+ Hint Resolve union_Inf.
+
+ Lemma union_sort :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (union s s').
+ Proof.
+ DoubleInd; case (X.compare x x'); intuition; constructor; auto.
+ apply Inf_eq with x'; trivial; apply union_Inf; trivial; apply Inf_eq with x; auto.
+ change (Inf x' (union (x :: l) l')); auto.
+ Qed.
+
+ Lemma union_1 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x (union s s') -> In x s \/ In x s'.
+ Proof.
+ DoubleInd; case (X.compare x x'); intuition; inversion_clear H; intuition.
+ elim (Hrec (x' :: l') H1 Hs' x0); intuition.
+ elim (Hrec l' H1 H5 x0); intuition.
+ elim (H0 x0); intuition.
+ Qed.
+
+ Lemma union_2 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x s -> In x (union s s').
+ Proof.
+ DoubleInd.
+ intros i Hi; case (X.compare x x'); intuition; inversion_clear Hi; auto.
+ Qed.
+
+ Lemma union_3 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x s' -> In x (union s s').
+ Proof.
+ DoubleInd.
+ intros i Hi; case (X.compare x x'); inversion_clear Hi; intuition.
+ constructor; apply X.eq_trans with x'; auto.
+ Qed.
+
+ Lemma inter_Inf :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt),
+ Inf a s -> Inf a s' -> Inf a (inter s s').
+ Proof.
+ DoubleInd.
+ intros i His His'; inversion His; inversion His'; subst.
+ case (X.compare x x'); intuition.
+ apply Inf_lt with x; auto.
+ apply H3; auto.
+ apply Inf_lt with x'; auto.
+ Qed.
+ Hint Resolve inter_Inf.
+
+ Lemma inter_sort :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (inter s s').
+ Proof.
+ DoubleInd; case (X.compare x x'); auto.
+ constructor; auto.
+ apply Inf_eq with x'; trivial; apply inter_Inf; trivial; apply Inf_eq with x; auto.
+ Qed.
+
+ Lemma inter_1 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x (inter s s') -> In x s.
+ Proof.
+ DoubleInd; case (X.compare x x'); intuition.
+ constructor 2; apply Hrec with (x'::l'); auto.
+ inversion_clear H; auto.
+ constructor 2; apply Hrec with l'; auto.
+ Qed.
+
+ Lemma inter_2 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x (inter s s') -> In x s'.
+ Proof.
+ DoubleInd; case (X.compare x x'); intuition; inversion_clear H.
+ constructor 1; apply X.eq_trans with x; auto.
+ constructor 2; auto.
+ Qed.
+
+ Lemma inter_3 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x s -> In x s' -> In x (inter s s').
+ Proof.
+ DoubleInd.
+ intros i His His'; elim (X.compare x x'); intuition.
+
+ inversion_clear His; auto.
+ generalize (Sort_Inf_In Hs' (cons_leA _ _ _ _ l0) His'); order.
+
+ inversion_clear His; auto; inversion_clear His'; auto.
+ constructor; apply X.eq_trans with x'; auto.
+
+ change (In i (inter (x :: l) l')).
+ inversion_clear His'; auto.
+ generalize (Sort_Inf_In Hs (cons_leA _ _ _ _ l0) His); order.
+ Qed.
+
+ Lemma diff_Inf :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt),
+ Inf a s -> Inf a s' -> Inf a (diff s s').
+ Proof.
+ DoubleInd.
+ intros i His His'; inversion His; inversion His'.
+ case (X.compare x x'); intuition.
+ apply Hrec; trivial.
+ apply Inf_lt with x; auto.
+ apply Inf_lt with x'; auto.
+ apply H10; trivial.
+ apply Inf_lt with x'; auto.
+ Qed.
+ Hint Resolve diff_Inf.
+
+ Lemma diff_sort :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (diff s s').
+ Proof.
+ DoubleInd; case (X.compare x x'); auto.
+ Qed.
+
+ Lemma diff_1 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x (diff s s') -> In x s.
+ Proof.
+ DoubleInd; case (X.compare x x'); intuition.
+ inversion_clear H; auto.
+ constructor 2; apply Hrec with (x'::l'); auto.
+ constructor 2; apply Hrec with l'; auto.
+ Qed.
+
+ Lemma diff_2 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x (diff s s') -> ~ In x s'.
+ Proof.
+ DoubleInd.
+ intros; intro Abs; inversion Abs.
+ case (X.compare x x'); intuition.
+
+ inversion_clear H.
+ generalize (Sort_Inf_In Hs' (cons_leA _ _ _ _ l0) H3); order.
+ apply Hrec with (x'::l') x0; auto.
+
+ inversion_clear H3.
+ generalize (Sort_Inf_In H1 H2 (diff_1 H1 H5 H)); order.
+ apply Hrec with l' x0; auto.
+
+ inversion_clear H3.
+ generalize (Sort_Inf_In Hs (cons_leA _ _ _ _ l0) (diff_1 Hs H5 H)); order.
+ apply H0 with x0; auto.
+ Qed.
+
+ Lemma diff_3 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt),
+ In x s -> ~ In x s' -> In x (diff s s').
+ Proof.
+ DoubleInd.
+ intros i His His'; elim (X.compare x x'); intuition; inversion_clear His; auto.
+ elim His'; constructor; apply X.eq_trans with x; auto.
+ Qed.
+
+ Lemma equal_1 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'),
+ Equal s s' -> equal s s' = true.
+ Proof.
+ simple induction s; unfold Equal.
+ intro s'; case s'; auto.
+ simpl; intuition.
+ elim (H e); intros; assert (A : In e nil); auto; inversion A.
+ intros x l Hrec s'.
+ case s'.
+ intros; elim (H x); intros; assert (A : In x nil); auto; inversion A.
+ intros x' l' Hs Hs'; inversion Hs; inversion Hs'; subst.
+ simpl; case (X.compare x); intros; auto.
+
+ elim (H x); intros.
+ assert (A : In x (x' :: l')); auto; inversion_clear A.
+ order.
+ generalize (Sort_Inf_In H5 H6 H4); order.
+
+ apply Hrec; intuition; elim (H a); intros.
+ assert (A : In a (x' :: l')); auto; inversion_clear A; auto.
+ generalize (Sort_Inf_In H1 H2 H0); order.
+ assert (A : In a (x :: l)); auto; inversion_clear A; auto.
+ generalize (Sort_Inf_In H5 H6 H0); order.
+
+ elim (H x'); intros.
+ assert (A : In x' (x :: l)); auto; inversion_clear A.
+ order.
+ generalize (Sort_Inf_In H1 H2 H4); order.
+ Qed.
+
+ Lemma equal_2 : forall s s' : t, equal s s' = true -> Equal s s'.
+ Proof.
+ simple induction s; unfold Equal.
+ intro s'; case s'; intros.
+ intuition.
+ simpl in H; discriminate H.
+ intros x l Hrec s'.
+ case s'.
+ intros; simpl in H; discriminate.
+ intros x' l'; simpl; case (X.compare x); intros; auto; try discriminate.
+ elim (Hrec l' H a); intuition; inversion_clear H2; auto.
+ constructor; apply X.eq_trans with x; auto.
+ constructor; apply X.eq_trans with x'; auto.
+ Qed.
+
+ Lemma subset_1 :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'),
+ Subset s s' -> subset s s' = true.
+ Proof.
+ intros s s'; generalize s' s; clear s s'.
+ simple induction s'; unfold Subset.
+ intro s; case s; auto.
+ intros; elim (H e); intros; assert (A : In e nil); auto; inversion A.
+ intros x' l' Hrec s; case s.
+ simpl; auto.
+ intros x l Hs Hs'; inversion Hs; inversion Hs'; subst.
+ simpl; case (X.compare x); intros; auto.
+
+ assert (A : In x (x' :: l')); auto; inversion_clear A.
+ order.
+ generalize (Sort_Inf_In H5 H6 H0); order.
+
+ apply Hrec; intuition.
+ assert (A : In a (x' :: l')); auto; inversion_clear A; auto.
+ generalize (Sort_Inf_In H1 H2 H0); order.
+
+ apply Hrec; intuition.
+ assert (A : In a (x' :: l')); auto; inversion_clear A; auto.
+ inversion_clear H0.
+ order.
+ generalize (Sort_Inf_In H1 H2 H4); order.
+ Qed.
+
+ Lemma subset_2 : forall s s' : t, subset s s' = true -> Subset s s'.
+ Proof.
+ intros s s'; generalize s' s; clear s s'.
+ simple induction s'; unfold Subset.
+ intro s; case s; auto.
+ simpl; intros; discriminate H.
+ intros x' l' Hrec s; case s.
+ intros; inversion H0.
+ intros x l; simpl; case (X.compare x); intros; auto.
+ discriminate H.
+ inversion_clear H0.
+ constructor; apply X.eq_trans with x; auto.
+ constructor 2; apply Hrec with l; auto.
+ constructor 2; apply Hrec with (x::l); auto.
+ Qed.
+
+ Lemma empty_sort : Sort empty.
+ Proof.
+ unfold empty; constructor.
+ Qed.
+
+ Lemma empty_1 : Empty empty.
+ Proof.
+ unfold Empty, empty; intuition; inversion H.
+ Qed.
+
+ Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true.
+ Proof.
+ unfold Empty; intro s; case s; simpl; intuition.
+ elim (H e); auto.
+ Qed.
+
+ Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s.
+ Proof.
+ unfold Empty; intro s; case s; simpl; intuition;
+ inversion H0.
+ Qed.
+
+ Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s).
+ Proof.
+ unfold elements; auto.
+ Qed.
+
+ Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s.
+ Proof.
+ unfold elements; auto.
+ Qed.
+
+ Lemma elements_3 : forall (s : t) (Hs : Sort s), Sort (elements s).
+ Proof.
+ unfold elements; auto.
+ Qed.
+
+ Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.
+ Proof.
+ intro s; case s; simpl; intros; inversion H; auto.
+ Qed.
+
+ Lemma min_elt_2 :
+ forall (s : t) (Hs : Sort s) (x y : elt),
+ min_elt s = Some x -> In y s -> ~ X.lt y x.
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H.
+ intros a l; case l; intros; inversion H0; inversion_clear H1; subst.
+ order.
+ inversion H2.
+ order.
+ inversion_clear Hs.
+ inversion_clear H3.
+ generalize (H H1 e y (refl_equal (Some e)) H2); order.
+ Qed.
+
+ Lemma min_elt_3 : forall s : t, min_elt s = None -> Empty s.
+ Proof.
+ unfold Empty; intro s; case s; simpl; intuition;
+ inversion H; inversion H0.
+ Qed.
+
+ Lemma max_elt_1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H.
+ intros x l; case l; simpl.
+ intuition.
+ inversion H0; auto.
+ intros.
+ constructor 2; apply (H _ H0).
+ Qed.
+
+ Lemma max_elt_2 :
+ forall (s : t) (Hs : Sort s) (x y : elt),
+ max_elt s = Some x -> In y s -> ~ X.lt x y.
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H.
+ intros x l; case l; simpl.
+ intuition.
+ inversion H0; subst.
+ inversion_clear H1.
+ order.
+ inversion H3.
+ intros; inversion_clear Hs; inversion_clear H3; inversion_clear H1.
+ assert (In e (e::l0)) by auto.
+ generalize (H H2 x0 e H0 H1); order.
+ generalize (H H2 x0 y H0 H3); order.
+ Qed.
+
+ Lemma max_elt_3 : forall s : t, max_elt s = None -> Empty s.
+ Proof.
+ unfold Empty; simple induction s; simpl.
+ red; intros; inversion H0.
+ intros x l; case l; simpl; intros.
+ inversion H0.
+ elim (H H0 e); auto.
+ Qed.
+
+ Definition choose_1 :
+ forall (s : t) (x : elt), choose s = Some x -> In x s := min_elt_1.
+
+ Definition choose_2 : forall s : t, choose s = None -> Empty s := min_elt_3.
+
+ Lemma fold_1 :
+ forall (s : t) (Hs : Sort s) (A : Set) (i : A) (f : elt -> A -> A),
+ fold f s i = fold_left (fun a e => f e a) (elements s) i.
+ Proof.
+ induction s.
+ simpl; trivial.
+ intros.
+ inversion_clear Hs.
+ simpl; auto.
+ Qed.
+
+ Lemma cardinal_1 :
+ forall (s : t) (Hs : Sort s),
+ cardinal s = length (elements s).
+ Proof.
+ auto.
+ Qed.
+
+ Lemma filter_Inf :
+ forall (s : t) (Hs : Sort s) (x : elt) (f : elt -> bool),
+ Inf x s -> Inf x (filter f s).
+ Proof.
+ simple induction s; simpl.
+ intuition.
+ intros x l Hrec Hs a f Ha; inversion_clear Hs; inversion_clear Ha.
+ case (f x).
+ constructor; auto.
+ apply Hrec; auto.
+ apply Inf_lt with x; auto.
+ Qed.
+
+ Lemma filter_sort :
+ forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (filter f s).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec Hs f; inversion_clear Hs.
+ case (f x); auto.
+ constructor; auto.
+ apply filter_Inf; auto.
+ Qed.
+
+ Lemma filter_1 :
+ forall (s : t) (x : elt) (f : elt -> bool),
+ compat_bool X.eq f -> In x (filter f s) -> In x s.
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H0.
+ intros x l Hrec a f Hf.
+ case (f x); simpl.
+ inversion_clear 1.
+ constructor; auto.
+ constructor 2; apply (Hrec a f Hf); trivial.
+ constructor 2; apply (Hrec a f Hf); trivial.
+ Qed.
+
+ Lemma filter_2 :
+ forall (s : t) (x : elt) (f : elt -> bool),
+ compat_bool X.eq f -> In x (filter f s) -> f x = true.
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H0.
+ intros x l Hrec a f Hf.
+ generalize (Hf x); case (f x); simpl; auto.
+ inversion_clear 2; auto.
+ symmetry; auto.
+ Qed.
+
+ Lemma filter_3 :
+ forall (s : t) (x : elt) (f : elt -> bool),
+ compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s).
+ Proof.
+ simple induction s; simpl.
+ intros; inversion H0.
+ intros x l Hrec a f Hf.
+ generalize (Hf x); case (f x); simpl.
+ inversion_clear 2; auto.
+ inversion_clear 2; auto.
+ rewrite <- (H a (X.eq_sym H1)); intros; discriminate.
+ Qed.
+
+ Lemma for_all_1 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f ->
+ For_all (fun x => f x = true) s -> for_all f s = true.
+ Proof.
+ simple induction s; simpl; auto; unfold For_all.
+ intros x l Hrec f Hf.
+ generalize (Hf x); case (f x); simpl.
+ auto.
+ intros; rewrite (H x); auto.
+ Qed.
+
+ Lemma for_all_2 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f ->
+ for_all f s = true -> For_all (fun x => f x = true) s.
+ Proof.
+ simple induction s; simpl; auto; unfold For_all.
+ intros; inversion H1.
+ intros x l Hrec f Hf.
+ intros A a; intros.
+ assert (f x = true).
+ generalize A; case (f x); auto.
+ rewrite H0 in A; simpl in A.
+ inversion_clear H; auto.
+ rewrite (Hf a x); auto.
+ Qed.
+
+ Lemma exists_1 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true.
+ Proof.
+ simple induction s; simpl; auto; unfold Exists.
+ intros.
+ elim H0; intuition.
+ inversion H2.
+ intros x l Hrec f Hf.
+ generalize (Hf x); case (f x); simpl.
+ auto.
+ destruct 2 as [a (A1,A2)].
+ inversion_clear A1.
+ rewrite <- (H a (X.eq_sym H0)) in A2; discriminate.
+ apply Hrec; auto.
+ exists a; auto.
+ Qed.
+
+ Lemma exists_2 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s.
+ Proof.
+ simple induction s; simpl; auto; unfold Exists.
+ intros; discriminate.
+ intros x l Hrec f Hf.
+ case_eq (f x); intros.
+ exists x; auto.
+ destruct (Hrec f Hf H0) as [a (A1,A2)].
+ exists a; auto.
+ Qed.
+
+ Lemma partition_Inf_1 :
+ forall (s : t) (Hs : Sort s) (f : elt -> bool) (x : elt),
+ Inf x s -> Inf x (fst (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ intuition.
+ intros x l Hrec Hs f a Ha; inversion_clear Hs; inversion_clear Ha.
+ generalize (Hrec H f a).
+ case (f x); case (partition f l); simpl.
+ auto.
+ intros; apply H2; apply Inf_lt with x; auto.
+ Qed.
+
+ Lemma partition_Inf_2 :
+ forall (s : t) (Hs : Sort s) (f : elt -> bool) (x : elt),
+ Inf x s -> Inf x (snd (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ intuition.
+ intros x l Hrec Hs f a Ha; inversion_clear Hs; inversion_clear Ha.
+ generalize (Hrec H f a).
+ case (f x); case (partition f l); simpl.
+ intros; apply H2; apply Inf_lt with x; auto.
+ auto.
+ Qed.
+
+ Lemma partition_sort_1 :
+ forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (fst (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec Hs f; inversion_clear Hs.
+ generalize (Hrec H f); generalize (partition_Inf_1 H f).
+ case (f x); case (partition f l); simpl; auto.
+ Qed.
+
+ Lemma partition_sort_2 :
+ forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (snd (partition f s)).
+ Proof.
+ simple induction s; simpl.
+ auto.
+ intros x l Hrec Hs f; inversion_clear Hs.
+ generalize (Hrec H f); generalize (partition_Inf_2 H f).
+ case (f x); case (partition f l); simpl; auto.
+ Qed.
+
+ Lemma partition_1 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.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_2 :
+ forall (s : t) (f : elt -> bool),
+ compat_bool X.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.
+
+ Definition eq : t -> t -> Prop := Equal.
+
+ Lemma eq_refl : forall s : t, eq s s.
+ Proof.
+ unfold eq, Equal; intuition.
+ Qed.
+
+ Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s.
+ Proof.
+ unfold eq, Equal; intros; destruct (H a); intuition.
+ Qed.
+
+ Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''.
+ Proof.
+ unfold eq, Equal; intros; destruct (H a); destruct (H0 a); intuition.
+ Qed.
+
+ Inductive lt : t -> t -> Prop :=
+ | lt_nil : forall (x : elt) (s : t), lt nil (x :: s)
+ | lt_cons_lt :
+ forall (x y : elt) (s s' : t), X.lt x y -> lt (x :: s) (y :: s')
+ | lt_cons_eq :
+ forall (x y : elt) (s s' : t),
+ X.eq x y -> lt s s' -> lt (x :: s) (y :: s').
+ Hint Constructors lt.
+
+ Lemma lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''.
+ Proof.
+ intros s s' s'' H; generalize s''; clear s''; elim H.
+ intros x l s'' H'; inversion_clear H'; auto.
+ intros x x' l l' E s'' H'; inversion_clear H'; auto.
+ constructor; apply X.lt_trans with x'; auto.
+ constructor; apply lt_eq with x'; auto.
+ intros.
+ inversion_clear H3.
+ constructor; apply eq_lt with y; auto.
+ constructor 3; auto; apply X.eq_trans with y; auto.
+ Qed.
+
+ Lemma lt_not_eq :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), lt s s' -> ~ eq s s'.
+ Proof.
+ unfold eq, Equal.
+ intros s s' Hs Hs' H; generalize Hs Hs'; clear Hs Hs'; elim H; intros; intro.
+ elim (H0 x); intros.
+ assert (X : In x nil); auto; inversion X.
+ inversion_clear Hs; inversion_clear Hs'.
+ elim (H1 x); intros.
+ assert (X : In x (y :: s'0)); auto; inversion_clear X.
+ order.
+ generalize (Sort_Inf_In H4 H5 H8); order.
+ inversion_clear Hs; inversion_clear Hs'.
+ elim H2; auto; split; intros.
+ generalize (Sort_Inf_In H4 H5 H8); intros.
+ elim (H3 a); intros.
+ assert (X : In a (y :: s'0)); auto; inversion_clear X; auto.
+ order.
+ generalize (Sort_Inf_In H6 H7 H8); intros.
+ elim (H3 a); intros.
+ assert (X : In a (x :: s0)); auto; inversion_clear X; auto.
+ order.
+ Qed.
+
+ Definition compare :
+ forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Compare lt eq s s'.
+ Proof.
+ simple induction s.
+ intros; case s'.
+ constructor 2; apply eq_refl.
+ constructor 1; auto.
+ intros a l Hrec s'; case s'.
+ constructor 3; auto.
+ intros a' l' Hs Hs'.
+ case (X.compare a a'); [ constructor 1 | idtac | constructor 3 ]; auto.
+ elim (Hrec l');
+ [ constructor 1
+ | constructor 2
+ | constructor 3
+ | inversion Hs
+ | inversion Hs' ]; auto.
+ generalize e; unfold eq, Equal; intuition; inversion_clear H.
+ constructor; apply X.eq_trans with a; auto.
+ destruct (e1 a0); auto.
+ constructor; apply X.eq_trans with a'; auto.
+ destruct (e1 a0); auto.
+ Defined.
+
+End Raw.
+
+(** * 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 E := X.
+ Module Raw := Raw X.
+
+ Record slist : Set := {this :> Raw.t; sorted : sort X.lt this}.
+ Definition t := slist.
+ Definition elt := X.t.
+
+ Definition In (x : elt) (s : t) := InA X.eq x s.(this).
+ 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.
+
+ Definition In_1 (s : t) := Raw.MX.In_eq (l:=s.(this)).
+
+ Definition mem (x : elt) (s : t) := Raw.mem x s.
+ Definition mem_1 (s : t) := Raw.mem_1 (sorted s).
+ Definition mem_2 (s : t) := Raw.mem_2 (s:=s).
+
+ Definition add x s := Build_slist (Raw.add_sort (sorted s) x).
+ Definition add_1 (s : t) := Raw.add_1 (sorted s).
+ Definition add_2 (s : t) := Raw.add_2 (sorted s).
+ Definition add_3 (s : t) := Raw.add_3 (sorted s).
+
+ Definition remove x s := Build_slist (Raw.remove_sort (sorted s) x).
+ Definition remove_1 (s : t) := Raw.remove_1 (sorted s).
+ Definition remove_2 (s : t) := Raw.remove_2 (sorted s).
+ Definition remove_3 (s : t) := Raw.remove_3 (sorted s).
+
+ Definition singleton x := Build_slist (Raw.singleton_sort x).
+ Definition singleton_1 := Raw.singleton_1.
+ Definition singleton_2 := Raw.singleton_2.
+
+ Definition union (s s' : t) :=
+ Build_slist (Raw.union_sort (sorted s) (sorted s')).
+ Definition union_1 (s s' : t) := Raw.union_1 (sorted s) (sorted s').
+ Definition union_2 (s s' : t) := Raw.union_2 (sorted s) (sorted s').
+ Definition union_3 (s s' : t) := Raw.union_3 (sorted s) (sorted s').
+
+ Definition inter (s s' : t) :=
+ Build_slist (Raw.inter_sort (sorted s) (sorted s')).
+ Definition inter_1 (s s' : t) := Raw.inter_1 (sorted s) (sorted s').
+ Definition inter_2 (s s' : t) := Raw.inter_2 (sorted s) (sorted s').
+ Definition inter_3 (s s' : t) := Raw.inter_3 (sorted s) (sorted s').
+
+ Definition diff (s s' : t) :=
+ Build_slist (Raw.diff_sort (sorted s) (sorted s')).
+ Definition diff_1 (s s' : t) := Raw.diff_1 (sorted s) (sorted s').
+ Definition diff_2 (s s' : t) := Raw.diff_2 (sorted s) (sorted s').
+ Definition diff_3 (s s' : t) := Raw.diff_3 (sorted s) (sorted s').
+
+ Definition equal (s s' : t) := Raw.equal s s'.
+ Definition equal_1 (s s' : t) := Raw.equal_1 (sorted s) (sorted s').
+ Definition equal_2 (s s' : t) := Raw.equal_2 (s:=s) (s':=s').
+
+ Definition subset (s s' : t) := Raw.subset s s'.
+ Definition subset_1 (s s' : t) := Raw.subset_1 (sorted s) (sorted s').
+ Definition subset_2 (s s' : t) := Raw.subset_2 (s:=s) (s':=s').
+
+ Definition empty := Build_slist Raw.empty_sort.
+ Definition empty_1 := Raw.empty_1.
+
+ Definition is_empty (s : t) := Raw.is_empty s.
+ Definition is_empty_1 (s : t) := Raw.is_empty_1 (s:=s).
+ Definition is_empty_2 (s : t) := Raw.is_empty_2 (s:=s).
+
+ Definition elements (s : t) := Raw.elements s.
+ Definition elements_1 (s : t) := Raw.elements_1 (s:=s).
+ Definition elements_2 (s : t) := Raw.elements_2 (s:=s).
+ Definition elements_3 (s : t) := Raw.elements_3 (sorted s).
+
+ Definition min_elt (s : t) := Raw.min_elt s.
+ Definition min_elt_1 (s : t) := Raw.min_elt_1 (s:=s).
+ Definition min_elt_2 (s : t) := Raw.min_elt_2 (sorted s).
+ Definition min_elt_3 (s : t) := Raw.min_elt_3 (s:=s).
+
+ Definition max_elt (s : t) := Raw.max_elt s.
+ Definition max_elt_1 (s : t) := Raw.max_elt_1 (s:=s).
+ Definition max_elt_2 (s : t) := Raw.max_elt_2 (sorted s).
+ Definition max_elt_3 (s : t) := Raw.max_elt_3 (s:=s).
+
+ Definition choose := min_elt.
+ Definition choose_1 := min_elt_1.
+ Definition choose_2 := min_elt_3.
+
+ Definition fold (B : Set) (f : elt -> B -> B) (s : t) := Raw.fold (B:=B) f s.
+ Definition fold_1 (s : t) := Raw.fold_1 (sorted s).
+
+ Definition cardinal (s : t) := Raw.cardinal s.
+ Definition cardinal_1 (s : t) := Raw.cardinal_1 (sorted s).
+
+ Definition filter (f : elt -> bool) (s : t) :=
+ Build_slist (Raw.filter_sort (sorted s) f).
+ Definition filter_1 (s : t) := Raw.filter_1 (s:=s).
+ Definition filter_2 (s : t) := Raw.filter_2 (s:=s).
+ Definition filter_3 (s : t) := Raw.filter_3 (s:=s).
+
+ Definition for_all (f : elt -> bool) (s : t) := Raw.for_all f s.
+ Definition for_all_1 (s : t) := Raw.for_all_1 (s:=s).
+ Definition for_all_2 (s : t) := Raw.for_all_2 (s:=s).
+
+ Definition exists_ (f : elt -> bool) (s : t) := Raw.exists_ f s.
+ Definition exists_1 (s : t) := Raw.exists_1 (s:=s).
+ Definition exists_2 (s : t) := Raw.exists_2 (s:=s).
+
+ Definition partition (f : elt -> bool) (s : t) :=
+ let p := Raw.partition f s in
+ (Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f),
+ Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)).
+ Definition partition_1 (s : t) := Raw.partition_1 s.
+ Definition partition_2 (s : t) := Raw.partition_2 s.
+
+ Definition eq (s s' : t) := Raw.eq s s'.
+ Definition eq_refl (s : t) := Raw.eq_refl s.
+ Definition eq_sym (s s' : t) := Raw.eq_sym (s:=s) (s':=s').
+ Definition eq_trans (s s' s'' : t) :=
+ Raw.eq_trans (s:=s) (s':=s') (s'':=s'').
+
+ Definition lt (s s' : t) := Raw.lt s s'.
+ Definition lt_trans (s s' s'' : t) :=
+ Raw.lt_trans (s:=s) (s':=s') (s'':=s'').
+ Definition lt_not_eq (s s' : t) := Raw.lt_not_eq (sorted s) (sorted s').
+
+ Definition compare : forall s s' : t, Compare lt eq s s'.
+ Proof.
+ intros; elim (Raw.compare (sorted s) (sorted s'));
+ [ constructor 1 | constructor 2 | constructor 3 ];
+ auto.
+ Defined.
+
+End Make.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 21:23:36 +0000