← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

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

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/List/Properties.agda
19
19
open import Data.Nat.Properties
20
20
open import Data.Product as Prod hiding (map)
21
21
open import Function
 
22
import Algebra.FunctionProperties
22
23
import Relation.Binary.EqReasoning as EqR
23
24
open import Relation.Binary.PropositionalEquality as P
24
25
  using (_≡_; _≢_; _≗_; refl)
27
28
open import Relation.Unary using (Decidable)
28
29
 
29
30
private
 
31
  open module FP {a} {A : Set a} =
 
32
    Algebra.FunctionProperties (_≡_ {A = A})
30
33
  open module LMP {ℓ} = RawMonadPlus (List.monadPlus {ℓ = ℓ})
31
34
  module LM {a} {A : Set a} = Monoid (List.monoid A)
32
35
 
33
 
∷-injective : ∀ {a} {A : Set a} {x y xs ys} →
34
 
              (x ∷ xs ∶ List A) ≡ y ∷ ys → x ≡ y × xs ≡ ys
 
36
∷-injective : ∀ {a} {A : Set a} {x y : A} {xs ys} →
 
37
              x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys
35
38
∷-injective refl = (refl , refl)
36
39
 
37
 
∷ʳ-injective : ∀ {a} {A : Set a} {x y} xs ys →
38
 
               (xs ∷ʳ x ∶ List A) ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
 
40
∷ʳ-injective : ∀ {a} {A : Set a} {x y : A} xs ys →
 
41
               xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
39
42
∷ʳ-injective []          []          refl = (refl , refl)
40
43
∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with ∷-injective eq
41
44
∷ʳ-injective (x ∷ xs)    (.x ∷ ys)   eq   | (refl , eq′) =
339
342
  reverse ys ++ reverse (x ∷ xs)       ∎
340
343
  where open P.≡-Reasoning
341
344
 
 
345
reverse-map-commute :
 
346
  ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → (xs : List A) →
 
347
  map f (reverse xs) ≡ reverse (map f xs)
 
348
reverse-map-commute f []       = refl
 
349
reverse-map-commute f (x ∷ xs) = begin
 
350
  map f (reverse (x ∷ xs))   ≡⟨ P.cong (map f) $ unfold-reverse x xs ⟩
 
351
  map f (reverse xs ∷ʳ x)    ≡⟨ map-++-commute f (reverse xs) ([ x ]) ⟩
 
352
  map f (reverse xs) ∷ʳ f x  ≡⟨ P.cong (λ y → y ∷ʳ f x) $ reverse-map-commute f xs ⟩
 
353
  reverse (map f xs) ∷ʳ f x  ≡⟨ P.sym $ unfold-reverse (f x) (map f xs) ⟩
 
354
  reverse (map f (x ∷ xs))   ∎
 
355
  where open P.≡-Reasoning
 
356
 
 
357
reverse-involutive : ∀ {a} {A : Set a} → Involutive (reverse {A = A})
 
358
reverse-involutive [] = refl
 
359
reverse-involutive (x ∷ xs) = begin
 
360
  reverse (reverse (x ∷ xs))   ≡⟨ P.cong reverse $ unfold-reverse x xs ⟩
 
361
  reverse (reverse xs ∷ʳ x)    ≡⟨ reverse-++-commute (reverse xs) ([ x ]) ⟩
 
362
  x ∷ reverse (reverse (xs))   ≡⟨ P.cong (λ y → x ∷ y) $ reverse-involutive xs ⟩
 
363
  x ∷ xs                       ∎
 
364
  where open P.≡-Reasoning
 
365
 
342
366
-- The list monad.
343
367
 
344
368
module Monad where
347
371
  left-zero f = refl
348
372
 
349
373
  right-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) →
350
 
               (xs >>= const ∅) ≡ (∅ ∶ List B)
 
374
               (xs >>= const ∅) ≡ ∅ {A = B}
351
375
  right-zero []       = refl
352
376
  right-zero (x ∷ xs) = right-zero xs
353
377
 
410
434
 
411
435
  -- ∅ is a left zero for _⊛_.
412
436
 
413
 
  left-zero : ∀ {ℓ} {A B : Set ℓ} xs → (∅ ∶ List (A → B)) ⊛ xs ≡ ∅
 
437
  left-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) → ∅ ⊛ xs ≡ ∅ {A = B}
414
438
  left-zero xs = begin
415
439
    ∅ ⊛ xs          ≡⟨ refl ⟩
416
440
    (∅ >>= pam xs)  ≡⟨ Monad.left-zero (pam xs) ⟩