Library structures.Lattices
Class CDLattice (L : Type) :=
{
cdl_poset :> Poset L;
lsup : ∀ {I}, (I → L) → L;
linf : ∀ {I}, (I → L) → L;
lsup_sup {I} (u : I → L) :> IsSup u (lsup u);
linf_inf {I} (u : I → L) :> IsInf u (linf u);
sup_inf {I J} (x : ∀ i:I, J i → L) :
lsup (fun i ⇒ linf (fun j ⇒ x i j)) =
linf (fun f : (∀ i, J i) ⇒ lsup (fun i ⇒ x i (f i)));
}.
(*
Delimit Scope cdlat_scope with cdlat.
Bind Scope cdlat_scope with cdlattice.
*)
The notations below work well in the context of completely
distributive monads.
Notation "'sup' i .. j , M" := (lsup (fun i ⇒ .. (lsup (fun j ⇒ M)) .. ))
(at level 65, i binder, j binder, right associativity).
Notation "'inf' i .. j , M" := (linf (fun i ⇒ .. (linf (fun j ⇒ M)) .. ))
(at level 65, i binder, j binder, right associativity).
Section PROPERTIES.
Context {L} `{HL : !CDLattice L}.
Lemma inf_sup {I J} (x : ∀ i:I, J i → L) :
inf i, sup j, x i j = sup f, inf i, x i (f i).
End PROPERTIES.
Joins and meets with predicates
Definition fsup `{CDLattice} {I} (P : I → Prop) (f : I → L) :=
lsup (I := sig P) (fun x ⇒ f (proj1_sig x)).
Notation "'sup' { x | P } , M" :=
(fsup (fun x ⇒ P) (fun x ⇒ M))
(at level 65, x name, right associativity).
Notation "'sup' { x : A | P } , M" :=
(fsup (fun x : A ⇒ P) (fun x : A ⇒ M))
(at level 65, A at next level, x name, right associativity).
Definition finf `{CDLattice} {I} (P : I → Prop) (f : I → L) :=
linf (I := sig P) (fun x ⇒ f (proj1_sig x)).
Notation "'inf' { x | P } , M" :=
(finf (fun x ⇒ P) (fun x ⇒ M))
(at level 65, x name, right associativity).
Notation "'inf' { x : A | P } , M" :=
(finf (fun x : A ⇒ P) (fun x : A ⇒ M))
(at level 65, x name, right associativity).
Section PREDICATES.
Context `{Lcdl : CDLattice}.
Lemma fsup_ub {I} (i : I) (P : I → Prop) (x : I → L) :
P i → x i ≤ fsup P x.
Lemma fsup_at {I} (i : I) (P : I → Prop) (x : L) (y : I → L) :
P i → x ≤ y i → x ≤ fsup P y.
Lemma fsup_lub {I} (P : I → Prop) (x : I → L) (y : L) :
(∀ i, P i → x i ≤ y) → fsup P x ≤ y.
Lemma finf_lb {I} (i : I) (P : I → Prop) (x : I → L) :
P i → finf P x ≤ x i.
Lemma finf_at {I} (i : I) (P : I → Prop) (x : I → L) (y : L) :
P i → x i ≤ y → finf P x ≤ y.
Lemma finf_glb {I} (P : I → Prop) (x : L) (y : I → L) :
(∀ i, P i → x ≤ y i) → x ≤ finf P y.
End PREDICATES.
Least element
Definition join (x y : L) :=
sup b : bool, if b then x else y.
Lemma join_ub_l x y :
ref x (join x y).
Lemma join_ub_r x y :
ref y (join x y).
Lemma join_lub x y z :
ref x z → ref y z → ref (join x y) z.
Lemma join_l x y z :
ref x y →
ref x (join y z).
Lemma join_r x y z :
ref x z →
ref x (join y z).
Lemma ref_join x y :
x ≤ y ↔ join x y = y.
Definition meet (x y : L) :=
inf b : bool, if b then x else y.
Lemma meet_lb_l x y :
ref (meet x y) x.
Lemma meet_lb_r x y :
ref (meet x y) y.
Lemma meet_glb x y z :
ref x y → ref x z → ref x (meet y z).
Lemma meet_l x y z :
ref x z →
ref (meet x y) z.
Lemma meet_r x y z :
ref y z →
ref (meet x y) z.
Lemma ref_meet x y :
x ≤ y ↔ meet x y = x.
Lemma join_undef_l x :
join undef x = x.
Lemma join_top_l x :
join top x = top.
Lemma join_meet_l x y z :
join (meet x y) z = meet (join x z) (join y z).
(* ... foo_bar_l, foo_bar_r ... *)
Lemma join_comm x y :
join x y = join y x.
Lemma meet_comm x y :
meet x y = meet y x.
Lemma join_idemp x :
join x x = x.
Lemma meet_idemp x :
meet x x = x.
These properties are more than enough to completely define the
derived operations, so that relying on their concrete definition
should not be necessary.