Lvc.Lattice

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

Class BoundedSemiLattice (A : Type) := {
  bsl_partial_order :> PartialOrder A;

  bottom : A;
  join : A → A → 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_respects_eq :> Proper (poEq ==> poEq ==> poEq) join;
  join_respects_le :> Proper (poLe ==> poLe ==> poLe) join
}.

Generalizable Variable A.

Infix "\*/" := join (at level 50, left associativity) : lattice_scope.

Local Open Scope lattice_scope.

Section SemiLatticeTheory.
  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.