semantics.tower.llat

L-lattices and L-monotone functions

Require Import base ord.

Module LLat.
  Record mixin_of (T : clat) := Mixin {
    lt : T T Prop;
    _ : x y z, lt x y (y z) lt x z;
    _ : x y z, (x y) lt y z lt x z;
    _ : I (F : I T) x,
        lt (inf F) x i, lt (F i) x
  }.

  Section ClassDef.
    Record class_of (T : Type) := Class {
      base : CLat.class_of T;
      mixin : mixin_of (CLat.Pack base T)
    }.
    Local Coercion base : class_of >-> CLat.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 ( : mixin_of (@CLat.Pack T T)) :=
      [find pt | CLat.sort pt T | "is not a clat"]
      [find pe | CLat.class pt pe]
      [find m | m | "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.
    Definition clat := @CLat.Pack cT xclass xT.
  End ClassDef.

  Module Exports.
    Coercion base : class_of >-> CLat.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.

    Coercion clat : type >-> CLat.type.
    Canonical clat.

    Notation llat := type.
    Notation LLatMixin := Mixin.
    Notation LLat T m := (@pack T _ m _ id _ id _ id).

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

Definition ord_l_op (T : llat) (x y : T) := LLat.lt (LLat.class T) x y.
Notation "x ⊏ y" := (ord_l_op x%ORD y%ORD)
  (at level 99, y at next level, no associativity) : ord_scope.
Notation "x ⊏ y :> T" := ((x:T) (y:T))
  (at level 99, y at next level, no associativity) : ord_scope.

Section LLatLemmas.
  Variable (T : llat).
  Implicit Types (x y z : T).

  Lemma lt_left x y z : (x y) (y z) x z.
  Proof. by case: T x y z ?[?[]]. Qed.

  Lemma lt_right x y z : (x y) (y z) x z.
  Proof. by case: T x y z ?[?[]]. Qed.

  Lemma lt_inf I (F : I T) x : (inf F x) i, F i x.
  Proof. case: T F x ?[?[*]]; by eauto. Qed.
End LLatLemmas.

Class lmonotone {T : llat} (f : T T) : Prop := {
  lmonotone_to_monotone :> monotone f;
  lmonoP : x y, (f x f y) x y
}.

The L-lattice of complemented propositions

The Chu construction over Prop

Reserved Notation "x ^+" (at level 3, left associativity, format "x ^+").
Reserved Notation "x ^-" (at level 3, left associativity, format "x ^-").

Record lprop := mk_lprop { chuL : Prop; chuR : Prop; _ : chuL chuR False }.
Arguments mk_lprop l r p : rename, clear implicits.

Notation "p ^+" := (chuL p).
Notation "p ^-" := (chuR p).

Section Chu.
  Implicit Types (p q r : lprop).
  Implicit Types (x y z : Prop).

  Lemma chuP p : p^+ p^- False.
  Proof. by case: p. Qed.

  Definition chu_le p q := (chuL p chuL q) (chuR q chuR p).

  Lemma chu_le_refl : reflexive chu_le.
  Proof. by split. Qed.

  Lemma chu_le_trans : transitive chu_le.
  Proof. move p q r [ ] [ ]. split. by rewrite . by rewrite . Qed.

  Canonical chu_proMixin := ProMixin chu_le_refl chu_le_trans.
  Canonical lprop_proType := Eval hnf in ProType lprop chu_proMixin.

  Lemma chu_eq p q : chuL p = chuL q chuR p = chuR q p = q.
  Proof.
    move: p q [ ] [ ] /= . destruct , .
    f_equal. exact: pi.
  Qed.


  Lemma chu_le_eq p q : p q q p p = q.
  Proof.
    move [ ] [ ]. apply: chu_eq; exact: le_eq.
  Qed.


  Canonical chu_ordMixin := OrdMixin chu_le_eq.
  Canonical lprop_ordType := Eval hnf in OrdType lprop chu_ordMixin.

  Program Definition chu_inf T (F : T lprop) := mk_lprop (inf (chuL \o F)) (sup (chuR \o F)) _.
  Next Obligation.
    rewrite prop_exE in . case: y /=. apply: chuP. exact: H.
  Qed.

  Lemma chu_infP T (F : T lprop) : is_glb F (chu_inf F).
  Proof.
    move x /=. split. move [/= ] i. split. rewrite . exact: allE (i) _.
    rewrite -. exact: exI (i) _. move h. split /=. apply: allI i /=.
    by case: (h i). apply: exE i /=. by case: (h i).
  Qed.


  Canonical chu_clatMixin := CLatMixin chu_infP.
  Canonical lprop_clat := Eval hnf in CLat lprop chu_clatMixin.

  Definition chu_lt (A B : lprop) : Prop :=
    chuR A chuL B.

  Lemma chu_lt_left p q r :
    chu_lt p q (q r) chu_lt p r.
  Proof.
    move [na pb] [bc _]. split //. exact: bc.
  Qed.


  Lemma chu_lt_right p q r :
    (p q) chu_lt q r chu_lt p r.
  Proof.
    move [_ ba] [nb pc]. split //. exact: ba.
  Qed.


  Lemma chu_lt_inf I (F : I lprop) p :
    chu_lt (inf F) p i, chu_lt (F i) p.
  Proof.
    move [/=]. rewrite prop_exE /= -[i nfi] pa. exists i. by split.
  Qed.


  Canonical chu_llatMixin := LLatMixin chu_lt_left chu_lt_right chu_lt_inf.
  Canonical chu_llat := Eval hnf in LLat lprop chu_llatMixin.
End Chu.

Products of L-lattices

Section IProdLLat.
Variables (T : Type) (F : T llat).
Implicit Types (f g h : iprod F) (x : T).

Definition iprod_lt f g := x, f x g x.

Lemma iprod_lt_left f g h :
  iprod_lt f g (g h) iprod_lt f h.
Proof.
  move -[x lt_fx_gx] le_g_h. exists x. exact: lt_left (le_g_h x).
Qed.


Lemma iprod_lt_right f g h :
  (f g) iprod_lt g h iprod_lt f h.
Proof.
  move le_f_g [x lt_gx_hx]. exists x. exact: lt_right (le_f_g x) _.
Qed.


Lemma iprod_lt_inf I (P : I iprod F) f :
  iprod_lt (inf P) f i, iprod_lt (P i) f.
Proof.
  case x /lt_inf[i lt_Px_fx]. exists i. exists x. exact: lt_Px_fx.
Qed.


Canonical iprod_llatMixin := LLatMixin iprod_lt_left iprod_lt_right iprod_lt_inf.
Canonical iprod_llat := Eval hnf in LLat (iprod F) iprod_llatMixin.
End IProdLLat.