Agda + Lattice + Poset

ひさしぶりにagdaを触ってみた．
コンパイラと標準ライブラリを最新版に更新して，あちこち眺めた．
コンパイラが2Gのメモリを食い潰すくらいに標準ライブラリが充実してきているみたい．
Equational Reasoningができるようになっているらしい．

試しに見よう見まねで束から半順序を作ってみた．

LatticePoset.agda

open import Algebra

module LatticePoset (L : Lattice) where
open Lattice L

open import Relation.Binary
open import Algebra.Props.Lattice
open import Data.Product

import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid

_≤_ : Rel carrier
x ≤ y = x ∨ y ≈ y

_≤'_ : Rel carrier
x ≤' y = x ∧ y ≈ x

infix 4 _≤_ _≤'_

≤-≤'-inc : ∀ {x y} → x ≤ y → x ≤' y
≤-≤'-inc {x} {y} p = begin
  x ∧ y ≈⟨ ∧-pres-≈ refl (sym p) ⟩
  x ∧ (x ∨ y) ≈⟨ proj₂ absorptive x y ⟩
  x ∎

≤'-≤-inc : ∀ {x y} → x ≤' y → x ≤ y
≤'-≤-inc {x} {y} p = begin
  x ∨ y ≈⟨ ∨-pres-≈ (sym p) refl ⟩
  (x ∧ y) ∨ y ≈⟨ ∨-comm (x ∧ y) y ⟩
  y ∨ (x ∧ y) ≈⟨ ∨-pres-≈ refl (∧-comm x y) ⟩
  y ∨ y ∧ x ≈⟨ proj₁ absorptive y x ⟩
  y ∎

≤-refl : _≈_ ⇒ _≤_
≤-refl {x} {y} p = begin
  x ∨ y ≈⟨ ∨-pres-≈ p refl ⟩
  y ∨ y ≈⟨ ∨-idempotent L y ⟩
  y ∎

≤-trans : Transitive _≤_
≤-trans {x} {y} {z} p q = begin
  x ∨ z ≈⟨ ∨-pres-≈ refl (sym q) ⟩
  x ∨ (y ∨ z) ≈⟨ sym (∨-assoc x y z) ⟩ 
  (x ∨ y) ∨ z ≈⟨ ∨-pres-≈ p refl ⟩
  y ∨ z ≈⟨ q ⟩
  z ∎

≤-resp-≈ : _≤_ Respects₂ _≈_
≤-resp-≈ = (λ {x} {y} {z} p q → begin x ∨ z ≈⟨ ∨-pres-≈ refl (sym p) ⟩
                                      x ∨ y ≈⟨ q ⟩
                                      y ≈⟨ p ⟩
                                      z ∎) ,
           λ {x} {y} {z} p q → begin z ∨ x ≈⟨ ∨-pres-≈ (sym p) refl ⟩
                                     y ∨ x ≈⟨ q ⟩
                                     x ∎

≤-antisym : Antisymmetric _≈_ _≤_
≤-antisym {x} {y} p q = begin
  x ≈⟨ sym q ⟩ 
  y ∨ x ≈⟨ ∨-comm y x ⟩
  x ∨ y ≈⟨ p ⟩
  y ∎

≤-isPreorder : IsPreorder _≈_ _≤_
≤-isPreorder = record {
                 isEquivalence = isEquivalence;
                 reflexive = ≤-refl;
                 trans = ≤-trans;
                 ∼-resp-≈ = ≤-resp-≈
               }

≤-isPartialOrder : IsPartialOrder _≈_ _≤_
≤-isPartialOrder = record {
                     isPreorder = ≤-isPreorder;
                     antisym = ≤-antisym
                   }

LatticePoset : Poset
LatticePoset = record {
                 carrier = carrier;
                 _≈_ = _≈_;
                 _≤_ = _≤_;
                 isPartialOrder = ≤-isPartialOrder
               }