From de335c3955bc81c80c590e31e543267b5b0edfb9 Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Tue, 8 Aug 2017 13:45:27 +0200
Subject: [PATCH] Added join-semilattice

---
 FiniteSets/fsets/properties.v |  9 +++++++++
 FiniteSets/lattice.v          | 23 +++++++++++++++++++++++
 2 files changed, 32 insertions(+)

diff --git a/FiniteSets/fsets/properties.v b/FiniteSets/fsets/properties.v
index b0d6cf7..f11d59e 100644
--- a/FiniteSets/fsets/properties.v
+++ b/FiniteSets/fsets/properties.v
@@ -1,6 +1,7 @@
 Require Import HoTT HitTactics.
 From fsets Require Import operations extensionality.
 Require Export representations.definition disjunction.
+Require Import lattice.
 
 (* Lemmas relating operations to the membership predicate *)
 Section characterize_isIn.
@@ -119,6 +120,14 @@ Section properties.
   Context {A : Type}.
   Context `{Univalence}.
 
+  Instance: bottom(FSet A) := ∅.
+  Instance: maximum(FSet A) := U.
+
+  Global Instance joinsemilattice_fset : JoinSemiLattice (FSet A).
+  Proof.
+    split ; toHProp.
+  Defined.  
+
   (** comprehension properties *)
   Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = ∅.
   Proof.
diff --git a/FiniteSets/lattice.v b/FiniteSets/lattice.v
index 4500d92..616e923 100644
--- a/FiniteSets/lattice.v
+++ b/FiniteSets/lattice.v
@@ -55,6 +55,29 @@ Arguments NeutralL {_} _ _.
 Arguments NeutralR {_} _ _.
 Arguments Absorption {_} _ _.
 
+Section JoinSemiLattice.
+  Variable A : Type.
+  Context {max_L : maximum A} {empty_L : bottom A}.
+
+  Class JoinSemiLattice :=
+    {
+      commutative_max_js :> Commutative max_L ;
+      associative_max_js :> Associative max_L ;
+      idempotent_max_js :> Idempotent max_L ;
+      neutralL_max_js :> NeutralL max_L empty_L ;
+      neutralR_max_js :> NeutralR max_L empty_L ;
+    }.
+End JoinSemiLattice.
+
+Arguments JoinSemiLattice _ {_} {_}.
+
+Create HintDb joinsemilattice_hints.
+Hint Resolve associativity : joinsemilattice_hints.
+Hint Resolve commutative : joinsemilattice_hints.
+Hint Resolve idempotency : joinsemilattice_hints.
+Hint Resolve neutralityL : joinsemilattice_hints.
+Hint Resolve neutralityR : joinsemilattice_hints.
+
 Section Lattice.
   Variable A : Type.
   Context {max_L : maximum A} {min_L : minimum A} {empty_L : bottom A}.