-- Equivalence between two characterizations of Semilattices:
-- + as a commutative and idempotent semigroup
-- + as a partial order with join for any two elements

open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; subst ; sym)
open import Data.Product using (_,_ ; _×_ ; proj₁ ; proj₂)

module Semilattice (A : Set) where

record Reflexive (_R_ : A → A → Set) : Set where
  constructor mk-refl
  field
    reflexive : ∀ {a : A} → a R a

record Antisymmetric (_R_ : A → A → Set) : Set where
  constructor mk-antisym
  field
    antisym : ∀ {a b : A} → a R b → b R a → a ≡ b

record Transitive (_R_ : A → A → Set) : Set where
  constructor mk-trans
  field
    transitive : ∀ {a b c : A} → b R c → a R b → a R c

record PartialOrder (_≤_ : A → A → Set) : Set where
  field
    reflexive  : Reflexive _≤_
    antisym    : Antisymmetric _≤_
    transitive : Transitive _≤_

record OrderTheoreticSemilattice : Set₁ where
  constructor mk-osl
  field
    _≤_ : A → A → Set
    _⋁_ : A → A → A
    ≤-partial-order : PartialOrder _≤_

    ⋁-upper-bound : ∀ {x y : A} → (x ≤ (x ⋁ y)) × (y ≤ (x ⋁ y))
    ⋁-least-upper-bound : ∀ {x y d : A} → (x ≤ d) → (y ≤ d) → (x ⋁ y) ≤ d

record Associative (_∙_ : A → A → A) : Set where
  constructor mk-assoc
  field
    assoc : ∀ {a b c : A} → a ∙ (b ∙ c) ≡ (a ∙ b) ∙ c

record Commutative (_∙_ : A → A → A) : Set where
  constructor mk-comm
  field
    comm : ∀ {a b : A} → a ∙ b ≡ b ∙ a

record Idempotent (_∙_ : A → A → A) : Set where
  constructor mk-idem
  field
    idem : ∀ {a : A} → a ∙ a ≡ a

record Semilattice : Set where
  constructor mk-sl
  field
    _∙_ : A → A → A
    ∙-assoc : Associative _∙_
    ∙-comm  : Commutative _∙_
    ∙-idem  : Idempotent _∙_

module InducedOrder (_∙_ : A → A → A)
                    (∙-idem : Idempotent _∙_)
                    (∙-comm : Commutative _∙_)
                    (∙-assoc : Associative _∙_) where

  open Associative ∙-assoc
  open Commutative ∙-comm
  open Idempotent ∙-idem
  
  infix 5 _≤ᵢ_
  data _≤ᵢ_ : A → A → Set where
    ord : ∀ (a b : A) → a ≤ᵢ a ∙ b

  char : ∀ {a b : A} → a ≤ᵢ b → b ≡ a ∙ b
  char (ord a b) rewrite
    (assoc {a} {a} {b})
    | (idem {a}) = refl

  ≤ᵢ-reflexive : Reflexive _≤ᵢ_
  Reflexive.reflexive ≤ᵢ-reflexive {a} =
    subst (λ x → a ≤ᵢ x) (idem {a}) (ord a a)

  ≤ᵢ-antisym : Antisymmetric _≤ᵢ_
  Antisymmetric.antisym ≤ᵢ-antisym {a} {b} a≤ᵢb b≤ᵢa rewrite
    (char a≤ᵢb)
    | (char b≤ᵢa)
    | (comm {a} {b})
    | (sym (assoc {b} {a} {a}))
    | (idem {a})
    | (comm {b} {a})
    | (sym (assoc {a} {b} {b}))
    | (idem {b})
    = refl

  ≤ᵢ-transitive : Transitive _≤ᵢ_
  Transitive.transitive ≤ᵢ-transitive {a} {b} {c} b≤ᵢc a≤ᵢb rewrite
    (char b≤ᵢc)
    | (char a≤ᵢb)
    | (sym (assoc {a} {b} {c})) = ord a (b ∙ c)

  ≤ᵢ-partial-order : PartialOrder _≤ᵢ_
  PartialOrder.reflexive ≤ᵢ-partial-order = ≤ᵢ-reflexive
  PartialOrder.antisym ≤ᵢ-partial-order = ≤ᵢ-antisym
  PartialOrder.transitive ≤ᵢ-partial-order = ≤ᵢ-transitive


to : Semilattice → OrderTheoreticSemilattice
to sl = mk-osl _≤_ _∙_ ≤ᵢ-partial-order ub lub
   where open Semilattice sl
         open InducedOrder _∙_ ∙-idem ∙-comm ∙-assoc renaming (_≤ᵢ_ to _≤_)
         open Commutative ∙-comm
         open Associative ∙-assoc

         ub : ∀ {a b : A} → a ≤ (a ∙ b) × b ≤ (a ∙ b)
         ub {a} {b} =
           (ord a b) , subst (λ x → b ≤ x) comm (ord b a)

         lub : {a b x : A} → a ≤ x → b ≤ x → (a ∙ b) ≤ x
         lub {a} {b} {x} a≤x b≤x rewrite
          (char b≤x)
          | (char a≤x)
          | (assoc {a} {b} {x}) = ord (a ∙ b) x

from : OrderTheoreticSemilattice → Semilattice
from osl = mk-sl _⋁_ (mk-assoc assoc) (mk-comm comm) (mk-idem idem)
  where open OrderTheoreticSemilattice osl
        open Transitive (PartialOrder.transitive ≤-partial-order)
        open Reflexive (PartialOrder.reflexive ≤-partial-order)
        open Antisymmetric (PartialOrder.antisym ≤-partial-order)

        assoc : ∀ {a b c : A} → a ⋁ (b ⋁ c) ≡ (a ⋁ b) ⋁ c
        assoc {x} {y} {z} = antisym
          (let (x⋁y≤a , z≤a) = ⋁-upper-bound {x ⋁ y} {z} in
            ⋁-least-upper-bound
              (transitive x⋁y≤a (proj₁ ⋁-upper-bound))
              (⋁-least-upper-bound
                (transitive x⋁y≤a (proj₂ ⋁-upper-bound))
                z≤a))
          (let (x≤a , y⋁z≤a) = ⋁-upper-bound {x} {y ⋁ z} in
            ⋁-least-upper-bound
              (⋁-least-upper-bound
                x≤a
                (transitive y⋁z≤a (proj₁ ⋁-upper-bound)))
              (transitive y⋁z≤a (proj₂ ⋁-upper-bound)))

        idem : ∀ {a : A} → a ⋁ a ≡ a
        idem {a} = antisym
          (⋁-least-upper-bound {a} {a} {a} reflexive reflexive)
          (proj₁ ⋁-upper-bound)

        comm : ∀ {a b : A} → (a ⋁ b) ≡ (b ⋁ a)
        comm {a} {b} = antisym
          (⋁-least-upper-bound (proj₂ ⋁-upper-bound) (proj₁ ⋁-upper-bound))
          (⋁-least-upper-bound (proj₂ ⋁-upper-bound) (proj₁ ⋁-upper-bound))