Library liblayers.logic.PseudoJoin

Require Import Coq.NArith.NArith.
Require Import Coq.Lists.List.
Require Import liblayers.lib.Decision.
Require Export liblayers.logic.Structures.
Require Export liblayers.logic.LayerData.

Pseudo-joins and some properties

Class PseudoJoin A `{Ale: Le A} `{Aoplus: Oplus A} (lb: A): Prop :=
  {
    oplus_preorder :>
      PreOrder (≤);
    oplus_lower_bound :>
      LowerBound (≤) lb;
    oplus_monotonic :>
      Proper ((≤) ==> (≤) ==> (≤)) (⊕);
    oplus_id_left_le :>
      LeftIdentity (≤) (⊕) lb;
    oplus_assoc_le:
      Associative (≤) (⊕);
    oplus_comm_le:
      Commutative (≤) (⊕);
    oplus_le_left :>
      LeftUpperBound (≤) (⊕)
  }.

Global Instance oplus_params:
  Params (@oplus) 2.

By default, we want associativity to be used in terms of ≡, because it can be used for rewriting regardless of variance. This is why oplus_assoc_le above is not declared as an instance. Note that the ≤ version (as well as flip (≤)) can be recovered by following the subrelation instances.

Section EQUIV_INSTANCES.
  Local Existing Instance oplus_assoc_le.
  Local Existing Instance oplus_comm_le.
  Local Existing Instance le_equiv_assoc.
  Local Existing Instance le_equiv_comm.

  Global Instance oplus_assoc_equiv `{PseudoJoin}:
    Associative (≡) (⊕) := _.
  Global Instance oplus_assoc_comm `{PseudoJoin}:
    Commutative (≡) (⊕) := _.
End EQUIV_INSTANCES.

Sometimes we need those in terms of eq.

Global Instance oplus_id_left `{PseudoJoin} `{HA: !Antisymmetric A eq (≤)}:
  LeftIdentity eq (⊕) lb.
Proof.
  intros x.
  apply antisymmetry.
  apply id_left.
  apply right_upper_bound.
Qed.

Global Instance oplus_comm `{PseudoJoin} `{HA: !Antisymmetric A eq (≤)}:
  Commutative eq (⊕).
Proof.
  intros x y.
  apply antisymmetry; apply commutativity.
Qed.

Combined, specialized versions of associativity, used to accelerate tactics.

Lemma oplus_assoc_equiv2 `{PseudoJoin} x y y2 z:
  ((x ⊕ y ) ⊕ y2 ) ⊕ z ≡ x ⊕ (y ⊕ (y2 ⊕ z )).
Proof.
  rewrite associativity.
  rewrite associativity.
  reflexivity.
Qed.

Lemma oplus_assoc_equiv3 `{PseudoJoin} x y y2 y3 z:
  (((x ⊕ y ) ⊕ y2 ) ⊕ y3 ) ⊕ z ≡ x ⊕ (y ⊕ (y2 ⊕ (y3 ⊕ z ))).
Proof.
  rewrite oplus_assoc_equiv2.
  rewrite associativity.
  reflexivity.
Qed.

Ltac oplus_assoc_simpl_term T:=
  lazymatch T with

| (((?x ⊕ ?y) ⊕ ?y2) ⊕ ?y3) ⊕ ?z ⇒ rewrite (oplus_assoc_equiv3 x y y2 y3 z)
| ((?x ⊕ ?y) ⊕ ?y2) ⊕ ?z ⇒ rewrite (oplus_assoc_equiv2 x y y2 z)
| (?x ⊕ ?y) ⊕ ?z ⇒ rewrite (oplus_assoc_equiv x y z)
end.

Lemma oplus_assoc_comm_equiv `{PseudoJoin} x y z:
  (x ⊕ y ) ⊕ z ≡ y ⊕ (x ⊕ z ).
Proof.
  rewrite (commutativity x y).
  rewrite associativity.
  reflexivity.
Qed.

Data-indexed version

Class SimPseudoJoin V E T
    `{VErg: CategoryOps V E}
    `{Tsim: Sim V E T}
    `{Toplus: ∀ v, Oplus (T v)}
    (lb: ∀ v, T v): Prop :=
  {
    oplus_sim_quiv_sim :>
      CategorySim V E T;
    oplus_sim_lower_bound v1 v2 e x :>
      Convertible x (lb v1) →
      @LowerBound (T v1) (T v2) (simRR v1 v2 e) x;
    oplus_sim_monotonic :>
      Monotonic
        (fun v ⇒ (@oplus (T v) _))
        (forallr R, sim R ++> sim R ++> sim R);
    oplus_sim_id_left_le v x :>
      Convertible x (lb v) →
      LeftIdentity (sim id) (⊕) x;
    oplus_sim_assoc_le v:
      @Associative (T v) (sim id) (⊕);
    oplus_sim_comm_le v:
      @Commutative (T v) (sim id) (⊕);
    oplus_sim_le_left v :>
      @LeftUpperBound (T v) (sim id) (⊕)
  }.

Local Existing Instance cat_sim_cat.

XXX: Because of its form, oplus_sim_monotonic cannot be resolved by the monotonicity tactic or setoid rewriting. For the id case, we can work around this with an explicitely specialized instance.

Global Instance oplus_le_monotonic `{SimPseudoJoin} v:
  @Proper (T v → T v → T v) (sim id ++> sim id ++> sim id) (⊕).
Proof.
  apply oplus_sim_monotonic.
Qed.

Section SIM_EQUIV_INSTANCES.
  Local Existing Instance oplus_sim_assoc_le.
  Local Existing Instance oplus_sim_comm_le.
  Local Existing Instance le_equiv_assoc.
  Local Existing Instance le_equiv_comm.

  Global Instance oplus_sim_assoc_equiv `{SimPseudoJoin} D:
    @Associative (T D) (≡) (⊕) := _.
  Global Instance oplus_sim_comm_equiv `{SimPseudoJoin} D:
    @Commutative (T D) (≡) (⊕) := _.
End SIM_EQUIV_INSTANCES.

Global Instance oplus_sim_id_left `{SimPseudoJoin} D:
  Antisymmetric (T D) eq (≤) →
  @LeftIdentity (T D) eq (⊕) (lb D).
Proof.
  intros Hantisym y.
  apply antisymmetry.
  apply id_left.
  apply right_upper_bound.
Qed.

Global Instance oplus_sim_comm `{SimPseudoJoin} D:
  Antisymmetric (T D) eq (≤) →
  @Commutative (T D) eq (⊕).
Proof.
  intros Hantisym x y.
  apply antisymmetry; apply commutativity.
Qed.

Deriving the PseudoJoins on (T D)

Global Instance sim_pseudojoin `(SimPseudoJoin):
∀ D, PseudoJoin (T D) (lb D).
Proof.
intros D; split; typeclasses eauto.
Qed.

A more complete join

Section SIMJOIN.
  Context {V E T} `{HVET: CategorySim V E T}.
  Context `{Top: ∀ v, Oplus (T v)}.

  Class SimLUB v (x y z: T v) :=
    {
      hlub_ub_l: sim id x z;
      hlub_ub_r: sim id y z;
      hlub_intro v' (e: E v v') t: sim e x t → sim e y t → sim e z t
    }.

  Class SimJoin :=
    is_join v x y :> SimLUB v x y (x ⊕ y).

  Context `{Hop: !SimJoin}.

  Local Instance simjoin_sim v1 v2 (e: E v1 v2):
    Monotonic (⊕) (sim e ++> sim e ++> sim e).
  Proof.
    repeat rstep.
    apply hlub_intro.
    + htransitivity y; eauto.
      apply hlub_ub_l.
    + htransitivity y0; eauto.
      eapply hlub_ub_r.
  Qed.

  Local Instance simjoin_pjoin (bot: ∀ v, T v):
    (∀ v1 v2 e, LowerBound (simRR v1 v2 e) (bot v1)) →
    SimPseudoJoin V E T bot.
  Proof.
    split.
    - assumption.
    - intros v1 v2 e x Hx.
      rewrite Hx.
      eauto.
    - rauto.
    - intros v x Hx.
      rewrite Hx; clear x Hx.
      intros x.
      eapply hlub_intro.
      + eapply lower_bound.
      + reflexivity.
    - intros v x y z.
      eapply hlub_intro.
      + apply hlub_intro.
        × apply hlub_ub_l.
        × transitivity (y ⊕ z).
          apply hlub_ub_l.
          apply hlub_ub_r.
      + transitivity (y ⊕ z).
        × apply hlub_ub_r.
        × apply hlub_ub_r.
    - intros v x y.
      apply hlub_intro.
      + eapply hlub_ub_r.
      + eapply hlub_ub_l.
    - intros v x y.
      eapply hlub_ub_l.
  Qed.
End SIMJOIN.

Arguments SimJoin V E T {_ _ _}.

Normalization procedure

Booleans have a pseudo-join structure

Global Instance bool_oplus : Oplus bool := { oplus := orb }.

Global Instance bool_pjoin : PseudoJoin bool false.
Proof.
split; typeclasses eauto.
Qed.

Product of pseudo-join structures

Section PSEUDOJOIN_PROD.
  Context {A Ale Aoplus Alb} `{HA: @PseudoJoin A Ale Aoplus Alb}.
  Context {B Ble Boplus Blb} `{HB: @PseudoJoin B Ble Boplus Blb}.

  Local Instance prod_le_op : Le (A × B) :=
    { le := (≤) × (≤) }.

  Local Instance prod_oplus: Oplus (A × B)%type :=
    {
      oplus x y :=
        match x, y with
          | (xa, xb), (ya, yb) ⇒ (xa ⊕ ya, xb ⊕ yb)
        end
    }.

  Local Instance prod_pjoin : PseudoJoin (A × B)%type (Alb , Blb ).
  Proof.
    split.
    × simpl.
      typeclasses eauto.
    × intros [a b].
      constructor;
      apply lower_bound.
    × intros [xa1 xb1] [xa2 xb2] [Hxa Hxb] [ya1 yb1] [ya2 yb2] [Hya Hyb].
      simpl in ×.
      solve_monotonic.
    × intros [a b].
      constructor; simpl;
        apply id_left.
    × intros [xa xb] [ya yb] [za zb].
      constructor; simpl;
        apply associativity.
    × intros [xa xb] [ya yb].
      unfold oplus;
        simpl.
      split; simpl; apply commutativity.
    × intros [xa xb] [ya yb].
      constructor; simpl;
        apply left_upper_bound.
  Qed.
End PSEUDOJOIN_PROD.

Adjoining an extra element

Definition extension A := (A × bool)%type.

Section PSEUDOJOIN_EXTENSION.
  Context `{PseudoJoin}.

  Definition ext_le: relation (extension A) :=
    (≤) × leb.

  Definition ext_inj (a: A): extension A :=
    (a , false ).

  Definition ext_elem: extension A :=
    (lb , true ).

  Definition ext_map {B} (f: A → B) (x: extension A): extension B :=
    match x with (a, b) ⇒ (f a, b) end.

  Local Instance ext_le_op : Le (extension A) := prod_le_op.
  Local Instance ext_oplus : Oplus (extension A) := prod_oplus.
  Local Instance ext_pjoin : PseudoJoin (extension A) (ext_inj lb) := prod_pjoin.
End PSEUDOJOIN_EXTENSION.