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
}.
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.