Lattice.agda

module Lattice where

open import Prelude
open import PartialOrder as PO
open import SemiLattice  as SL
import Chain
open POrder using (Dual)

record Lattice (A : Set) : Set1 where
  field
    sl : SemiLattice A
    _⊔_ : A -> A -> A
    prf : IsSemiLattice (Dual (SemiLat.po sl)) _⊔_

module Lat {A : Set}(L : Lattice A) where

  private
    module LL    = Lattice L
    module SLL   = SemiLat LL.sl

  private
    sl' : SemiLattice A
    sl' = record { po = Dual SLL.po; _⊓_ = LL._⊔_; prf = LL.prf }

    module SLL'  = SemiLat sl'
      hiding   ( Monotone
               ; Antitone
               ; _==_; ==-refl; ==-sym; ==-trans
               ; po
               )
      renaming ( _≤_          to _≥_
               ; ≤-refl       to ≥-refl
               ; ≤-trans      to ≥-trans
               ; ≤-antisym    to ≥-antisym
               ; ==≤-L        to ==≥-R
               ; ==≤-R        to ==≥-L
               ; _⊓_          to _⊔_
               ; ⊓-lbL        to ⊔-ubL
               ; ⊓-lbR        to ⊔-ubR
               ; ⊓-glb        to ⊔-lub
               ; ⊓-commute    to ⊔-commute
               ; ⊓-assoc      to ⊔-assoc
               ; ⊓-idem       to ⊔-idem
               ; ≤⊓-L         to ≥⊔-L
               ; ≤⊓-R         to ≥⊔-R
               ; ⊓-monotone-R to ⊔-monotone-R
               ; ⊓-monotone-L to ⊔-monotone-L
               ; ≤⊓-compat    to ≥⊔-compat
               ; ⊓-cong       to ⊔-cong
               ; ⊓-cong-L     to ⊔-cong-L
               ; ⊓-cong-R     to ⊔-cong-R
               )

  open SLL  public
  open SLL' public

  DualLattice : Lattice A
  DualLattice = record { sl = sl'; _⊔_ = _⊓_; prf = SemiLattice.prf LL.sl }

module MeetJoin {A : Set}(L : Lattice A) where 

  private module L = Lat L
  open L

  open module C== = Chain _==_ (\x -> ==-refl) (\x y z -> ==-trans)

  -- Experiment with very explicit proof
  ⊓⊔-absorb-LL = \{x y} ->
    (x ⊓ (x ⊔ y)) == x  from
      ≤-antisym
        ((x ⊓ (x ⊔ y)) ≤ x from ⊓-lbL)
        (x ≤ (x ⊓ (x ⊔ y)) from
          ⊓-glb (x ≤ x       from ≤-refl)
                (x ≤ (x ⊔ y) from ⊔-ubL)
        )

  ⊓⊔-eq : forall {x y} -> (x ⊓ y) == (x ⊔ y) -> x == y
  ⊓⊔-eq {x}{y} p =
    chain> x
       === x ⊓ (x ⊔ y) by ==-sym ⊓⊔-absorb-LL
       === x ⊓ (x ⊓ y) by ==-sym (⊓-cong-R p)
       === (x ⊓ x) ⊓ y by {!!} -- ⊓-assoc
       === x ⊓ y       by ⊓-cong-L ⊓-idem
       === y ⊓ x       by ⊓-commute
       === (y ⊓ y) ⊓ x by ⊓-cong-L (==-sym ⊓-idem)
       === y ⊓ (y ⊓ x) by ==-sym ⊓-assoc
       === y ⊓ (x ⊓ y) by ⊓-cong-R ⊓-commute
       === y ⊓ (x ⊔ y) by {! !} -- ⊓-cong-R p
       === y ⊓ (y ⊔ x) by ⊓-cong-R ⊔-commute
       === y           by ⊓⊔-absorb-LL

module JoinMeet {A : Set}(L : Lattice A) =
  MeetJoin (Lat.DualLattice L)
  hiding (⊓⊔-eq)
  renaming (⊓⊔-absorb-LL to ⊔⊓-absorb-LL)