Library Containers.SetConstructs
Require Import SetInterface SetAVLInstance.
Require Import SetFacts SetProperties.
Generalizable All Variables.
Local Transparent set.
Require Import SetFacts SetProperties.
Generalizable All Variables.
Local Transparent set.
This module provides a couple of common set constructions. They
are built with and for the AVL instance and are not parameterized
by an FSet implementation.
Mapping a function on a set
Section Mapping.
Local Open Scope set_scope.
Context `{HA : OrderedType A, HB: OrderedType B}.
Variable f : A → B.
Definition map (s : set A) : set B :=
fold (fun a acc ⇒ add (f a) acc) s {}.
Context `{f_m : Proper _ (_eq ==> _eq) f}.
Property map_spec : ∀ s,
∀ b, In b (map s) ↔ ∃ a, In a s ∧ b === f a.
Proof.
intro s.
apply fold_rec_weak with
(P := fun s r ⇒ ∀ b, In b r ↔ ∃ a, In a s ∧ b === f a);
clear s.
intros; rewrite H0; clear H0; split; intros [z Hz];
∃ z; [rewrite <- H | rewrite H]; exact Hz.
intros; rewrite empty_iff; firstorder; contradiction (empty_1 H).
intros; rewrite add_iff; rewrite H0; clear H0; split; intro.
destruct H0. ∃ x; split; intuition.
destruct H0 as [z Hz]; ∃ z; rewrite add_iff; intuition.
destruct H0 as [z Hz]; rewrite add_iff in Hz; destruct Hz.
destruct H0. left; rewrite H0; auto.
right; ∃ z; auto.
Qed.
Global Opaque map.
Local Transparent In FSet_OrderedType.
Instance map_m : Proper (_eq ==> _eq) map.
Proof.
intros s s' H z.
setoid_rewrite map_spec; firstorder.
Qed.
Corollary map_1 : ∀ a s, In a s → In (f a) (map s).
Proof.
intros; rewrite map_spec; firstorder.
Qed.
Corollary map_2 : ∀ b s, In b (map s) → ∃ a, In a s ∧ b === f a.
intros; rewrite map_spec in H; assumption.
Qed.
Definition map_iff := map_spec.
End Mapping.
Local Open Scope set_scope.
Context `{HA : OrderedType A, HB: OrderedType B}.
Variable f : A → B.
Definition map (s : set A) : set B :=
fold (fun a acc ⇒ add (f a) acc) s {}.
Context `{f_m : Proper _ (_eq ==> _eq) f}.
Property map_spec : ∀ s,
∀ b, In b (map s) ↔ ∃ a, In a s ∧ b === f a.
Proof.
intro s.
apply fold_rec_weak with
(P := fun s r ⇒ ∀ b, In b r ↔ ∃ a, In a s ∧ b === f a);
clear s.
intros; rewrite H0; clear H0; split; intros [z Hz];
∃ z; [rewrite <- H | rewrite H]; exact Hz.
intros; rewrite empty_iff; firstorder; contradiction (empty_1 H).
intros; rewrite add_iff; rewrite H0; clear H0; split; intro.
destruct H0. ∃ x; split; intuition.
destruct H0 as [z Hz]; ∃ z; rewrite add_iff; intuition.
destruct H0 as [z Hz]; rewrite add_iff in Hz; destruct Hz.
destruct H0. left; rewrite H0; auto.
right; ∃ z; auto.
Qed.
Global Opaque map.
Local Transparent In FSet_OrderedType.
Instance map_m : Proper (_eq ==> _eq) map.
Proof.
intros s s' H z.
setoid_rewrite map_spec; firstorder.
Qed.
Corollary map_1 : ∀ a s, In a s → In (f a) (map s).
Proof.
intros; rewrite map_spec; firstorder.
Qed.
Corollary map_2 : ∀ b s, In b (map s) → ∃ a, In a s ∧ b === f a.
intros; rewrite map_spec in H; assumption.
Qed.
Definition map_iff := map_spec.
End Mapping.
Section CartesianProduct.
Local Open Scope set_scope.
Context `{HA : OrderedType A, HB: OrderedType B}.
Local Open Scope set_scope.
Context `{HA : OrderedType A, HB: OrderedType B}.
Definition map_add (s' : set B) (a : A) (acc : set (A × B)) :=
fold (fun b acc ⇒ add (a, b) acc) s' acc.
fold (fun b acc ⇒ add (a, b) acc) s' acc.
Property map_add_spec : ∀ s' a acc,
∀ x, In x (map_add s' a acc) ↔
In x acc ∨ (fst x === a ∧ In (snd x) s').
Proof.
intros s' a acc.
apply fold_rec_weak with
(P := fun svu r ⇒ ∀ x,
In x r ↔ (In x acc ∨ (fst x === a ∧ In (snd x) svu))).
intros; rewrite H0, H; reflexivity.
intros; intuition. contradiction (empty_1 H1).
intros b m s Hb IH [xa xb]; simpl.
rewrite add_iff, IH; clear IH; simpl; rewrite add_iff; intuition auto.
inversion_clear H0; right; split; auto; apply add_1; auto.
left; constructor; auto.
Qed.
Property cart_prod_spec : ∀ s s',
∀ x, In x (cart_prod s s') ↔ In (fst x) s ∧ In (snd x) s'.
Proof.
intros s s'.
apply fold_rec_weak with
(P := fun svu r ⇒ ∀ x,
In x r ↔ In (fst x ) svu ∧ In (snd x) s').
intros; rewrite H0, !H; reflexivity.
intros [a b]; rewrite !empty_iff; tauto.
intros a acc svu Ha IH [xa xb]; simpl.
rewrite map_add_spec, IH, add_iff; simpl; clear IH.
intuition.
Qed.
∀ x, In x (map_add s' a acc) ↔
In x acc ∨ (fst x === a ∧ In (snd x) s').
Proof.
intros s' a acc.
apply fold_rec_weak with
(P := fun svu r ⇒ ∀ x,
In x r ↔ (In x acc ∨ (fst x === a ∧ In (snd x) svu))).
intros; rewrite H0, H; reflexivity.
intros; intuition. contradiction (empty_1 H1).
intros b m s Hb IH [xa xb]; simpl.
rewrite add_iff, IH; clear IH; simpl; rewrite add_iff; intuition auto.
inversion_clear H0; right; split; auto; apply add_1; auto.
left; constructor; auto.
Qed.
Property cart_prod_spec : ∀ s s',
∀ x, In x (cart_prod s s') ↔ In (fst x) s ∧ In (snd x) s'.
Proof.
intros s s'.
apply fold_rec_weak with
(P := fun svu r ⇒ ∀ x,
In x r ↔ In (fst x ) svu ∧ In (snd x) s').
intros; rewrite H0, !H; reflexivity.
intros [a b]; rewrite !empty_iff; tauto.
intros a acc svu Ha IH [xa xb]; simpl.
rewrite map_add_spec, IH, add_iff; simpl; clear IH.
intuition.
Qed.
Now that we have the specs, we hide the implementations.
cart_prod is a morphism
Instance cart_prod_m : Proper (_eq ==> _eq ==> _eq) cart_prod.
Proof.
intros s s' Hs t t' Ht z.
setoid_rewrite cart_prod_spec. rewrite Hs, Ht; reflexivity.
Qed.
Proof.
intros s s' Hs t t' Ht z.
setoid_rewrite cart_prod_spec. rewrite Hs, Ht; reflexivity.
Qed.
Properties of cart_prod in the FSetInterface style
Corollary cart_prod_1 : ∀ s s' a b,
In a s → In b s' → In (a, b) (cart_prod s s').
Proof.
intros; rewrite cart_prod_spec; simpl; tauto.
Qed.
Corollary cart_prod_2 : ∀ s s' a b,
In (a, b) (cart_prod s s') → In a s.
Proof.
intros; rewrite cart_prod_spec in H; simpl in H; tauto.
Qed.
Corollary cart_prod_3 : ∀ s s' a b,
In (a, b) (cart_prod s s') → In b s'.
Proof.
intros; rewrite cart_prod_spec in H; simpl in H; tauto.
Qed.
Definition cart_prod_iff := cart_prod_spec.
End CartesianProduct.
In a s → In b s' → In (a, b) (cart_prod s s').
Proof.
intros; rewrite cart_prod_spec; simpl; tauto.
Qed.
Corollary cart_prod_2 : ∀ s s' a b,
In (a, b) (cart_prod s s') → In a s.
Proof.
intros; rewrite cart_prod_spec in H; simpl in H; tauto.
Qed.
Corollary cart_prod_3 : ∀ s s' a b,
In (a, b) (cart_prod s s') → In b s'.
Proof.
intros; rewrite cart_prod_spec in H; simpl in H; tauto.
Qed.
Definition cart_prod_iff := cart_prod_spec.
End CartesianProduct.
Definition powerset (s : set A) : set (set A) :=
fold add_one s (singleton {}).
Local Transparent Equal _eq.
Local Transparent In FSet_OrderedType.
fold add_one s (singleton {}).
Local Transparent Equal _eq.
Local Transparent In FSet_OrderedType.
Property add_one_spec :
∀ x m s, In s (add_one x m) ↔
(In s m ∨ ∃ s', In s' m ∧ s [=] {x; s'}).
Proof.
intros x m.
apply fold_rec_weak with
(P := fun mvu r ⇒ ∀ s, In s r ↔
(In s m ∨ ∃ s', In s' mvu ∧ s [=] {x; s'})).
intros; rewrite ?H0, ?H; intuition; right.
destruct H2 as [z [Hz1 Hz2]]; ∃ z; rewrite <-H; split; auto.
destruct H2 as [z [Hz1 Hz2]]; ∃ z; rewrite H; split; auto.
intros; intuition.
destruct H0 as [z [abs _]]; contradiction (empty_1 abs).
intros s' a mvu Hx' IH s.
rewrite add_iff; rewrite IH; clear IH; intuition.
right; ∃ s'; split; [apply add_1 | rewrite H0]; reflexivity.
right; destruct H as [z [Hz1 Hz2]]; ∃ z; split; auto.
apply add_2; auto.
destruct H0 as [z [Hz1 Hz2]]; rewrite add_iff in Hz1;
destruct Hz1; [left | right; right; ∃ z].
rewrite H, Hz2; reflexivity.
split; assumption.
Qed.
Property powerset_spec :
∀ s s', In s' (powerset s) ↔ s' [<=] s.
Proof.
intros s.
apply fold_rec_weak with
(P := fun svu r ⇒ ∀ s', s' \In r ↔ s' [<=] svu).
intros; rewrite H0, H; reflexivity.
intros; rewrite singleton_iff; split; intro.
rewrite <- H; reflexivity.
symmetry; refine (empty_is_empty_1 _).
intros z Hz; contradiction (empty_1 (H z Hz)).
intros x m svu Hx IH s'.
rewrite add_one_spec, IH.
split; intro H.
destruct H.
exact (fun z Hz ⇒ add_2 _ (H z Hz)).
destruct H as [z [Hz1 Hz2]].
rewrite Hz2; rewrite IH in Hz1; rewrite Hz1; reflexivity.
destruct (subset_dec s' svu) as [Hsub|Hnsub]; [left | right].
exact Hsub.
∃ (remove x s'); split.
rewrite IH.
intros z Hz; rewrite remove_iff in Hz; destruct Hz.
assert (Hz' := H z H0); rewrite add_iff in Hz'; destruct Hz'.
contradiction (H1 H2). assumption.
symmetry; apply add_remove.
destruct (In_dec x s'); auto.
contradiction Hnsub; intros z Hz.
assert (Hz' := H z Hz); rewrite add_iff in Hz'; destruct Hz'.
rewrite H0 in n; contradiction (n Hz). assumption.
Qed.
∀ x m s, In s (add_one x m) ↔
(In s m ∨ ∃ s', In s' m ∧ s [=] {x; s'}).
Proof.
intros x m.
apply fold_rec_weak with
(P := fun mvu r ⇒ ∀ s, In s r ↔
(In s m ∨ ∃ s', In s' mvu ∧ s [=] {x; s'})).
intros; rewrite ?H0, ?H; intuition; right.
destruct H2 as [z [Hz1 Hz2]]; ∃ z; rewrite <-H; split; auto.
destruct H2 as [z [Hz1 Hz2]]; ∃ z; rewrite H; split; auto.
intros; intuition.
destruct H0 as [z [abs _]]; contradiction (empty_1 abs).
intros s' a mvu Hx' IH s.
rewrite add_iff; rewrite IH; clear IH; intuition.
right; ∃ s'; split; [apply add_1 | rewrite H0]; reflexivity.
right; destruct H as [z [Hz1 Hz2]]; ∃ z; split; auto.
apply add_2; auto.
destruct H0 as [z [Hz1 Hz2]]; rewrite add_iff in Hz1;
destruct Hz1; [left | right; right; ∃ z].
rewrite H, Hz2; reflexivity.
split; assumption.
Qed.
Property powerset_spec :
∀ s s', In s' (powerset s) ↔ s' [<=] s.
Proof.
intros s.
apply fold_rec_weak with
(P := fun svu r ⇒ ∀ s', s' \In r ↔ s' [<=] svu).
intros; rewrite H0, H; reflexivity.
intros; rewrite singleton_iff; split; intro.
rewrite <- H; reflexivity.
symmetry; refine (empty_is_empty_1 _).
intros z Hz; contradiction (empty_1 (H z Hz)).
intros x m svu Hx IH s'.
rewrite add_one_spec, IH.
split; intro H.
destruct H.
exact (fun z Hz ⇒ add_2 _ (H z Hz)).
destruct H as [z [Hz1 Hz2]].
rewrite Hz2; rewrite IH in Hz1; rewrite Hz1; reflexivity.
destruct (subset_dec s' svu) as [Hsub|Hnsub]; [left | right].
exact Hsub.
∃ (remove x s'); split.
rewrite IH.
intros z Hz; rewrite remove_iff in Hz; destruct Hz.
assert (Hz' := H z H0); rewrite add_iff in Hz'; destruct Hz'.
contradiction (H1 H2). assumption.
symmetry; apply add_remove.
destruct (In_dec x s'); auto.
contradiction Hnsub; intros z Hz.
assert (Hz' := H z Hz); rewrite add_iff in Hz'; destruct Hz'.
rewrite H0 in n; contradiction (n Hz). assumption.
Qed.
Now that we have the specs, we hide the implementations.
powerset is a morphism
Instance powerset_m : Proper (_eq ==> _eq) powerset.
Proof.
intros s s' H z.
setoid_rewrite powerset_spec. rewrite H; reflexivity.
Qed.
Proof.
intros s s' H z.
setoid_rewrite powerset_spec. rewrite H; reflexivity.
Qed.
Properties of powerset in the FSetInterface style
Corollary powerset_1 : ∀ s s', s' [<=] s → In s' (powerset s).
Proof.
intros; rewrite powerset_spec; assumption.
Qed.
Corollary powerset_2 : ∀ s s', In s' (powerset s) → s' [<=] s.
Proof.
intros; rewrite powerset_spec in H; assumption.
Qed.
Definition powerset_iff := powerset_spec.
End PowerSet.
Proof.
intros; rewrite powerset_spec; assumption.
Qed.
Corollary powerset_2 : ∀ s s', In s' (powerset s) → s' [<=] s.
Proof.
intros; rewrite powerset_spec in H; assumption.
Qed.
Definition powerset_iff := powerset_spec.
End PowerSet.
Diagonal product
Section DiagonalProduct.
Local Open Scope set_scope.
Context `{HA : OrderedType A}.
Require Import Recdef.
Function diag_prod (s : set A) {measure cardinal} : set (A × A) :=
match min_elt s with
| None ⇒ {}
| Some x ⇒
let s' := remove x s in
map_add s' x (diag_prod s')
end.
Proof.
intros.
rewrite <- remove_cardinal_1 with s x.
constructor.
exact (min_elt_1 teq).
Defined.
Global Opaque diag_prod.
Property diag_prod_spec : ∀ s,
∀ x, In x (diag_prod s) ↔
In (fst x) s ∧ In (snd x) s ∧ (fst x) <<< (snd x).
Proof.
intro s.
apply diag_prod_ind with
(P := fun s r ⇒ ∀ x, In x r ↔
(In (fst x) s ∧ In (snd x) s ∧ fst x <<< snd x)); clear s.
intros s' Hs' [a b]; simpl.
apply min_elt_3 in Hs'.
apply empty_is_empty_1 in Hs'.
rewrite !Hs', !empty_iff; tauto.
intros s x Hx s' IH [a b]; rewrite map_add_spec, IH; simpl.
destruct (min_elt_dec s); inversion Hx; subst; clear Hx.
clear IH; unfold s'; clear s'; rewrite !remove_iff; intuition.
rewrite H; assumption.
destruct (compare_dec a b); auto.
contradiction H2; transitivity a; auto.
contradiction (Hmin b H0); rewrite <- H; assumption.
destruct (eq_dec a x); [right | left].
intuition; rewrite <- H1; exact (lt_not_eq H2).
intuition. symmetry; assumption.
intro abs; apply (Hmin a H0); rewrite abs; assumption.
Qed.
Local Transparent Equal _eq In FSet_OrderedType.
Local Open Scope set_scope.
Context `{HA : OrderedType A}.
Require Import Recdef.
Function diag_prod (s : set A) {measure cardinal} : set (A × A) :=
match min_elt s with
| None ⇒ {}
| Some x ⇒
let s' := remove x s in
map_add s' x (diag_prod s')
end.
Proof.
intros.
rewrite <- remove_cardinal_1 with s x.
constructor.
exact (min_elt_1 teq).
Defined.
Global Opaque diag_prod.
Property diag_prod_spec : ∀ s,
∀ x, In x (diag_prod s) ↔
In (fst x) s ∧ In (snd x) s ∧ (fst x) <<< (snd x).
Proof.
intro s.
apply diag_prod_ind with
(P := fun s r ⇒ ∀ x, In x r ↔
(In (fst x) s ∧ In (snd x) s ∧ fst x <<< snd x)); clear s.
intros s' Hs' [a b]; simpl.
apply min_elt_3 in Hs'.
apply empty_is_empty_1 in Hs'.
rewrite !Hs', !empty_iff; tauto.
intros s x Hx s' IH [a b]; rewrite map_add_spec, IH; simpl.
destruct (min_elt_dec s); inversion Hx; subst; clear Hx.
clear IH; unfold s'; clear s'; rewrite !remove_iff; intuition.
rewrite H; assumption.
destruct (compare_dec a b); auto.
contradiction H2; transitivity a; auto.
contradiction (Hmin b H0); rewrite <- H; assumption.
destruct (eq_dec a x); [right | left].
intuition; rewrite <- H1; exact (lt_not_eq H2).
intuition. symmetry; assumption.
intro abs; apply (Hmin a H0); rewrite abs; assumption.
Qed.
Local Transparent Equal _eq In FSet_OrderedType.
diag_prod is a morphism
Instance diag_prod_m : Proper (_eq ==> _eq) diag_prod.
Proof.
intros s s' H z.
setoid_rewrite diag_prod_spec. rewrite H; reflexivity.
Qed.
Proof.
intros s s' H z.
setoid_rewrite diag_prod_spec. rewrite H; reflexivity.
Qed.
Properties of diag_prod in the FSetInterface style
Corollary diag_prod_1 : ∀ s x y, In x s → In y s → x <<< y →
In (x, y) (diag_prod s).
Proof.
intros; rewrite diag_prod_spec; tauto.
Qed.
Corollary diag_prod_2 : ∀ s x y, In (x, y) (diag_prod s) → In x s.
Proof.
intros; rewrite diag_prod_spec in H; tauto.
Qed.
Corollary diag_prod_3 : ∀ s x y, In (x, y) (diag_prod s) → In y s.
Proof.
intros; rewrite diag_prod_spec in H; tauto.
Qed.
Corollary diag_prod_4 : ∀ s x y, In (x, y) (diag_prod s) → x <<< y.
Proof.
intros; rewrite diag_prod_spec in H; tauto.
Qed.
Definition diag_prod_iff := diag_prod_spec.
End DiagonalProduct.
In (x, y) (diag_prod s).
Proof.
intros; rewrite diag_prod_spec; tauto.
Qed.
Corollary diag_prod_2 : ∀ s x y, In (x, y) (diag_prod s) → In x s.
Proof.
intros; rewrite diag_prod_spec in H; tauto.
Qed.
Corollary diag_prod_3 : ∀ s x y, In (x, y) (diag_prod s) → In y s.
Proof.
intros; rewrite diag_prod_spec in H; tauto.
Qed.
Corollary diag_prod_4 : ∀ s x y, In (x, y) (diag_prod s) → x <<< y.
Proof.
intros; rewrite diag_prod_spec in H; tauto.
Qed.
Definition diag_prod_iff := diag_prod_spec.
End DiagonalProduct.
Section DisjointUnion.
Local Open Scope set_scope.
Context `{HA : OrderedType A, HB: OrderedType B}.
Definition disj_union (s : set A) (s' : set B) : set (A + B) :=
union (map (@inl A B) s) (map (@inr A B) s').
Property disj_union_spec : ∀ s s',
∀ (x : A + B), In x (disj_union s s') ↔
match x with
| inl a ⇒ In a s
| inr b ⇒ In b s'
end.
Proof.
intros; unfold disj_union.
rewrite union_iff, 2map_iff.
destruct x as [a|b]; firstorder; inversion_clear H0;
rewrite H1; assumption.
repeat intro; Tactics.tconstructor ltac:(assumption).
repeat intro; Tactics.tconstructor ltac:(assumption).
Qed.
Global Opaque disj_union.
Local Transparent Equal _eq In FSet_OrderedType.
Instance disj_union_m : Proper (_eq ==> _eq ==> _eq) disj_union.
Proof.
repeat intro.
setoid_rewrite disj_union_spec.
destruct a; [rewrite H | rewrite H0]; reflexivity.
Qed.
Property disj_union_1 :
∀ s s' a, In a s → In (inl _ a) (disj_union s s').
Proof.
intros; rewrite disj_union_spec; auto.
Qed.
Property disj_union_2 :
∀ s s' b, In b s' → In (inr _ b) (disj_union s s').
Proof.
intros; rewrite disj_union_spec; auto.
Qed.
Property disj_union_3 : ∀ s s' x, In x (disj_union s s') →
match x with inl a ⇒ In a s | inr b ⇒ In b s' end.
Proof.
intros; rewrite disj_union_spec in H; auto.
Qed.
Definition disj_union_iff := disj_union_spec.
End DisjointUnion.
Local Open Scope set_scope.
Context `{HA : OrderedType A, HB: OrderedType B}.
Definition disj_union (s : set A) (s' : set B) : set (A + B) :=
union (map (@inl A B) s) (map (@inr A B) s').
Property disj_union_spec : ∀ s s',
∀ (x : A + B), In x (disj_union s s') ↔
match x with
| inl a ⇒ In a s
| inr b ⇒ In b s'
end.
Proof.
intros; unfold disj_union.
rewrite union_iff, 2map_iff.
destruct x as [a|b]; firstorder; inversion_clear H0;
rewrite H1; assumption.
repeat intro; Tactics.tconstructor ltac:(assumption).
repeat intro; Tactics.tconstructor ltac:(assumption).
Qed.
Global Opaque disj_union.
Local Transparent Equal _eq In FSet_OrderedType.
Instance disj_union_m : Proper (_eq ==> _eq ==> _eq) disj_union.
Proof.
repeat intro.
setoid_rewrite disj_union_spec.
destruct a; [rewrite H | rewrite H0]; reflexivity.
Qed.
Property disj_union_1 :
∀ s s' a, In a s → In (inl _ a) (disj_union s s').
Proof.
intros; rewrite disj_union_spec; auto.
Qed.
Property disj_union_2 :
∀ s s' b, In b s' → In (inr _ b) (disj_union s s').
Proof.
intros; rewrite disj_union_spec; auto.
Qed.
Property disj_union_3 : ∀ s s' x, In x (disj_union s s') →
match x with inl a ⇒ In a s | inr b ⇒ In b s' end.
Proof.
intros; rewrite disj_union_spec in H; auto.
Qed.
Definition disj_union_iff := disj_union_spec.
End DisjointUnion.