Library set2
Defines functions specifically expecting sets of pairs;
Require Export set.
Require Import Bool.
Require Import decidable.
Require Import Setoid.
Section pair.
Context {A B} {DS:DecidableType A} {DS':DecidableType B}.
Global Instance DS_pair A B {DS:DecidableType A} {DS':DecidableType B} : DecidableType (A×B).
Proof.
split; intros.
destruct x, y.
destruct (DS_decide a a0).
+ destruct (DS_decide b b0).
× left; subst; reflexivity.
× right. intros contra; inversion contra. contradiction.
+ right. intros contra; inversion contra. contradiction.
Defined.
End pair.
Section prod.
Context {A B} {DS:DecidableType A} {DS':DecidableType B}.
Definition set_prod : set A → set B → set (A×B) :=
ListSet.set_prod (A:=A) (B:=B).
Lemma set_prod_In : ∀ (x : set A) (y : set B) (a : A) (b : B),
set_In (a, b) (set_prod x y) ↔ set_In a x ∧ set_In b y.
Proof.
Transparent set.
apply List.in_prod_iff.
Opaque set.
Qed.
End prod.
Section others.
Context {A B} {DS:DecidableType A} {DS':DecidableType B}.
Definition set2_inter_fst (x:set (A×B)) (xa:set A) :=
set_filter (fun ab ⇒ fst ab \in? xa) x.
Definition set2_inter_snd (x:set (A×B)) (xb:set B) :=
set_filter (fun ab ⇒ snd ab \in? xb) x.
Lemma set2_inter_fst_In : ∀ x xa a b,
(a, b) \in set2_inter_fst x xa ↔ (a, b) \in x ∧ a \in xa.
Proof.
intros. unfold set2_inter_fst.
rewrite set_filter_In. simpl. rewrite set_mem_correct_iff.
reflexivity.
Qed.
Lemma set2_inter_snd_In : ∀ x xb a b,
(a, b) \in set2_inter_snd x xb ↔ (a, b) \in x ∧ b \in xb.
Proof.
intros. unfold set2_inter_snd.
rewrite set_filter_In. simpl. rewrite set_mem_correct_iff.
reflexivity.
Qed.
Definition set2_diff_fst (x:set (A×B)) xa : set (A×B) :=
set_filter (fun ab ⇒ negb (fst ab \in? xa)) x.
Definition set2_diff_snd (x:set (A×B)) xb :=
set_filter (fun ab ⇒ negb (snd ab \in? xb)) x.
Lemma set2_diff_fst_In : ∀ x xa a b,
(a, b) \in set2_diff_fst x xa ↔ (a, b) \in x ∧ ¬ a \in xa.
Proof.
intros. unfold set2_diff_fst.
rewrite set_filter_In. simpl. rewrite negb_true_iff.
rewrite set_mem_complete_iff.
reflexivity.
Qed.
Lemma set2_diff_snd_In : ∀ x xb a b,
(a, b) \in set2_diff_snd x xb ↔ (a, b) \in x ∧ ¬ b \in xb.
Proof.
intros. unfold set2_diff_snd.
rewrite set_filter_In. simpl. rewrite negb_true_iff.
rewrite set_mem_complete_iff.
reflexivity.
Qed.
Lemma set2_diff_fst_union_distr_l : ∀ (x1 x2: set (A×B)) xa,
set2_diff_fst (x1 \cup x2) xa \equiv set2_diff_fst x1 xa \cup set2_diff_fst x2 xa.
Proof.
intros.
apply set_same_In_iff; intros.
destruct a.
rewrite set_union_In.
rewrite 3!set2_diff_fst_In.
rewrite set_union_In.
rewrite and_or_distr_l. reflexivity.
Qed.
Lemma set2_diff_fst_union_distr_r : ∀ x V1 V2,
set2_diff_fst x (V1 \cup V2) \equiv set2_diff_fst x V1 \cap set2_diff_fst x V2.
Proof.
intros.
apply set_same_In_iff; intros.
destruct a.
rewrite set_inter_In.
rewrite 3!set2_diff_fst_In.
rewrite set_union_In.
rewrite not_or_iff.
repeat split; apply H.
Qed.
Lemma set2_diff_fst_inter_distr_l : ∀ x1 x2 V,
set2_diff_fst (x1 \cap x2) V \equiv set2_diff_fst x1 V \cap set2_diff_fst x2 V.
Proof.
intros.
apply set_same_In_iff; intros.
destruct a.
rewrite set_inter_In.
rewrite 3!set2_diff_fst_In.
rewrite set_inter_In.
repeat split; apply H.
Qed.
Lemma set2_diff_fst_inter_distr_r : ∀ x V1 V2,
set2_diff_fst x (V1 \cap V2) \equiv set2_diff_fst x V1 \cup set2_diff_fst x V2.
Proof.
intros.
apply set_same_In_iff; intros.
destruct a.
rewrite set_union_In.
rewrite 3!set2_diff_fst_In.
rewrite set_inter_In.
rewrite not_and_iff by (apply dec_is_decidable; apply set_In_dec).
rewrite and_comm.
rewrite and_or_distr_l.
rewrite 2!and_comm with (B:=(a, b) \in x). reflexivity.
Qed.
Lemma set2_diff_fst_emptyset_l : ∀ xb,
set2_diff_fst \emptyset xb \equiv \emptyset.
Proof.
intros.
apply set_same_In_iff; intros.
destruct a. rewrite set2_diff_fst_In.
split; intros.
- destruct H; inversion H.
- inversion H.
Qed.
Lemma set2_diff_fst_emptyset_r : ∀ x,
set2_diff_fst x \emptyset \equiv x.
Proof.
intros. apply set_same_In_iff; intros.
destruct a.
rewrite set2_diff_fst_In.
split; intros.
- apply H.
- split.
+ apply H.
+ intros contra. inversion contra.
Qed.
Lemma set2_diff_fst_twice : ∀ x xb1 xb2,
set2_diff_fst (set2_diff_fst x xb1) xb2 \equiv (set2_diff_fst x xb1) \cap (set2_diff_fst x xb2).
Proof.
intros.
apply set_same_In_iff; intros. destruct a.
rewrite set_inter_In.
rewrite 3!set2_diff_fst_In.
repeat split; apply H.
Qed.
Global Add Parametric Morphism : set2_diff_fst
with signature set_same ==> set_same ==> set_same as set_same_set2_diff_fst.
Proof.
intros. apply set_same_In_iff; intros.
destruct a. rewrite 2!set2_diff_fst_In. rewrite H, H0. reflexivity.
Qed.
Definition set2_inner_fst (x y:set(A×B)) : set (B×B) :=
set_map (fun abab ⇒ (snd(fst(abab)), snd(snd(abab))))
(set_filter (fun abab ⇒ if DS_decide (fst(fst(abab))) (fst(snd(abab)))
then true else false)
(set_prod x y)).
Lemma set2_inner_fst_In : ∀ x y b b',
(b, b') \in set2_inner_fst x y ↔ (∃ a, (a, b) \in x ∧ (a, b') \in y).
Proof.
intros.
unfold set2_inner_fst.
rewrite set_map_In.
split; intros.
- destruct H as [((a0, b0), (a1, b1)) H].
rewrite set_filter_In in H. simpl in H. decompose [and] H; clear H.
rewrite set_prod_In in H2. destruct H2.
inversion H1; subst.
destruct (DS_decide a0 a1); [| discriminate H3].
subst a1. ∃ a0. split; assumption.
- destruct H as [a [H0 H1]].
∃ ((a, b), (a, b')). rewrite set_filter_In. simpl.
repeat split.
rewrite set_prod_In; split; assumption.
destruct (DS_decide a a); [|contradiction n; reflexivity]. reflexivity.
Qed.
Lemma set2_inner_fst_emptyset_l :
∀ x, set2_inner_fst \emptyset x \equiv \emptyset.
Proof.
intros.
apply set_same_In_iff; intros.
destruct a. rewrite set2_inner_fst_In.
split; intros.
- destruct H as [i H]. destruct H; inversion H.
- inversion H.
Qed.
Lemma set2_inner_fst_union_distr_l :
∀ x1 x2 x,
set2_inner_fst (x1 ∪ x2) x ≡ set2_inner_fst x1 x ∪ set2_inner_fst x2 x.
Proof.
intros. apply set_same_In_iff; intros.
destruct a. rewrite set_union_In.
rewrite 3!set2_inner_fst_In. split; intros.
- destruct H as [i [H H0]]. rewrite set_union_In in H. destruct H.
+ left. ∃ i. split; assumption.
+ right. ∃ i. split; assumption.
- destruct H.
+ destruct H as [i [H H0]]. ∃ i. split.
× rewrite set_union_In. left; assumption.
× assumption.
+ destruct H as [i [H H0]]. ∃ i. split.
× rewrite set_union_In. right; assumption.
× assumption.
Qed.
Lemma set2_inner_fst_union_distr_r :
∀ x1 x2 x,
set2_inner_fst x (x1 ∪ x2) ≡ set2_inner_fst x x1 ∪ set2_inner_fst x x2.
Proof.
intros. apply set_same_In_iff; intros.
destruct a. rewrite set_union_In.
rewrite 3!set2_inner_fst_In. split; intros.
- destruct H as [i [H H0]]. rewrite set_union_In in H0. destruct H0.
+ left. ∃ i. split; assumption.
+ right. ∃ i. split; assumption.
- destruct H.
+ destruct H as [i [H H0]]. ∃ i. split.
× assumption.
× rewrite set_union_In. left; assumption.
+ destruct H as [i [H H0]]. ∃ i. split.
× assumption.
× rewrite set_union_In. right; assumption.
Qed.
Lemma set2_inner_fst_diff_lr : ∀ x1 x2 xb,
set2_inner_fst x1 (set2_diff_fst x2 xb) \equiv set2_inner_fst (set2_diff_fst x1 xb) x2.
Proof.
intros. apply set_same_In_iff; intros.
destruct a.
rewrite 2!set2_inner_fst_In. split; intros.
- destruct H as [i [H H0]]. ∃ i.
rewrite set2_diff_fst_In in ×. destruct H0. repeat split; assumption.
- destruct H as [i [H H0]]. ∃ i.
rewrite set2_diff_fst_In in ×. destruct H. repeat split; assumption.
Qed.
Global Add Parametric Morphism : set2_inner_fst
with signature set_same ==> set_same ==> set_same as set_same_set2_inner_fst.
Proof.
intros. apply set_same_In_iff; intros.
destruct a. rewrite 2!set2_inner_fst_In. split; intros.
- destruct H1 as [i H1]. ∃ i. rewrite <- H, <- H0. assumption.
- destruct H1 as [i H1]. ∃ i. rewrite H, H0. assumption.
Qed.
End others.