Lvc.Infra.Lattice

Require Export Containers.OrderedType Setoid Coq.Classes.Morphisms Computable.
Require Export PartialOrder.
Require Import EqDec DecSolve.

Class BoundedSemiLattice (A : Type) `{PartialOrder A} := {
  bottom : A;
  join : A → A → A;

  bottom_least : ∀ a, poLe bottom a;

  join_idempotent : ∀ a, poEq (join a a) a;
  join_commutative : ∀ a b, poEq (join a b) (join b a);
  join_associative : ∀ a b c, poEq (join (join a b) c) (join a (join b c));
  join_poLe : ∀ a b, poLe a (join a b);

  join_respects_eq :> Proper (poEq ==> poEq ==> poEq) join;
  join_respects_le :> Proper (poLe ==> poLe ==> poLe) join
}.

Infix "⊔" := join (at level 70, no associativity).
Notation "⊥" := bottom (at level 70, no associativity).

Instance pair_boundedsemilattice A B `{BoundedSemiLattice A} `{BoundedSemiLattice B}
  : BoundedSemiLattice (A × B) := {
  bottom := (bottom, bottom);
  join x y := (join (fst x) (fst y), join (snd x) (snd y))
}.
Proof.
  - intros [a b]; split; simpl; eapply bottom_least.
  - intros [a b]; split; simpl; eapply join_idempotent.
  - intros [a1 a2] [b1 b2]; split; simpl; eapply join_commutative.
  - intros [a1 a2] [b1 b2] [c1 c2]; split; simpl; eapply join_associative.
  - intros [a1 a2] [b1 b2]; split; simpl; eapply join_poLe.
  - intros [a1 a2] [b1 b2] [EQa EQb] [c1 c2] [d1 d2] [EQc EQd]; simpl in *;
      split; eapply join_respects_eq; eauto.
  - intros [a1 a2] [b1 b2] [LEa LEb] [c1 c2] [d1 d2] [LEc LEd]; simpl in *;
      split; eapply join_respects_le; eauto.
Defined.

Instance bool_boundedsemilattice
  : BoundedSemiLattice bool := {
  bottom := false;
  join := orb
}.
Proof.
  - intros []; simpl; eauto.
  - intros []; simpl; eauto.
  - intros [] []; simpl; eauto.
  - intros [] [] []; simpl; eauto.
  - intros [] []; simpl; eauto.
  - intros [] [] LE [] [] LE'; simpl in *; eauto.
Defined.

Require Import OptionR.

Definition ojoin A join (x y:option A) :=
  match x, y with
  | x, None ⇒ x
  | None, y ⇒ y
  | Some x, Some y ⇒ Some (join x y)
  end.

Instance ojoin_poEq A `{BoundedSemiLattice A}
  : Proper (poEq ==> poEq ==> poEq) (ojoin A join).
Proof.
  unfold Proper, respectful.
  intros ? ? EQ ? ? EQ'; inversion EQ; inversion EQ'; subst; simpl;
    eauto using option_R.
  econstructor. rewrite H1, H4. reflexivity.
Qed.

Instance ojoin_poLe A `{BoundedSemiLattice A}
  : Proper (poLe ==> poLe ==> poLe) (ojoin A join).
Proof.
  unfold Proper, respectful.
  intros ? [y|] EQ ? [y'|] EQ'; inversion EQ; inversion EQ'; subst; simpl;
    eauto using fstNoneOrR.
  - econstructor. rewrite H5. rewrite join_commutative. eapply join_poLe.
  - econstructor. rewrite H3. eapply join_poLe.
  - econstructor. rewrite H3. rewrite H6. reflexivity.
Qed.

Instance option_boundedsemilattice A `{BoundedSemiLattice A}
  : @BoundedSemiLattice (option A) (PartialOrder_option_fstNoneOrR _) := {
  bottom := None;
  join := ojoin _ join
}.
Proof.
  - intros [a|]; simpl; eauto using fstNoneOrR.
  - intros [a|]; simpl; eauto using option_R, join_idempotent.
  - intros [a|] [b|]; simpl; eauto using option_R, join_commutative.
  - intros [a1|] [b1|] [c1|]; simpl; eauto using option_R, join_associative.
  - intros [a|] [b|]; simpl; eauto using fstNoneOrR, join_poLe.
Defined.

Section SemiLatticeTheory.
  Variable A : Type.
  Context `{l : BoundedSemiLattice A}.
  Hint Immediate join_idempotent join_commutative join_associative.

End SemiLatticeTheory.


Inductive withTop (A:Type) :=
| Top : withTop A
| wTA (a:A) : withTop A.

Arguments Top [A].
Arguments wTA [A] a.

Instance withTop_eq_dec A `{EqDec A eq} : EqDec (withTop A) eq.
Proof.
  hnf. destruct x,y; eauto; try dec_solve.
  destruct (H a a0); try dec_solve.
  hnf in e. subst. left; eauto.
Qed.