← Back to branch summary

~ubuntu-branches/ubuntu/vivid/agda-stdlib/vivid

« back to all changes in this revision

Viewing changes to src/Relation/Binary/Vec/Pointwise.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (1.1.3)
  • Revision ID: package-import@ubuntu.com-20111129170035-00v3pq4mmhoo5ulf
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/Relation/Binary/Vec/Pointwise.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Pointwise lifting of relations to vectors
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
module Relation.Binary.Vec.Pointwise where
8
8
 
9
9
open import Category.Applicative.Indexed
10
10
open import Data.Fin
 
11
open import Data.Nat
11
12
open import Data.Plus as Plus hiding (equivalent; map)
12
13
open import Data.Vec as Vec hiding ([_]; map)
13
14
import Data.Vec.Properties as VecProp
14
15
open import Function
15
16
open import Function.Equality using (_⟨$⟩_)
16
17
open import Function.Equivalence as Equiv
17
 
  using (_⇔_; module Equivalent)
18
 
open import Level
 
18
  using (_⇔_; module Equivalence)
 
19
import Level
19
20
open import Relation.Binary
20
21
open import Relation.Binary.PropositionalEquality as P using (_≡_)
21
22
open import Relation.Nullary
44
45
 
45
46
  equivalent : ∀ {_∼_ : Rel A a} {n} {xs ys : Vec A n} →
46
47
               Pointwise _∼_ xs ys ⇔ Pointwise′ _∼_ xs ys
47
 
  equivalent {_∼_} = Equiv.equivalent (to _ _) from
 
48
  equivalent {_∼_} = Equiv.equivalence (to _ _) from
48
49
    where
49
50
    to : ∀ {n} (xs ys : Vec A n) →
50
51
         Pointwise _∼_ xs ys → Pointwise′ _∼_ xs ys
104
105
  Pointwise-≡ : ∀ {n} {xs ys : Vec A n} →
105
106
                Pointwise _≡_ xs ys ⇔ xs ≡ ys
106
107
  Pointwise-≡ =
107
 
    Equiv.equivalent
108
 
      (to ∘ _⟨$⟩_ (Equivalent.to equivalent))
 
108
    Equiv.equivalence
 
109
      (to ∘ _⟨$⟩_ (Equivalence.to equivalent))
109
110
      (λ xs≡ys → P.subst (Pointwise _≡_ _) xs≡ys (refl P.refl))
110
111
    where
111
112
    to : ∀ {n} {xs ys : Vec A n} → Pointwise′ _≡_ xs ys → xs ≡ ys
126
127
          Reflexive _∼_ →
127
128
          Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys
128
129
  ∙⁺⇒⁺∙ {_∼_} x∼x =
129
 
    Plus.map (_⟨$⟩_ (Equivalent.from equivalent)) ∘
 
130
    Plus.map (_⟨$⟩_ (Equivalence.from equivalent)) ∘
130
131
    helper ∘
131
 
    _⟨$⟩_ (Equivalent.to equivalent)
 
132
    _⟨$⟩_ (Equivalence.to equivalent)
132
133
    where
133
134
    helper : ∀ {n} {xs ys : Vec A n} →
134
135
             Pointwise′ (Plus _∼_) xs ys → Plus (Pointwise′ _∼_) xs ys
139
140
      y ∷ ys  ∎
140
141
      where
141
142
      xs∼xs : Pointwise′ _∼_ xs xs
142
 
      xs∼xs = Equivalent.to equivalent ⟨$⟩ refl x∼x
 
143
      xs∼xs = Equivalence.to equivalent ⟨$⟩ refl x∼x
143
144
 
144
145
open Dummy public
145
146
 
153
154
  data D : Set where
154
155
    i j x y z : D
155
156
 
156
 
  data _R_ : Rel D zero where
 
157
  data _R_ : Rel D Level.zero where
157
158
    iRj : i R j
158
159
    xRy : x R y
159
160
    yRz : y R z
164
165
    y  ∼⁺⟨ [ yRz ] ⟩∎
165
166
    z  ∎
166
167
 
 
168
  ix : Vec D 2
167
169
  ix = i ∷ x ∷ []
 
170
 
 
171
  jz : Vec D 2
168
172
  jz = j ∷ z ∷ []
169
173
 
170
174
  ix∙⁺jz : Pointwise′ (Plus _R_) ix jz
180
184
         Pointwise (Plus _R_) xs ys →
181
185
         Plus (Pointwise _R_) xs ys)
182
186
  counterexample ∙⁺⇒⁺∙ =
183
 
    ¬ix⁺∙jz (Equivalent.to Plus.equivalent ⟨$⟩
184
 
               Plus.map (_⟨$⟩_ (Equivalent.to equivalent))
185
 
                 (∙⁺⇒⁺∙ (Equivalent.from equivalent ⟨$⟩ ix∙⁺jz)))
 
187
    ¬ix⁺∙jz (Equivalence.to Plus.equivalent ⟨$⟩
 
188
               Plus.map (_⟨$⟩_ (Equivalence.to equivalent))
 
189
                 (∙⁺⇒⁺∙ (Equivalence.from equivalent ⟨$⟩ ix∙⁺jz)))
186
190
 
187
191
-- Map.
188
192