(** 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.

Set Implicit Arguments.

(** 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.

(** [a]⊆[b], 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 #<a href="http://coq.inria.fr/V8.1/faq.html##htoc37">Coq's FAQ, "5.2  Axioms."</a># *)
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).



(* ==> Init *)
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.
Proof. firstorder. Qed.

Definition greatest_sup : greatest r s <* sup r s.
Proof. firstorder. Qed.

Definition included_ub_lb : s <* ub r (lb r s).
Proof. firstorder. Qed.

Definition included_lb_ub : s <* lb r (ub r s).
Proof. firstorder. Qed.

Definition included_lb : s0 <* s1 -> lb r s1 <* lb r s0.
Proof. firstorder. Qed.

Definition included_ub : s0 <* s1 -> ub r s1 <* ub r s0.
Proof. firstorder. Qed.

Definition sup_bound : sup r (lb r s) <* lb r s.
Proof. firstorder. Qed.

Definition inf_bound : inf r (ub r s) <* ub r s.
Proof. firstorder. Qed.

(** arbitrary join produces arbitrary meet and vice versa *)
Definition sup_included_inf : sup r (lb r s) <* inf r s.
Proof. firstorder. Qed.

Definition inf_included_sup : inf r (ub r s) <* sup r s.
Proof. firstorder. Qed.

Let ext_eq_axiom_local := @ext_eq_axiom U.

Definition lb_idemp : lb r s = lb r (ub r (lb r s)).
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition ub_idemp : ub r s = ub r (lb r (ub r s)).
Proof. firstorder using ext_eq_axiom_local. Qed.

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

(** [unique] to [uniqueness] *)
Definition unique2ness : forall x, unique s x -> uniqueness s.
Proof.
refine (fun x p => _).
unfold uniqueness.
refine (fun x0 x1 x0in x1in => _).
refine (let p0 := proj2 p in _).
refine (eq_ind _ (fun dep => dep = _) (p0 x1 x1in) _ (p0 x0 x0in)).
Qed.

Definition uniqueness_ex : forall x, s x -> uniqueness s -> unique s x.
Proof. firstorder. Qed.

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 _).
Proof. firstorder. Qed.

Definition full_greatest : greatest (@included (subset U)) (@full _) (@full _).
Proof. firstorder. Qed.

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).
Proof. firstorder. Qed.



(** * Lattice **)

(** [included] is a poset **)
Definition included_order : order _ (@included U).
Proof. firstorder using Build_order ext_eq_axiom_local. Qed.



(** ** Relating [included], [union], [intersection] *)

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

(** intersection is a lower bound *)
Definition bound_intersection : lb2_inc a b (a /*\ b).
Proof. firstorder. Qed.

Definition included_union_eq : a <* b -> (b = a \*/ b).
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition included_intersection_eq : a <* b -> (a = a /*\ b).
Proof. firstorder using ext_eq_axiom_local. Qed.

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).
Proof.
refine (conj (@included_union_eq _ _ _) _).
refine (fun eq0 => _).
rewrite eq0.
refine (proj1 (bound_union a b)).
Qed.

Definition inc_equiv_intersection : a <* b <-> (a = a /*\ b).
Proof.
refine (conj (@included_intersection_eq _ _ _) _).
refine (fun eq0 => _).
rewrite eq0.
refine (proj2 (bound_intersection a b)).
Qed.

Definition union_supremum
	: least (@included U) (ub2_inc a b) (a \*/ b).
Proof. firstorder. Qed.

Definition intersection_infimum
	: greatest (@included U) (lb2_inc a b) (a /*\ b).
Proof. firstorder. Qed.



(** ** Algebraic properties *)

Definition idemp_union : a = a \*/ a.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition idemp_intersection : a = a /*\ a.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition comm_union : a \*/ b = b \*/ a.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition comm_intersection : a /*\ b = b /*\ a.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition assoc_union : (a \*/ b) \*/ c = a \*/ (b \*/ c).
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition assoc_intersection : (a /*\ b) /*\ c = a /*\ (b /*\ c).
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition absorp_union : a = a /*\ (a \*/ b).
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition absorp_intersection : a = a \*/ (a /*\ b).
Proof. firstorder using ext_eq_axiom_local. Qed.



(** * Distributive lattice **)

Definition distrib_union : 
	a \*/ (b0 /*\ b1) = (a \*/ b0) /*\ (a \*/ b1).
Proof. firstorder using Build_order  ext_eq_axiom_local. Qed.

Definition distrib_intersection :
	a /*\ (b0 \*/ b1) = (a /*\ b0) \*/ (a /*\ b1).
Proof. firstorder using ext_eq_axiom_local. Qed.



(** * Bounded lattice **)

Definition is_empty_eq : is_empty a <-> @empty _ = a.
Proof.
refine (conj
		(fun _ => ext_eq_axiom_local (fun _ => conj _ _))
		(fun eq0 => eq_ind _ (@is_empty _) _ _ eq0))
	; firstorder.
Qed.

Definition is_full_eq : is_full a <-> @full _ = a.
Proof.
refine (conj
		(fun _ => ext_eq_axiom_local (fun _ => conj _ _))
		(fun eq0 => eq_ind _ (@is_full _) _ _ eq0))
	; firstorder.
Qed.

Definition neutral_empty : a = a \*/ @empty _.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition neutral_full : a = a /*\ @full _.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition absorbing_empty : @empty _ = a /*\ @empty _.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition absorbing_full : @full _ = a \*/ @full _.
Proof. firstorder using ext_eq_axiom_local. Qed.



(** * Heyting algebra *)

(** ** Definitions of rpc *)

Definition rpc_equiv_greatest
	: greatest (@included U) (fun c => a /*\ c <* b) (a *-> b).
Proof. firstorder. Qed.

Definition rpc_equiv_equiv
	: forall c, c <* (a *-> b) <-> c /*\ a <* b.
Proof. firstorder. Qed.

(** ** Miscellaneous *)

Definition complement_intersect : @empty _ = a /*\ ~* a.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition rpc_id : is_full (a *-> a).
Proof. firstorder. Qed.

Definition conclusion_included_in_rpc : b <* (a *-> b).
Proof. firstorder. Qed.

Definition conclusion_eq_rpc : b = b /*\ (a *-> b).
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition rpc_eval : a /*\ (a *-> b) = a /*\ b.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition rpc_equiv_included : a <* b <-> is_full (a *-> b).
Proof. firstorder. Qed.

Definition rpc_full : @full _ = a *-> @full _.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition full_rpc : a = @full _ *-> a.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition empty_rpc : @full _ = @empty _ *-> a.
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition distrib_rpc_intersection :
	a *-> b0 /*\ b1 = (a *-> b0) /*\ (a *-> b1).
Proof. firstorder using ext_eq_axiom_local. Qed.

Definition distrib_union_rpc :
	b0 \*/ b1 *-> a = (b0 *-> a) /*\ (b1 *-> a).
Proof. firstorder using ext_eq_axiom_local. Qed.



(** * Axioms of intuitionistic logic *)

Definition intuitionistic_k : is_full (a *-> (b *-> a)).
Proof. firstorder. Qed.

Definition intuitionistic_s : is_full
	((a *-> (b *-> c)) *-> ((a *-> b) *-> (a *-> c))).
Proof. firstorder. Qed.

Definition intuitionistic_conj_elim_left : is_full
	((a /*\ b) *-> a).
Proof. firstorder. Qed.

Definition intuitionistic_conj_elim_right : is_full
	((a /*\ b) *-> b).
Proof. firstorder. Qed.

Definition intuitionistic_conj_intro : is_full
	(a *-> b *-> a /*\ b).
Proof. firstorder. Qed.

Definition intuitionistic_disj_intro_left : is_full
	(a *-> a \*/ b).
Proof. firstorder. Qed.

Definition intuitionistic_disj_intro_right : is_full
	(b *-> a \*/ b).
Proof. firstorder. Qed.

Definition intuitionistic_disj_elim : is_full
	((a0 *-> b) *-> ((a1 *-> b) *-> (a0 \*/ a1 *-> b))).
Proof. firstorder. Qed.

Definition intuitionistic_contradiction_elim : is_full
	(@empty U *-> a).
Proof. firstorder. Qed.

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.
Proof. firstorder. Qed.

Definition singleton_included : forall (s : subset U) a,
	s a -> (eq a) <* s.
Proof. congruence. Qed.

Definition couple (a b : U) := eq a \*/ eq b.

Definition couple_comm : forall a b, couple a b = couple b a.
Proof. firstorder using ext_eq_axiom_local. Qed.

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.
Proof.
refine (fun U s => ext_eq_axiom (fun x => conj _ _)).
refine (fun in0 => _).
	refine (Build_map _ _ x in0 (refl_equal _)).
refine (fun in0 => _).
	destruct in0 as [x1 in1 eq1].
	refine (eq_ind _ s in1 _ (sym_eq eq1)).
Qed.

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.
Proof.
refine (fun U0 U1 U2 f12 f01 s => ext_eq_axiom (fun x => conj _ _)).
refine (fun in0 => _).
	destruct in0 as [x1 in1 eq1].
	destruct in1 as [x2 in2 eq2].
	refine (Build_map _ _ x2 in2 _).
	refine (eq_ind _ (fun dep => x = f12 dep) eq1 _ eq2).
refine (fun in0 => _).
	destruct in0 as [x1 in1 eq1].
	refine (Build_map _ _ (f01 x1) _ _).
	refine (Build_map _ _ x1 in1 (refl_equal _)).
	refine (eq1).
Qed.



(** * 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).
Proof.
refine (fun U0 U1 f x => ext_eq_axiom (fun x0 => conj _ _)).
refine (fun in0 => _).
	destruct in0 as [x1 in1 eq1].
	refine (sym_eq (eq_ind _ (fun dep => _ = f dep) eq1 _ (sym_eq in1))).
refine (fun eq0 => _).
	refine (Build_map _ _ x (refl_equal _) (sym_eq eq0)).
Qed.



(** μ, 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).
Proof.
refine (fun U0 U1 f x => ext_eq_axiom (fun x0 => conj _ _)).
refine (fun in0 => _).
	destruct in0 as [x1 in1 eq1].
	destruct in1 as [x2 in2 in3].
	refine (Build_big_union (map (map f) x) x0 (map f x2) _ _).
		refine (Build_map _ _ x2 in2 (refl_equal _)).
		refine (Build_map _ _ x1 in3 eq1).
refine (fun in0 => _).
	destruct in0 as [a1 sa1 ax1].
	destruct sa1 as [x1 in1 eq1].
	rewrite eq1 in ax1.
	destruct ax1 as [x2 in2 eq2].
	refine (Build_map _ _ x2 _ eq2).
	refine (Build_big_union _ _ x1 in1 in2).
Qed.

Definition monad_id_left : forall (U : Type) (a : subset U),
	a = big_union (eq a).
Proof.
refine (fun U a => _).
refine (ext_eq_axiom _).
unfold ext_eq.
firstorder using ext_eq Build_big_union.
congruence.
Qed.

Definition monad_id_right : forall (U : Type) (a : subset U),
	a = big_union (map (@eq _) a).
Proof.
refine (fun U a => _).
refine (ext_eq_axiom _).
unfold ext_eq.
refine (fun x => conj _ _).
refine (fun in0 => _).
	refine (Build_big_union _ _ (eq x) _ (refl_equal _)).
	refine (Build_map _ _ x in0 (refl_equal _)).
refine (fun in0 => _).
	destruct in0 as [b p0 p1].
	destruct p0 as [c p2 p3].
	rewrite p3 in p1.
	rewrite <- p1.
	refine (p2).
Qed.

Definition monad_assoc : forall (U : Type) (a : subset (subset (subset U))),
	big_union (big_union a) = big_union (map (@big_union _) a).
Proof.
refine (fun U a => _).
refine (ext_eq_axiom _).
unfold ext_eq.
refine (fun x => conj _ _).
refine (fun in0 => _).
	destruct in0 as [b p0 p1].
	destruct p0 as [c p2 p3].
	refine (Build_big_union _ _ (big_union c) _ _).
		refine (Build_map _ _ c p2 (refl_equal _)).
		refine (Build_big_union _ _ b p3 p1).
refine (fun in0 => _).
	destruct in0 as [b p0 p1].
	destruct p0 as [c p2 p3].
	rewrite p3 in p1.
	clear b p3.
	destruct p1 as [d p4 p5].
	refine (Build_big_union _ _ d _ p5).
	refine (Build_big_union _ _ c p2 p4).
Qed.