File Lattice

From MatchingLogic.Utils Require Export stdpp_ext.

Class OrderedSet A : Type :=
  { leq : relation A;
    leq_order : order A leq;
  }.

Program Definition OrderedSet_dual {A : Type} (OS : OrderedSet A) : OrderedSet A :=
  {| leq := fun x y ⇒ @leq A OS y x;
     leq_order := {| ord_refl := _; ord_trans := _; ord_antisym := _; |};
  |}.


Definition upperBound {A : Type} {OS : OrderedSet A} (X: propset A) (ub: A) : Prop :=
  ∀ (x: A), x ∈ X → leq x ub.

Definition leastUpperBound {A : Type} {OS : OrderedSet A} (X: propset A) (lub: A) : Prop :=
  upperBound X lub ∧
  ∀ (ub : A), upperBound X ub → leq lub ub.

Definition lowerBound {A : Type} {OS : OrderedSet A} (X: propset A) (lb: A) : Prop :=
  ∀ (x : A), x ∈ X → leq lb x.

Definition greatestLowerBound {A : Type} {OS : OrderedSet A} (X : propset A) (glb : A) : Prop :=
  lowerBound X glb ∧
  ∀ (lb : A), lowerBound X lb → leq lb glb.

Definition upperBoundsOf {A : Type} {OS : OrderedSet A} (X : propset A) : propset A :=
  PropSet (fun x ⇒ upperBound X x).

Definition lowerBoundsOf {A : Type} {OS : OrderedSet A} (X : propset A) : propset A :=
  PropSet (fun x ⇒ lowerBound X x).

Definition isMeet {A : Type} {OS : OrderedSet A} (meet : propset A → A) : Prop :=
  ∀ (X : propset A), greatestLowerBound X (meet X).

Definition isJoin {A : Type} {OS : OrderedSet A} (join : propset A → A) : Prop :=
  ∀ (X : propset A), leastUpperBound X (join X).

Definition joinFromMeet {A : Type} {OS : OrderedSet A} (meet : propset A → A)
  : propset A → A :=
  fun X ⇒ meet (upperBoundsOf X).

Lemma joinFromMeet_lub: ∀ (A : Type) (OS : OrderedSet A)
                                (meet : propset A → A),
     isMeet meet → isJoin (joinFromMeet meet).

Definition meetFromJoin {A : Type} {OS : OrderedSet A} (join : propset A → A)
   : propset A → A :=
  fun X ⇒ join (lowerBoundsOf X).

(* Exactly a dual of joinFromMeet_lub. But there should be some way to avoid duplication. *)
Lemma meetFromJoin_glb: ∀ (A : Type) (OS : OrderedSet A)
                                (join : propset A → A),
     isJoin join → isMeet (meetFromJoin join).

Class CompleteLattice A `{OrderedSet A} :=
  {
    meet : propset A → A;
    join : propset A → A;
    meet_isMeet : isMeet meet;
    join_isJoin : isJoin join;
  }.

Program Definition CompleteLattice_dual {A : Type} {OS : OrderedSet A} (CL : CompleteLattice A)
  : @CompleteLattice A (@OrderedSet_dual A OS) :=
  {| meet := join;
     join := meet;
     meet_isMeet := _;
     join_isJoin := _
  |}.

Definition MonotonicFunction {A : Type} {OS : OrderedSet A}
           (f : A → A) :=
  ∀ (x y : A), leq x y → leq (f x) (f y).

Definition AntiMonotonicFunction {A : Type} {OS : OrderedSet A}
           (f : A → A) :=
  ∀ (x y : A), leq x y → leq (f y) (f x).

Lemma MonotonicFunction_dual {A : Type} :
  ∀ (OS : OrderedSet A) (f : A → A),
    @MonotonicFunction A OS f → @MonotonicFunction A (OrderedSet_dual OS) f.

Definition PrefixpointsOf {A : Type} {OS : OrderedSet A} (f : A → A) : propset A :=
  PropSet (fun x ⇒ leq (f x) x).

Definition LeastFixpointOf {A : Type} {OS : OrderedSet A} {L : CompleteLattice A}
           (f : A → A) : A :=
  meet (PrefixpointsOf f).

Arguments LeastFixpointOf : simpl never.

Definition PostfixpointsOf {A : Type} {OS : OrderedSet A} (f : A → A) : propset A :=
  PropSet (fun x ⇒ leq x (f x)).

Definition GreatestFixpointOf {A : Type} {OS : OrderedSet A} {L : CompleteLattice A}
           (f : A → A) : A :=
  join (PostfixpointsOf f).

Arguments GreatestFixpointOf : simpl never.

Lemma PrefixpointsOfDualArePostfixpoints {A : Type} :
  ∀ (OS : OrderedSet A) (f : A → A),
    @PrefixpointsOf A (@OrderedSet_dual A OS) = @PostfixpointsOf A OS.

Lemma PostfixpointsOfDualArePrefixpoints {A : Type} :
  ∀ (OS : OrderedSet A) (f : A → A),
    @PostfixpointsOf A (@OrderedSet_dual A OS) = @PrefixpointsOf A OS.

Lemma GreatestFixpointOnDualIsLeastFixpoint {A : Type} :
  ∀ (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A),
    @GreatestFixpointOf A (@OrderedSet_dual A OS) (@CompleteLattice_dual A OS L) f = LeastFixpointOf f.

Proposition GreatestFixpoint_greaterThanPostfixpoint:
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A) (x : A),
    leq x (f x) → leq x (GreatestFixpointOf f).

Proposition GreatestFixpoint_GreaterThanFixpoint :
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A) (x : A),
    x = (f x) → leq x (GreatestFixpointOf f).

Definition isFixpoint {A : Type} (f : A → A) (p : A) : Prop :=
  f p = p.

Theorem GreatestFixpoint_fixpoint:
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A),
    MonotonicFunction f → isFixpoint f (@GreatestFixpointOf A OS L f).

Theorem LeastFixpoint_fixpoint:
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A),
    MonotonicFunction f → isFixpoint f (@LeastFixpointOf A OS L f).

Proposition LeastFixpoint_LesserThanPrefixpoint:
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A) (x : A),
    leq (f x) x → leq (LeastFixpointOf f) x.

Proposition LeastFixpoint_LesserThanFixpoint :
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A) (x : A),
    x = (f x) → leq (LeastFixpointOf f) x.

Proposition LeastFixpoint_unique :
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A) (f : A → A) (Sfix : A),
    leq (f Sfix) Sfix →
    (∀ x, leq (f x) x → leq Sfix x) →
    Sfix = LeastFixpointOf f.

Proposition LeastFixpoint_unique_2 :
  ∀ (A : Type) (OS : OrderedSet A) (L : CompleteLattice A)
    (f : A → A)
    (Sfix : A),
    (MonotonicFunction f) →
    (f Sfix) = Sfix →
    (∀ x, (f x) = x → leq Sfix x) →
    Sfix = LeastFixpointOf f.

Lemma lfp_preserves_order {A : Type} (OS : OrderedSet A) (L : CompleteLattice A) (f g : A → A) :
  MonotonicFunction f → MonotonicFunction g →
  (∀ (x : A), leq (f x) (g x)) →
  leq (LeastFixpointOf f) (LeastFixpointOf g).

From Coq Require Import Logic.FunctionalExtensionality Logic.PropExtensionality.

Section propset_lattice.
  Variable U : Type.

  Program Definition PropsetOrderedSet : OrderedSet (propset U) :=
  {| leq := subseteq;
  |}.


  Definition propset_Meet (ee : propset (propset U)) : propset U :=
    PropSet (fun m ⇒ ∀ e : propset U,
        e ∈ ee → m ∈ e).

  Lemma propset_Meet_is_meet : @isMeet (propset U) PropsetOrderedSet propset_Meet.

  Definition PowersetLattice : CompleteLattice (propset U) :=
    {| meet := propset_Meet;
       join := joinFromMeet propset_Meet;
       meet_isMeet := propset_Meet_is_meet;
       join_isJoin := joinFromMeet_lub (propset U) PropsetOrderedSet propset_Meet propset_Meet_is_meet;
    |}.

End propset_lattice.