← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Data/Bool/Properties.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Bool/Properties.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- A bunch of properties
3
5
------------------------------------------------------------------------
4
6
 
9
11
open import Function
10
12
open import Function.Equality using (_⟨$⟩_)
11
13
open import Function.Equivalence
12
 
  using (_⇔_; equivalent; module Equivalent)
 
14
  using (_⇔_; equivalence; module Equivalence)
13
15
open import Algebra
14
16
open import Algebra.Structures
15
17
import Algebra.RingSolver.Simple as Solver
16
18
import Algebra.RingSolver.AlmostCommutativeRing as ACR
17
 
open import Relation.Binary.PropositionalEquality
18
 
  hiding (proof-irrelevance)
19
 
open ≡-Reasoning
20
 
import Algebra.FunctionProperties as P; open P _≡_
 
19
open import Relation.Binary.PropositionalEquality as P
 
20
  using (_≡_; _≢_; refl)
 
21
open P.≡-Reasoning
 
22
import Algebra.FunctionProperties as FP; open FP (_≡_ {A = Bool})
21
23
open import Data.Product
22
24
open import Data.Sum
23
25
open import Data.Empty
67
69
       x ∧ (y ∨ z)
68
70
                      ≡⟨ distˡ x y z ⟩
69
71
       x ∧ y ∨ x ∧ z
70
 
                      ≡⟨ cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
 
72
                      ≡⟨ P.cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
71
73
       y ∧ x ∨ z ∧ x
72
74
                      ∎
73
75
 
76
78
isCommutativeSemiring-∨-∧ = record
77
79
  { +-isCommutativeMonoid = record
78
80
    { isSemigroup = record
79
 
      { isEquivalence = isEquivalence
 
81
      { isEquivalence = P.isEquivalence
80
82
      ; assoc         = ∨-assoc
81
 
      ; ∙-cong        = cong₂ _∨_
 
83
      ; ∙-cong        = P.cong₂ _∨_
82
84
      }
83
85
    ; identityˡ = λ _ → refl
84
86
    ; comm      = ∨-comm
85
87
    }
86
88
  ; *-isCommutativeMonoid = record
87
89
    { isSemigroup = record
88
 
      { isEquivalence = isEquivalence
 
90
      { isEquivalence = P.isEquivalence
89
91
      ; assoc         = ∧-assoc
90
 
      ; ∙-cong        = cong₂ _∧_
 
92
      ; ∙-cong        = P.cong₂ _∧_
91
93
      }
92
94
      ; identityˡ = λ _ → refl
93
95
    ; comm      = ∧-comm
128
130
       x ∨ (y ∧ z)
129
131
                          ≡⟨ distˡ x y z ⟩
130
132
       (x ∨ y) ∧ (x ∨ z)
131
 
                          ≡⟨ cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
 
133
                          ≡⟨ P.cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
132
134
       (y ∨ x) ∧ (z ∨ x)
133
135
                          ∎
134
136
 
137
139
isCommutativeSemiring-∧-∨ = record
138
140
  { +-isCommutativeMonoid = record
139
141
    { isSemigroup = record
140
 
      { isEquivalence = isEquivalence
 
142
      { isEquivalence = P.isEquivalence
141
143
      ; assoc         = ∧-assoc
142
 
      ; ∙-cong        = cong₂ _∧_
 
144
      ; ∙-cong        = P.cong₂ _∧_
143
145
      }
144
146
    ; identityˡ = λ _ → refl
145
147
    ; comm      = ∧-comm
146
148
    }
147
149
  ; *-isCommutativeMonoid = record
148
150
    { isSemigroup = record
149
 
      { isEquivalence = isEquivalence
 
151
      { isEquivalence = P.isEquivalence
150
152
      ; assoc         = ∨-assoc
151
 
      ; ∙-cong        = cong₂ _∨_
 
153
      ; ∙-cong        = P.cong₂ _∨_
152
154
      }
153
155
    ; identityˡ = λ _ → refl
154
156
    ; comm      = ∨-comm
184
186
 
185
187
  not-∧-inverse : Inverse false not _∧_
186
188
  not-∧-inverse =
187
 
    ¬x∧x≡⊥ , (λ x → ∧-comm x (not x) ⟨ trans ⟩ ¬x∧x≡⊥ x)
 
189
    ¬x∧x≡⊥ , (λ x → ∧-comm x (not x) ⟨ P.trans ⟩ ¬x∧x≡⊥ x)
188
190
    where
189
191
    ¬x∧x≡⊥ : LeftInverse false not _∧_
190
192
    ¬x∧x≡⊥ false = refl
192
194
 
193
195
  not-∨-inverse : Inverse true not _∨_
194
196
  not-∨-inverse =
195
 
    ¬x∨x≡⊤ , (λ x → ∨-comm x (not x) ⟨ trans ⟩ ¬x∨x≡⊤ x)
 
197
    ¬x∨x≡⊤ , (λ x → ∨-comm x (not x) ⟨ P.trans ⟩ ¬x∨x≡⊤ x)
196
198
    where
197
199
    ¬x∨x≡⊤ : LeftInverse true not _∨_
198
200
    ¬x∨x≡⊤ false = refl
202
204
isBooleanAlgebra = record
203
205
  { isDistributiveLattice = record
204
206
      { isLattice = record
205
 
          { isEquivalence = isEquivalence
 
207
          { isEquivalence = P.isEquivalence
206
208
          ; ∨-comm        = ∨-comm
207
209
          ; ∨-assoc       = ∨-assoc
208
 
          ; ∨-cong        = cong₂ _∨_
 
210
          ; ∨-cong        = P.cong₂ _∨_
209
211
          ; ∧-comm        = ∧-comm
210
212
          ; ∧-assoc       = ∧-assoc
211
 
          ; ∧-cong        = cong₂ _∧_
 
213
          ; ∧-cong        = P.cong₂ _∧_
212
214
          ; absorptive    = absorptive
213
215
          }
214
216
      ; ∨-∧-distribʳ = proj₂ distrib-∨-∧
215
217
      }
216
218
  ; ∨-complementʳ = proj₂ not-∨-inverse
217
219
  ; ∧-complementʳ = proj₂ not-∧-inverse
218
 
  ; ¬-cong        = cong not
 
220
  ; ¬-cong        = P.cong not
219
221
  }
220
222
 
221
223
booleanAlgebra : BooleanAlgebra _ _
235
237
 
236
238
  xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
237
239
  xor-is-ok true  y = refl
238
 
  xor-is-ok false y = sym $ proj₂ CS.*-identity _
 
240
  xor-is-ok false y = P.sym $ proj₂ CS.*-identity _
239
241
    where module CS = CommutativeSemiring commutativeSemiring-∨-∧
240
242
 
241
243
commutativeRing-xor-∧ : CommutativeRing _ _
267
269
 
268
270
⇔→≡ : {b₁ b₂ b : Bool} → b₁ ≡ b ⇔ b₂ ≡ b → b₁ ≡ b₂
269
271
⇔→≡ {true } {true }         hyp = refl
270
 
⇔→≡ {true } {false} {true } hyp = sym (Equivalent.to hyp ⟨$⟩ refl)
271
 
⇔→≡ {true } {false} {false} hyp = Equivalent.from hyp ⟨$⟩ refl
272
 
⇔→≡ {false} {true } {true } hyp = Equivalent.from hyp ⟨$⟩ refl
273
 
⇔→≡ {false} {true } {false} hyp = sym (Equivalent.to hyp ⟨$⟩ refl)
 
272
⇔→≡ {true } {false} {true } hyp = P.sym (Equivalence.to hyp ⟨$⟩ refl)
 
273
⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp ⟨$⟩ refl
 
274
⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp ⟨$⟩ refl
 
275
⇔→≡ {false} {true } {false} hyp = P.sym (Equivalence.to hyp ⟨$⟩ refl)
274
276
⇔→≡ {false} {false}         hyp = refl
275
277
 
276
278
T-≡ : ∀ {b} → T b ⇔ b ≡ true
277
 
T-≡ {false} = equivalent (λ ())       (λ ())
278
 
T-≡ {true}  = equivalent (const refl) (const _)
 
279
T-≡ {false} = equivalence (λ ())       (λ ())
 
280
T-≡ {true}  = equivalence (const refl) (const _)
279
281
 
280
282
T-∧ : ∀ {b₁ b₂} → T (b₁ ∧ b₂) ⇔ (T b₁ × T b₂)
281
 
T-∧ {true}  {true}  = equivalent (const (_ , _)) (const _)
282
 
T-∧ {true}  {false} = equivalent (λ ())          proj₂
283
 
T-∧ {false} {_}     = equivalent (λ ())          proj₁
 
283
T-∧ {true}  {true}  = equivalence (const (_ , _)) (const _)
 
284
T-∧ {true}  {false} = equivalence (λ ())          proj₂
 
285
T-∧ {false} {_}     = equivalence (λ ())          proj₁
284
286
 
285
287
T-∨ : ∀ {b₁ b₂} → T (b₁ ∨ b₂) ⇔ (T b₁ ⊎ T b₂)
286
 
T-∨ {true}  {b₂}    = equivalent inj₁ (const _)
287
 
T-∨ {false} {true}  = equivalent inj₂ (const _)
288
 
T-∨ {false} {false} = equivalent inj₁ [ id , id ]
 
288
T-∨ {true}  {b₂}    = equivalence inj₁ (const _)
 
289
T-∨ {false} {true}  = equivalence inj₂ (const _)
 
290
T-∨ {false} {false} = equivalence inj₁ [ id , id ]
289
291
 
290
292
proof-irrelevance : ∀ {b} (p q : T b) → p ≡ q
291
293
proof-irrelevance {true}  _  _  = refl