← Back to branch summary

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

« back to all changes in this revision

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

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/Props/DistributiveLattice.agda
1
1
------------------------------------------------------------------------
2
2
-- The Agda standard library
3
3
--
 
4
-- Compatibility module. Pending for removal. Use
 
5
-- Algebra.Properties.DistributiveLattice instead.
4
6
------------------------------------------------------------------------
5
7
 
6
8
open import Algebra
10
11
         {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
11
12
         where
12
13
 
13
 
open DistributiveLattice DL
14
 
import Algebra.Props.Lattice
15
 
private
16
 
  open module L = Algebra.Props.Lattice lattice public
17
 
    hiding (replace-equality)
18
 
open import Algebra.Structures
19
 
import Algebra.FunctionProperties as P; open P _≈_
20
 
open import Relation.Binary
21
 
import Relation.Binary.EqReasoning as EqR; open EqR setoid
22
 
open import Function
23
 
open import Function.Equality using (_⟨$⟩_)
24
 
open import Function.Equivalence using (_⇔_; module Equivalence)
25
 
open import Data.Product
26
 
 
27
 
∨-∧-distrib : _∨_ DistributesOver _∧_
28
 
∨-∧-distrib = ∨-∧-distribˡ , ∨-∧-distribʳ
29
 
  where
30
 
  ∨-∧-distribˡ : _∨_ DistributesOverˡ _∧_
31
 
  ∨-∧-distribˡ x y z = begin
32
 
    x ∨ y ∧ z          ≈⟨ ∨-comm _ _ ⟩
33
 
    y ∧ z ∨ x          ≈⟨ ∨-∧-distribʳ _ _ _ ⟩
34
 
    (y ∨ x) ∧ (z ∨ x)  ≈⟨ ∨-comm _ _ ⟨ ∧-cong ⟩ ∨-comm _ _ ⟩
35
 
    (x ∨ y) ∧ (x ∨ z)  ∎
36
 
 
37
 
∧-∨-distrib : _∧_ DistributesOver _∨_
38
 
∧-∨-distrib = ∧-∨-distribˡ , ∧-∨-distribʳ
39
 
  where
40
 
  ∧-∨-distribˡ : _∧_ DistributesOverˡ _∨_
41
 
  ∧-∨-distribˡ x y z = begin
42
 
    x ∧ (y ∨ z)                ≈⟨ sym (proj₂ absorptive _ _) ⟨ ∧-cong ⟩ refl ⟩
43
 
    (x ∧ (x ∨ y)) ∧ (y ∨ z)    ≈⟨ (refl ⟨ ∧-cong ⟩ ∨-comm _ _) ⟨ ∧-cong ⟩ refl ⟩
44
 
    (x ∧ (y ∨ x)) ∧ (y ∨ z)    ≈⟨ ∧-assoc _ _ _ ⟩
45
 
    x ∧ ((y ∨ x) ∧ (y ∨ z))    ≈⟨ refl ⟨ ∧-cong ⟩ sym (proj₁ ∨-∧-distrib _ _ _) ⟩
46
 
    x ∧ (y ∨ x ∧ z)            ≈⟨ sym (proj₁ absorptive _ _) ⟨ ∧-cong ⟩ refl ⟩
47
 
    (x ∨ x ∧ z) ∧ (y ∨ x ∧ z)  ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩
48
 
    x ∧ y ∨ x ∧ z              ∎
49
 
 
50
 
  ∧-∨-distribʳ : _∧_ DistributesOverʳ _∨_
51
 
  ∧-∨-distribʳ x y z = begin
52
 
    (y ∨ z) ∧ x    ≈⟨ ∧-comm _ _ ⟩
53
 
    x ∧ (y ∨ z)    ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
54
 
    x ∧ y ∨ x ∧ z  ≈⟨ ∧-comm _ _ ⟨ ∨-cong ⟩ ∧-comm _ _ ⟩
55
 
    y ∧ x ∨ z ∧ x  ∎
56
 
 
57
 
 
58
 
∧-∨-isDistributiveLattice : IsDistributiveLattice _≈_ _∧_ _∨_
59
 
∧-∨-isDistributiveLattice = record
60
 
  { isLattice    = ∧-∨-isLattice
61
 
  ; ∨-∧-distribʳ = proj₂ ∧-∨-distrib
62
 
  }
63
 
 
64
 
∧-∨-distributiveLattice : DistributiveLattice _ _
65
 
∧-∨-distributiveLattice = record
66
 
  { _∧_                   = _∨_
67
 
  ; _∨_                   = _∧_
68
 
  ; isDistributiveLattice = ∧-∨-isDistributiveLattice
69
 
  }
70
 
 
71
 
 
72
 
replace-equality :
73
 
  {_≈′_ : Rel Carrier dl₂} →
74
 
  (∀ {x y} → x ≈ y ⇔ x ≈′ y) → DistributiveLattice _ _
75
 
replace-equality {_≈′_} ≈⇔≈′ = record
76
 
  { _≈_                   = _≈′_
77
 
  ; _∧_                   = _∧_
78
 
  ; _∨_                   = _∨_
79
 
  ; isDistributiveLattice = record
80
 
    { isLattice    = Lattice.isLattice (L.replace-equality ≈⇔≈′)
81
 
    ; ∨-∧-distribʳ = λ x y z → to ⟨$⟩ ∨-∧-distribʳ x y z
82
 
    }
83
 
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
 
14
open import Algebra.Properties.DistributiveLattice DL public