← Back to branch summary

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

« back to all changes in this revision

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

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Tags: upstream-0.3
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Relation/Binary/List/Pointwise.agda
 
1
------------------------------------------------------------------------
 
2
-- Pointwise lifting of relations to lists
 
3
------------------------------------------------------------------------
 
4
 
 
5
module Relation.Binary.List.Pointwise where
 
6
 
 
7
open import Data.Function
 
8
open import Data.Product
 
9
open import Data.List
 
10
open import Level
 
11
open import Relation.Nullary
 
12
open import Relation.Binary renaming (Rel to Rel₂)
 
13
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
 
14
 
 
15
private
 
16
 module Dummy {A : Set} where
 
17
 
 
18
  infixr 5 _∷_
 
19
 
 
20
  data Rel (_∼_ : Rel₂ A zero) : List A → List A → Set where
 
21
    []  : Rel _∼_ [] []
 
22
    _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Rel _∼_ xs ys) →
 
23
          Rel _∼_ (x ∷ xs) (y ∷ ys)
 
24
 
 
25
  head : ∀ {_∼_ x y xs ys} → Rel _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
 
26
  head (x∼y ∷ xs∼ys) = x∼y
 
27
 
 
28
  tail : ∀ {_∼_ x y xs ys} → Rel _∼_ (x ∷ xs) (y ∷ ys) → Rel _∼_ xs ys
 
29
  tail (x∼y ∷ xs∼ys) = xs∼ys
 
30
 
 
31
  reflexive : ∀ {≈ ∼} → ≈ ⇒ ∼ → (Rel ≈) ⇒ (Rel ∼)
 
32
  reflexive ≈⇒∼ []            = []
 
33
  reflexive ≈⇒∼ (x≈y ∷ xs≈ys) = ≈⇒∼ x≈y ∷ reflexive ≈⇒∼ xs≈ys
 
34
 
 
35
  refl : ∀ {∼} → Reflexive ∼ → Reflexive (Rel ∼)
 
36
  refl rfl {[]}     = []
 
37
  refl rfl {x ∷ xs} = rfl ∷ refl rfl
 
38
 
 
39
  symmetric : ∀ {∼} → Symmetric ∼ → Symmetric (Rel ∼)
 
40
  symmetric sym []            = []
 
41
  symmetric sym (x∼y ∷ xs∼ys) = sym x∼y ∷ symmetric sym xs∼ys
 
42
 
 
43
  transitive : ∀ {∼} → Transitive ∼ → Transitive (Rel ∼)
 
44
  transitive trans []            []            = []
 
45
  transitive trans (x∼y ∷ xs∼ys) (y∼z ∷ ys∼zs) =
 
46
    trans x∼y y∼z ∷ transitive trans xs∼ys ys∼zs
 
47
 
 
48
  antisymmetric : ∀ {≈ ≤} → Antisymmetric ≈ ≤ →
 
49
                  Antisymmetric (Rel ≈) (Rel ≤)
 
50
  antisymmetric antisym []            []            = []
 
51
  antisymmetric antisym (x∼y ∷ xs∼ys) (y∼x ∷ ys∼xs) =
 
52
    antisym x∼y y∼x ∷ antisymmetric antisym xs∼ys ys∼xs
 
53
 
 
54
  respects₂ : ∀ {≈ ∼} → ∼ Respects₂ ≈ → (Rel ∼) Respects₂ (Rel ≈)
 
55
  respects₂ {≈} {∼} resp =
 
56
    (λ {xs} {ys} {zs} → resp¹ {xs} {ys} {zs}) ,
 
57
    (λ {xs} {ys} {zs} → resp² {xs} {ys} {zs})
 
58
    where
 
59
    resp¹ : ∀ {xs} → (Rel ∼ xs) Respects (Rel ≈)
 
60
    resp¹ []            []            = []
 
61
    resp¹ (x≈y ∷ xs≈ys) (z∼x ∷ zs∼xs) =
 
62
      proj₁ resp x≈y z∼x ∷ resp¹ xs≈ys zs∼xs
 
63
 
 
64
    resp² : ∀ {ys} → (flip (Rel ∼) ys) Respects (Rel ≈)
 
65
    resp² []            []            = []
 
66
    resp² (x≈y ∷ xs≈ys) (x∼z ∷ xs∼zs) =
 
67
      proj₂ resp x≈y x∼z ∷ resp² xs≈ys xs∼zs
 
68
 
 
69
  decidable : ∀ {∼} → Decidable ∼ → Decidable (Rel ∼)
 
70
  decidable dec []       []       = yes []
 
71
  decidable dec []       (y ∷ ys) = no (λ ())
 
72
  decidable dec (x ∷ xs) []       = no (λ ())
 
73
  decidable dec (x ∷ xs) (y ∷ ys) with dec x y
 
74
  ... | no ¬x∼y = no (¬x∼y ∘ head)
 
75
  ... | yes x∼y with decidable dec xs ys
 
76
  ...           | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
 
77
  ...           | yes xs∼ys = yes (x∼y ∷ xs∼ys)
 
78
 
 
79
  isEquivalence : ∀ {≈} → IsEquivalence ≈ → IsEquivalence (Rel ≈)
 
80
  isEquivalence eq = record
 
81
    { refl  = refl       Eq.refl
 
82
    ; sym   = symmetric  Eq.sym
 
83
    ; trans = transitive Eq.trans
 
84
    } where module Eq = IsEquivalence eq
 
85
 
 
86
  isPreorder : ∀ {≈ ∼} → IsPreorder ≈ ∼ → IsPreorder (Rel ≈) (Rel ∼)
 
87
  isPreorder pre = record
 
88
    { isEquivalence = isEquivalence Pre.isEquivalence
 
89
    ; reflexive     = reflexive     Pre.reflexive
 
90
    ; trans         = transitive    Pre.trans
 
91
    ; ∼-resp-≈      = respects₂     Pre.∼-resp-≈
 
92
    } where module Pre = IsPreorder pre
 
93
 
 
94
  isDecEquivalence : ∀ {≈} → IsDecEquivalence ≈ →
 
95
                     IsDecEquivalence (Rel ≈)
 
96
  isDecEquivalence eq = record
 
97
    { isEquivalence = isEquivalence Dec.isEquivalence
 
98
    ; _≟_           = decidable     Dec._≟_
 
99
    } where module Dec = IsDecEquivalence eq
 
100
 
 
101
  isPartialOrder : ∀ {≈ ≤} → IsPartialOrder ≈ ≤ →
 
102
                   IsPartialOrder (Rel ≈) (Rel ≤)
 
103
  isPartialOrder po = record
 
104
    { isPreorder = isPreorder    PO.isPreorder
 
105
    ; antisym    = antisymmetric PO.antisym
 
106
    } where module PO = IsPartialOrder po
 
107
 
 
108
  -- Rel _≡_ coincides with _≡_.
 
109
 
 
110
  Rel≡⇒≡ : Rel _≡_ ⇒ _≡_
 
111
  Rel≡⇒≡ []                    = PropEq.refl
 
112
  Rel≡⇒≡ (PropEq.refl ∷ xs∼ys) with Rel≡⇒≡ xs∼ys
 
113
  Rel≡⇒≡ (PropEq.refl ∷ xs∼ys) | PropEq.refl = PropEq.refl
 
114
 
 
115
  ≡⇒Rel≡ : _≡_ ⇒ Rel _≡_
 
116
  ≡⇒Rel≡ PropEq.refl = refl PropEq.refl
 
117
 
 
118
open Dummy public
 
119
 
 
120
preorder : Preorder _ _ _ → Preorder _ _ _
 
121
preorder p = record
 
122
  { isPreorder = isPreorder (Preorder.isPreorder p)
 
123
  }
 
124
 
 
125
setoid : Setoid _ _ → Setoid _ _
 
126
setoid s = record
 
127
  { isEquivalence = isEquivalence (Setoid.isEquivalence s)
 
128
  }
 
129
 
 
130
decSetoid : DecSetoid _ _ → DecSetoid _ _
 
131
decSetoid d = record
 
132
  { isDecEquivalence = isDecEquivalence (DecSetoid.isDecEquivalence d)
 
133
  }
 
134
 
 
135
poset : Poset _ _ _ → Poset _ _ _
 
136
poset p = record
 
137
  { isPartialOrder = isPartialOrder (Poset.isPartialOrder p)
 
138
  }