Library Stdlib.MSets.MSetInterface
Finite set library
- the lack of iter function, useless since Coq is purely functional
- the use of option types instead of Not_found exceptions
- the use of nat instead of int for the cardinal function
- WSetsOn : functorial signature for weak sets
- WSets : self-contained version of WSets
- SetsOn : functorial signature for ordered sets
- Sets : self-contained version of Sets
- WRawSets : a signature for weak sets that may be ill-formed
- RawSets : same for ordered sets
Require Export Bool SetoidList RelationClasses Morphisms
RelationPairs Equalities Orders OrdersFacts.
Set Implicit Arguments.
Module Type TypElt.
Parameters t elt : Type.
End TypElt.
Module Type HasWOps (Import T:TypElt).
Parameter empty : t.
The empty set.
Test whether a set is empty or not.
mem x s tests whether x belongs to the set s.
add x s returns a set containing all elements of s,
plus x. If x was already in s, s is returned unchanged.
singleton x returns the one-element set containing only x.
remove x s returns a set containing all elements of s,
except x. If x was not in s, s is returned unchanged.
Set union.
Set intersection.
Set difference.
equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
subset s1 s2 tests whether the set s1 is a subset of
the set s2.
fold f s a computes (f xN ... (f x2 (f x1 a))...),
where x1 ... xN are the elements of s.
The order in which elements of s are presented to f is
unspecified.
for_all p s checks if all elements of the set
satisfy the predicate p.
exists p s checks if at least one element of
the set satisfies the predicate p.
filter p s returns the set of all elements in s
that satisfy predicate p.
partition p s returns a pair of sets (s1, s2), where
s1 is the set of all the elements of s that satisfy the
predicate p, and s2 is the set of all the elements of
s that do not satisfy p.
Return the number of elements of a set.
Return the list of all elements of the given set, in any order.
Return one element of the given set, or None if
the set is empty. Which element is chosen is unspecified.
Equal sets could return different elements.
the abstract type of sets
Functorial signature for weak sets
First, we ask for all the functions
Logical predicates
Parameter In : elt -> t -> Prop.
#[global]
Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
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.
Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Definition eq : t -> t -> Prop := Equal.
Include IsEq.
#[global]
Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
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.
Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Definition eq : t -> t -> Prop := Equal.
Include IsEq.
eq is obviously an equivalence, for subtyping only
Specifications of set operators
Section Spec.
Variable s s': t.
Variable x y : elt.
Variable f : elt -> bool.
Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).
Parameter mem_spec : mem x s = true <-> In x s.
Parameter equal_spec : equal s s' = true <-> s[=]s'.
Parameter subset_spec : subset s s' = true <-> s[<=]s'.
Parameter empty_spec : Empty empty.
Parameter is_empty_spec : is_empty s = true <-> Empty s.
Parameter add_spec : In y (add x s) <-> E.eq y x \/ In y s.
Parameter remove_spec : In y (remove x s) <-> In y s /\ ~E.eq y x.
Parameter singleton_spec : In y (singleton x) <-> E.eq y x.
Parameter union_spec : In x (union s s') <-> In x s \/ In x s'.
Parameter inter_spec : In x (inter s s') <-> In x s /\ In x s'.
Parameter diff_spec : In x (diff s s') <-> In x s /\ ~In x s'.
Parameter fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (flip f) (elements s) i.
Parameter cardinal_spec : cardinal s = length (elements s).
Parameter filter_spec : compatb f ->
(In x (filter f s) <-> In x s /\ f x = true).
Parameter for_all_spec : compatb f ->
(for_all f s = true <-> For_all (fun x => f x = true) s).
Parameter exists_spec : compatb f ->
(exists_ f s = true <-> Exists (fun x => f x = true) s).
Parameter partition_spec1 : compatb f ->
fst (partition f s) [=] filter f s.
Parameter partition_spec2 : compatb f ->
snd (partition f s) [=] filter (fun x => negb (f x)) s.
Parameter elements_spec1 : InA E.eq x (elements s) <-> In x s.
When compared with ordered sets, here comes the only
property that is really weaker:
Parameter elements_spec2w : NoDupA E.eq (elements s).
Parameter choose_spec1 : choose s = Some x -> In x s.
Parameter choose_spec2 : choose s = None -> Empty s.
End Spec.
End WSetsOn.
Parameter choose_spec1 : choose s = Some x -> In x s.
Parameter choose_spec2 : choose s = None -> Empty s.
End Spec.
End WSetsOn.
Static signature for weak sets
Functorial signature for sets on ordered elements
Total ordering between sets. Can be used as the ordering function
for doing sets of sets.
Return the smallest element of the given set
(with respect to the E.compare ordering),
or None if the set is empty.
Same as min_elt, but returns the largest element of the
given set.
End HasOrdOps.
Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps.
Module Type SetsOn (E : OrderedType).
Include WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
Section Spec.
Variable s s': t.
Variable x y : elt.
Parameter compare_spec : CompSpec eq lt s s' (compare s s').
Additional specification of elements
Remark: since fold is specified via elements, this stronger
specification of elements has an indirect impact on fold,
which can now be proved to receive elements in increasing order.
Parameter min_elt_spec1 : min_elt s = Some x -> In x s.
Parameter min_elt_spec2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
Parameter min_elt_spec3 : min_elt s = None -> Empty s.
Parameter max_elt_spec1 : max_elt s = Some x -> In x s.
Parameter max_elt_spec2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
Parameter max_elt_spec3 : max_elt s = None -> Empty s.
Additional specification of choose
Parameter choose_spec3 : choose s = Some x -> choose s' = Some y ->
Equal s s' -> E.eq x y.
End Spec.
End SetsOn.
Equal s s' -> E.eq x y.
End Spec.
End SetsOn.
Static signature for sets on ordered elements
Module Type Sets.
Declare Module E : OrderedType.
Include SetsOn E.
End Sets.
Module Type S := Sets.
Some subtyping tests
WSetsOn ---> WSets | | | | V V SetsOn ---> Sets Module S_WS (M : Sets) <: WSets := M. Module Sfun_WSfun (E:OrderedType)(M : SetsOn E) <: WSetsOn E := M. Module S_Sfun (M : Sets) <: SetsOn M.E := M. Module WS_WSfun (M : WSets) <: WSetsOn M.E := M.
Signatures for set representations with ill-formed values.
- A first module deals with the datatype (eg. list or tree) without
- A second module implements the exact Sets interface by
First, we ask for all the functions
Is a set well-formed or ill-formed ?
In order to be able to validate (at least some) particular sets as
well-formed, we ask for a boolean function for (semi-)deciding
predicate Ok. If Ok isn't decidable, isok may be the
always-false function.
MS:
Dangerous instance, the isok s = true hypothesis cannot be discharged
with typeclass resolution. Is it really an instance?
Logical predicates
Parameter In : elt -> t -> Prop.
#[global]
Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
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.
Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Definition eq : t -> t -> Prop := Equal.
#[global]
Declare Instance eq_equiv : Equivalence eq.
#[global]
Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
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.
Notation "s [=] t" := (Equal s t) (at level 70, no associativity).
Notation "s [<=] t" := (Subset s t) (at level 70, no associativity).
Definition eq : t -> t -> Prop := Equal.
#[global]
Declare Instance eq_equiv : Equivalence eq.
First, all operations are compatible with the well-formed predicate.
#[global]
Declare Instance empty_ok : Ok empty.
#[global]
Declare Instance add_ok s x `(Ok s) : Ok (add x s).
#[global]
Declare Instance remove_ok s x `(Ok s) : Ok (remove x s).
#[global]
Declare Instance singleton_ok x : Ok (singleton x).
#[global]
Declare Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
#[global]
Declare Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
#[global]
Declare Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
#[global]
Declare Instance filter_ok s f `(Ok s) : Ok (filter f s).
#[global]
Declare Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
#[global]
Declare Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
Now, the specifications, with constraints on the input sets.
Section Spec.
Variable s s': t.
Variable x y : elt.
Variable f : elt -> bool.
Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).
Parameter mem_spec : forall `{Ok s}, mem x s = true <-> In x s.
Parameter equal_spec : forall `{Ok s, Ok s'},
equal s s' = true <-> s[=]s'.
Parameter subset_spec : forall `{Ok s, Ok s'},
subset s s' = true <-> s[<=]s'.
Parameter empty_spec : Empty empty.
Parameter is_empty_spec : is_empty s = true <-> Empty s.
Parameter add_spec : forall `{Ok s},
In y (add x s) <-> E.eq y x \/ In y s.
Parameter remove_spec : forall `{Ok s},
In y (remove x s) <-> In y s /\ ~E.eq y x.
Parameter singleton_spec : In y (singleton x) <-> E.eq y x.
Parameter union_spec : forall `{Ok s, Ok s'},
In x (union s s') <-> In x s \/ In x s'.
Parameter inter_spec : forall `{Ok s, Ok s'},
In x (inter s s') <-> In x s /\ In x s'.
Parameter diff_spec : forall `{Ok s, Ok s'},
In x (diff s s') <-> In x s /\ ~In x s'.
Parameter fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (flip f) (elements s) i.
Parameter cardinal_spec : forall `{Ok s},
cardinal s = length (elements s).
Parameter filter_spec : compatb f ->
(In x (filter f s) <-> In x s /\ f x = true).
Parameter for_all_spec : compatb f ->
(for_all f s = true <-> For_all (fun x => f x = true) s).
Parameter exists_spec : compatb f ->
(exists_ f s = true <-> Exists (fun x => f x = true) s).
Parameter partition_spec1 : compatb f ->
fst (partition f s) [=] filter f s.
Parameter partition_spec2 : compatb f ->
snd (partition f s) [=] filter (fun x => negb (f x)) s.
Parameter elements_spec1 : InA E.eq x (elements s) <-> In x s.
Parameter elements_spec2w : forall `{Ok s}, NoDupA E.eq (elements s).
Parameter choose_spec1 : choose s = Some x -> In x s.
Parameter choose_spec2 : choose s = None -> Empty s.
End Spec.
End WRawSets.
From weak raw sets to weak usual sets
We avoid creating induction principles for the Record
Definition elt := E.t.
Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
Definition t := t_.
Arguments Mkt this {is_ok}.
#[global]
Hint Resolve is_ok : typeclass_instances.
Definition In (x : elt)(s : t) := M.In x (this s).
Definition Equal (s s' : t) := forall a : elt, In a s <-> In a s'.
Definition Subset (s s' : t) := forall a : elt, In a s -> In a s'.
Definition Empty (s : t) := forall a : elt, ~ In a s.
Definition For_all (P : elt -> Prop)(s : t) := forall x, In x s -> P x.
Definition Exists (P : elt -> Prop)(s : t) := exists x, In x s /\ P x.
Definition mem (x : elt)(s : t) := M.mem x s.
Definition add (x : elt)(s : t) : t := Mkt (M.add x s).
Definition remove (x : elt)(s : t) : t := Mkt (M.remove x s).
Definition singleton (x : elt) : t := Mkt (M.singleton x).
Definition union (s s' : t) : t := Mkt (M.union s s').
Definition inter (s s' : t) : t := Mkt (M.inter s s').
Definition diff (s s' : t) : t := Mkt (M.diff s s').
Definition equal (s s' : t) := M.equal s s'.
Definition subset (s s' : t) := M.subset s s'.
Definition empty : t := Mkt M.empty.
Definition is_empty (s : t) := M.is_empty s.
Definition elements (s : t) : list elt := M.elements s.
Definition choose (s : t) : option elt := M.choose s.
Definition fold (A : Type)(f : elt -> A -> A)(s : t) : A -> A := M.fold f s.
Definition cardinal (s : t) := M.cardinal s.
Definition filter (f : elt -> bool)(s : t) : t := Mkt (M.filter f s).
Definition for_all (f : elt -> bool)(s : t) := M.for_all f s.
Definition exists_ (f : elt -> bool)(s : t) := M.exists_ f s.
Definition partition (f : elt -> bool)(s : t) : t * t :=
let p := M.partition f s in (Mkt (fst p), Mkt (snd p)).
#[global]
Instance In_compat : Proper (E.eq==>eq==>iff) In.
Definition eq : t -> t -> Prop := Equal.
#[global]
Instance eq_equiv : Equivalence eq.
Definition eq_dec : forall (s s':t), { eq s s' }+{ ~eq s s' }.
Section Spec.
Variable s s' : t.
Variable x y : elt.
Variable f : elt -> bool.
Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).
Lemma mem_spec : mem x s = true <-> In x s.
Lemma equal_spec : equal s s' = true <-> Equal s s'.
Lemma subset_spec : subset s s' = true <-> Subset s s'.
Lemma empty_spec : Empty empty.
Lemma is_empty_spec : is_empty s = true <-> Empty s.
Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s.
Lemma remove_spec : In y (remove x s) <-> In y s /\ ~E.eq y x.
Lemma singleton_spec : In y (singleton x) <-> E.eq y x.
Lemma union_spec : In x (union s s') <-> In x s \/ In x s'.
Lemma inter_spec : In x (inter s s') <-> In x s /\ In x s'.
Lemma diff_spec : In x (diff s s') <-> In x s /\ ~In x s'.
Lemma fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Lemma cardinal_spec : cardinal s = length (elements s).
Lemma filter_spec : compatb f ->
(In x (filter f s) <-> In x s /\ f x = true).
Lemma for_all_spec : compatb f ->
(for_all f s = true <-> For_all (fun x => f x = true) s).
Lemma exists_spec : compatb f ->
(exists_ f s = true <-> Exists (fun x => f x = true) s).
Lemma partition_spec1 : compatb f -> Equal (fst (partition f s)) (filter f s).
Lemma partition_spec2 : compatb f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
Lemma elements_spec1 : InA E.eq x (elements s) <-> In x s.
Lemma elements_spec2w : NoDupA E.eq (elements s).
Lemma choose_spec1 : choose s = Some x -> In x s.
Lemma choose_spec2 : choose s = None -> Empty s.
End Spec.
End WRaw2SetsOn.
Module WRaw2Sets (D:DecidableType)(M:WRawSets D) <: WSets with Module E := D.
Module E := D.
Include WRaw2SetsOn D M.
End WRaw2Sets.
Same approach for ordered sets
Module Type RawSets (E : OrderedType).
Include WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.
Section Spec.
Variable s s': t.
Variable x y : elt.
Specification of compare
Additional specification of elements
Specification of min_elt
Parameter min_elt_spec1 : min_elt s = Some x -> In x s.
Parameter min_elt_spec2 : forall `{Ok s}, min_elt s = Some x -> In y s -> ~ E.lt y x.
Parameter min_elt_spec3 : min_elt s = None -> Empty s.
Parameter min_elt_spec2 : forall `{Ok s}, min_elt s = Some x -> In y s -> ~ E.lt y x.
Parameter min_elt_spec3 : min_elt s = None -> Empty s.
Specification of max_elt
Parameter max_elt_spec1 : max_elt s = Some x -> In x s.
Parameter max_elt_spec2 : forall `{Ok s}, max_elt s = Some x -> In y s -> ~ E.lt x y.
Parameter max_elt_spec3 : max_elt s = None -> Empty s.
Parameter max_elt_spec2 : forall `{Ok s}, max_elt s = Some x -> In y s -> ~ E.lt x y.
Parameter max_elt_spec3 : max_elt s = None -> Empty s.
Additional specification of choose
Parameter choose_spec3 : forall `{Ok s, Ok s'},
choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.
End Spec.
End RawSets.
choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.
End Spec.
End RawSets.
From Raw to usual sets
Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
Include WRaw2SetsOn O M.
Definition compare (s s':t) := M.compare s s'.
Definition min_elt (s:t) : option elt := M.min_elt s.
Definition max_elt (s:t) : option elt := M.max_elt s.
Definition lt (s s':t) := M.lt s s'.
Specification of lt
#[global]
Instance lt_strorder : StrictOrder lt.
#[global]
Instance lt_compat : Proper (eq==>eq==>iff) lt.
Section Spec.
Variable s s' s'' : t.
Variable x y : elt.
Lemma compare_spec : CompSpec eq lt s s' (compare s s').
Instance lt_strorder : StrictOrder lt.
#[global]
Instance lt_compat : Proper (eq==>eq==>iff) lt.
Section Spec.
Variable s s' s'' : t.
Variable x y : elt.
Lemma compare_spec : CompSpec eq lt s s' (compare s s').
Additional specification of elements
Specification of min_elt
Lemma min_elt_spec1 : min_elt s = Some x -> In x s.
Lemma min_elt_spec2 : min_elt s = Some x -> In y s -> ~ O.lt y x.
Lemma min_elt_spec3 : min_elt s = None -> Empty s.
Lemma min_elt_spec2 : min_elt s = Some x -> In y s -> ~ O.lt y x.
Lemma min_elt_spec3 : min_elt s = None -> Empty s.
Specification of max_elt
Lemma max_elt_spec1 : max_elt s = Some x -> In x s.
Lemma max_elt_spec2 : max_elt s = Some x -> In y s -> ~ O.lt x y.
Lemma max_elt_spec3 : max_elt s = None -> Empty s.
Lemma max_elt_spec2 : max_elt s = Some x -> In y s -> ~ O.lt x y.
Lemma max_elt_spec3 : max_elt s = None -> Empty s.
Additional specification of choose
Lemma choose_spec3 :
choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y.
End Spec.
End Raw2SetsOn.
Module Raw2Sets (O:OrderedType)(M:RawSets O) <: Sets with Module E := O.
Module E := O.
Include Raw2SetsOn O M.
End Raw2Sets.
choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y.
End Spec.
End Raw2SetsOn.
Module Raw2Sets (O:OrderedType)(M:RawSets O) <: Sets with Module E := O.
Module E := O.
Include Raw2SetsOn O M.
End Raw2Sets.
It is in fact possible to provide an ordering on sets with
very little information on them (more or less only the In
predicate). This generic build of ordering is in fact not
used for the moment, we rather use a simpler version
dedicated to sets-as-sorted-lists, see MakeListOrdering.
Module Type IN (O:OrderedType).
Parameter Inline t : Type.
Parameter Inline In : O.t -> t -> Prop.
#[global]
Declare Instance In_compat : Proper (O.eq==>eq==>iff) In.
Definition Equal s s' := forall x, In x s <-> In x s'.
Definition Empty s := forall x, ~In x s.
End IN.
Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
Module Import MO := OrderedTypeFacts O.
Definition eq : t -> t -> Prop := Equal.
#[global]
Instance eq_equiv : Equivalence eq.
#[global]
Instance : Proper (O.eq==>eq==>iff) In.
Definition Below x s := forall y, In y s -> O.lt y x.
Definition Above x s := forall y, In y s -> O.lt x y.
Definition EquivBefore x s s' :=
forall y, O.lt y x -> (In y s <-> In y s').
Definition EmptyBetween x y s :=
forall z, In z s -> O.lt z y -> O.lt z x.
Definition lt s s' := exists x, EquivBefore x s s' /\
((In x s' /\ Below x s) \/
(In x s /\ exists y, In y s' /\ O.lt x y /\ EmptyBetween x y s')).
#[global]
Instance : Proper (O.eq==>eq==>eq==>iff) EquivBefore.
#[global]
Instance : Proper (O.eq==>eq==>iff) Below.
#[global]
Instance : Proper (O.eq==>eq==>iff) Above.
#[global]
Instance : Proper (O.eq==>O.eq==>eq==>iff) EmptyBetween.
#[global]
Instance lt_compat : Proper (eq==>eq==>iff) lt.
#[global]
Instance lt_strorder : StrictOrder lt.
Lemma lt_empty_r : forall s s', Empty s' -> ~ lt s s'.
Definition Add x s s' := forall y, In y s' <-> O.eq x y \/ In y s.
Lemma lt_empty_l : forall x s1 s2 s2',
Empty s1 -> Above x s2 -> Add x s2 s2' -> lt s1 s2'.
Lemma lt_add_lt : forall x1 x2 s1 s1' s2 s2',
Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' ->
O.lt x1 x2 -> lt s1' s2'.
Lemma lt_add_eq : forall x1 x2 s1 s1' s2 s2',
Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' ->
O.eq x1 x2 -> lt s1 s2 -> lt s1' s2'.
End MakeSetOrdering.
Module MakeListOrdering (O:OrderedType).
Module MO:=OrderedTypeFacts O.
Local Notation t := (list O.t).
Local Notation In := (InA O.eq).
Definition eq s s' := forall x, In x s <-> In x s'.
#[global]
Instance eq_equiv : Equivalence eq := _.
Inductive lt_list : t -> t -> Prop :=
| lt_nil : forall x s, lt_list nil (x :: s)
| lt_cons_lt : forall x y s s',
O.lt x y -> lt_list (x :: s) (y :: s')
| lt_cons_eq : forall x y s s',
O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s').
#[global]
Hint Constructors lt_list : core.
Definition lt := lt_list.
#[global]
Hint Unfold lt : core.
#[global]
Instance lt_strorder : StrictOrder lt.
#[global]
Instance lt_compat' :
Proper (eqlistA O.eq==>eqlistA O.eq==>iff) lt.
Lemma eq_cons :
forall l1 l2 x y,
O.eq x y -> eq l1 l2 -> eq (x :: l1) (y :: l2).
#[global]
Hint Resolve eq_cons : core.
Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.
#[global]
Hint Resolve cons_CompSpec : core.
End MakeListOrdering.