← Back to branch summary

~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Algebra/Props/Lattice.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/Props/Lattice.agda
 
1
------------------------------------------------------------------------
 
2
-- Some derivable properties
 
3
------------------------------------------------------------------------
 
4
 
 
5
open import Algebra
 
6
 
 
7
module Algebra.Props.Lattice (l : Lattice) where
 
8
 
 
9
open Lattice l
 
10
open import Algebra.Structures
 
11
import Algebra.FunctionProperties as P; open P _≈_
 
12
import Relation.Binary.EqReasoning as EqR; open EqR setoid
 
13
open import Data.Function
 
14
open import Data.Product
 
15
 
 
16
∧-idempotent : Idempotent _∧_
 
17
∧-idempotent x = begin
 
18
  x ∧ x            ≈⟨ refl ⟨ ∧-cong ⟩ sym (proj₁ absorptive _ _) ⟩
 
19
  x ∧ (x ∨ x ∧ x)  ≈⟨ proj₂ absorptive _ _ ⟩
 
20
  x                ∎
 
21
 
 
22
∨-idempotent : Idempotent _∨_
 
23
∨-idempotent x = begin
 
24
  x ∨ x      ≈⟨ refl ⟨ ∨-cong ⟩ sym (∧-idempotent _) ⟩
 
25
  x ∨ x ∧ x  ≈⟨ proj₁ absorptive _ _ ⟩
 
26
  x          ∎
 
27
 
 
28
-- The dual construction is also a lattice.
 
29
 
 
30
∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
 
31
∧-∨-isLattice = record
 
32
  { isEquivalence = isEquivalence
 
33
  ; ∨-comm        = ∧-comm
 
34
  ; ∨-assoc       = ∧-assoc
 
35
  ; ∨-cong        = ∧-cong
 
36
  ; ∧-comm        = ∨-comm
 
37
  ; ∧-assoc       = ∨-assoc
 
38
  ; ∧-cong        = ∨-cong
 
39
  ; absorptive    = swap absorptive
 
40
  }
 
41
 
 
42
∧-∨-lattice : Lattice
 
43
∧-∨-lattice = record
 
44
  { _∧_       = _∨_
 
45
  ; _∨_       = _∧_
 
46
  ; isLattice = ∧-∨-isLattice
 
47
  }