# 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.

# Definitions

Section definition0.
Universum. We consider subsets of U.
Variable U : Type.

Definition subset := U -> Prop.
Let op2_type := subset -> subset -> subset.

∈, "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
Definition ext_eq a b := forall x : U, a x <-> b x.

ab, non-strictly
Definition included (a b:subset) := forall x, a x -> b x.

"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.

Definition empty : subset := fun x => False.

the whole U
Definition full : subset := fun x => True.

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.

rpc = relative pseudo-complement
Definition rpc : op2_type := @pw _ _ _ (fun a b:Prop => a -> b).

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).
dual relation
Definition rel_dual := fun x y => r y x.
End relation_independent.

Section poset_bound.
Variable (U : Type).

# Subsets of a poset

lb = lower bound
Definition lb (r : relation U) a := fun x => forall x0, a x0 -> r x x0.

ub = upper bound
Definition ub r := lb (rel_dual r).

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).

inf = infimum
Definition inf r a := greatest r (lb r a).

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.

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)).

the least (with respect to an antisymmetric relation) element is unique
Definition unique_least_antisym :
antisymmetric _ r -> uniqueness (least r s).

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.

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).

# Lattice

included is a poset
Definition included_order : order _ (@included U).

## Relating included, union, intersection

union is an upper bound
Definition bound_union : ub2_inc a b (a \*/ b).

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).

## Algebraic properties

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).

# Bounded lattice

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 _.

# Heyting algebra

## Definitions of rpc

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.

## Miscellaneous

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).

# Axioms of intuitionistic logic

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.

# Miscellaneous

Section definition5.
Variable (U : Type).
Let ext_eq_axiom_local := @ext_eq_axiom U.

finite set
Definition from_list (l : list U) := fun x => In x l.

graph theory
Definition clique (r:relation U) c := forall a, c a -> forall b, c b -> r a b.

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.

# subset is a functor

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.

# Monad of subsets

η, 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).

μ, 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.

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).