semantics.ord.frame

Require Import base protype ordtype clat.

Module Frame.
  Record mixin_of (T : clat) := Mixin {
    _ : forall I (F : I -> T) (x : T), x ∧ (∃ i, F i) ≤ ∃ i, x ∧ F i
  }.

  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 b0 (m0 : mixin_of (@CLat.Pack T b0 T)) :=
      [find pt | CLat.sort pt ~ T | "is not a clat"]
      [find pe | CLat.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.
    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 frame := type.
    Notation FrameMixin := Mixin.
    Notation Frame T m := (@pack T _ m _ id _ id _ id).

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

Definition imp {T : frame} (x y : T) : T :=
  ∃ z : T | z ∧ x ≤ y, z.
Notation "x → y" := (imp x y)
  (at level 98, right associativity) : ord_scope.

Section FrameLaws.
  Variable (T : frame).
  Implicit Types (x y z : T).

  Lemma meetxE I (F : I -> T) x : (x ∧ ∃ i, F i) = ∃ i, x ∧ F i.
  Proof.
    apply: le_eq. by case: T F x => ?[?[]].
    apply: exE => i. apply: meet_mono => //. exact: exI.
  Qed.

  Lemma meetEx I (F : I -> T) x : ((∃ i, F i) ∧ x) = ∃ i, F i ∧ x.
  Proof. rewrite meetC meetxE. f_equal. fext=> i. by rewrite meetC. Qed.

  Lemma impI x y z : x ∧ y ≤ z -> x ≤ y → z.
  Proof.
    move=> le_xy_z. exact: exIc (x) le_xy_z le_refl.
  Qed.

  Lemma impEr x y : (x → y) ∧ x ≤ y.
  Proof.
    rewrite/imp meetEx. focus=> w. rewrite meetEx.
    apply: exE. exact.
  Qed.

  Lemma impEl x y : x ∧ (x → y) ≤ y.
  Proof. rewrite meetC. exact: impEr. Qed.

  Lemma impP x y z : (x ∧ y ≤ z) <-> (x ≤ y → z).
  Proof. split. exact: impI. move->. exact: impEr. Qed.

  Global Instance imp_proper :
    Proper (ord_op --> ord_op ++> ord_op) (@imp T).
  Proof.
    move=> x1 x2 lex y1 y2 ley. apply/impP. rewrite lex -ley. exact/impP.
  Qed.

  Ltac focus := nointr (repeat (focus1p || apply: impI)).

  Lemma meetxJ x y z : (x ∧ (y ∨ z)) = (x ∧ y ∨ x ∧ z).
  Proof.
    apply: le_eq; last by cauto. rewrite meetC. apply/impP.
    focus; rewrite meetC. exact: joinIl. exact: joinIr.
  Qed.

  Lemma meetJx x y z : ((x ∨ y) ∧ z) = (x ∧ z ∨ y ∧ z).
  Proof. by rewrite meetC meetxJ meetC [_ ∧ y]meetC. Qed.

  Lemma imp_cut y x z :
    x ≤ y → z -> x ≤ y -> x ≤ z.
  Proof.
    move=> le_x_yz le_x_y. rewrite -[x]meetxx {1}le_x_yz le_x_y. exact/impP.
  Qed.
  Arguments imp_cut y {x z} le_x_yz le_x_y.

  Lemma impxx x : (x → x) = ⊤.
  Proof. apply: top_eq. apply/impP. exact: meetEr. Qed.

  Lemma impTx x : (⊤ → x) = x.
  Proof.
    apply: le_eq. rewrite -[_ → _]meetxT. exact/impP.
    apply/impP. by rewrite meetxT.
  Qed.

  Lemma impxT x : (x → ⊤) = ⊤.
  Proof.
    apply: top_eq. apply/impP. exact: topI.
  Qed.

  Lemma impBx x : (⊥ → x) = ⊤.
  Proof.
    apply: top_eq. apply/impP. rewrite meetTx. exact: botE.
  Qed.

  Lemma impJx x y z : (x ∨ y → z) = ((x → z) ∧ (y → z)).
  Proof.
    apply/le_eq. focus. apply: (imp_cut x). apply: meetEl. f_equiv. exact: joinIl.
    exact: meetEr. apply: (imp_cut y); last by exact: meetEr. apply: meetEl.
    f_equiv. exact: joinIr. focus. rewrite meetxJ. focus. apply/impP.
    exact: meetEl. apply/impP. exact: meetEr.
  Qed.

  Lemma impxJ x y z : (x → y) ∨ (x → z) ≤ x → y ∨ z.
  Proof.
    focus. apply: joinIl. exact: impEr. apply: joinIr. exact: impEr.
  Qed.

  Lemma impMx x y z : (x ∧ y → z) = (x → (y → z)).
  Proof.
    apply: le_eq. focus. rewrite -meetA. exact: impEr.
    focus. rewrite meetA. apply/impP. exact/impP.
  Qed.

  Lemma impxM x y z : (x → y ∧ z) = ((x → y) ∧ (x → z)).
  Proof.
    apply: le_eq. focus; rewrite impEr; by cauto.
    focus; apply/impP; by cauto.
  Qed.

  Lemma impEx I (F : I -> T) x :
    ((sup F) → x) = ∀ i, F i → x.
  Proof.
    apply: le_eq. apply: allI => i. f_equiv. exact: exI.
    focus. rewrite meetxE. focus=> i. apply/impP.
    exact: allE (i) le_refl.
  Qed.

  Lemma impxA I (F : I -> T) x :
    (x → inf F) = ∀ i, x → F i.
  Proof.
    apply: le_eq. focus=> i. rewrite impEr. exact: allE.
    focus=> i. apply/impP. exact: allE (i) le_refl.
  Qed.

  Lemma weaken x y : y ≤ x → y.
  Proof. apply: impI. exact: meetEl. Qed.

  Lemma meetHl x y : ((x → y) ∧ x) = (y ∧ x).
  Proof.
    apply: le_eq. apply: meetI. exact: impEr. exact: meetEr.
    apply: meetI. apply: meetEl. exact: weaken. exact: meetEr.
  Qed.

  Lemma meetHr x y : ((x → y) ∧ y) = y.
  Proof. apply: le_eq. exact: meetEr. apply: meetI => //. exact: weaken. Qed.

  Lemma imp_def w y z :
    (w ∧ y ≤ z) ->
    (forall x, (x ∧ y ≤ z) -> (x ≤ w)) ->
    (y → z) = w.
  Proof.
    move=> h1 h2. apply: le_eq. exact/h2/impP. exact/impP/h1.
  Qed.
End FrameLaws.