← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Fin/Dec.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/Fin/Dec.agda
6
6
 
7
7
module Data.Fin.Dec where
8
8
 
9
 
open import Data.Function
 
9
open import Function
 
10
import Data.Bool as Bool
10
11
open import Data.Nat hiding (_<_)
11
12
open import Data.Vec hiding (_∈_)
 
13
open import Data.Vec.Equality as VecEq
 
14
  using () renaming (module HeterogeneousEquality to HetVecEq)
12
15
open import Data.Fin
13
16
open import Data.Fin.Subset
14
17
open import Data.Fin.Subset.Props
15
18
open import Data.Product as Prod
16
19
open import Data.Empty
 
20
open import Function
 
21
import Function.Equivalence as Eq
17
22
open import Level hiding (Lift)
 
23
open import Relation.Binary
 
24
import Relation.Binary.HeterogeneousEquality as H
18
25
open import Relation.Nullary
 
26
import Relation.Nullary.Decidable as Dec
19
27
open import Relation.Unary using (Pred)
20
28
 
21
29
infix 4 _∈?_
40
48
any? : ∀ {n} {P : Fin n → Set} →
41
49
       ((f : Fin n) → Dec (P f)) →
42
50
       Dec (∃ P)
43
 
any? {zero}  {P} dec = no ((¬ Fin 0 ∶ λ()) ∘ proj₁)
 
51
any? {zero}  {P} dec = no (((λ()) ∶ ¬ Fin 0) ∘ proj₁)
44
52
any? {suc n} {P} dec with dec zero | any? (restrict dec)
45
53
...                  | yes p | _            = yes (_ , p)
46
54
...                  | _     | yes (_ , p') = yes (_ , p')
92
100
all? : ∀ {n} {P : Fin n → Set} →
93
101
       (∀ f → Dec (P f)) →
94
102
       Dec (∀ f → P f)
95
 
all? dec with all∈? {q = all inside} (λ {f} _ → dec f)
96
 
...      | yes ∀p = yes (λ f → ∀p (allInside f))
 
103
all? dec with all∈? {q = ⊤} (λ {f} _ → dec f)
 
104
...      | yes ∀p = yes (λ f → ∀p ∈⊤)
97
105
...      | no ¬∀p = no  (λ ∀p → ¬∀p (λ {f} _ → ∀p f))
98
106
 
99
107
decLift : ∀ {n} {P : Fin n → Set} →
153
161
            ((j : Fin′ (suc i)) → P (inject j))
154
162
  extend′ g zero    = P0
155
163
  extend′ g (suc j) = g j
 
164
 
 
165
-- Decision procedure for _⊆_ (obtained via the natural lattice
 
166
-- order).
 
167
 
 
168
infix 4 _⊆?_
 
169
 
 
170
_⊆?_ : ∀ {n} → Decidable (_⊆_ {n = n})
 
171
p₁ ⊆? p₂ =
 
172
  Dec.map (Eq.sym NaturalPoset.orders-equivalent) $
 
173
  Dec.map′ H.≅-to-≡ H.≡-to-≅ $
 
174
  Dec.map′ HetVecEq.to-≅ HetVecEq.from-≅ $
 
175
  VecEq.DecidableEquality._≟_ Bool.decSetoid p₁ (p₁ ∩ p₂)