Module Sets
Require Import
Utf8
Coqlib String ToString Util
Maps ShareTree TreeAl AdomLib
Integers.
Local Unset Elimination Schemes.
Set Implicit Arguments.
Coercion is_true :
bool >->
Sortclass.
Definition orb_left (
x y:
bool) :
x →
x ||
y.
Proof.
now intros ->. Qed.
Definition orb_right (
x y:
bool) :
y →
x ||
y.
Proof.
Ltac bleft :=
apply orb_left.
Ltac bright :=
apply orb_right.
Module Type SET.
Parameter t :
Type.
Parameter elt :
Type.
Parameter union:
t ->
t ->
t.
Parameter inter:
t ->
t ->
t.
Parameter le :
t ->
t ->
bool.
Parameter empty:
t.
Parameter add:
elt ->
t ->
t.
Parameter mem :
elt ->
t ->
bool.
Parameter elements :
t ->
list elt.
Parameter fold :
forall (
A :
Type) (
f:
elt ->
A ->
A),
t ->
A ->
A.
Parameter le_spec :
forall s1 s2,
(
forall x,
mem x s1 ->
mem x s2) <->
le s1 s2 =
true.
Parameter mem_empty:
forall x, ~
mem x empty.
Parameter mem_add:
forall x y s,
mem x (
add y s) <->
mem x s \/
x =
y.
Parameter mem_union:
forall b s1 s2,
mem b (
union s1 s2) =
mem b s1 ||
mem b s2.
Parameter mem_inter:
forall b s1 s2,
mem b (
inter s1 s2) <->
mem b s1 /\
mem b s2.
Parameter elements_spec :
forall s x,
mem x s <->
List.In x (
elements s).
Parameter elements_norepet :
forall s,
list_norepet (
elements s).
Parameter fold_spec :
forall A f s a,
@
fold A f s a =
List.fold_right f a (
elements s).
Hint Resolve mem_union.
End SET.
Module SetOp (
S :
SET).
Definition build (
l:
list S.elt) :
S.t :=
List.fold_left (
fun a b =>
S.add b a)
l S.empty.
Lemma mem_build x l :
S.mem x (
build l) <->
In x l.
Proof.
Definition singleton x :=
S.add x S.empty.
Lemma mem_singleton :
forall x y,
S.mem x (
singleton y) <->
x =
y.
Proof.
Definition union_list (
l:
list S.t) :
S.t :=
List.fold_left S.union l S.empty.
Lemma In_union_list:
forall l b s,
List.In s l ->
S.mem b s ->
S.mem b (
union_list l).
Proof.
Instance toString `{
ToString S.elt} :
ToString S.t :=
{
to_string x :=
( "{ " ++
List.fold_left
(
fun a e =>
to_string e ++ "; " ++
a
)
(
S.elements x)
"}"
)%
string
}.
Local Instance Sleb :
leb_op S.t :=
S.le.
Local Instance Sjoin :
join_op S.t S.t :=
S.union.
Lemma elements_empty :
S.elements S.empty =
nil.
Proof.
Definition rem s x s' :
Prop :=
(∀
y,
S.mem y s → (
x =
y ∨
S.mem y s')) ∧
(∀
y,
S.mem y s' →
x ≠
y ∧
S.mem y s).
Lemma foldspec A f :
∀
P :
S.t →
A →
A →
Prop,
(∀
s s'
a b x,
S.mem x s →
rem s x s' →
P s'
a b →
P s a (
f x b)) →
∀
a, (∀
s, (∀
x, ¬
S.mem x s) →
P s a a) → ∀
s,
P s a (
S.fold f s a).
Proof.
intros P H a H0 s.
rewrite S.fold_spec.
generalize (
S.elements_norepet s).
generalize (
S.elements_spec s).
generalize (
S.elements s).
intros l.
revert s a H0.
induction l as [|
x l IH].
simpl.
intros s a H0 H1 H2.
apply H0.
intros x K.
apply (
proj1 (
H1 _)
K).
intros s a H0 H1 H2.
simpl.
apply (
H _ (
build l)).
apply H1.
left;
reflexivity.
split.
intros y H3.
specialize (
H1 y).
destruct (
proj1 H1 H3)
as [
X|
X].
auto.
right.
apply mem_build,
X.
inv H2;
auto.
intros y X.
split.
intros ->.
apply H5,
mem_build,
X.
specialize (
H1 y).
apply (
proj2 H1).
simpl.
right.
apply mem_build,
X.
apply IH.
auto.
intros y.
apply mem_build.
inv H2;
auto.
Qed.
Definition existsb (
f:
S.elt →
bool) (
s:
S.t) :
bool :=
S.fold (λ
x b,
b ||
f(
x))
s false.
Lemma existsb_exists f s :
existsb f s =
true ↔ (∃
x,
S.mem x s ∧
f x =
true).
Proof.
unfold existsb.
apply foldspec.
intros s0 s'
a b x IN [
H K] [
X Y].
destruct b;
simpl.
clear Y.
specialize (
X eq_refl).
destruct X as (
y &
IN' &
X).
split.
intros _.
exists y.
split;
auto.
apply K,
IN'.
reflexivity.
clear X.
split.
intros X.
exists x.
auto.
intros (
y &
INy &
Hy).
specialize (
H y INy).
intuition.
congruence.
refine (
false_not_true _ _).
apply Y.
eauto.
intros s0 H;
split.
intros X;
apply (
false_not_true X).
intros (
x &
X &
X').
eelim H;
eassumption.
Qed.
Corollary existsb_forall f s :
existsb f s =
false ↔ (∀
x,
S.mem x s →
f x =
false).
Proof.
destruct (
existsb_exists f s)
as [
A B].
destruct (
existsb f s);
split;
intros H.
eq_some_inv.
destruct (
A eq_refl)
as (
x &
IN &
X).
rewrite <-
X.
auto.
intros x IN.
destruct (
f x)
eqn:
E.
specialize (
B (
ex_intro _ x (
conj IN E))).
auto.
reflexivity.
reflexivity.
Qed.
Inductive classify_t :=
Empty |
Singleton (
v:
S.elt) |
Large.
Definition classify (
s:
S.t) :
classify_t :=
S.fold (λ
e a,
match a with Empty =>
Singleton e |
Singleton _ |
Large =>
Large end)
s Empty.
Lemma classify_correct s :
match classify s with
|
Empty => ∀
x, ¬
S.mem x s
|
Singleton e =>
S.mem e s ∧ ∀
x,
S.mem x s →
x =
e
|
Large => ∃
x y,
x ≠
y ∧
S.mem x s ∧
S.mem y s
end.
Proof.
unfold classify.
apply foldspec;
auto.
clear.
intros s s'
a [|
e|]
x Hxs [
H H0]
H1.
-
split.
assumption.
intros x'
H2.
destruct (
H _ H2);
auto.
elim (
H1 x');
assumption.
-
exists x,
e.
split; [|
split].
apply H0.
intuition.
easy.
apply H0;
intuition.
-
destruct H1 as (
y &
z &
Hyz &
Hy &
Hz).
destruct (
H0 _ Hy);
destruct (
H0 _ Hz);
vauto.
Qed.
Definition is_singleton (
s:
S.t) :
option S.elt :=
match classify s with Singleton e =>
Some e |
_ =>
None end.
Lemma is_singleton_correct s e :
is_singleton s =
Some e →
S.mem e s ∧ ∀
x,
S.mem x s →
x =
e.
Proof.
Definition map (
f:
S.elt →
S.elt) (
s:
S.t) :
S.t :=
S.fold (
fun k s =>
S.add (
f k)
s)
s S.empty.
Lemma map_in f (
s:
S.t) : ∀
x,
S.mem x s →
S.mem (
f x) (
map f s).
Proof.
unfold map.
intros.
apply or_introl with (
B:=
S.mem (
f x)
S.empty)
in H.
revert H.
apply foldspec;
intros.
-
apply S.mem_add.
destruct H2. 2:
now intuition.
destruct H0.
destruct (
H0 _ H2)
as [->|];
auto.
-
now firstorder.
Qed.
End SetOp.
Module Tree2Set (
T:
SHARETREE) <:
SET with Definition elt :=
T.elt.
Definition t :=
T.t unit.
Definition elt :=
T.elt.
Definition beq :
t ->
t ->
bool :=
T.beq (
fun _ _ =>
true).
Program Definition union (
x y:
t) :
t :=
T.shcombine (
fun _ a b =>
match a return _ with Some _ =>
a |
None =>
b end)
_ x y.
Next Obligation.
destruct v; auto. Qed.
Program Definition inter (
x y:
t) :
t :=
T.shcombine (
fun _ a b =>
match a return _ with Some _ =>
b |
None =>
a end)
_ x y.
Next Obligation.
destruct v; auto. Qed.
Definition mem (
v:
elt) (
x:
t) :
bool :=
match T.get v x with Some _ =>
true |
None =>
false end.
Program Definition le (
x y:
t) :
bool :=
T.shforall2 (
fun _ a b =>
match a,
b return _ with
|
None,
_ |
Some _,
Some _ =>
true
|
_,
_ =>
false
end)
_ x y.
Next Obligation.
destruct v; auto. Qed.
Definition elements (
x:
t) :
list elt :=
T.fold (
fun b v _ =>
v::
b)
x nil.
Definition empty :=
T.empty unit.
Definition add x s :=
T.set x tt s.
Definition rem x s :
t :=
T.remove x s.
Definition fold A (
f:
elt ->
A ->
A) :
t ->
A ->
A :=
T.fold (
fun a e _ =>
f e a).
Lemma le_spec :
forall s1 s2,
(
forall x,
mem x s1 ->
mem x s2) <->
le s1 s2 =
true.
Proof.
Lemma mem_empty:
forall x, ~
mem x empty.
Proof.
Lemma mem_add:
forall x y s,
mem x (
add y s) <->
mem x s \/
x =
y.
Proof.
Lemma mem_rem:
forall x y s,
mem x (
rem y s) <->
mem x s /\
x <>
y.
Proof.
Lemma mem_union:
forall b s1 s2,
mem b (
union s1 s2) =
mem b s1 ||
mem b s2.
Proof.
Lemma mem_inter:
forall b s1 s2,
mem b (
inter s1 s2) <->
mem b s1 /\
mem b s2.
Proof.
Lemma elements_spec :
forall s x,
mem x s <->
List.In x (
elements s).
Proof.
Lemma elements_norepet :
forall s,
list_norepet (
elements s).
Proof.
Lemma fold_spec A f s (
a:
A) :
fold f s a =
List.fold_right f a (
elements s).
Proof.
End Tree2Set.
Module PSet :=
Tree2Set PShareTree.
Module PSetOp :=
SetOp PSet.
Lemma pset_beq_mem (
s t:
PSet.t) :
PSet.beq s t =
true →
∀
x:
PSet.elt,
PSet.mem x s =
PSet.mem x t.
Proof.
Module ZSet :=
Tree2Set ZShareTree.
Module ZSetOp :=
SetOp ZSet.
Global Instance ZSet_gamma :
gamma_op ZSet.t int :=
fun s i =>
ZSet.mem (
Int.unsigned i)
s.
Section NOREP.
Context (
A:
Type) (
f:
A →
positive).
Fixpoint norep_aux (
l:
list A) (
s:
PSet.t) {
struct l} :
bool :=
match l with
|
nil =>
true
|
a ::
l' =>
let h :=
f(
a)
in
if PSet.mem h s
then false
else norep_aux l' (
PSet.add h s)
end.
Lemma norep_aux_correct :
∀
l s,
if norep_aux l s
then
list_norepet (
List.map f l) ∧
∀
h,
List.In h (
List.map f l) →
PSet.mem h s =
true →
False
else
(¬
list_norepet (
List.map f l)) ∨
∃
a,
List.In a l ∧
PSet.mem (
f a)
s
.
Proof.
induction l as [|
a l IH].
simpl.
intuition.
vauto.
intros s.
simpl.
destruct (
PSet.mem (
f a)
s)
eqn:
Ha.
vauto.
specialize (
IH (
PSet.add (
f a)
s)).
destruct (
norep_aux).
-
destruct IH as (
NR &
NI).
split.
constructor;
auto.
intros IN.
apply (
NI (
f a)
IN).
apply PSet.mem_add.
auto.
intros h [ <- |
IN ]
H.
rewrite H in Ha.
eq_some_inv.
apply (
NI _ IN).
apply PSet.mem_add.
auto.
-
destruct IH as [
NNR | (
v &
V &
IN) ].
+
left.
intros K.
inv K.
apply NNR.
assumption.
+
destruct (
peq (
f a) (
f v)).
left.
intros K;
inv K.
apply H1.
rewrite in_map_iff.
vauto.
right.
exists v.
split.
right;
exact V.
apply PSet.mem_add in IN.
intuition.
Qed.
Definition norepet_map (
l:
list A) :
bool :=
norep_aux l PSet.empty.
Lemma norepet_map_iff (
l:
list A) :
norepet_map l ↔
list_norepet (
List.map f l).
Proof.
End NOREP.