Ord.mlat
A meet semi lattice is an ordType in which we can compute all finite colimits.
Require Import base order adjunction jlat.
Module MLat.
Record mixin_of (T : ordType) := Mixin {
top : T;
meet : T -> T -> T;
_ : forall x, x <= top;
_ : forall x y, is_glb (pairb x y) (meet 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 mlat := type.
Notation MLat T m := (@pack T _ m _ _ id _ id).
Notation MLatMixin := Mixin.
Notation "[ 'mlat' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'mlat' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'mlat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'mlat' 'of' T ]") : form_scope.
End Exports.
End MLat.
Export MLat.Exports.
Definition top (X : mlat) : X := MLat.top (MLat.class X).
Definition meet (X : mlat) : X -> X -> X := MLat.meet (MLat.class X).
Arguments top {X}.
Arguments meet {X} x y.
Notation "x '\cap' y" := (meet x y) (at level 40, left associativity) : ord_scope.
Section MeetAxioms.
Variable X : mlat.
Implicit Types (x y z : X).
Lemma meet_axiom {x y} : is_glb (pairb x y) (x \cap y).
Proof. by case: X x y => ?[?[]]. Qed.
Lemma topI x : x <= top.
Proof. by case: X x => ?[?[]]. Qed.
End MeetAxioms.
Hint Resolve topI.
Arguments meet_axiom {T x y} z : rename.
(* Duality to jlat *)
Section ReverseMLat.
Variable (T : jlat).
Implicit Types (x y : T^r).
Definition reverse_top : T^r := bot.
Definition reverse_meet x y : T^r := join x y.
Lemma reverse_le_top x : x <= reverse_top. exact: botE. Qed.
Lemma reverse_le_meet x y : is_glb (pairb x y) (reverse_meet x y).
Proof. exact: join_axiom. Qed.
Canonical reverse_mlatMixin := MLatMixin reverse_le_top reverse_le_meet.
Canonical reverse_mlat := Eval hnf in MLat T^r reverse_mlatMixin.
End ReverseMLat.
Section ReverseJLat.
Variable (T : mlat).
Implicit Types (x y : T^r).
Definition reverse_bot : T^r := top.
Definition reverse_join x y : T^r := meet x y.
Lemma reverse_le_bot x : reverse_bot <= x. exact: topI. Qed.
Lemma reverse_le_join x y : is_lub (pairb x y) (reverse_join x y).
Proof. exact: meet_axiom. Qed.
Canonical reverse_jlatMixin := JLatMixin reverse_le_bot reverse_le_join.
Canonical reverse_jlat := Eval hnf in JLat T^r reverse_jlatMixin.
End ReverseJLat.
Section MeetLemmas.
Variable X : mlat.
Implicit Types (x y z : X).
Let Y := reverse_jlat X.
Lemma meetI x y z : x <= y -> x <= z -> x <= y \cap z.
Proof. exact: (@joinE Y). Qed.
Lemma meetEl x y z : x <= z -> x \cap y <= z.
Proof. exact: (@joinIl Y). Qed.
Lemma meetEr x y z : y <= z -> x \cap y <= z.
Proof. exact: (@joinIr Y). Qed.
Lemma meetxx : idempotent (@meet X).
Proof. exact: (@joinxx Y). Qed.
Lemma meetC : commutative (@meet X).
Proof. exact: (@joinC Y). Qed.
Lemma meetA : associative (@meet X).
Proof. exact: (@joinA Y). Qed.
Lemma meetAC : right_commutative (@meet X).
Proof. exact: (@joinAC Y). Qed.
Lemma meetCA : left_commutative (@meet X).
Proof. exact: (@joinCA Y). Qed.
Lemma meetACA : interchange (@meet X) (@meet X).
Proof. exact: (@joinACA Y). Qed.
Lemma meetTx x : top \cap x = x.
Proof. exact: (@joinBx Y). Qed.
Lemma meetxT x : x \cap top = x.
Proof. exact: (@joinxB Y). Qed.
Lemma top_eq x : top <= x -> x = top.
Proof. exact: (@bot_eq Y). Qed.
Lemma le_meetP x y : (x <= y) <-> (y \cap x = x).
Proof. exact: (@le_joinP Y). Qed.
Lemma meet_mono (x1 x2 y1 y2 : X) :
x1 <= x2 -> y1 <= y2 -> x1 \cap y1 <= x2 \cap y2.
Proof. exact: (@join_mono Y). Qed.
Global Instance meet_monor x : monotone (meet x).
Proof. move=> y1 y2. exact: (@join_monor Y). Qed.
Global Instance meet_monol y : monotone (meet^~ y).
Proof. move=> x1 x2. exact: (@join_monol Y). Qed.
Global Instance meet_proper : Proper (ord_op ++> ord_op ++> ord_op) (@meet X).
Proof. move=> x y le1 x2 y2 le2. exact: (@join_proper Y). Qed.
Canonical meet_monoid := Monoid.Law meetA meetTx meetxT.
Canonical meet_comoid := Monoid.ComLaw meetC.
End MeetLemmas.
Section MeetMFun.
Variables (X Y : mlat) (f : X -> Y).
Context {fP : monotone f}.
Lemma monoM x y : f (x \cap y) <= f x \cap f y.
Proof. exact: (@monoJ (reverse_jlat X) (reverse_jlat Y)). Qed.
End MeetMFun.
Lemma mk_meet {X : proType} (op : X -> X -> X) (x y : X) :
op x y <= x ->
op x y <= y ->
(forall z, z <= x -> z <= y -> z <= op x y) ->
is_glb (pairb x y) (op x y).
Proof. exact: (@mk_join (reverse_proType X)). Qed.
Notation "\cap_ i F" := (\big[meet/top]_i F%ORD)
(at level 36, F at level 36, i at level 0,
format "'[' \cap_ i '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i <- r | P ) F" := (\big[meet/top]_(i <- r | P%B) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cap_ ( i <- r | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i <- r ) F" := (\big[meet/top]_(i <- r) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cap_ ( i <- r ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( m <= i < n | P ) F" := (\big[meet/top]_(m <= i < n | P%B) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cap_ ( m <= i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( m <= i < n ) F" := (\big[meet/top]_(m <= i < n) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cap_ ( m <= i < n ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i | P ) F" := (\big[meet/top]_(i | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
format "'[' \cap_ ( i | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i : t | P ) F" := (\big[meet/top]_(i : t | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cap_ ( i : t ) F" := (\big[meet/top]_(i : t) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cap_ ( i < n | P ) F" := (\big[meet/top]_(i < n | P%B) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cap_ ( i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i < n ) F" := (\big[meet/top]_(i < n) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cap_ ( i < n ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i 'in' A | P ) F" := (\big[meet/top]_(i in A | P%B) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cap_ ( i 'in' A | P ) F ']'") : ord_scope.
Notation "\cap_ ( i 'in' A ) F" := (\big[meet/top]_(i in A) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cap_ ( i 'in' A ) '/ ' F ']'") : ord_scope.
Section MeetBigops.
Variable (I : eqType) (T : mlat).
Implicit Types (r : seq I) (P : pred I) (F : I -> T) (x : T).
Let X := reverse_jlat T.
Lemma bigcapP r P F x :
{in r, forall i, P i -> x <= F i} <-> (x <= \cap_(i <- r | P i) F i).
Proof. exact: (@bigcupP I X). Qed.
Lemma bigcapI r P F x :
{in r, forall i, P i -> x <= F i} -> x <= \cap_(i <- r | P i) F i.
Proof. exact: (@bigcupE I X). Qed.
Lemma bigcapE r P F i x :
i \in r -> P i -> F i <= x -> \cap_(i <- r | P i) F i <= x.
Proof. exact: (@bigcupI I X). Qed.
End MeetBigops.
Section MeetAdjunction.
Variable (X Y : mlat) (f : X -> Y).
Context {g : Y -> X} {fP : is_adjunction f g}.
Let Xr := reverse_jlat X.
Let Yr := reverse_jlat Y.
Lemma adjM x y : f^* (x \cap y) = f^* x \cap f^* y.
Proof. exact: (@adjJ Yr Xr). Qed.
Lemma adjT : f^* top = top.
Proof. exact: (@adjB Yr Xr). Qed.
Lemma adjMb (I : Type) (r : seq I) (P : pred I) (F : I -> Y) :
f^* (\cap_(i <- r | P i) F i) = \cap_(i <- r | P i) f^* (F i).
Proof. exact: (@adjJb Yr Xr). Qed.
End MeetAdjunction.
Section MeetClosure.
Variable (X : mlat) (c : X -> X).
Context {cP : is_closure c}.
Let Y := reverse_jlat X.
Lemma closureM x y : c (c x \cap c y) = c x \cap c y.
Proof. exact: (@kernelJ Y). Qed.
Lemma closureT : c top = top.
Proof. exact: (@kernelB Y). Qed.
End MeetClosure.
Section MeetKernel.
Variable (X : mlat) (k : X -> X).
Context {kP : is_kernel k}.
Let Y := reverse_jlat X.
Lemma kernelM x y : k (k x \cap k y) = k (x \cap y).
Proof. exact: (@closureJ Y). Qed.
End MeetKernel.
Module MLat.
Record mixin_of (T : ordType) := Mixin {
top : T;
meet : T -> T -> T;
_ : forall x, x <= top;
_ : forall x y, is_glb (pairb x y) (meet 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 mlat := type.
Notation MLat T m := (@pack T _ m _ _ id _ id).
Notation MLatMixin := Mixin.
Notation "[ 'mlat' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'mlat' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'mlat' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'mlat' 'of' T ]") : form_scope.
End Exports.
End MLat.
Export MLat.Exports.
Definition top (X : mlat) : X := MLat.top (MLat.class X).
Definition meet (X : mlat) : X -> X -> X := MLat.meet (MLat.class X).
Arguments top {X}.
Arguments meet {X} x y.
Notation "x '\cap' y" := (meet x y) (at level 40, left associativity) : ord_scope.
Section MeetAxioms.
Variable X : mlat.
Implicit Types (x y z : X).
Lemma meet_axiom {x y} : is_glb (pairb x y) (x \cap y).
Proof. by case: X x y => ?[?[]]. Qed.
Lemma topI x : x <= top.
Proof. by case: X x => ?[?[]]. Qed.
End MeetAxioms.
Hint Resolve topI.
Arguments meet_axiom {T x y} z : rename.
(* Duality to jlat *)
Section ReverseMLat.
Variable (T : jlat).
Implicit Types (x y : T^r).
Definition reverse_top : T^r := bot.
Definition reverse_meet x y : T^r := join x y.
Lemma reverse_le_top x : x <= reverse_top. exact: botE. Qed.
Lemma reverse_le_meet x y : is_glb (pairb x y) (reverse_meet x y).
Proof. exact: join_axiom. Qed.
Canonical reverse_mlatMixin := MLatMixin reverse_le_top reverse_le_meet.
Canonical reverse_mlat := Eval hnf in MLat T^r reverse_mlatMixin.
End ReverseMLat.
Section ReverseJLat.
Variable (T : mlat).
Implicit Types (x y : T^r).
Definition reverse_bot : T^r := top.
Definition reverse_join x y : T^r := meet x y.
Lemma reverse_le_bot x : reverse_bot <= x. exact: topI. Qed.
Lemma reverse_le_join x y : is_lub (pairb x y) (reverse_join x y).
Proof. exact: meet_axiom. Qed.
Canonical reverse_jlatMixin := JLatMixin reverse_le_bot reverse_le_join.
Canonical reverse_jlat := Eval hnf in JLat T^r reverse_jlatMixin.
End ReverseJLat.
Section MeetLemmas.
Variable X : mlat.
Implicit Types (x y z : X).
Let Y := reverse_jlat X.
Lemma meetI x y z : x <= y -> x <= z -> x <= y \cap z.
Proof. exact: (@joinE Y). Qed.
Lemma meetEl x y z : x <= z -> x \cap y <= z.
Proof. exact: (@joinIl Y). Qed.
Lemma meetEr x y z : y <= z -> x \cap y <= z.
Proof. exact: (@joinIr Y). Qed.
Lemma meetxx : idempotent (@meet X).
Proof. exact: (@joinxx Y). Qed.
Lemma meetC : commutative (@meet X).
Proof. exact: (@joinC Y). Qed.
Lemma meetA : associative (@meet X).
Proof. exact: (@joinA Y). Qed.
Lemma meetAC : right_commutative (@meet X).
Proof. exact: (@joinAC Y). Qed.
Lemma meetCA : left_commutative (@meet X).
Proof. exact: (@joinCA Y). Qed.
Lemma meetACA : interchange (@meet X) (@meet X).
Proof. exact: (@joinACA Y). Qed.
Lemma meetTx x : top \cap x = x.
Proof. exact: (@joinBx Y). Qed.
Lemma meetxT x : x \cap top = x.
Proof. exact: (@joinxB Y). Qed.
Lemma top_eq x : top <= x -> x = top.
Proof. exact: (@bot_eq Y). Qed.
Lemma le_meetP x y : (x <= y) <-> (y \cap x = x).
Proof. exact: (@le_joinP Y). Qed.
Lemma meet_mono (x1 x2 y1 y2 : X) :
x1 <= x2 -> y1 <= y2 -> x1 \cap y1 <= x2 \cap y2.
Proof. exact: (@join_mono Y). Qed.
Global Instance meet_monor x : monotone (meet x).
Proof. move=> y1 y2. exact: (@join_monor Y). Qed.
Global Instance meet_monol y : monotone (meet^~ y).
Proof. move=> x1 x2. exact: (@join_monol Y). Qed.
Global Instance meet_proper : Proper (ord_op ++> ord_op ++> ord_op) (@meet X).
Proof. move=> x y le1 x2 y2 le2. exact: (@join_proper Y). Qed.
Canonical meet_monoid := Monoid.Law meetA meetTx meetxT.
Canonical meet_comoid := Monoid.ComLaw meetC.
End MeetLemmas.
Section MeetMFun.
Variables (X Y : mlat) (f : X -> Y).
Context {fP : monotone f}.
Lemma monoM x y : f (x \cap y) <= f x \cap f y.
Proof. exact: (@monoJ (reverse_jlat X) (reverse_jlat Y)). Qed.
End MeetMFun.
Lemma mk_meet {X : proType} (op : X -> X -> X) (x y : X) :
op x y <= x ->
op x y <= y ->
(forall z, z <= x -> z <= y -> z <= op x y) ->
is_glb (pairb x y) (op x y).
Proof. exact: (@mk_join (reverse_proType X)). Qed.
Notation "\cap_ i F" := (\big[meet/top]_i F%ORD)
(at level 36, F at level 36, i at level 0,
format "'[' \cap_ i '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i <- r | P ) F" := (\big[meet/top]_(i <- r | P%B) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cap_ ( i <- r | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i <- r ) F" := (\big[meet/top]_(i <- r) F%ORD)
(at level 36, F at level 36, i, r at level 50,
format "'[' \cap_ ( i <- r ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( m <= i < n | P ) F" := (\big[meet/top]_(m <= i < n | P%B) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cap_ ( m <= i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( m <= i < n ) F" := (\big[meet/top]_(m <= i < n) F%ORD)
(at level 36, F at level 36, i, m, n at level 50,
format "'[' \cap_ ( m <= i < n ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i | P ) F" := (\big[meet/top]_(i | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
format "'[' \cap_ ( i | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i : t | P ) F" := (\big[meet/top]_(i : t | P%B) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cap_ ( i : t ) F" := (\big[meet/top]_(i : t) F%ORD)
(at level 36, F at level 36, i at level 50,
only parsing) : ord_scope.
Notation "\cap_ ( i < n | P ) F" := (\big[meet/top]_(i < n | P%B) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cap_ ( i < n | P ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i < n ) F" := (\big[meet/top]_(i < n) F%ORD)
(at level 36, F at level 36, i, n at level 50,
format "'[' \cap_ ( i < n ) '/ ' F ']'") : ord_scope.
Notation "\cap_ ( i 'in' A | P ) F" := (\big[meet/top]_(i in A | P%B) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cap_ ( i 'in' A | P ) F ']'") : ord_scope.
Notation "\cap_ ( i 'in' A ) F" := (\big[meet/top]_(i in A) F%ORD)
(at level 36, F at level 36, i, A at level 50,
format "'[' \cap_ ( i 'in' A ) '/ ' F ']'") : ord_scope.
Section MeetBigops.
Variable (I : eqType) (T : mlat).
Implicit Types (r : seq I) (P : pred I) (F : I -> T) (x : T).
Let X := reverse_jlat T.
Lemma bigcapP r P F x :
{in r, forall i, P i -> x <= F i} <-> (x <= \cap_(i <- r | P i) F i).
Proof. exact: (@bigcupP I X). Qed.
Lemma bigcapI r P F x :
{in r, forall i, P i -> x <= F i} -> x <= \cap_(i <- r | P i) F i.
Proof. exact: (@bigcupE I X). Qed.
Lemma bigcapE r P F i x :
i \in r -> P i -> F i <= x -> \cap_(i <- r | P i) F i <= x.
Proof. exact: (@bigcupI I X). Qed.
End MeetBigops.
Section MeetAdjunction.
Variable (X Y : mlat) (f : X -> Y).
Context {g : Y -> X} {fP : is_adjunction f g}.
Let Xr := reverse_jlat X.
Let Yr := reverse_jlat Y.
Lemma adjM x y : f^* (x \cap y) = f^* x \cap f^* y.
Proof. exact: (@adjJ Yr Xr). Qed.
Lemma adjT : f^* top = top.
Proof. exact: (@adjB Yr Xr). Qed.
Lemma adjMb (I : Type) (r : seq I) (P : pred I) (F : I -> Y) :
f^* (\cap_(i <- r | P i) F i) = \cap_(i <- r | P i) f^* (F i).
Proof. exact: (@adjJb Yr Xr). Qed.
End MeetAdjunction.
Section MeetClosure.
Variable (X : mlat) (c : X -> X).
Context {cP : is_closure c}.
Let Y := reverse_jlat X.
Lemma closureM x y : c (c x \cap c y) = c x \cap c y.
Proof. exact: (@kernelJ Y). Qed.
Lemma closureT : c top = top.
Proof. exact: (@kernelB Y). Qed.
End MeetClosure.
Section MeetKernel.
Variable (X : mlat) (k : X -> X).
Context {kP : is_kernel k}.
Let Y := reverse_jlat X.
Lemma kernelM x y : k (k x \cap k y) = k (x \cap y).
Proof. exact: (@closureJ Y). Qed.
End MeetKernel.
Instances
Section PropMLat.
Implicit Types (P Q : Prop).
Lemma prop_le_top P : P <= True. by []. Qed.
Lemma prop_le_meet P Q : is_glb (pairb P Q) (P /\ Q).
Proof. apply: mk_meet; by firstorder. Qed.
Canonical prop_mlatMixin := MLatMixin prop_le_top prop_le_meet.
Canonical prop_mlat := Eval hnf in MLat Prop prop_mlatMixin.
End PropMLat.
Section PairMLat.
Variable (X Y : mlat).
Implicit Types (p q r : X * Y).
Definition pair_top : X * Y := (top, top).
Definition pair_meet p q := (p.1 \cap q.1, p.2 \cap q.2).
Lemma pair_le_top p : p <= pair_top. by split=>/=. Qed.
Lemma pair_le_meet p q : is_glb (pairb p q) (pair_meet p q).
Proof. exact: (@pair_le_join (reverse_jlat X) (reverse_jlat Y)). Qed.
Canonical pair_mlatMixin := MLatMixin pair_le_top pair_le_meet.
Canonical pair_mlat := Eval hnf in MLat (X * Y) pair_mlatMixin.
End PairMLat.
Section IProdMLat.
Variables (T : Type) (F : T -> mlat).
Implicit Types (f g : iprod F).
Definition iprod_top : iprod F := fun _ => top.
Definition iprod_meet f g : iprod F := fun x => f x \cap g x.
Lemma iprod_le_top f : f <= iprod_top. move=> x. exact: topI. Qed.
Lemma iprod_le_meet f g : is_glb (pairb f g) (iprod_meet f g).
Proof. exact: (@iprod_le_join T (reverse_jlat \o F)). Qed.
Canonical iprod_mlatMixin := MLatMixin iprod_le_top iprod_le_meet.
Canonical iprod_mlat := Eval hnf in MLat (iprod F) iprod_mlatMixin.
End IProdMLat.
Canonical prod_mlat (T : Type) (X : mlat) :=
Eval hnf in MLat (T -> X) (@iprod_mlatMixin T (fun _ => X)).
Instance top_monotone {X : proType} {Y : mlat} : monotone (top : X -> Y).
Proof. by []. Qed.
Instance meet_monotone {X : proType} {Y : mlat} (f g : X -> Y)
{fP : monotone f} {gP : monotone g} : monotone (f \cap g).
Proof.
move=> x y. exact: (@join_monotone (reverse_proType X) (reverse_jlat Y)).
Qed.
Section MFunMLat.
Variables (X : proType) (Y : mlat).
Implicit Types (f g : {mono X -> Y}).
Definition mfun_top : {mono X -> Y} := mfun top.
Definition mfun_meet f g : {mono X -> Y} := mfun ((f : X -> Y) \cap g).
Lemma mfun_le_top f : f <= mfun_top. exact: topI. Qed.
Lemma mfun_le_meet f g : is_glb (pairb f g) (mfun_meet f g).
Proof.
apply: mk_meet. exact: meetEl. exact: meetEr. move=> h. exact: meetI.
Qed.
Canonical mfun_mlatMixin := MLatMixin mfun_le_top mfun_le_meet.
Canonical mfun_mlat := Eval hnf in MLat {mono X -> Y} mfun_mlatMixin.
End MFunMLat.
Lemma rev_botE (T : mlat) : (bot : T^r) = top.
Proof. by []. Qed.
Lemma rev_topE (T : jlat) : (top : T^r) = bot.
Proof. by []. Qed.
Lemma rev_joinE (T : mlat) (x y : T^r) : (x \cup y) = (x \cap y).
Proof. by []. Qed.
Lemma rev_meetE (T : jlat) (x y : T^r) : (x \cap y) = (x \cup y).
Proof. by []. Qed.
Definition bot_simpl := (bot_simpl, rev_botE).
Definition join_simpl := (join_simpl, rev_joinE).
Lemma prop_topE : (top : Prop) = True. by []. Qed.
Lemma pair_topE (X Y : mlat) : (top : X * Y) = (top, top). by []. Qed.
Lemma iprod_topE (T : Type) (F : T -> mlat) (x : T) :
(top : iprod F) x = top.
Proof. by []. Qed.
Lemma prod_topE (T : Type) (X : mlat) (x : T) :
(top : T -> X) x = top.
Proof. by []. Qed.
Lemma mfun_topE (X : proType) (Y : mlat) (x : X) :
(top : {mono X -> Y}) x = top.
Proof. by []. Qed.
Lemma prop_meetE (P Q : Prop) : (P \cap Q) = (P /\ Q).
Proof. by []. Qed.
Lemma pair_meetE (X Y : mlat) (x1 x2 : X) (y1 y2 : Y) :
((x1,y1) \cap (x2,y2)) = (x1 \cap x2, y1 \cap y2).
Proof. by []. Qed.
Lemma iprod_meetE (T : Type) (F : T -> mlat) (f g : iprod F) (x : T) :
(f \cap g) x = (f x \cap g x).
Proof. by []. Qed.
Lemma prod_meetE (T : Type) (X : mlat) (f g : T -> X) (x : T) :
(f \cap g) x = f x \cap g x.
Proof. by []. Qed.
Lemma mfun_meetE (X : proType) (Y : mlat) (f g : {mono X -> Y}) (x : X) :
(f \cap g) x = f x \cap g x.
Proof. by []. Qed.
Definition top_simpl :=
(prop_topE, prod_topE, mfun_topE, iprod_topE, pair_topE, rev_topE).
Definition meet_simpl :=
(prop_meetE, prod_meetE, mfun_meetE, iprod_meetE, pair_meetE, rev_meetE).