Library Coq.MSets.MSetPositive
Efficient implementation of
MSetInterface.S for positive keys,
inspired from the
FMapPositive module.
This module was adapted by Alexandre Ren, Damien Pous, and Thomas
Braibant (2010, LIG, CNRS, UMR 5217), from the
FMapPositive
module of Pierre Letouzey and Jean-Christophe Filliâtre, which in
turn comes from the
FMap framework of a work by Xavier Leroy and
Sandrine Blazy (used for building certified compilers).
Require Import Bool BinPos Orders MSetInterface.
Set Implicit Arguments.
Local Open Scope lazy_bool_scope.
Local Open Scope positive_scope.
LocalLocalLocal
Even if positive can be seen as an ordered type with respect to the
usual order (see above), we can also use a lexicographic order over bits
(lower bits are considered first). This is more natural when using
positive as indexes for sets or maps (see FSetPositive and FMapPositive.
Module PositiveOrderedTypeBits <:
UsualOrderedType.
Definition t:=
positive.
Include HasUsualEq <+
UsualIsEq.
Definition eqb :=
Pos.eqb.
Definition eqb_eq :=
Pos.eqb_eq.
Include HasEqBool2Dec.
Fixpoint bits_lt (
p q:
positive) :
Prop :=
match p,
q with
|
xH,
xI _ =>
True
|
xH,
_ =>
False
|
xO p,
xO q =>
bits_lt p q
|
xO _,
_ =>
True
|
xI p,
xI q =>
bits_lt p q
|
xI _,
_ =>
False
end.
Definition lt:=
bits_lt.
Lemma bits_lt_antirefl :
forall x :
positive,
~ bits_lt x x.
Lemma bits_lt_trans :
forall x y z :
positive,
bits_lt x y ->
bits_lt y z ->
bits_lt x z.
Instance lt_compat :
Proper (
eq==>eq==>iff)
lt.
Instance lt_strorder :
StrictOrder lt.
Fixpoint compare x y :=
match x,
y with
|
x~1,
y~1 =>
compare x y
|
x~1,
_ =>
Gt
|
x~0,
y~0 =>
compare x y
|
x~0,
_ =>
Lt
| 1,
y~1 =>
Lt
| 1, 1 =>
Eq
| 1,
y~0 =>
Gt
end.
Lemma compare_spec :
forall x y,
CompSpec eq lt x y (
compare x y).
End PositiveOrderedTypeBits.
Module PositiveSet <:
S with Module E:=
PositiveOrderedTypeBits.
Module E:=
PositiveOrderedTypeBits.
Definition elt :=
positive.
Inductive tree :=
|
Leaf :
tree
|
Node :
tree ->
bool ->
tree ->
tree.
Scheme tree_ind :=
Induction for tree Sort Prop.
Definition t :=
tree.
Definition empty :=
Leaf.
Fixpoint is_empty (
m :
t) :
bool :=
match m with
|
Leaf =>
true
|
Node l b r =>
negb b &&& is_empty l &&& is_empty r
end.
Fixpoint mem (
i :
positive) (
m :
t) :
bool :=
match m with
|
Leaf =>
false
|
Node l o r =>
match i with
| 1 =>
o
|
i~0 =>
mem i l
|
i~1 =>
mem i r
end
end.
Fixpoint add (
i :
positive) (
m :
t) :
t :=
match m with
|
Leaf =>
match i with
| 1 =>
Node Leaf true Leaf
|
i~0 =>
Node (
add i Leaf)
false Leaf
|
i~1 =>
Node Leaf false (
add i Leaf)
end
|
Node l o r =>
match i with
| 1 =>
Node l true r
|
i~0 =>
Node (
add i l)
o r
|
i~1 =>
Node l o (
add i r)
end
end.
Definition singleton i :=
add i empty.
helper function to avoid creating empty trees that are not leaves
reverses y and concatenate it with x
the additional argument, i, records the current path, in
reverse order (this should be more efficient: we reverse this argument
only at present nodes only, rather than at each node of the tree).
we also use this convention in all functions below
uses a to accumulate values rather than doing a lot of concatenations
would it be more efficient to use a path like in the above functions ?
lexicographic product, defined using a notation to keep things lazy
Notation lex u v :=
match u with Eq =>
v |
Lt =>
Lt |
Gt =>
Gt end.
Definition compare_bool a b :=
match a,
b with
|
false,
true =>
Lt
|
true,
false =>
Gt
|
_,
_ =>
Eq
end.
Fixpoint compare (
m m':
t):
comparison :=
match m,
m' with
|
Leaf,
_ =>
if is_empty m' then Eq else Lt
|
_,
Leaf =>
if is_empty m then Eq else Gt
|
Node l o r,
Node l' o' r' =>
lex (
compare_bool o o') (
lex (
compare l l') (
compare r r'))
end.
Definition In i t :=
mem i t = true.
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 :=
Equal.
Definition lt m m' :=
compare m m' = Lt.
Specification of In
Specification of eq
Specification of mem
Additional lemmas for mem
Specification of empty
Specification of node
Specification of is_empty
Specification of subset
Specification of equal (via subset)
(Specified) definition of compare
Lemma lex_Opp:
forall u v u' v',
u = CompOpp u' ->
v = CompOpp v' ->
lex u v = CompOpp (
lex u' v').
Lemma compare_bool_inv:
forall b b',
compare_bool b b' = CompOpp (
compare_bool b' b).
Lemma compare_inv:
forall s s',
compare s s' = CompOpp (
compare s' s).
Lemma lex_Eq:
forall u v,
lex u v = Eq <-> u=Eq /\ v=Eq.
Lemma compare_bool_Eq:
forall b1 b2,
compare_bool b1 b2 = Eq <-> eqb b1 b2 = true.
Lemma compare_equal:
forall s s',
compare s s' = Eq <-> equal s s' = true.
Lemma compare_gt:
forall s s',
compare s s' = Gt ->
lt s' s.
Lemma compare_eq:
forall s s',
compare s s' = Eq ->
eq s s'.
Lemma compare_spec :
forall s s' :
t,
CompSpec eq lt s s' (
compare s s').
Section lt_spec.
Inductive ct:
comparison ->
comparison ->
comparison ->
Prop :=
|
ct_xxx:
forall x,
ct x x x
|
ct_xex:
forall x,
ct x Eq x
|
ct_exx:
forall x,
ct Eq x x
|
ct_glx:
forall x,
ct Gt Lt x
|
ct_lgx:
forall x,
ct Lt Gt x.
Lemma ct_cxe:
forall x,
ct (
CompOpp x)
x Eq.
Lemma ct_xce:
forall x,
ct x (
CompOpp x)
Eq.
Lemma ct_lxl:
forall x,
ct Lt x Lt.
Lemma ct_gxg:
forall x,
ct Gt x Gt.
Lemma ct_xll:
forall x,
ct x Lt Lt.
Lemma ct_xgg:
forall x,
ct x Gt Gt.
Local Hint Constructors ct:
ct.
Local Hint Resolve ct_cxe ct_xce ct_lxl ct_xll ct_gxg ct_xgg:
ct.
Ltac ct :=
trivial with ct.
Lemma ct_lex:
forall u v w u' v' w',
ct u v w ->
ct u' v' w' ->
ct (
lex u u') (
lex v v') (
lex w w').
Lemma ct_compare_bool:
forall a b c,
ct (
compare_bool a b) (
compare_bool b c) (
compare_bool a c).
Lemma compare_x_Leaf:
forall s,
compare s Leaf = if is_empty s then Eq else Gt.
Lemma compare_empty_x:
forall a,
is_empty a = true ->
forall b,
compare a b = if is_empty b then Eq else Lt.
Lemma compare_x_empty:
forall a,
is_empty a = true ->
forall b,
compare b a = if is_empty b then Eq else Gt.
Lemma ct_compare:
forall a b c,
ct (
compare a b) (
compare b c) (
compare a c).
End lt_spec.
Instance lt_strorder :
StrictOrder lt.
Local Instance compare_compat_1 :
Proper (
eq==>Logic.eq==>Logic.eq)
compare.
Instance compare_compat :
Proper (
eq==>eq==>Logic.eq)
compare.
Local Instance lt_compat :
Proper (
eq==>eq==>iff)
lt.
Specification of add
Specification of remove
Specification of singleton
Specification of union
Specification of inter
Specification of diff
Specification of fold
Specification of cardinal
Specification of filter
Specification of for_all
Specification of exists
Specification of partition
Specification of elements
Specification of choose
Specification of min_elt
Specification of max_elt