Library Beroal.Subset
Subset defined as an unary predicate. This library uses less Inductive definitions comparing to Coq.Sets.Ensembles. Extensively uses firstorder tactic.
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Lists.List.
Require Import Beroal.Init.
Require Beroal.FunListArg.
specialize pw
Definition pw a0 a1 b
: (a0 -> a0 -> b) -> (a1 -> a0) -> (a1 -> a0) -> a1 -> b
:= FunListArg.pw a0 a1 b 2.
: (a0 -> a0 -> b) -> (a1 -> a0) -> (a1 -> a0) -> a1 -> b
:= FunListArg.pw a0 a1 b 2.
Universum. We consider subsets of U.
∈, "belongs to" = standard application of a function. E.g. in the context (s : subset U, x : U), s x means "x∈s".
extensionally equal subsets
a⊆b, non-strictly
"inhabited", "is not empty" = ex
Inductive intersect (a b:subset) : Prop :=
Build_intersect (x : _) (_ : a x) (_ : b x).
Definition disjoint (a b:subset) := ~ intersect a b.
∅
the whole U
is U
Definition is_full (a:subset) := forall x, a x.
Definition is_empty (a:subset) := forall x, ~ a x.
Definition union : op2_type := @pw _ _ _ or.
Definition intersection : op2_type := @pw _ _ _ and.
Definition is_empty (a:subset) := forall x, ~ a x.
Definition union : op2_type := @pw _ _ _ or.
Definition intersection : op2_type := @pw _ _ _ and.
rpc = relative pseudo-complement
Because of this axiom we can use eq for extensionally equal subsets. See Coq's FAQ, "5.2 Axioms."
Axiom ext_eq_axiom : forall a b, ext_eq a b -> a = b.
End definition0.
Notation "a <* b" := (included a b) (at level 70, no associativity).
Notation "a \*/ b" := (union a b) (at level 50, left associativity).
Notation "a /*\ b" := (intersection a b) (at level 40, left associativity).
Notation "a *-> b" := (rpc a b)
(at level 65, right associativity).
Definition pseudo_complement (U : Type) (a:subset U) := a *-> @empty _.
Notation "~* a" := (pseudo_complement a) (at level 35, right associativity).
Definition difference (U : Type) (a b:subset U) := a /*\ ~* b.
Notation "a *\ b" := (difference a b) (at level 40, left associativity).
Section relation_independent.
Variable (a b : Type) (r : a -> b -> Prop).
End definition0.
Notation "a <* b" := (included a b) (at level 70, no associativity).
Notation "a \*/ b" := (union a b) (at level 50, left associativity).
Notation "a /*\ b" := (intersection a b) (at level 40, left associativity).
Notation "a *-> b" := (rpc a b)
(at level 65, right associativity).
Definition pseudo_complement (U : Type) (a:subset U) := a *-> @empty _.
Notation "~* a" := (pseudo_complement a) (at level 35, right associativity).
Definition difference (U : Type) (a b:subset U) := a /*\ ~* b.
Notation "a *\ b" := (difference a b) (at level 40, left associativity).
Section relation_independent.
Variable (a b : Type) (r : a -> b -> Prop).
dual relation
Definition rel_dual := fun x y => r y x.
End relation_independent.
Section poset_bound.
Variable (U : Type).
End relation_independent.
Section poset_bound.
Variable (U : Type).
lb = lower bound
ub = upper bound
lb of a couple
Definition lb2 (r : relation U) x0 x1 := fun x => r x x0 /\ r x x1.
Definition ub2 (r : relation U) := lb2 (rel_dual r).
Definition least r a := fun x => a x /\ lb r a x.
Definition greatest r := least (rel_dual r).
Definition ub2 (r : relation U) := lb2 (rel_dual r).
Definition least r a := fun x => a x /\ lb r a x.
Definition greatest r := least (rel_dual r).
inf = infimum
sup = supremum
Definition sup r := inf (rel_dual r).
End poset_bound.
Section poset_bound_fact.
Variable (U : Type) (r : relation U) (s s0 s1 : subset U).
Definition least_inf : least r s <* inf r s.
Definition greatest_sup : greatest r s <* sup r s.
Definition included_ub_lb : s <* ub r (lb r s).
Definition included_lb_ub : s <* lb r (ub r s).
Definition included_lb : s0 <* s1 -> lb r s1 <* lb r s0.
Definition included_ub : s0 <* s1 -> ub r s1 <* ub r s0.
Definition sup_bound : sup r (lb r s) <* lb r s.
Definition inf_bound : inf r (ub r s) <* ub r s.
End poset_bound.
Section poset_bound_fact.
Variable (U : Type) (r : relation U) (s s0 s1 : subset U).
Definition least_inf : least r s <* inf r s.
Definition greatest_sup : greatest r s <* sup r s.
Definition included_ub_lb : s <* ub r (lb r s).
Definition included_lb_ub : s <* lb r (ub r s).
Definition included_lb : s0 <* s1 -> lb r s1 <* lb r s0.
Definition included_ub : s0 <* s1 -> ub r s1 <* ub r s0.
Definition sup_bound : sup r (lb r s) <* lb r s.
Definition inf_bound : inf r (ub r s) <* ub r s.
arbitrary join produces arbitrary meet and vice versa
Definition sup_included_inf : sup r (lb r s) <* inf r s.
Definition inf_included_sup : inf r (ub r s) <* sup r s.
Let ext_eq_axiom_local := @ext_eq_axiom U.
Definition lb_idemp : lb r s = lb r (ub r (lb r s)).
Definition ub_idemp : ub r s = ub r (lb r (ub r s)).
Definition inf_included_sup : inf r (ub r s) <* sup r s.
Let ext_eq_axiom_local := @ext_eq_axiom U.
Definition lb_idemp : lb r s = lb r (ub r (lb r s)).
Definition ub_idemp : ub r s = ub r (lb r (ub r s)).
the least (with respect to an antisymmetric relation) element is unique
unique to uniqueness
Definition unique2ness : forall x, unique s x -> uniqueness s.
Definition uniqueness_ex : forall x, s x -> uniqueness s -> unique s x.
End poset_bound_fact.
Section definition7.
Variable U : Type.
Definition uniqueness_ex : forall x, s x -> uniqueness s -> unique s x.
End poset_bound_fact.
Section definition7.
Variable U : Type.
bounds with respect to included
Definition lb2_inc := lb2 (@included U).
Definition ub2_inc := ub2 (@included U).
Definition empty_least : least (@included (subset U)) (@full _) (@empty _).
Definition full_greatest : greatest (@included (subset U)) (@full _) (@full _).
End definition7.
Section definition4.
Variable (U : Type) (a a0 a1 b b0 b1 c : subset U).
Let ext_eq_axiom_local := @ext_eq_axiom U.
Definition ext_eq_included : ext_eq a b <-> (a <* b /\ b <* a).
Definition ub2_inc := ub2 (@included U).
Definition empty_least : least (@included (subset U)) (@full _) (@empty _).
Definition full_greatest : greatest (@included (subset U)) (@full _) (@full _).
End definition7.
Section definition4.
Variable (U : Type) (a a0 a1 b b0 b1 c : subset U).
Let ext_eq_axiom_local := @ext_eq_axiom U.
Definition ext_eq_included : ext_eq a b <-> (a <* b /\ b <* a).
included is a poset
union is an upper bound
intersection is a lower bound
Definition bound_intersection : lb2_inc a b (a /*\ b).
Definition included_union_eq : a <* b -> (b = a \*/ b).
Definition included_intersection_eq : a <* b -> (a = a /*\ b).
End definition4.
Section definition8.
Variable (U : Type) (a a0 a1 b b0 b1 c : subset U).
Let ext_eq_axiom_local := @ext_eq_axiom U.
Definition inc_equiv_union : a <* b <-> (b = a \*/ b).
Definition inc_equiv_intersection : a <* b <-> (a = a /*\ b).
Definition union_supremum
: least (@included U) (ub2_inc a b) (a \*/ b).
Definition intersection_infimum
: greatest (@included U) (lb2_inc a b) (a /*\ b).
Definition included_union_eq : a <* b -> (b = a \*/ b).
Definition included_intersection_eq : a <* b -> (a = a /*\ b).
End definition4.
Section definition8.
Variable (U : Type) (a a0 a1 b b0 b1 c : subset U).
Let ext_eq_axiom_local := @ext_eq_axiom U.
Definition inc_equiv_union : a <* b <-> (b = a \*/ b).
Definition inc_equiv_intersection : a <* b <-> (a = a /*\ b).
Definition union_supremum
: least (@included U) (ub2_inc a b) (a \*/ b).
Definition intersection_infimum
: greatest (@included U) (lb2_inc a b) (a /*\ b).
Definition idemp_union : a = a \*/ a.
Definition idemp_intersection : a = a /*\ a.
Definition comm_union : a \*/ b = b \*/ a.
Definition comm_intersection : a /*\ b = b /*\ a.
Definition assoc_union : (a \*/ b) \*/ c = a \*/ (b \*/ c).
Definition assoc_intersection : (a /*\ b) /*\ c = a /*\ (b /*\ c).
Definition absorp_union : a = a /*\ (a \*/ b).
Definition absorp_intersection : a = a \*/ (a /*\ b).
Definition distrib_union :
a \*/ (b0 /*\ b1) = (a \*/ b0) /*\ (a \*/ b1).
Definition distrib_intersection :
a /*\ (b0 \*/ b1) = (a /*\ b0) \*/ (a /*\ b1).
Definition is_empty_eq : is_empty a <-> @empty _ = a.
Definition is_full_eq : is_full a <-> @full _ = a.
Definition neutral_empty : a = a \*/ @empty _.
Definition neutral_full : a = a /*\ @full _.
Definition absorbing_empty : @empty _ = a /*\ @empty _.
Definition absorbing_full : @full _ = a \*/ @full _.
Definition rpc_equiv_greatest
: greatest (@included U) (fun c => a /*\ c <* b) (a *-> b).
Definition rpc_equiv_equiv
: forall c, c <* (a *-> b) <-> c /*\ a <* b.
Definition complement_intersect : @empty _ = a /*\ ~* a.
Definition rpc_id : is_full (a *-> a).
Definition conclusion_included_in_rpc : b <* (a *-> b).
Definition conclusion_eq_rpc : b = b /*\ (a *-> b).
Definition rpc_eval : a /*\ (a *-> b) = a /*\ b.
Definition rpc_equiv_included : a <* b <-> is_full (a *-> b).
Definition rpc_full : @full _ = a *-> @full _.
Definition full_rpc : a = @full _ *-> a.
Definition empty_rpc : @full _ = @empty _ *-> a.
Definition distrib_rpc_intersection :
a *-> b0 /*\ b1 = (a *-> b0) /*\ (a *-> b1).
Definition distrib_union_rpc :
b0 \*/ b1 *-> a = (b0 *-> a) /*\ (b1 *-> a).
Definition intuitionistic_k : is_full (a *-> (b *-> a)).
Definition intuitionistic_s : is_full
((a *-> (b *-> c)) *-> ((a *-> b) *-> (a *-> c))).
Definition intuitionistic_conj_elim_left : is_full
((a /*\ b) *-> a).
Definition intuitionistic_conj_elim_right : is_full
((a /*\ b) *-> b).
Definition intuitionistic_conj_intro : is_full
(a *-> b *-> a /*\ b).
Definition intuitionistic_disj_intro_left : is_full
(a *-> a \*/ b).
Definition intuitionistic_disj_intro_right : is_full
(b *-> a \*/ b).
Definition intuitionistic_disj_elim : is_full
((a0 *-> b) *-> ((a1 *-> b) *-> (a0 \*/ a1 *-> b))).
Definition intuitionistic_contradiction_elim : is_full
(@empty U *-> a).
End definition8.
finite set
graph theory
singleton = eq
Check fun a : U => (refl_equal _) : (eq a) a.
Check fun a b : U => (fun p => p) : (eq a) b -> a = b.
Definition singleton_unique : forall (s : subset U) (a : U),
unique (eq a) a.
Definition singleton_included : forall (s : subset U) a,
s a -> (eq a) <* s.
Definition couple (a b : U) := eq a \*/ eq b.
Definition couple_comm : forall a b, couple a b = couple b a.
End definition5.
Inductive map (U0 U1 : Type) (f : U0 -> U1) (s : subset U0) x1 : Prop
:= Build_map (x0 : _) (_ : s x0) (_ : x1 = f x0).
Definition functor_pres_id : forall (U : Type) (s : subset U),
s = map (@Beroal.Init.id _) s.
Definition functor_pres_comp : forall (U0 U1 U2 : Type)
(f12 : U1 -> U2) (f01 : U0 -> U1) (s : subset U0),
map f12 (map f01 s) = map (cf f12 f01) s.
η, return = singleton. singleton is a natural transformation.
Definition singleton_nt_law : forall (U0 U1 : Type) (f : U0 -> U1) (x : U0),
map f (eq x) = eq (f x).
map f (eq x) = eq (f x).
μ, join
Inductive big_union (U : Type) (ss : subset (subset U)) x : Prop
:= Build_big_union (s : _) (_ : ss s) (_ : s x).
Definition bind (U0 U1:Type) (s : subset U0) (f : U0 -> subset U1)
:= (big_union (map f s)) : subset U1.
:= Build_big_union (s : _) (_ : ss s) (_ : s x).
Definition bind (U0 U1:Type) (s : subset U0) (f : U0 -> subset U1)
:= (big_union (map f s)) : subset U1.
big_union is a natural transformation
Definition big_union_nt_law : forall (U0 U1 : Type)
(f : U0 -> U1) (x : subset (subset U0)),
map f (big_union x) = big_union (map (map f) x).
Definition monad_id_left : forall (U : Type) (a : subset U),
a = big_union (eq a).
Definition monad_id_right : forall (U : Type) (a : subset U),
a = big_union (map (@eq _) a).
Definition monad_assoc : forall (U : Type) (a : subset (subset (subset U))),
big_union (big_union a) = big_union (map (@big_union _) a).
(f : U0 -> U1) (x : subset (subset U0)),
map f (big_union x) = big_union (map (map f) x).
Definition monad_id_left : forall (U : Type) (a : subset U),
a = big_union (eq a).
Definition monad_id_right : forall (U : Type) (a : subset U),
a = big_union (map (@eq _) a).
Definition monad_assoc : forall (U : Type) (a : subset (subset (subset U))),
big_union (big_union a) = big_union (map (@big_union _) a).