Module LatticeSignatures

Lattice signatures.

Require Import Utf8.

Definition incl {A} (P1 P2:A->Prop) :=
  forall a, P1 a -> P2 a.
Notation "P1P2" := (incl P1 P2) (at level 20).

Module WLattice.

  Record t {A:Type} {B:Type} : Type := make {
    leb: A -> A -> bool;
    top: A;
    join: A -> A -> A;
    widen: A -> A -> A;

    gamma: A -> B -> Prop;
    gamma_monotone: forall {a1} {a2},
      leb a1 a2 = true -> gamma a1gamma a2;
    gamma_top: forall x, gamma top x
  }.

  Implicit Arguments t [].
  Hint Resolve @gamma_monotone @gamma_top.

End WLattice.