Library Lattice

Constructions of semi-lattices.

Require Import Coqlib.
Require Import Maps.
Require Import FSets.

Signatures of semi-lattices
A semi-lattice is a type t equipped with an equivalence relation eq, a boolean equivalence test beq, a partial order ge, a smallest element bot, and an upper bound operation lub. Note that we do not demand that lub computes the least upper bound.

Module Type SEMILATTICE.

  Variable t: Type.
  Variable eq: t -> t -> Prop.
  Hypothesis eq_refl: forall x, eq x x.
  Hypothesis eq_sym: forall x y, eq x y -> eq y x.
  Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
  Variable beq: t -> t -> bool.
  Hypothesis beq_correct: forall x y, beq x y = true -> eq x y.
  Variable ge: t -> t -> Prop.
  Hypothesis ge_refl: forall x y, eq x y -> ge x y.
  Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
  Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
  Variable bot: t.
  Hypothesis ge_bot: forall x, ge x bot.
  Variable lub: t -> t -> t.
  Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x).
  Hypothesis ge_lub_left: forall x y, ge (lub x y) x.

End SEMILATTICE.
A semi-lattice ``with top'' is similar, but also has a greatest element top.

Module Type SEMILATTICE_WITH_TOP.

  Include Type SEMILATTICE.
  Variable top: t.
  Hypothesis ge_top: forall x, ge top x.

End SEMILATTICE_WITH_TOP.

Semi-lattice over maps
Given a semi-lattice with top L, the following functor implements a semi-lattice structure over finite maps from positive numbers to L.t. The default value for these maps is either L.top or L.bot.

Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP.

Inductive t_ : Type :=
  | Bot_except: PTree.t L.t -> t_
  | Top_except: PTree.t L.t -> t_.

Definition t: Type := t_.

Definition get (p: positive) (x: t) : L.t :=
  match x with
  | Bot_except m =>
      match m!p with None => L.bot | Some x => x end
  | Top_except m =>
      match m!p with None => L.top | Some x => x end
  end.

Definition set (p: positive) (v: L.t) (x: t) : t :=
  match x with
  | Bot_except m =>
      Bot_except (if L.beq v L.bot then PTree.remove p m else PTree.set p v m)
  | Top_except m =>
      Top_except (if L.beq v L.top then PTree.remove p m else PTree.set p v m)
  end.

Lemma gss:
  forall p v x,
  L.eq (get p (set p v x)) v.


Lemma gso:
  forall p q v x,
  p <> q -> get p (set q v x) = get p x.


Definition eq (x y: t) : Prop :=
  forall p, L.eq (get p x) (get p y).

Lemma eq_refl: forall x, eq x x.


Lemma eq_sym: forall x y, eq x y -> eq y x.


Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.


Definition beq (x y: t) : bool :=
  match x, y with
  | Bot_except m, Bot_except n => PTree.beq L.beq m n
  | Top_except m, Top_except n => PTree.beq L.beq m n
  | _, _ => false
  end.

Lemma beq_correct: forall x y, beq x y = true -> eq x y.


Definition ge (x y: t) : Prop :=
  forall p, L.ge (get p x) (get p y).

Lemma ge_refl: forall x y, eq x y -> ge x y.


Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.


Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.


Definition bot := Bot_except (PTree.empty L.t).

Lemma get_bot: forall p, get p bot = L.bot.


Lemma ge_bot: forall x, ge x bot.


Definition top := Top_except (PTree.empty L.t).

Lemma get_top: forall p, get p top = L.top.


Lemma ge_top: forall x, ge top x.


Definition opt_lub (x y: L.t) : option L.t :=
  let z := L.lub x y in
  if L.beq z L.top then None else Some z.

Definition lub (x y: t) : t :=
  match x, y with
  | Bot_except m, Bot_except n =>
      Bot_except
        (PTree.combine
           (fun a b =>
              match a, b with
              | Some u, Some v => Some (L.lub u v)
              | None, _ => b
              | _, None => a
              end)
           m n)
  | Bot_except m, Top_except n =>
      Top_except
        (PTree.combine
           (fun a b =>
              match a, b with
              | Some u, Some v => opt_lub u v
              | None, _ => b
              | _, None => None
              end)
        m n)
  | Top_except m, Bot_except n =>
      Top_except
        (PTree.combine
           (fun a b =>
              match a, b with
              | Some u, Some v => opt_lub u v
              | None, _ => None
              | _, None => a
              end)
        m n)
  | Top_except m, Top_except n =>
      Top_except
        (PTree.combine
           (fun a b =>
              match a, b with
              | Some u, Some v => opt_lub u v
              | _, _ => None
              end)
           m n)
  end.

Lemma lub_commut:
  forall x y, eq (lub x y) (lub y x).


Lemma ge_lub_left:
  forall x y, ge (lub x y) x.


End LPMap.

Semi-lattice over a set.
Given a set S: FSetInterface.S, the following functor implements a semi-lattice over these sets, ordered by inclusion.

Module LFSet (S: FSetInterface.S) <: SEMILATTICE.

  Definition t := S.t.

  Definition eq (x y: t) := S.Equal x y.
  Definition eq_refl: forall x, eq x x := S.eq_refl.
  Definition eq_sym: forall x y, eq x y -> eq y x := S.eq_sym.
  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := S.eq_trans.
  Definition beq: t -> t -> bool := S.equal.
  Definition beq_correct: forall x y, beq x y = true -> eq x y := S.equal_2.

  Definition ge (x y: t) := S.Subset y x.
  Lemma ge_refl: forall x y, eq x y -> ge x y.
  
  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
  
  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
  

  Definition bot: t := S.empty.
  Lemma ge_bot: forall x, ge x bot.
  

  Definition lub: t -> t -> t := S.union.
  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
  

  Lemma ge_lub_left: forall x y, ge (lub x y) x.
  

End LFSet.

Flat semi-lattice
Given a type with decidable equality X, the following functor returns a semi-lattice structure over X.t complemented with a top and a bottom element. The ordering is the flat ordering Bot < Inj x < Top.

Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP.

Inductive t_ : Type :=
  | Bot: t_
  | Inj: X.t -> t_
  | Top: t_.

Definition t : Type := t_.

Definition eq (x y: t) := (x = y).
Definition eq_refl: forall x, eq x x := (@refl_equal t).
Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).

Definition beq (x y: t) : bool :=
  match x, y with
  | Bot, Bot => true
  | Inj u, Inj v => if X.eq u v then true else false
  | Top, Top => true
  | _, _ => false
  end.

Lemma beq_correct: forall x y, beq x y = true -> eq x y.


Definition ge (x y: t) : Prop :=
  match x, y with
  | Top, _ => True
  | _, Bot => True
  | Inj a, Inj b => a = b
  | _, _ => False
  end.

Lemma ge_refl: forall x y, eq x y -> ge x y.


Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.


Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.


Definition bot: t := Bot.

Lemma ge_bot: forall x, ge x bot.


Definition top: t := Top.

Lemma ge_top: forall x, ge top x.


Definition lub (x y: t) : t :=
  match x, y with
  | Bot, _ => y
  | _, Bot => x
  | Top, _ => Top
  | _, Top => Top
  | Inj a, Inj b => if X.eq a b then Inj a else Top
  end.

Lemma lub_commut: forall x y, eq (lub x y) (lub y x).


Lemma ge_lub_left: forall x y, ge (lub x y) x.


End LFlat.

Boolean semi-lattice
This semi-lattice has only two elements, bot and top, trivially ordered.

Module LBoolean <: SEMILATTICE_WITH_TOP.

Definition t := bool.

Definition eq (x y: t) := (x = y).
Definition eq_refl: forall x, eq x x := (@refl_equal t).
Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).

Definition beq : t -> t -> bool := eqb.

Lemma beq_correct: forall x y, beq x y = true -> eq x y.
Proof eqb_prop.

Definition ge (x y: t) : Prop := x = y \/ x = true.

Lemma ge_refl: forall x y, eq x y -> ge x y.


Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.


Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.


Definition bot := false.

Lemma ge_bot: forall x, ge x bot.


Definition top := true.

Lemma ge_top: forall x, ge top x.


Definition lub (x y: t) := x || y.

Lemma lub_commut: forall x y, eq (lub x y) (lub y x).


Lemma ge_lub_left: forall x y, ge (lub x y) x.


End LBoolean.