← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic

« back to all changes in this revision

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

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/Props/DistributiveLattice.agda
2
2
-- Some derivable properties
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
open import Algebra
6
8
 
7
9
module Algebra.Props.DistributiveLattice
8
 
         (dl : DistributiveLattice)
 
10
         {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
9
11
         where
10
12
 
11
 
open DistributiveLattice dl
12
 
import Algebra.Props.Lattice as L; open L lattice public
 
13
open DistributiveLattice DL
 
14
import Algebra.Props.Lattice
 
15
private
 
16
  open module L = Algebra.Props.Lattice lattice public
 
17
    hiding (replace-equality)
13
18
open import Algebra.Structures
14
19
import Algebra.FunctionProperties as P; open P _≈_
 
20
open import Relation.Binary
15
21
import Relation.Binary.EqReasoning as EqR; open EqR setoid
16
 
open import Data.Function
 
22
open import Function
 
23
open import Function.Equality using (_⟨$⟩_)
 
24
open import Function.Equivalence using (_⇔_; module Equivalent)
17
25
open import Data.Product
18
26
 
19
27
∨-∧-distrib : _∨_ DistributesOver _∧_
54
62
  ; ∨-∧-distribʳ = proj₂ ∧-∨-distrib
55
63
  }
56
64
 
57
 
∧-∨-distributiveLattice : DistributiveLattice
 
65
∧-∨-distributiveLattice : DistributiveLattice _ _
58
66
∧-∨-distributiveLattice = record
59
67
  { _∧_                   = _∨_
60
68
  ; _∨_                   = _∧_
61
69
  ; isDistributiveLattice = ∧-∨-isDistributiveLattice
62
70
  }
 
71
 
 
72
-- One can replace the underlying equality with an equivalent one.
 
73
 
 
74
replace-equality :
 
75
  {_≈′_ : Rel Carrier dl₂} →
 
76
  (∀ {x y} → x ≈ y ⇔ x ≈′ y) → DistributiveLattice _ _
 
77
replace-equality {_≈′_} ≈⇔≈′ = record
 
78
  { _≈_                   = _≈′_
 
79
  ; _∧_                   = _∧_
 
80
  ; _∨_                   = _∨_
 
81
  ; isDistributiveLattice = record
 
82
    { isLattice    = Lattice.isLattice (L.replace-equality ≈⇔≈′)
 
83
    ; ∨-∧-distribʳ = λ x y z → to ⟨$⟩ ∨-∧-distribʳ x y z
 
84
    }
 
85
  } where open module E {x y} = Equivalent (≈⇔≈′ {x} {y})