← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Vec/Equality.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/Vec/Equality.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Semi-heterogeneous vector equality
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
module Data.Vec.Equality where
8
8
 
9
9
open import Data.Vec
10
10
open import Data.Nat using (suc)
11
11
open import Function
12
 
open import Level
 
12
open import Level using (_⊔_)
13
13
open import Relation.Binary
14
 
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 
14
open import Relation.Binary.PropositionalEquality as P using (_≡_)
15
15
 
16
16
module Equality {s₁ s₂} (S : Setoid s₁ s₂) where
17
17
 
32
32
  length-equal : ∀ {n¹} {xs¹ : Vec A n¹}
33
33
                   {n²} {xs² : Vec A n²} →
34
34
                 xs¹ ≈ xs² → n¹ ≡ n²
35
 
  length-equal []-cong        = PropEq.refl
36
 
  length-equal (_ ∷-cong eq₂) = PropEq.cong suc $ length-equal eq₂
 
35
  length-equal []-cong        = P.refl
 
36
  length-equal (_ ∷-cong eq₂) = P.cong suc $ length-equal eq₂
37
37
 
38
38
  refl : ∀ {n} (xs : Vec A n) → xs ≈ xs
39
39
  refl []       = []-cong
79
79
    helper : ¬ (x ∷ xs ≈ y ∷ ys)
80
80
    helper (x≊y ∷-cong _) = ¬x≊y x≊y
81
81
 
82
 
module HeterogeneousEquality {a} {A : Set a} where
83
 
 
84
 
  open import Relation.Binary.HeterogeneousEquality as HetEq
85
 
    using (_≅_)
86
 
  open Equality (PropEq.setoid A)
87
 
 
88
 
  to-≅ : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
89
 
         xs ≈ ys → xs ≅ ys
90
 
  to-≅ []-cong                      = HetEq.refl
91
 
  to-≅ (PropEq.refl ∷-cong xs¹≈xs²) with length-equal xs¹≈xs²
92
 
  ... | PropEq.refl = HetEq.cong (_∷_ _) $ to-≅ xs¹≈xs²
93
 
 
94
 
  from-≅ : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
95
 
           xs ≅ ys → xs ≈ ys
96
 
  from-≅ {xs = []}     {ys = []}       _          = refl _
97
 
  from-≅ {xs = x ∷ xs} {ys = .x ∷ .xs} HetEq.refl = refl _
98
 
  from-≅ {xs = _ ∷ _}  {ys = []}       ()
99
 
  from-≅ {xs = []}     {ys = _ ∷ _}    ()
 
82
module PropositionalEquality {a} {A : Set a} where
 
83
 
 
84
  open Equality (P.setoid A)
 
85
 
 
86
  to-≡ : ∀ {n} {xs ys : Vec A n} → xs ≈ ys → xs ≡ ys
 
87
  to-≡ []-cong                 = P.refl
 
88
  to-≡ (P.refl ∷-cong xs¹≈xs²) = P.cong (_∷_ _) $ to-≡ xs¹≈xs²
 
89
 
 
90
  from-≡ : ∀ {n} {xs ys : Vec A n} → xs ≡ ys → xs ≈ ys
 
91
  from-≡ P.refl = refl _