semantics.ord.clat

Complete Lattices

A complete lattice is an ordType T together with an operation inf which computes greatest lower bounds of arbitrary families.
inf : forall I, (I -> T) -> T infP : is_glb F (inf F)
Every complete lattice also has a least element, binary meets as well as arbitrary suprema, a greatest elements and binary joins.
Categorically, we consider complete sup-semilattices, i.e., we demand that morphisms preserve arbitrary suprema. This is mostly because sup-semilattices specialize to frames.
Require Import base protype ordtype.

Module CLat.
  Record mixin_of (T : ordType) := Mixin {
    inf : forall I, (I -> T) -> T;
    _ : forall I (F : I -> T), is_glb F (inf F)
  }.

  Section ClassDef.
    Record class_of (T : Type) := Class {
      base : Ord.class_of T;
      mixin : mixin_of (Ord.Pack base T)
    }.
    Local Coercion base : class_of >-> Ord.class_of.

    Structure type := Pack {sort; _ : class_of sort; _ : Type }.
    Local Coercion sort : type >-> Sortclass.

    Variable (T : Type) (cT : type).
    Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
    Definition clone c of phant_id class c := @Pack T c T.
    Let xT := let: Pack T _ _ := cT in T.
    Notation xclass := (class : class_of xT).

    Definition pack b0 (m0 : mixin_of (@Ord.Pack T b0 T)) :=
      [find pt | Ord.sort pt ~ T | "is not an ordType"]
      [find pe | Ord.class pt ~ pe]
      [find m | m ~ m0 | "is not the right mixin"]
      @Pack T (@Class T pe m) T.

    Definition proType := @Pro.Pack cT xclass xT.
    Definition ordType := @Ord.Pack cT xclass xT.
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> Ord.class_of.
    Coercion mixin : class_of >-> mixin_of.
    Coercion sort : type >-> Sortclass.

    Coercion proType : type >-> Pro.type.
    Canonical proType.

    Coercion ordType : type >-> Ord.type.
    Canonical ordType.

    Notation clat := type.
    Notation CLatMixin := Mixin.
    Notation CLat T m := (@pack T _ m _ id _ id _ id).

    Notation "[ 'clatMixin' 'of' T ]" := (class _ : mixin_of T)
      (at level 0, format "[ 'clatMixin' 'of' T ]") : form_scope.
    Notation "[ 'clat' 'of' T 'for' C ]" := (@clone T C _ idfun)
      (at level 0, format "[ 'clat' 'of' T 'for' C ]") : form_scope.
    Notation "[ 'clat' 'of' T ]" := (@clone T _ _ id)
      (at level 0, format "[ 'clat' 'of' T ]") : form_scope.
  End Exports.
End CLat.
Export CLat.Exports.

Operations


Definition inf {T : clat} {I : Type} (F : I -> T) : T :=
  CLat.inf (CLat.class T) F.

Definition sup {T : clat} {I : Type} (F : I -> T) : T :=
  inf (fun (p : { x : T | is_ub F x}) => sval p).

Definition bot {T : clat} : T := inf id.

Definition top {T : clat} : T := inf (fun b : False => match b with end).

Definition meet {T : clat} (x y : T) : T := inf (pairb x y).

Definition join {T : clat} (x y : T) : T := inf (fun (p : { z : T | (x z) /\ (y z) }) => sval p).

Definition supguard {T : clat} (P : Prop) (x : T) : T :=
  sup (fun (_ : P) => x).

Definition infguard {T : clat} (P : Prop) (x : T) : T :=
  inf (fun (_ : P) => x).

Notation "∀ x .. y , s" := (inf (fun x => .. (inf (fun y => s%ORD)) .. ))
  (at level 98, x binder, y binder, right associativity,
   format "'[' ∀ x .. y , '/ ' s ']'") : ord_scope.
Notation "∀ x .. y | p , s" := (inf (fun x => .. (inf (fun y => infguard p s%ORD)) .. ))
  (at level 98, x binder, y binder, right associativity,
   format "'[' ∀ x .. y | p , '/ ' s ']'") : ord_scope.

Notation "∃ x .. y , s" := (sup (fun x => .. (sup (fun y => s%ORD)) .. ))
  (at level 98, x binder, y binder, right associativity,
   format "'[' ∃ x .. y , '/ ' s ']'") : ord_scope.
Notation "∃ x .. y | p , s" := (sup (fun x => .. (sup (fun y => supguard p s%ORD)) .. ))
  (at level 98, x binder, y binder, right associativity,
   format "'[' ∃ x .. y | p , '/ ' s ']'") : ord_scope.

Notation "⊤" := top : ord_scope.
Notation "⊥" := bot : ord_scope.
Infix "∧" := meet (at level 80, right associativity) : ord_scope.
Infix "∨" := join (at level 85, right associativity) : ord_scope.

Inf-closed predicates

Definition inf_closed {A : clat} (P : A -> Prop) :=
  forall I (F : I -> A), (forall i, P (F i)) -> P (inf F).

Sup-closed predicates

Definition sup_closed {A : clat} (P : A -> Prop) :=
  forall I (F : I -> A), (forall i, P (F i)) -> P (sup F).

Section Rules.
  Variable (T : clat).
  Implicit Types (x y z : T).

  Lemma all_axiom I (F : I -> T) : is_glb F (inf F).
  Proof. by case: T F => [?[?[]]]. Qed.

  Lemma allI I (F : I -> T) x : (forall i, x F i) -> x inf F.
  Proof. exact/glbP/all_axiom. Qed.

  Lemma allE I (F : I -> T) x i : F i x -> inf F x.
  Proof. move<-. exact/lbP/all_axiom. Qed.

  Lemma allIc I (P : I -> Prop) (F : I -> T) x :
    (forall i, P i -> x F i) -> x i | P i, F i.
  Proof. move=> h. apply: allI => i. apply: allI. exact: h. Qed.

  Lemma allEc I (P : I -> Prop) (F : I -> T) x i :
    P i -> F i x -> i | P i, F i x.
  Proof. move=> pi h. apply: allE (i) _. exact: allE pi h. Qed.

  Lemma ex_axiom I (F : I -> T) : is_lub F (sup F).
  Proof.
    apply: mk_lub.
    - move=> x. apply: allI => -[y /=]. exact.
    - move=> y ub. exact: allE (exist _ y ub) le_refl.
  Qed.

  Lemma exE I (F : I -> T) x : (forall i, F i x) -> sup F x.
  Proof. exact/lubP/ex_axiom. Qed.

  Lemma exI I (F : I -> T) x i : x F i -> x sup F.
  Proof. move->. exact/ubP/ex_axiom. Qed.

  Lemma exEc I (P : I -> Prop) (F : I -> T) x :
    (forall i, P i -> F i x) -> i | P i, F i x.
  Proof. move=> h. apply: exE => i. apply: exE. exact: h. Qed.

  Lemma exIc I (P : I -> Prop) (F : I -> T) x i :
    P i -> x F i -> x i | P i, F i.
  Proof. move=> pi h. apply: exI (i) _. exact: exI pi h. Qed.

  Lemma botE x : x.
  Proof. exact: allE le_refl. Qed.

  Lemma topI x : x .
  Proof. exact: allI. Qed.

  Lemma meet_axiom x y : is_glb (pairb x y) (x y).
  Proof. exact: all_axiom. Qed.

  Lemma meetI x y z : x y -> x z -> x y z.
  Proof. move=> le_x_y le_x_z. by apply: allI => -[]/=. Qed.

  Lemma meetEl x y z : x z -> x y z.
  Proof. move=> le_x_z. exact: allE true _. Qed.

  Lemma meetEr x y z : y z -> x y z.
  Proof. move=> le_y_z. exact: allE false _. Qed.

  Lemma join_axiom x y : is_lub (pairb x y) (x y).
  Proof.
    move=> z. split.
    - move=> le_xy_z -[] /=; rewrite -le_xy_z; by apply: allI => -[w [/=]].
    - move=> h. apply: allE (exist _ z _) _ => //=. split.
      exact: (h true). exact: (h false).
  Qed.

  Lemma joinE x y z : x z -> y z -> x y z.
  Proof. move=> le_x_z le_y_z. by apply/join_axiom => -[]/=. Qed.

  Lemma joinIl x y z : x y -> x y z.
  Proof. move->. by apply: allI => -[?[]] /=. Qed.

  Lemma joinIr x y z : x z -> x y z.
  Proof. move->. by apply: allI => -[?[]] /=. Qed.
End Rules.

Hint Resolve botE topI.

Ltac focus1p :=
  match goal with
  | [|- ?x ?x] => exact: le_refl
  | [|- _ ] => exact: topI
  | [|- _] => exact: botE
  | [|- sup _ _] => apply: exE; intro
  | [|- supguard _ _ _] => apply: exE; intro
  | [|- _ inf _] => apply: allI; intro
  | [|- _ infguard _ _] => apply: allI; intro
  | [|- _ _ _] => apply: meetI
  | [|- _ _ _] => apply: joinE
  end.
Ltac focus := nointr (repeat focus1p).

Ltac focusn := done ||
  match goal with
  | [|- _ _ _] => (apply: meetEl; focusn) || (apply: meetEr; focusn)
  | [|- _ _ _] => (apply: joinIl; focusn) || (apply: joinIr; focusn)
  | [|- inf _ _] => apply: allE; focusn
  | [|- infguard _ _ _] => apply: allE; focusn
  | [|- _ sup _] => apply: exI; focusn
  | [|- _ supguard _ _] => apply: exI; focusn
  end.
Ltac cauto := try apply: le_eq; repeat focus1p; focusn.

Section JLatLaws.
  Variable (T : clat).
  Implicit Types (x y z : T).

  Lemma joinxx : idempotent (@join T).
  Proof. move=> x. cauto. Qed.

  Lemma joinC : commutative (@join T).
  Proof. move=> x y. cauto. Qed.

  Lemma joinA : associative (@join T).
  Proof. move=> x y z. cauto. Qed.

  Lemma joinAC : right_commutative (@join T).
  Proof. move=> x y z. cauto. Qed.

  Lemma joinCA : left_commutative (@join T).
  Proof. move=> x y z. cauto. Qed.

  Lemma joinACA : interchange (@join T) (@join T).
  Proof. move=> w x y z. cauto. Qed.

  Lemma joinBx x : ( x) = x.
  Proof. cauto. Qed.

  Lemma joinxB x : (x ) = x.
  Proof. cauto. Qed.

  Lemma bot_eq x : x -> x = .
  Proof. move=> h. cauto. Qed.

  Lemma le_joinP x y : (x y) <-> ((x y) = y).
  Proof. split=> [h|<-]; cauto. Qed.

  Lemma join_mono x1 x2 y1 y2 : x1 x2 -> y1 y2 -> x1 y1 x2 y2.
  Proof. move=> h1 h2. cauto. Qed.

  Global Instance join_proper : Proper (ord_op ++> ord_op ++> ord_op) (@join T).
  Proof. move=> x1 x2 le1 y1 y2 le2. cauto. Qed.

  Canonical join_monoid := Monoid.Law joinA joinBx joinxB.
  Canonical join_comoid := Monoid.ComLaw joinC.
End JLatLaws.

Section MLatLaws.
  Variable (T : clat).
  Implicit Types (x y z : T).

  Lemma meetxx : idempotent (@meet T).
  Proof. move=> x. cauto. Qed.

  Lemma meetC : commutative (@meet T).
  Proof. move=> x y. cauto. Qed.

  Lemma meetA : associative (@meet T).
  Proof. move=> x y z. cauto. Qed.

  Lemma meetAC : right_commutative (@meet T).
  Proof. move=> x y z. cauto. Qed.

  Lemma meetCA : left_commutative (@meet T).
  Proof. move=> x y z. cauto. Qed.

  Lemma meetACA : interchange (@meet T) (@meet T).
  Proof. move=> w x y z. cauto. Qed.

  Lemma meetTx x : ( x) = x.
  Proof. cauto. Qed.

  Lemma meetxT x : (x ) = x.
  Proof. cauto. Qed.

  Lemma top_eq x : x -> x = .
  Proof. move=> h. cauto. Qed.

  Lemma le_meetP x y : (x y) <-> (x = (x y)).
  Proof. split=> [h|->]; cauto. Qed.

  Lemma meet_mono x1 x2 y1 y2 : x1 x2 -> y1 y2 -> x1 y1 x2 y2.
  Proof. move=> h1 h2. cauto. Qed.

  Global Instance meet_proper : Proper (ord_op ++> ord_op ++> ord_op) (@meet T).
  Proof. move=> x1 x2 le1 y1 y2 le2. cauto. Qed.

  Canonical meet_monoid := Monoid.Law meetA meetTx meetxT.
  Canonical meet_comoid := Monoid.ComLaw meetC.
End MLatLaws.

Section LatLaws.
  Variable (T : clat).
  Implicit Types (x y z : T).

  Lemma meetxK x y : (x (y x)) = x.
  Proof. cauto. Qed.

  Lemma meetKx x y : (x (x y)) = x.
  Proof. cauto. Qed.

  Lemma joinxK x y : (x (y x)) = x.
  Proof. cauto. Qed.

  Lemma joinKx x y : (x (x y)) = x.
  Proof. cauto. Qed.

  Lemma joinTx x : ( x) = .
  Proof. cauto. Qed.

  Lemma joinxT x : (x ) = .
  Proof. cauto. Qed.

  Lemma meetBx x : ( x) = .
  Proof. cauto. Qed.

  Lemma meetxB x : (x ) = .
  Proof. cauto. Qed.
End LatLaws.

Section CLatLaws.
  Variable (T : clat).

  Lemma all_mono I (F G : I -> T) :
    (forall i, F i G i) -> i, F i i, G i.
  Proof. move=> h. cauto. Qed.

  Lemma ex_mono I (F G : I -> T) :
    (forall i, F i G i) -> i, F i i, G i.
  Proof. move=> h. cauto. Qed.
End CLatLaws.

Section CLatDef.
  Variable (T : clat).
  Implicit Types (x y z : T).

  Lemma top_def x : x -> = x.
  Proof. move=> h. cauto. Qed.

  Lemma bot_def x : x -> = x.
  Proof. move=> h. cauto. Qed.

  Lemma join_def x y z :
    x z ->
    y z ->
    (forall w, x w -> y w -> z w) ->
    (x y) = z.
  Proof.
    move=> h1 h2 h3. apply: le_eq. cauto. apply: h3; cauto.
  Qed.

  Lemma meet_def x y z :
    z x ->
    z y ->
    (forall w, w x -> w y -> w z) ->
    (x y) = z.
  Proof.
    move=> h1 h2 h3. apply: le_eq. apply: h3; cauto. cauto.
  Qed.

  Lemma ex_def I (F : I -> T) x :
    (forall i, F i x) ->
    (forall y, (forall i, F i y) -> x y) ->
    sup F = x.
  Proof.
    move=> h1 h2. apply: le_eq. cauto. apply: h2 => i. cauto.
  Qed.

  Lemma all_def I (F : I -> T) x :
    (forall i, x F i) ->
    (forall y, (forall i, y F i) -> y x) ->
    inf F = x.
  Proof.
    move=> h1 h2. apply: le_eq. apply: h2 => i. cauto. cauto.
  Qed.
End CLatDef.

Section ReverseCLat.
  Variable X : clat.

  Definition rev_inf I (F : I -> X^r) : X^r := sup F.

  Lemma rev_infP I (F : I -> X^r) : is_glb F (rev_inf F).
  Proof.
    apply: mk_glb.
    - move=> i. rewrite rev_leE /rev_inf. by cauto.
    - move=> /=x xP. rewrite rev_leE /rev_inf. focus=> i. exact: xP.
  Qed.

  Canonical reverse_clatMixin := CLatMixin rev_infP.
  Canonical reverse_clat := Eval hnf in CLat X^r reverse_clatMixin.
End ReverseCLat.

Lemma rev_allE (X : clat) I (F : I -> X) :
  @inf (reverse_clat X) I F = @sup X I F.
Proof. by []. Qed.

Lemma rev_allEc (X : clat) I (F : I -> X^r) (P : I -> Prop) :
  ( i | P i, F i) = i | P i, (F i : X).
Proof. by []. Qed.

Lemma rev_exE (X : clat) I (F : I -> X) :
  @sup (reverse_clat X) I F = @inf X I F.
Proof.
  apply: ex_def. move=> i. rewrite rev_leE. cauto. move=> /= x xP. rewrite rev_leE. focus=> i. exact: xP.
Qed.

Lemma rev_exEc (X : clat) I (F : I -> X^r) (P : I -> Prop) :
  ( i | P i, F i) = i | P i, (F i : X).
Proof.
  rewrite rev_exE. f_equal. fext=> i. exact: rev_exE.
Qed.