open import Algebra
module Algebra.Props.Lattice (l : Lattice) where
open Lattice l
open import Algebra.Structures
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product
∧-idempotent : Idempotent _∧_
∧-idempotent x = begin
x ∧ x ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym (proj₁ absorptive _ _) ⟩
x ∧ (x ∨ x ∧ x) ≈⟨ proj₂ absorptive _ _ ⟩
x ∎
∨-idempotent : Idempotent _∨_
∨-idempotent x = begin
x ∨ x ≈⟨ refl ⟨ ∨-pres-≈ ⟩ sym (∧-idempotent _) ⟩
x ∨ x ∧ x ≈⟨ proj₁ absorptive _ _ ⟩
x ∎
∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
∧-∨-isLattice = record
{ isEquivalence = isEquivalence
; ∨-comm = ∧-comm
; ∨-assoc = ∧-assoc
; ∨-pres-≈ = ∧-pres-≈
; ∧-comm = ∨-comm
; ∧-assoc = ∨-assoc
; ∧-pres-≈ = ∨-pres-≈
; absorptive = swap absorptive
}
∧-∨-lattice : Lattice
∧-∨-lattice = record
{ _∧_ = _∨_
; _∨_ = _∧_
; isLattice = ∧-∨-isLattice
}