Timings for MSetList.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./MSets/MSetList.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./MSets/MSetList.timing
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** * Finite sets library *)
(** This file proposes an implementation of the non-dependent
interface [MSetInterface.S] using strictly ordered list. *)
Require Export MSetInterface OrdersFacts OrdersLists.
(** * 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 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 : 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' :=
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.
Module MakeRaw (X: OrderedType) <: RawSets X.
Module Import MX := OrderedTypeFacts X.
Module Import ML := OrderedTypeLists X.
(** ** Proofs of set operation specifications. *)
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).
Existing Instance X.eq_equiv.
#[local]
Hint Extern 20 => solve [order] : core.
Definition IsOk s := Sort s.
Class Ok (s:t) : Prop := ok : Sort s.
#[local]
Hint Resolve ok : core.
#[local]
Hint Unfold Ok : core.
Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
Lemma inf_iff : forall x l, Inf x l <-> inf x l = true.
intros x l; split; intro H.
rewrite <- compare_lt_iff in H; rewrite H; reflexivity.
destruct l as [|y ys]; simpl in *.
revert H; case_eq (X.compare x y); try discriminate; [].
rewrite compare_lt_iff in Ha.
Lemma isok_iff : forall l, sort X.lt l <-> Ok l.
change (inf y ys && isok ys = true).
rewrite andb_true_iff; tauto.
change (inf x xs && isok xs = true) in H.
rewrite andb_true_iff, <- inf_iff in H.
destruct H; constructor; tauto.
#[local]
Hint Extern 1 (Ok _) => rewrite <- isok_iff : core.
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.
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.
induction s; intros x Hs; inv; simpl.
elim_compare x a; rewrite InA_cons; intuition; try order.
Lemma add_inf :
forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s).
simple induction s; simpl.
intros; elim_compare x a; inv; intuition.
#[local]
Hint Resolve add_inf : core.
Global Instance add_ok s x : forall `(Ok s), Ok (add x s).
repeat rewrite <- isok_iff; revert s x.
simple induction s; simpl.
intros; elim_compare x a; inv; auto.
Lemma add_spec :
forall (s : t) (x y : elt) (Hs : Ok s),
In y (add x s) <-> X.eq y x \/ In y s.
induction s; simpl; intros.
elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
Lemma remove_inf :
forall (s : t) (x a : elt) (Hs : Ok s), Inf a s -> Inf a (remove x s).
intros; elim_compare x a; inv; auto.
apply Inf_lt with a; auto.
#[local]
Hint Resolve remove_inf : core.
Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).
repeat rewrite <- isok_iff; revert s x.
intros; elim_compare x a; inv; auto.
Lemma remove_spec :
forall (s : t) (x y : elt) (Hs : Ok s),
In y (remove x s) <-> In y s /\ ~X.eq y x.
induction s; simpl; intros.
elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition;
try sort_inf_in; try order.
Global Instance singleton_ok x : Ok (singleton x).
unfold singleton; simpl; auto.
Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.
unfold singleton; simpl; split; intros; inv; auto.
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').
#[local]
Hint Resolve union_inf : core.
Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
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; order.
change (Inf x' (union (x :: l) l')); auto.
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'.
induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
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').
apply Inf_lt with x; auto.
apply Inf_lt with x'; auto.
#[local]
Hint Resolve inter_inf : core.
Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').
repeat rewrite <- isok_iff; revert s s'.
apply Inf_eq with x'; auto; apply inter_inf; auto; apply Inf_eq with x; auto.
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'.
induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
try sort_inf_in; try order.
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').
intros s s'; repeat rewrite <- isok_iff; revert s s'.
apply Inf_lt with x; auto.
apply Inf_lt with x'; auto.
apply Inf_lt with x'; auto.
#[local]
Hint Resolve diff_inf : core.
Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').
repeat rewrite <- isok_iff; revert s s'.
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'.
induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
try sort_inf_in; try order.
right; intuition; inv; auto.
Lemma equal_spec :
forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
equal s s' = true <-> Equal s s'.
induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl.
assert (In x' nil) by (rewrite H; auto).
assert (In x nil) by (rewrite <-H; auto).
elim_compare x x' as C; try discriminate.
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.
assert (In x (x'::s')) by (rewrite <- E; auto).
inv; try sort_inf_in; order.
assert (In x' (x::s)) by (rewrite E; auto).
inv; try sort_inf_in; order.
Lemma subset_spec :
forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
subset s s' = true <-> Subset s s'.
induction s' as [ | x' s' IH]; intros [ | x s] Hs Hs'; simpl; auto.
split; try red; intros; auto.
assert (In x nil) by (apply H; auto).
split; try red; intros; auto.
split; intros S y; specialize (S y).
rewrite !InA_cons, C in S.
intuition; try sort_inf_in; order.
assert (In x (x'::s')) by (apply S; auto).
inv; try sort_inf_in; order.
split; intros S y; specialize (S y).
intuition; try sort_inf_in; order.
Global Instance empty_ok : Ok empty.
Lemma empty_spec : Empty empty.
unfold Empty, empty; intuition; inv.
Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.
Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.
Lemma elements_spec2 : forall (s : t) (Hs : Ok s), sort X.lt (elements s).
intro s; repeat rewrite <- isok_iff; auto.
Lemma elements_spec2w : forall (s : t) (Hs : Ok s), NoDupA X.eq (elements s).
intro s; repeat rewrite <- isok_iff; auto.
Lemma min_elt_spec1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.
destruct s; simpl; inversion 1; auto.
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.
induction s as [ | x s IH]; simpl; inversion 2; subst.
intros; inv; try sort_inf_in; order.
Lemma min_elt_spec3 : forall s : t, min_elt s = None -> Empty s.
destruct s; simpl; red; intuition.
Lemma max_elt_spec1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.
induction s as [ | x s IH].
inversion 1; subst; auto.
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.
induction s as [ | a s IH].
assert (~X.lt x b) by (apply IH; auto).
assert (X.lt a b) by auto.
Lemma max_elt_spec3 : forall s : t, max_elt s = None -> Empty s.
induction s as [ | a s IH].
intros; elim IH with b; auto.
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'.
unfold choose; intros s s' x x' Hs Hs' Hx Hx' H.
apply min_elt_spec2 with s'; auto.
rewrite <-H; auto using min_elt_spec1.
apply min_elt_spec2 with s; auto.
rewrite H; auto using min_elt_spec1.
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.
Lemma cardinal_spec :
forall (s : t) (Hs : Ok s),
cardinal s = length (elements s).
Lemma filter_inf :
forall (s : t) (x : elt) (f : elt -> bool) (Hs : Ok s),
Inf x s -> Inf x (filter f s).
simple induction s; simpl.
intros x l Hrec a f Hs Ha; inv.
apply Inf_lt with x; auto.
Global Instance filter_ok s f : forall `(Ok s), Ok (filter f s).
repeat rewrite <- isok_iff; revert s f.
simple induction s; simpl.
intros x l Hrec f Hs; inv.
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).
induction s; simpl; intros.
destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition.
setoid_replace x with a; auto.
setoid_replace a with x in F; auto; congruence.
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).
unfold For_all; induction s; simpl; intros.
setoid_replace x with a; auto.
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).
unfold Exists; induction s; simpl; intros.
setoid_replace a with x in F; auto; congruence.
Lemma partition_inf1 :
forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
Inf x s -> Inf x (fst (partition f s)).
intros s f x; repeat rewrite <- isok_iff; revert s f x.
simple induction s; simpl.
intros x l Hrec f a Hs Ha; inv.
case (f x); case (partition f l); simpl.
intros; apply H2; apply Inf_lt with x; auto.
Lemma partition_inf2 :
forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
Inf x s -> Inf x (snd (partition f s)).
intros s f x; repeat rewrite <- isok_iff; revert s f x.
simple induction s; simpl.
intros x l Hrec f a Hs Ha; inv.
case (f x); case (partition f l); simpl.
intros; apply H2; apply Inf_lt with x; auto.
Global Instance partition_ok1 s f : forall `(Ok s), Ok (fst (partition f s)).
repeat rewrite <- isok_iff; revert s f.
simple induction s; simpl.
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.
Global Instance partition_ok2 s f : forall `(Ok s), Ok (snd (partition f s)).
repeat rewrite <- isok_iff; revert s f.
simple induction s; simpl.
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.
Lemma partition_spec1 :
forall (s : t) (f : elt -> bool),
Proper (X.eq==>eq) f -> Equal (fst (partition f s)) (filter f s).
simple induction s; simpl; auto; unfold Equal.
generalize (Hrec f Hf); clear Hrec.
destruct (partition f l) as [s1 s2]; simpl; intros.
split; inversion_clear 1; auto.
constructor 2; rewrite <- H; auto.
constructor 2; rewrite H; auto.
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).
simple induction s; simpl; auto; unfold Equal.
generalize (Hrec f Hf); clear Hrec.
destruct (partition f l) as [s1 s2]; simpl; intros.
split; inversion_clear 1; auto.
constructor 2; rewrite <- H; auto.
constructor 2; rewrite H; auto.
Definition In := InA X.eq.
#[global]
Instance In_compat : Proper (X.eq==>eq==> iff) In.
repeat red; intros; rewrite H, H0; auto.
Module L := MakeListOrdering X.
Definition eq_equiv := L.eq_equiv.
Definition lt l1 l2 :=
exists l1' l2', Ok l1' /\ Ok l2' /\ eq l1 l1' /\ eq l2 l2' /\ L.lt l1' l2'.
#[global]
Instance lt_strorder : StrictOrder lt.
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 *.
apply (StrictOrder_Irreflexive s2); auto.
intros s1 s2 s3 (s1' & s2' & B1 & B2 & E1 & E2 & L12)
(s2'' & s3' & B2' & B3 & E2' & E3 & L23).
repeat rewrite <- isok_iff in *.
assert (eqlistA X.eq s2' s2'').
apply SortA_equivlistA_eqlistA with (ltA:=X.lt); auto using @ok with *.
#[global]
Instance lt_compat : Proper (eq==>eq==>iff) lt.
intros s1 s2 E12 s3 s4 E34.
intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
exists s1', s3'; do 2 (split; trivial).
intros (s1' & s3' & B1 & B3 & E1 & E3 & LT).
exists s1', s3'; do 2 (split; trivial).
Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
induction s as [|x s IH]; intros [|x' s']; simpl; intuition auto with relations.
Lemma compare_spec : forall s s', Ok s -> Ok s' ->
CompSpec eq lt s s' (compare s s').
destruct (compare_spec_aux s s'); constructor; auto.
exists s, s'; repeat split; auto using @ok.
exists s', s; repeat split; auto using @ok.
(** * 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.
(** For this specific implementation, eq coincides with Leibniz equality *)
Module Type OrderedTypeWithLeibniz.
Parameter eq_leibniz : forall x y, eq x y -> x = y.
End OrderedTypeWithLeibniz.
Module Type SWithLeibniz.
Declare Module E : OrderedTypeWithLeibniz.
Parameter eq_leibniz : forall x y, eq x y -> x = y.
Module MakeWithLeibniz (X: OrderedTypeWithLeibniz) <: SWithLeibniz with Module E := X.
Include Raw2SetsOn X Raw.
Lemma eq_leibniz_list : forall xs ys, eqlistA X.eq xs ys -> xs = ys.
induction xs as [|x xs]; intros [|y ys] H; inversion H; [ | ].
apply X.eq_leibniz; congruence.
apply IHxs; subst; assumption.
Lemma eq_leibniz : forall s s', eq s s' -> s = s'.
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.
apply Eqdep_dec.eq_proofs_unicity.
intros x y; destruct (bool_dec x y); tauto.