← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Plus.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Plus.agda
 
1
------------------------------------------------------------------------
 
2
-- Transitive closures
 
3
------------------------------------------------------------------------
 
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
 
7
module Data.Plus where
 
8
 
 
9
open import Function
 
10
open import Function.Equivalence as Equiv using (_⇔_)
 
11
open import Level
 
12
open import Relation.Binary
 
13
 
 
14
------------------------------------------------------------------------
 
15
-- Transitive closure
 
16
 
 
17
infix 4 Plus
 
18
 
 
19
syntax Plus R x y = x [ R ]⁺ y
 
20
 
 
21
data Plus {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
 
22
  [_]     : ∀ {x y} (x∼y : x ∼ y) → x [ _∼_ ]⁺ y
 
23
  _∼⁺⟨_⟩_ : ∀ x {y z} (x∼⁺y : x [ _∼_ ]⁺ y) (y∼⁺z : y [ _∼_ ]⁺ z) →
 
24
            x [ _∼_ ]⁺ z
 
25
 
 
26
-- "Equational" reasoning notation. Example:
 
27
--
 
28
--   lemma =
 
29
--     x  ∼⁺⟨ [ lemma₁ ] ⟩
 
30
--     y  ∼⁺⟨ lemma₂ ⟩∎
 
31
--     z  ∎
 
32
 
 
33
finally : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} x y →
 
34
          x [ _∼_ ]⁺ y → x [ _∼_ ]⁺ y
 
35
finally _ _ = id
 
36
 
 
37
syntax finally x y x∼⁺y = x ∼⁺⟨ x∼⁺y ⟩∎ y ∎
 
38
 
 
39
infixr 2 _∼⁺⟨_⟩_
 
40
infix  2 finally
 
41
 
 
42
-- Map.
 
43
 
 
44
map : ∀ {a a′ ℓ ℓ′} {A : Set a} {A′ : Set a′}
 
45
        {_R_ : Rel A ℓ} {_R′_ : Rel A′ ℓ′} {f : A → A′} →
 
46
      _R_ =[ f ]⇒ _R′_ → Plus _R_ =[ f ]⇒ Plus _R′_
 
47
map R⇒R′ [ xRy ]             = [ R⇒R′ xRy ]
 
48
map R⇒R′ (x ∼⁺⟨ xR⁺z ⟩ zR⁺y) =
 
49
  _ ∼⁺⟨ map R⇒R′ xR⁺z ⟩ map R⇒R′ zR⁺y
 
50
 
 
51
------------------------------------------------------------------------
 
52
-- Alternative definition of transitive closure
 
53
 
 
54
-- A generalisation of Data.List.Nonempty.List⁺.
 
55
 
 
56
infixr 5 _∷_ _++_
 
57
infix  4 Plus′
 
58
 
 
59
syntax Plus′ R x y = x ⟨ R ⟩⁺ y
 
60
 
 
61
data Plus′ {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
 
62
  [_] : ∀ {x y} (x∼y : x ∼ y) → x ⟨ _∼_ ⟩⁺ y
 
63
  _∷_ : ∀ {x y z} (x∼y : x ∼ y) (y∼⁺z : y ⟨ _∼_ ⟩⁺ z) → x ⟨ _∼_ ⟩⁺ z
 
64
 
 
65
-- Transitivity.
 
66
 
 
67
_++_ : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} {x y z} →
 
68
       x ⟨ _∼_ ⟩⁺ y → y ⟨ _∼_ ⟩⁺ z → x ⟨ _∼_ ⟩⁺ z
 
69
[ x∼y ]      ++ y∼⁺z = x∼y ∷ y∼⁺z
 
70
(x∼y ∷ y∼⁺z) ++ z∼⁺u = x∼y ∷ (y∼⁺z ++ z∼⁺u)
 
71
 
 
72
-- Plus and Plus′ are equivalent.
 
73
 
 
74
equivalent : ∀ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} {x y} →
 
75
             Plus _∼_ x y ⇔ Plus′ _∼_ x y
 
76
equivalent {_∼_ = _∼_} = Equiv.equivalent complete sound
 
77
  where
 
78
  complete : Plus _∼_ ⇒ Plus′ _∼_
 
79
  complete [ x∼y ]             = [ x∼y ]
 
80
  complete (x ∼⁺⟨ x∼⁺y ⟩ y∼⁺z) = complete x∼⁺y ++ complete y∼⁺z
 
81
 
 
82
  sound : Plus′ _∼_ ⇒ Plus _∼_
 
83
  sound [ x∼y ]      = [ x∼y ]
 
84
  sound (x∼y ∷ y∼⁺z) = _ ∼⁺⟨ [ x∼y ] ⟩ sound y∼⁺z