← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Relation/Binary/List/Pointwise.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/Relation/Binary/List/Pointwise.agda
7
7
module Relation.Binary.List.Pointwise where
8
8
 
9
9
open import Function
 
10
open import Function.Inverse using (Inverse)
10
11
open import Data.Product hiding (map)
11
12
open import Data.List hiding (map)
12
13
open import Level
13
14
open import Relation.Nullary
 
15
import Relation.Nullary.Decidable as Dec using (map′)
14
16
open import Relation.Binary renaming (Rel to Rel₂)
15
 
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 
17
open import Relation.Binary.PropositionalEquality as P using (_≡_)
16
18
 
17
19
infixr 5 _∷_
18
20
 
127
129
                     {_≈_ : Rel₂ A ℓ} → IsDecEquivalence _≈_ →
128
130
                   IsDecEquivalence (Rel _≈_)
129
131
isDecEquivalence eq = record
130
 
  { isEquivalence = isEquivalence Dec.isEquivalence
131
 
  ; _≟_           = decidable     Dec._≟_
132
 
  } where module Dec = IsDecEquivalence eq
 
132
  { isEquivalence = isEquivalence DE.isEquivalence
 
133
  ; _≟_           = decidable     DE._≟_
 
134
  } where module DE = IsDecEquivalence eq
133
135
 
134
136
isPartialOrder : ∀ {a ℓ₁ ℓ₂} {A : Set a}
135
137
                   {_≈_ : Rel₂ A ℓ₁} {_≤_ : Rel₂ A ℓ₂} →
140
142
  ; antisym    = antisymmetric PO.antisym
141
143
  } where module PO = IsPartialOrder po
142
144
 
143
 
 
144
 
Rel≡⇒≡ : ∀ {a} {A : Set a} → Rel {A = A} _≡_ ⇒ _≡_
145
 
Rel≡⇒≡ []                    = PropEq.refl
146
 
Rel≡⇒≡ (PropEq.refl ∷ xs∼ys) with Rel≡⇒≡ xs∼ys
147
 
Rel≡⇒≡ (PropEq.refl ∷ xs∼ys) | PropEq.refl = PropEq.refl
148
 
 
149
 
≡⇒Rel≡ : ∀ {a} {A : Set a} → _≡_ ⇒ Rel {A = A} _≡_
150
 
≡⇒Rel≡ PropEq.refl = refl PropEq.refl
151
 
 
152
145
preorder : ∀ {p₁ p₂ p₃} → Preorder p₁ p₂ p₃ → Preorder _ _ _
153
146
preorder p = record
154
147
  { isPreorder = isPreorder (Preorder.isPreorder p)
169
161
poset p = record
170
162
  { isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
171
163
  }
 
164
 
 
165
-- Rel _≡_ coincides with _≡_.
 
166
 
 
167
Rel≡⇒≡ : ∀ {a} {A : Set a} → Rel {A = A} _≡_ ⇒ _≡_
 
168
Rel≡⇒≡ []               = P.refl
 
169
Rel≡⇒≡ (P.refl ∷ xs∼ys) with Rel≡⇒≡ xs∼ys
 
170
Rel≡⇒≡ (P.refl ∷ xs∼ys) | P.refl = P.refl
 
171
 
 
172
≡⇒Rel≡ : ∀ {a} {A : Set a} → _≡_ ⇒ Rel {A = A} _≡_
 
173
≡⇒Rel≡ P.refl = refl P.refl
 
174
 
 
175
Rel↔≡ : ∀ {a} {A : Set a} →
 
176
        Inverse (setoid (P.setoid A)) (P.setoid (List A))
 
177
Rel↔≡ = record
 
178
  { to         = record { _⟨$⟩_ = id; cong = Rel≡⇒≡ }
 
179
  ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Rel≡ }
 
180
  ; inverse-of = record
 
181
    { left-inverse-of  = λ _ → refl P.refl
 
182
    ; right-inverse-of = λ _ → P.refl
 
183
    }
 
184
  }
 
185
 
 
186
decidable-≡ : ∀ {a} {A : Set a} →
 
187
              Decidable {A = A} _≡_ → Decidable {A = List A} _≡_
 
188
decidable-≡ dec xs ys = Dec.map′ Rel≡⇒≡ ≡⇒Rel≡ (xs ≟ ys)
 
189
  where
 
190
  open DecSetoid (decSetoid (P.decSetoid dec))