Ord.jlat
A join semi lattice is an ordType in which we can compute all finite limits.
Require Import base order adjunction.
Module JLat.
Record mixin_of (T : ordType) := Mixin {
bot : T;
join : T -> T -> T;
_ : forall x, bot <= x;
_ : forall x y, is_lub (pairb x y) (join x y)
}.
Section ClassDef.
Record class_of (T : Type) := Class {
base : Ord.class_of T;
mixin : mixin_of (Ord.Pack base T)
}.
Local Coercion base : class_of >-> Ord.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (@Ord.Pack T b0 T)) :=
fun bT b & phant_id (Ord.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
Definition proType := @Pro.Pack cT xclass xT.
Definition ordType := @Ord.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> Ord.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion proType : type >-> Pro.type.
Canonical proType.
Coercion ordType : type >-> Ord.type.
Canonical ordType.
Notation jlat := type.
Notation JLat T m := (@pack T _ m _ _ id _ id).
Notation JLatMixin := Mixin.
Notation "[ 'jlat' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'jlat' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'jlat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'jlat' 'of' T ]") : form_scope.
End Exports.
End JLat.
Export JLat.Exports.
Definition bot (X : jlat) : X := JLat.bot (JLat.class X).
Definition join (X : jlat) : X -> X -> X := JLat.join (JLat.class X).
Arguments bot {X}.
Arguments join {X} x y.
Notation "x '\cup' y" := (join x y) (at level 50, left associativity) : ord_scope.
Section JoinLemmas.
Variable X : jlat.
Implicit Types (x y z : X).
Lemma join_axiom {x y} : is_lub (pairb x y) (x \cup y).
Proof. by case: X x y => ?[?[]]. Qed.
Lemma botE x : bot <= x.
Proof. by case: X x => ?[?[]]. Qed.
Hint Resolve botE.
Lemma joinE x y z : x <= z -> y <= z -> x \cup y <= z.
Proof. move=> le_x_z le_y_z. by rewrite join_axiom => -[]. Qed.
Lemma joinIl x y z : x <= y -> x <= y \cup z.
Proof. move->. exact: ubP true join_axiom. Qed.
Lemma joinIr x y z : x <= z -> x <= y \cup z.
Proof. move->. exact: ubP false join_axiom. Qed.
Lemma joinxx : idempotent (@join X).
Proof. move=> x. apply: le_eq. exact: joinE. exact: joinIl. Qed.
Lemma joinC : commutative (@join X).
Proof. move=> x y. by apply: le_eq; eauto using joinE, joinIl,joinIr. Qed.
Lemma joinA : associative (@join X).
Proof. move=> x y z. apply: le_eq; eauto 8 using joinE, joinIl, joinIr. Qed.
Lemma joinAC : right_commutative (@join X).
Proof. move=> x y z. by rewrite -joinA [_ \cup z]joinC joinA. Qed.
Lemma joinCA : left_commutative (@join X).
Proof. move=> x y z. by rewrite joinA [_ \cup y]joinC -joinA. Qed.
Lemma joinACA : interchange (@join X) (@join X).
Proof. move=> w x y z. by rewrite -joinA [x \cup _]joinCA joinA. Qed.
Lemma joinBx x : bot \cup x = x.
Proof. apply: le_eq. exact: joinE. exact: joinIr. Qed.
Lemma joinxB x : x \cup bot = x.
Proof. by rewrite joinC joinBx. Qed.
Lemma bot_eq x : x <= bot -> x = bot.
Proof. move=> h. exact: le_eq. Qed.
Lemma le_joinP x y : (x <= y) <-> (x \cup y = y).
Proof.
split=> [h|<-]. apply: le_eq; [exact: joinE|exact: joinIr]. exact: joinIl.
Qed.
Lemma join_mono (x1 x2 y1 y2 : X) :
x1 <= x2 -> y1 <= y2 -> x1 \cup y1 <= x2 \cup y2.
Proof. move=> h1 h2. apply: joinE; by eauto using joinIl, joinIr. Qed.
Global Instance join_monor x : monotone (join x).
Proof. move=> y1 y2. exact: join_mono. Qed.
Global Instance join_monol y : monotone (join^~ y).
Proof. move=> x1 x2 h. exact: join_mono. Qed.
Global Instance join_proper : Proper (ord_op ++> ord_op ++> ord_op) (@join X).
Proof. move=> x1 x2 le1 y1 y2 le2. exact: join_mono. Qed.
Canonical join_monoid := Monoid.Law joinA joinBx joinxB.
Canonical join_comoid := Monoid.ComLaw joinC.
End JoinLemmas.
Hint Resolve botE.
Arguments join_axiom {T x y} z : rename.
Section JoinMFun.
Variables (X Y : jlat) (f : X -> Y).
Context {fP : monotone f}.
Implicit Types (x y : X).
Lemma monoJ x y : f x \cup f y <= f (x \cup y).
Proof. apply: joinE; apply: mono. exact: joinIl. exact: joinIr. Qed.
End JoinMFun.
Lemma mk_join {X : proType} (op : X -> X -> X) (x y : X) :
x <= op x y ->
y <= op x y ->
(forall z, x <= z -> y <= z -> op x y <= z) ->
is_lub (pairb x y) (op x y).
Proof.
move=> h1 h2 h3 z. split=> [l[]/=|ub]. by rewrite h1. by rewrite h2.
apply: h3. exact: (ub true). exact: (ub false).
Qed.
Notation "\cup_ i F" := (\big[join/bot]_i F%ORD)
(at level 36, F at level 36, i at level 0,
format "'[' \cup_ i '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i <- r | P ) F" := (\big[join/bot]_(i <- r | P%B) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cup_ ( i <- r | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i <- r ) F" := (\big[join/bot]_(i <- r) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cup_ ( i <- r ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( m <= i < n | P ) F" := (\big[join/bot]_(m <= i < n | P%B) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cup_ ( m <= i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( m <= i < n ) F" := (\big[join/bot]_(m <= i < n) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cup_ ( m <= i < n ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i | P ) F" := (\big[join/bot]_(i | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
format "'[' \cup_ ( i | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i : t | P ) F" := (\big[join/bot]_(i : t | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cup_ ( i : t ) F" := (\big[join/bot]_(i : t) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cup_ ( i < n | P ) F" := (\big[join/bot]_(i < n | P%B) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cup_ ( i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i < n ) F" := (\big[join/bot]_(i < n) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cup_ ( i < n ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i 'in' A | P ) F" := (\big[join/bot]_(i in A | P%B) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cup_ ( i 'in' A | P ) F ']'") : ord_scope.
Notation "\cup_ ( i 'in' A ) F" := (\big[join/bot]_(i in A) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cup_ ( i 'in' A ) '/ ' F ']'") : ord_scope.
Section JoinBigops.
Variable (I : eqType) (T : jlat).
Implicit Types (r : seq I) (P : pred I) (F : I -> T) (x : T).
Lemma bigcupP r P F x :
{in r, forall i, P i -> F i <= x} <-> (\cup_(i <- r | P i) F i <= x).
Proof.
split=> h. elim: r h => [|i r ih] h. by rewrite big_nil.
rewrite big_cons. case: ifP => [pi|]. apply: joinE. apply: h pi.
by rewrite inE eqxx. apply: ih => j mem. apply: h. by rewrite inE mem orbT.
move=> _. apply: ih => j mem. apply: h. by rewrite inE mem orbT.
move=> i mem pi. apply: le_trans h. rewrite (big_rem _ mem) /= pi. exact: joinIl.
Qed.
Lemma bigcupE r P F x :
{in r, forall i, P i -> F i <= x} -> \cup_(i <- r | P i) F i <= x.
Proof. by rewrite bigcupP. Qed.
Lemma bigcupI r P F i x :
i \in r -> P i -> x <= F i -> x <= \cup_(i <- r | P i) F i.
Proof.
move=> h1 h2 h3. apply: le_trans h3 _. move: {x} i h1 h2.
change {in r, forall i, P i -> F i <= \cup_(j <- r | P j) F j}.
by rewrite bigcupP.
Qed.
End JoinBigops.
Section JoinAdjunction.
Variable (X Y : jlat) (f : X -> Y).
Context {g : Y -> X} {fP : is_adjunction f g}.
Lemma adjJ x y : f (x \cup y) = f x \cup f y.
Proof.
apply: lub_uniq join_axiom. rewrite -pairb_fun.
apply: adj_lub. exact: join_axiom.
Qed.
Lemma adjB : f bot = bot.
Proof. apply: bot_eq. by rewrite adjP. Qed.
Lemma adjJb (I : Type) (r : seq I) (P : pred I) (F : I -> X) :
f (\cup_(i <- r | P i) F i) = \cup_(i <- r | P i) f (F i).
Proof. apply: big_morph. exact: adjJ. exact: adjB. Qed.
End JoinAdjunction.
Section JoinClosure.
Variable (X : jlat) (c : X -> X).
Context {cP : is_closure c}.
Lemma closureJ x y :
c (c x \cup c y) = c (x \cup y).
Proof.
apply: closure_lub join_axiom => z. by rewrite pairb_fun join_axiom.
Qed.
End JoinClosure.
Section JoinKernel.
Variable (X : jlat) (k : X -> X).
Context {kP : is_kernel k}.
Lemma kernelJ x y :
k (k x \cup k y) = k x \cup k y.
Proof.
apply: (kernel_lub (f := pairb x y)). rewrite pairb_fun.
exact: join_axiom.
Qed.
Lemma kernelB : k bot = bot.
Proof. apply: bot_eq. exact: kernel_dec. Qed.
End JoinKernel.
Module JLat.
Record mixin_of (T : ordType) := Mixin {
bot : T;
join : T -> T -> T;
_ : forall x, bot <= x;
_ : forall x y, is_lub (pairb x y) (join x y)
}.
Section ClassDef.
Record class_of (T : Type) := Class {
base : Ord.class_of T;
mixin : mixin_of (Ord.Pack base T)
}.
Local Coercion base : class_of >-> Ord.class_of.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack b0 (m0 : mixin_of (@Ord.Pack T b0 T)) :=
fun bT b & phant_id (Ord.class bT) b =>
fun m & phant_id m0 m => Pack (@Class T b m) T.
Definition proType := @Pro.Pack cT xclass xT.
Definition ordType := @Ord.Pack cT xclass xT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> Ord.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion proType : type >-> Pro.type.
Canonical proType.
Coercion ordType : type >-> Ord.type.
Canonical ordType.
Notation jlat := type.
Notation JLat T m := (@pack T _ m _ _ id _ id).
Notation JLatMixin := Mixin.
Notation "[ 'jlat' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'jlat' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'jlat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'jlat' 'of' T ]") : form_scope.
End Exports.
End JLat.
Export JLat.Exports.
Definition bot (X : jlat) : X := JLat.bot (JLat.class X).
Definition join (X : jlat) : X -> X -> X := JLat.join (JLat.class X).
Arguments bot {X}.
Arguments join {X} x y.
Notation "x '\cup' y" := (join x y) (at level 50, left associativity) : ord_scope.
Section JoinLemmas.
Variable X : jlat.
Implicit Types (x y z : X).
Lemma join_axiom {x y} : is_lub (pairb x y) (x \cup y).
Proof. by case: X x y => ?[?[]]. Qed.
Lemma botE x : bot <= x.
Proof. by case: X x => ?[?[]]. Qed.
Hint Resolve botE.
Lemma joinE x y z : x <= z -> y <= z -> x \cup y <= z.
Proof. move=> le_x_z le_y_z. by rewrite join_axiom => -[]. Qed.
Lemma joinIl x y z : x <= y -> x <= y \cup z.
Proof. move->. exact: ubP true join_axiom. Qed.
Lemma joinIr x y z : x <= z -> x <= y \cup z.
Proof. move->. exact: ubP false join_axiom. Qed.
Lemma joinxx : idempotent (@join X).
Proof. move=> x. apply: le_eq. exact: joinE. exact: joinIl. Qed.
Lemma joinC : commutative (@join X).
Proof. move=> x y. by apply: le_eq; eauto using joinE, joinIl,joinIr. Qed.
Lemma joinA : associative (@join X).
Proof. move=> x y z. apply: le_eq; eauto 8 using joinE, joinIl, joinIr. Qed.
Lemma joinAC : right_commutative (@join X).
Proof. move=> x y z. by rewrite -joinA [_ \cup z]joinC joinA. Qed.
Lemma joinCA : left_commutative (@join X).
Proof. move=> x y z. by rewrite joinA [_ \cup y]joinC -joinA. Qed.
Lemma joinACA : interchange (@join X) (@join X).
Proof. move=> w x y z. by rewrite -joinA [x \cup _]joinCA joinA. Qed.
Lemma joinBx x : bot \cup x = x.
Proof. apply: le_eq. exact: joinE. exact: joinIr. Qed.
Lemma joinxB x : x \cup bot = x.
Proof. by rewrite joinC joinBx. Qed.
Lemma bot_eq x : x <= bot -> x = bot.
Proof. move=> h. exact: le_eq. Qed.
Lemma le_joinP x y : (x <= y) <-> (x \cup y = y).
Proof.
split=> [h|<-]. apply: le_eq; [exact: joinE|exact: joinIr]. exact: joinIl.
Qed.
Lemma join_mono (x1 x2 y1 y2 : X) :
x1 <= x2 -> y1 <= y2 -> x1 \cup y1 <= x2 \cup y2.
Proof. move=> h1 h2. apply: joinE; by eauto using joinIl, joinIr. Qed.
Global Instance join_monor x : monotone (join x).
Proof. move=> y1 y2. exact: join_mono. Qed.
Global Instance join_monol y : monotone (join^~ y).
Proof. move=> x1 x2 h. exact: join_mono. Qed.
Global Instance join_proper : Proper (ord_op ++> ord_op ++> ord_op) (@join X).
Proof. move=> x1 x2 le1 y1 y2 le2. exact: join_mono. Qed.
Canonical join_monoid := Monoid.Law joinA joinBx joinxB.
Canonical join_comoid := Monoid.ComLaw joinC.
End JoinLemmas.
Hint Resolve botE.
Arguments join_axiom {T x y} z : rename.
Section JoinMFun.
Variables (X Y : jlat) (f : X -> Y).
Context {fP : monotone f}.
Implicit Types (x y : X).
Lemma monoJ x y : f x \cup f y <= f (x \cup y).
Proof. apply: joinE; apply: mono. exact: joinIl. exact: joinIr. Qed.
End JoinMFun.
Lemma mk_join {X : proType} (op : X -> X -> X) (x y : X) :
x <= op x y ->
y <= op x y ->
(forall z, x <= z -> y <= z -> op x y <= z) ->
is_lub (pairb x y) (op x y).
Proof.
move=> h1 h2 h3 z. split=> [l[]/=|ub]. by rewrite h1. by rewrite h2.
apply: h3. exact: (ub true). exact: (ub false).
Qed.
Notation "\cup_ i F" := (\big[join/bot]_i F%ORD)
(at level 36, F at level 36, i at level 0,
format "'[' \cup_ i '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i <- r | P ) F" := (\big[join/bot]_(i <- r | P%B) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cup_ ( i <- r | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i <- r ) F" := (\big[join/bot]_(i <- r) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cup_ ( i <- r ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( m <= i < n | P ) F" := (\big[join/bot]_(m <= i < n | P%B) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cup_ ( m <= i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( m <= i < n ) F" := (\big[join/bot]_(m <= i < n) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cup_ ( m <= i < n ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i | P ) F" := (\big[join/bot]_(i | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
format "'[' \cup_ ( i | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i : t | P ) F" := (\big[join/bot]_(i : t | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cup_ ( i : t ) F" := (\big[join/bot]_(i : t) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cup_ ( i < n | P ) F" := (\big[join/bot]_(i < n | P%B) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cup_ ( i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i < n ) F" := (\big[join/bot]_(i < n) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cup_ ( i < n ) '/ ' F ']'") : ord_scope.
Notation "\cup_ ( i 'in' A | P ) F" := (\big[join/bot]_(i in A | P%B) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cup_ ( i 'in' A | P ) F ']'") : ord_scope.
Notation "\cup_ ( i 'in' A ) F" := (\big[join/bot]_(i in A) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cup_ ( i 'in' A ) '/ ' F ']'") : ord_scope.
Section JoinBigops.
Variable (I : eqType) (T : jlat).
Implicit Types (r : seq I) (P : pred I) (F : I -> T) (x : T).
Lemma bigcupP r P F x :
{in r, forall i, P i -> F i <= x} <-> (\cup_(i <- r | P i) F i <= x).
Proof.
split=> h. elim: r h => [|i r ih] h. by rewrite big_nil.
rewrite big_cons. case: ifP => [pi|]. apply: joinE. apply: h pi.
by rewrite inE eqxx. apply: ih => j mem. apply: h. by rewrite inE mem orbT.
move=> _. apply: ih => j mem. apply: h. by rewrite inE mem orbT.
move=> i mem pi. apply: le_trans h. rewrite (big_rem _ mem) /= pi. exact: joinIl.
Qed.
Lemma bigcupE r P F x :
{in r, forall i, P i -> F i <= x} -> \cup_(i <- r | P i) F i <= x.
Proof. by rewrite bigcupP. Qed.
Lemma bigcupI r P F i x :
i \in r -> P i -> x <= F i -> x <= \cup_(i <- r | P i) F i.
Proof.
move=> h1 h2 h3. apply: le_trans h3 _. move: {x} i h1 h2.
change {in r, forall i, P i -> F i <= \cup_(j <- r | P j) F j}.
by rewrite bigcupP.
Qed.
End JoinBigops.
Section JoinAdjunction.
Variable (X Y : jlat) (f : X -> Y).
Context {g : Y -> X} {fP : is_adjunction f g}.
Lemma adjJ x y : f (x \cup y) = f x \cup f y.
Proof.
apply: lub_uniq join_axiom. rewrite -pairb_fun.
apply: adj_lub. exact: join_axiom.
Qed.
Lemma adjB : f bot = bot.
Proof. apply: bot_eq. by rewrite adjP. Qed.
Lemma adjJb (I : Type) (r : seq I) (P : pred I) (F : I -> X) :
f (\cup_(i <- r | P i) F i) = \cup_(i <- r | P i) f (F i).
Proof. apply: big_morph. exact: adjJ. exact: adjB. Qed.
End JoinAdjunction.
Section JoinClosure.
Variable (X : jlat) (c : X -> X).
Context {cP : is_closure c}.
Lemma closureJ x y :
c (c x \cup c y) = c (x \cup y).
Proof.
apply: closure_lub join_axiom => z. by rewrite pairb_fun join_axiom.
Qed.
End JoinClosure.
Section JoinKernel.
Variable (X : jlat) (k : X -> X).
Context {kP : is_kernel k}.
Lemma kernelJ x y :
k (k x \cup k y) = k x \cup k y.
Proof.
apply: (kernel_lub (f := pairb x y)). rewrite pairb_fun.
exact: join_axiom.
Qed.
Lemma kernelB : k bot = bot.
Proof. apply: bot_eq. exact: kernel_dec. Qed.
End JoinKernel.
Instances
Section NatJLat.
Implicit Types (n m : nat).
Lemma nat_le_bot n : 0 <= n. by []. Qed.
Lemma nat_le_join m n : is_lub (pairb m n) (maxn m n).
Proof.
apply: mk_join => [||/=k le_m_k le_n_k]. exact: leq_maxl. exact: leq_maxr.
rewrite/ord_op/=/nat_le geq_max. exact/andP.
Qed.
Canonical nat_jlatMixin := JLatMixin nat_le_bot nat_le_join.
Canonical nat_jlat := Eval hnf in JLat nat nat_jlatMixin.
End NatJLat.
Section PropJLat.
Implicit Types (P Q : Prop).
Lemma prop_le_bot P : False <= P. by []. Qed.
Lemma prop_le_join P Q : is_lub (pairb P Q) (P \/ Q).
Proof. apply: mk_join; by firstorder. Qed.
Canonical prop_jlatMixin := JLatMixin prop_le_bot prop_le_join.
Canonical prop_jlat := Eval hnf in JLat Prop prop_jlatMixin.
End PropJLat.
Section PairJLat.
Variable (X Y : jlat).
Implicit Types (p q r : X * Y).
Definition pair_bot : X * Y := (bot, bot).
Definition pair_join p q := (p.1 \cup q.1, p.2 \cup q.2).
Lemma pair_le_bot p : pair_bot <= p. by split=>/=. Qed.
Lemma pair_le_join p q : is_lub (pairb p q) (pair_join p q).
Proof.
apply: mk_join; try solve [split=> /=; eauto using joinIl, joinIr].
move=> [x y] [/=le_p_x le_p_y] [/=le_q_x le_q_y]. split; exact: joinE.
Qed.
Canonical pair_jlatMixin := JLatMixin pair_le_bot pair_le_join.
Canonical pair_jlat := Eval hnf in JLat (X * Y) pair_jlatMixin.
End PairJLat.
Section IProdJLat.
Variables (T : Type) (F : T -> jlat).
Implicit Types (f g : iprod F).
Definition iprod_bot : iprod F := fun _ => bot.
Definition iprod_join f g : iprod F := fun x => f x \cup g x.
Lemma iprod_le_bot f : iprod_bot <= f. move=> x. exact: botE. Qed.
Lemma iprod_le_join f g : is_lub (pairb f g) (iprod_join f g).
Proof.
apply: mk_join => [||/=h le_f_h le_g_h] x. exact: joinIl. exact: joinIr.
exact: joinE.
Qed.
Canonical iprod_jlatMixin := JLatMixin iprod_le_bot iprod_le_join.
Canonical iprod_jlat := Eval hnf in JLat (iprod F) iprod_jlatMixin.
End IProdJLat.
Canonical prod_jlat (T : Type) (X : jlat) :=
Eval hnf in JLat (T -> X) (@iprod_jlatMixin T (fun _ => X)).
Instance bot_monotone {X : proType} {Y : jlat} : monotone (bot : X -> Y).
Proof. by []. Qed.
Instance join_monotone {X : proType} {Y : jlat} (f g : X -> Y)
{fP : monotone f} {gP : monotone g} : monotone (f \cup g).
Proof. move=> x y le_x_y /=. apply: join_mono; exact: mono. Qed.
Section MFunJLat.
Variables (X : proType) (Y : jlat).
Implicit Types (f g : {mono X -> Y}).
Definition mfun_bot : {mono X -> Y} := mfun bot.
Definition mfun_join f g : {mono X -> Y} := mfun ((f : X -> Y) \cup g).
Lemma mfun_le_bot f : mfun_bot <= f. exact: botE. Qed.
Lemma mfun_le_join f g : is_lub (pairb f g) (mfun_join f g).
Proof.
apply: mk_join. exact: joinIl. exact: joinIr. move=> h. exact: joinE.
Qed.
Canonical mfun_jlatMixin := JLatMixin mfun_le_bot mfun_le_join.
Canonical mfun_jlat := Eval hnf in JLat {mono X -> Y} mfun_jlatMixin.
End MFunJLat.
Lemma nat_botE : (bot : nat) = 0. by []. Qed.
Lemma prop_botE : (bot : Prop) = False. by []. Qed.
Lemma pair_botE (X Y : jlat) : (bot : X * Y) = (bot, bot). by []. Qed.
Lemma iprod_botE (T : Type) (F : T -> jlat) (x : T) :
(bot : iprod F) x = bot.
Proof. by []. Qed.
Lemma prod_botE (T : Type) (X : jlat) (x : T) :
(bot : T -> X) x = bot.
Proof. by []. Qed.
Lemma mfun_botE (X : proType) (Y : jlat) (x : X) :
(bot : {mono X -> Y}) x = bot.
Proof. by []. Qed.
Lemma nat_joinE (m n : nat) : (m \cup n) = maxn m n.
Proof. by []. Qed.
Lemma prop_joinE (P Q : Prop) : (P \cup Q) = (P \/ Q).
Proof. by []. Qed.
Lemma pair_joinE (X Y : jlat) (x1 x2 : X) (y1 y2 : Y) :
((x1,y1) \cup (x2,y2)) = (x1 \cup x2, y1 \cup y2).
Proof. by []. Qed.
Lemma iprod_joinE (T : Type) (F : T -> jlat) (f g : iprod F) (x : T) :
(f \cup g) x = (f x \cup g x).
Proof. by []. Qed.
Lemma prod_joinE (T : Type) (X : jlat) (f g : T -> X) (x : T) :
(f \cup g) x = f x \cup g x.
Proof. by []. Qed.
Lemma mfun_joinE (X : proType) (Y : jlat) (f g : {mono X -> Y}) (x : X) :
(f \cup g) x = f x \cup g x.
Proof. by []. Qed.
Definition bot_simpl :=
(prop_botE, prod_botE, mfun_botE, iprod_botE, pair_botE, nat_botE).
Definition join_simpl :=
(prop_joinE, prod_joinE, mfun_joinE, iprod_joinE, pair_joinE, nat_joinE).