Library structures.Lattice

Require Export structures.Poset.

Completely distributive lattices

Definition


Record cdlattice :=
  {
    cdl_poset :> poset;

    lsup : {I}, (I cdl_poset) cdl_poset;
    linf : {I}, (I cdl_poset) cdl_poset;

    sup_ub {I} (i : I) (x : I cdl_poset) :
      ref (x i) (lsup x);
    sup_lub {I} (x : I cdl_poset) (y : cdl_poset) :
      ( i, ref (x i) y)
      ref (lsup x) y;

    inf_lb {I} (i : I) (x : I cdl_poset) :
      ref (linf x) (x i);
    inf_glb {I} (x : cdl_poset) (y : I cdl_poset) :
      ( i, ref x (y i))
      ref x (linf y);

    sup_inf {I J} (x : i:I, J i cdl_poset) :
      lsup (fun ilinf (fun jx i j)) =
      linf (fun f : ( i, J i) ⇒ lsup (fun ix i (f i)));
  }.

Arguments lsup {_ _}.
Arguments linf {_ _}.
Arguments sup_ub {_ _}.
Arguments sup_lub {_ _}.
Arguments inf_lb {_ _}.
Arguments inf_glb {_ _}.

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 jM)) .. ))
  (at level 65, i binder, j binder, right associativity).

Notation "'inf' i .. j , M" := (linf (fun i ⇒ .. (linf (fun jM)) .. ))
  (at level 65, i binder, j binder, right associativity).

Properties of sup and inf


Section PROPERTIES.
  Context {L : cdlattice}.

  Lemma sup_at {I} (i : I) (x : L) (y : I L) :
    x [= y i x [= sup i, y i.

  Lemma inf_at {I} (i : I) (x : I L) (y : L) :
    x i [= y inf i, x i [= y.

  Lemma sup_iff {I} (x : I L) (y : L) :
    lsup x [= y i, x i [= y.

  Lemma inf_iff {I} (x : L) (y : I L) :
    x [= linf y i, x [= y i.

  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

It is often convenient to take the sup or inf by ranging over the elements of an index type which satisfy a given predicate.

Definition fsup {L : cdlattice} {I} (P : I Prop) (f : I L) :=
  lsup (I := sig P) (fun xf (proj1_sig x)).

Notation "'sup' { x | P } , M" :=
  (fsup (fun xP) (fun xM))
  (at level 65, x ident, right associativity).
Notation "'sup' { x : A | P } , M" :=
  (fsup (fun x : AP) (fun x : AM))
  (at level 65, A at next level, x ident, right associativity).

Definition finf {L : cdlattice} {I} (P : I Prop) (f : I L) :=
  linf (I := sig P) (fun xf (proj1_sig x)).

Notation "'inf' { x | P } , M" :=
  (finf (fun xP) (fun xM))
  (at level 65, x ident, right associativity).
Notation "'inf' { x : A | P } , M" :=
  (finf (fun x : AP) (fun x : AM))
  (at level 65, x ident, right associativity).

Section PREDICATES.
  Context {L : 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.

Derived operations


Section OPS.
  Context {L : cdlattice}.

Least element

  Definition bot : L :=
    sup i : Empty_set, match i with end.

  Lemma bot_lb x :
    ref bot x.

Binary joins


  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.

Greatest element


  Definition top : L :=
    inf i : Empty_set, match i with end.

  Lemma top_ub x :
    ref x top.

Binary meets


  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.

Properties


  Lemma join_bot_l x :
    join bot 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.

  Global Opaque bot top join meet.

End OPS.

Infix "||" := join (at level 50, left associativity).
Infix "&&" := meet (at level 40, left associativity).