Library FinSet.FinSet
Finite sets of countable types can be be defined such that
extensional set equality is strict equality (using Cyril Cohen's
quotient construction).
Require Coq.Setoids.Setoid.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import FinSet.Lib.ListSet.
Require Import FinSet.Quotients.UList.
Require Import FinSet.Lib.DProp.
Require Import FinSet.Quotients.Countable.
Require Import FinSet.Quotients.Retract.
Require Import FinSet.Quotients.Quotient.
Definition T (A:Type) {_:Countable A} : Type := Quotient (eq_set_ulist eq_countable).
Instance set_countable (A:Type) {_:Countable A} : Countable (T A).
Definition listset {A} {_:Countable A} : Retract (list A) (T A) :=
Retract.compose ulist (quotient (eq_set_ulist eq_countable)).
Lemma set_quotient A (_:Countable A) : ∀ x,
eq_set_list eq_countable (listset.(inj) (listset.(proj) x)) x.
Lemma set_unique A (_:Countable A) :
∀ x, nodup eq_countable (listset.(inj) x).
Set membership. A decidable proposition.
Definition mem (x:A) (u:T A) : DProp := mem_list eq_countable x (listset.(inj) u).
Local Notation "x ∈ u" := (mem x u) (at level 10).
Lemma mem_spec x u : x∈u ↔ mem_list eq_countable x (listset.(inj) u).
Lemma mem_spec_in x u : x∈u ↔ List.In x (listset.(inj) u).
Global Instance in_eq_set : Proper (eq==>eq_set_list eq_countable==>iff) (@List.In A).
Local Notation "x ∈ u" := (mem x u) (at level 10).
Lemma mem_spec x u : x∈u ↔ mem_list eq_countable x (listset.(inj) u).
Lemma mem_spec_in x u : x∈u ↔ List.In x (listset.(inj) u).
Global Instance in_eq_set : Proper (eq==>eq_set_list eq_countable==>iff) (@List.In A).
Bounded existential quantifier on decidable propositions.
Program Definition dexists (u:T A) (P:A→DProp) : DProp := {|
Holds := ∃ x, x∈u ∧ P x ;
Denies := ∀ x, x∈u → DNot (P x) ;
dec := dec_lift (dec (ListSet.dexists P u))
|}.
Holds := ∃ x, x∈u ∧ P x ;
Denies := ∀ x, x∈u → DNot (P x) ;
dec := dec_lift (dec (ListSet.dexists P u))
|}.
Bounded existential quantifier on decidable propositions.
Program Definition dforall (u:T A) (P:A→DProp) : DProp :=
DNot (dexists u (fun x ⇒ DNot (P x))).
End Quantifiers.
Module MembershipNotation.
Notation "x ∈ u" := (mem x u) (at level 10).
End MembershipNotation.
Import MembershipNotation.
DNot (dexists u (fun x ⇒ DNot (P x))).
End Quantifiers.
Module MembershipNotation.
Notation "x ∈ u" := (mem x u) (at level 10).
End MembershipNotation.
Import MembershipNotation.
Import List.ListNotations.
Local Open Scope list_scope.
Section SetOperations.
Context {A} {CA:Countable A}.
Context {B} {CB:Countable B}.
Definition empty : T A := listset.(proj) [].
Lemma empty_spec : ∀ x, ¬x∈empty.
Lemma empty_spec_iff : ∀ x, x∈empty ↔ False.
Definition singleton (a:A) : T A := listset.(proj) [a].
Lemma singleton_spec : ∀ x a, x∈(singleton a) ↔ x=a.
Corollary singleton_self : ∀ a, a∈(singleton a).
Definition union (u₁ u₂:T A) : T A := listset.(proj) (listset.(inj) u₁++ listset.(inj) u₂).
Lemma union_spec : ∀ x u₁ u₂, x∈(union u₁ u₂) ↔ x∈u₁ ∨ x∈u₂.
Union over a finite set of finite sets. Together with singleton
forms a monad (restricted to countable types). This monad allows
to build sets by comprehension.
Definition Union (u:T A) (F:A→T B) : T B :=
listset.(proj) (List.flat_map (fun x ⇒ listset.(inj) (F x)) (listset.(inj) u)).
Lemma Union_spec u F x : x ∈ (Union u F) ↔ ∃ y, y∈u ∧ x ∈ (F y).
End SetOperations.
listset.(proj) (List.flat_map (fun x ⇒ listset.(inj) (F x)) (listset.(inj) u)).
Lemma Union_spec u F x : x ∈ (Union u F) ↔ ∃ y, y∈u ∧ x ∈ (F y).
End SetOperations.
guard P is the last component of the comprehension syntax. It
lifts a proposition to a subset of the singleton type. It is used
to implement the "such that" clause of comprehension.
Definition guard (P:DProp) : T unit :=
if (dec P) then (listset).(proj) [tt] else empty.
Lemma guard_spec_tt P : tt∈(guard P) ↔ P.
Lemma guard_spec P : ∀ x, x∈(guard P) ↔ P.
Lemma guard_Union A (_:Countable A) P (u:T A) :
∀ x, x∈(Union (guard P) (fun _ ⇒ u)) ↔ x∈u ∧ P.
if (dec P) then (listset).(proj) [tt] else empty.
Lemma guard_spec_tt P : tt∈(guard P) ↔ P.
Lemma guard_spec P : ∀ x, x∈(guard P) ↔ P.
Lemma guard_Union A (_:Countable A) P (u:T A) :
∀ x, x∈(Union (guard P) (fun _ ⇒ u)) ↔ x∈u ∧ P.
Module ComprehensionNotations.
Delimit Scope comprehension with comprehension.
Notation "u ´⍪´ x ´∈´ v" := (Union v (fun x ⇒ u))
(at level 50, x ident, v at level 20, right associativity) : comprehension.
Notation "u ´st´ p" := (Union (guard p) (fun _ ⇒ u))
(at level 50, p at level 20, right associativity) : comprehension.
Notation "a ´\´ " := (singleton a) (at level 20) : comprehension.
Notation "´⦃´ x ´⦄´" := (x%comprehension).
End ComprehensionNotations.
Import ComprehensionNotations.
Definition inter {A} {_:Countable A} (u₁ u₂:T A) : T A := ⦃ x \ st x∈u₂ ⍪ x∈u₁ ⦄.
Lemma inter_spec A (_:Countable A) (u₁ u₂:T A) :
∀ x, x ∈ (inter u₁ u₂) ↔ x∈u₁ ∧ x∈u₂.
Definition subset {A} {_:Countable A} (u v:T A) : DProp := dforall u (fun x ⇒ x∈v).
Lemma double_inclusion A (_:Countable A) (u v:T A) :
subset u v → subset v u → u = v.
Instance PreOrder A (_:Countable A) : PreOrder subset.
Lemma set_ext A (_:Countable A) (u v:T A) : (∀ x, x∈u ↔ x∈v) → u=v.
Module SetNotations.
Notation "∅" := empty.
Notation "u₁ ∪ u₂" := (union u₁ u₂) (at level 40, left associativity).
Notation "u₁ ∩ u₂" := (inter u₁ u₂) (at level 40, left associativity).
Notation "u ⊆ v" := (subset u v) (at level 70, no associativity).
End SetNotations.
Import SetNotations.
Hint Rewrite union_spec inter_spec empty_spec_iff singleton_spec : set_simplify.
Hint Rewrite guard_Union Union_spec : set_simplify.
Ltac set_intuition :=
intros **;
apply set_ext; intros ?; autorewrite with set_simplify in *; intuition eauto.
Section Algebraic.
Context (A:Type) (cA:Countable A).
Lemma union_assoc (v₁ v₂ v₃:T A) : v₁∪(v₂∪v₃) = (v₁∪v₂)∪v₃.
Lemma union_empty_left_unit (v:T A) : ∅ ∪ v = v.
Lemma union_empty_right_unit (v:T A) : v ∪ ∅ = v.
Lemma union_commutative (v₁ v₂:T A) : v₁∪v₂ = v₂∪v₁.
Lemma union_idempotent (v:T A) : v∪v = v.
Note: intersection does not, in general, have a neutral
element. Indeed, it would be a set with all the elements of the
type, which is not necessarily finite.
Lemma inter_assoc (u₁ u₂ u₃:T A) : u₁∩(u₂∩u₃) = (u₁∩u₂)∩u₃.
Lemma inter_commutative (u₁ u₂:T A) : u₁∩u₂ = u₂∩u₁.
Lemma inter_idempotent (u:T A) : u∩u = u.
Lemma union_inter_distr (u₁ u₂ v:T A) : (u₁∩u₂)∪v = (u₁∪v) ∩ (u₂∪v).
Lemma inter_union_distr (v₁ v₂ u:T A) : (v₁∪v₂)∩u = (v₁∩u)∪(v₂∩u).
Lemma inter_commutative (u₁ u₂:T A) : u₁∩u₂ = u₂∩u₁.
Lemma inter_idempotent (u:T A) : u∩u = u.
Lemma union_inter_distr (u₁ u₂ v:T A) : (u₁∩u₂)∪v = (u₁∪v) ∩ (u₂∪v).
Lemma inter_union_distr (v₁ v₂ u:T A) : (v₁∪v₂)∩u = (v₁∩u)∪(v₂∩u).
Lemma empty_bottom : ∀ u, ∅ ⊆ u.
Lemma union_sup (v₁ v₂:T A) : ∀ u, v₁∪v₂ ⊆ u ↔ v₁⊆u ∧ v₂⊆u.
Lemma inter_inf (u₁ u₂:T A) : ∀ v, v ⊆ u₁∩u₂ ↔ v⊆u₁ ∧ v⊆u₂.
End Algebraic.