← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda-stdlib/wily

« back to all changes in this revision

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

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-05-27 19:29:25 UTC
  • mfrom: (8.1.1 experimental)
  • Revision ID: package-import@ubuntu.com-20130527192925-q2tadfousmn0xeav
Tags: 0.7-2
Upload to unstable 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Vec/Properties.agda
16
16
import Data.Nat.Properties as Nat
17
17
open import Data.Fin as Fin using (Fin; zero; suc; toℕ; fromℕ)
18
18
open import Data.Fin.Props using (_+′_)
 
19
open import Data.Empty using (⊥-elim)
19
20
open import Function
20
21
open import Function.Inverse using (_↔_)
21
22
open import Relation.Binary
118
119
lookup-++-+′ []       (y ∷ xs) (suc i) = lookup-++-+′ [] xs i
119
120
lookup-++-+′ (x ∷ xs) ys       i       = lookup-++-+′ xs ys i
120
121
 
 
122
-- Properties relating lookup and _[_]≔_.
 
123
 
 
124
lookup∘update : ∀ {a} {A : Set a} {n}
 
125
                (i : Fin n) (xs : Vec A n) x →
 
126
                lookup i (xs [ i ]≔ x) ≡ x
 
127
lookup∘update zero    (_ ∷ xs) x = refl
 
128
lookup∘update (suc i) (_ ∷ xs) x = lookup∘update i xs x
 
129
 
 
130
lookup∘update′ : ∀ {a} {A : Set a} {n} {i j : Fin n} →
 
131
                 i ≢ j → ∀ (xs : Vec A n) y →
 
132
                 lookup i (xs [ j ]≔ y) ≡ lookup i xs
 
133
lookup∘update′ {i = zero}  {zero}  i≢j      xs  y = ⊥-elim (i≢j refl)
 
134
lookup∘update′ {i = zero}  {suc j} i≢j (x ∷ xs) y = refl
 
135
lookup∘update′ {i = suc i} {zero}  i≢j (x ∷ xs) y = refl
 
136
lookup∘update′ {i = suc i} {suc j} i≢j (x ∷ xs) y =
 
137
  lookup∘update′ (i≢j ∘ P.cong suc) xs y
 
138
 
121
139
-- map is a congruence.
122
140
 
123
141
map-cong : ∀ {a b n} {A : Set a} {B : Set b} {f g : A → B} →