(** 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 #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). (* ==> 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.