Library lattices.Downset

Require Import Classical.
Require Import ClassicalChoice.
Require Import FunctionalExtensionality.
Require Import PropExtensionality.
Require Import coqrel.LogicalRelations.
Require Import structures.Lattice.
Require Import structures.Completion.

Interface

The downset lattice over a poset is a free distributive completion with respect to join-distributive morphisms. We use it as an intermediate step in the construction of the free completely distributive lattice (see Morris, 2005), and it could be used to construct traditional strategy models defined as prefix-closed sets of plays (which only feature angelic nondeterminism).

Module Sup <: LatticeCategory.

  Class Morphism {L M : cdlattice} (f : L → M) :=
    mor : ∀ {I} (x : I → L), f (lsup x) = sup i , f (x i).

  Lemma mor_join `{Morphism} x y :
    f (x || y) = f x || f y.
    Local Transparent join.
  Lemma mor_ref {L M : cdlattice} (f : L → M) :
    Morphism f →
    PosetMorphism f.

  Lemma id_mor (L : cdlattice) :
    Morphism (fun x:L ⇒ x).

  Lemma compose_mor {A B C : cdlattice} (g : B → C) (f : A → B) :
    Morphism f →
    Morphism g →
    Morphism (fun a ⇒ g (f a)).

  Hint Immediate mor_ref : typeclass_instances.

  Lemma mor_bot `{Morphism} :
    f bot = bot.
    Local Transparent bot.
End Sup.

Construction

Our construction is straightforward. We use predicate extensionality to prove antisymmetry, and the axiom of choice to prove distributivity.

Module Downset <: LatticeCompletion Sup.

  Record downset {C : poset} :=
    {
      has : C → Prop;
      closed x y : x [= y → has y → has x;
    }.

  Arguments downset : clear implicits.
  (*
  Definition F := downset.
   *)

  Section DOWNSETS.
    Context {C : poset}.

Partial order

    Program Definition Fpos : poset :=
      {|
        poset_carrier := downset C;
        ref x y := ∀ c, has x c → has y c;
      |}.

Distributive lattice

    Program Definition F : cdlattice :=
      {|
        cdl_poset := Fpos;
        lsup I x := {| has c := ∃ i , has (x i) c |};
        linf I x := {| has c := ∀ i, has (x i) c |};
      |}.

sup is downward closed.

inf is downward closed.

Distributivity.

Embedding

    Program Definition emb (c : C) : F :=
      {|
        has x := x [= c;
      |}.

    Lemma emb_mor (c1 c2 : C) :
      emb c1 [= emb c2 ↔ c1 [= c2.

    Lemma emb_join_dense :
      ∀ x, x = sup {c : C | emb c [= x }, emb c.

    Lemma emb_join_prime {I} c (x : I → F) :
      emb c [= lsup x ↔ ∃ i , emb c [= x i.

Simulator

    Context {L: cdlattice}.

    Definition ext (f : C → L) (x : F) : L :=
      sup {c : C | emb c [= x }, f c.

    Context {f : C → L} `{Hf : !PosetMorphism f}.

    Instance ext_mor :
      Sup.Morphism (ext f).

    Lemma ext_ana :
      (∀ x, ext f (emb x) = f x).

    Lemma ext_unique (g : F → L) `{Hg : !Sup.Morphism g} :
      (∀ x, g (emb x) = f x ) → ∀ x, g x = ext f x.

These are not required to implement the interface but can be useful when using the concrete implementation directly.

    Lemma has_eq_ext (x y : F) :
      (∀ c, has x c ↔ has y c ) → x = y.
  End DOWNSETS.

  Arguments F : clear implicits.
  Include (LatticeCompletionDefs Sup).

End Downset.

Notation downset := Downset.F.
Notation down := Downset.emb.