← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to src/Data/Fin/Props.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/Props.agda
13
13
  renaming (_≤_ to _ℕ≤_; _<_ to _ℕ<_; _+_ to _ℕ+_)
14
14
open N.≤-Reasoning
15
15
import Data.Nat.Properties as N
16
 
open import Data.Function
17
 
open import Data.Function.Equality as FunS using (_⟨$⟩_)
18
 
open import Data.Function.Injection
 
16
open import Function
 
17
open import Function.Equality as FunS using (_⟨$⟩_)
 
18
open import Function.Injection
19
19
  using (Injection; module Injection)
20
20
open import Relation.Nullary
21
21
open import Relation.Binary
29
29
 
30
30
private
31
31
  drop-suc : ∀ {o} {m n : Fin o} →
32
 
             suc m ≡ (Fin (suc o) ∶ suc n) → m ≡ n
 
32
             suc m ≡ (suc n ∶ Fin (suc o)) → m ≡ n
33
33
  drop-suc refl = refl
34
34
 
35
35
preorder : ℕ → Preorder _ _ _
95
95
inject-lemma {i = suc i} zero    = refl
96
96
inject-lemma {i = suc i} (suc j) = cong suc (inject-lemma j)
97
97
 
98
 
inject+-lemma : ∀ m k → m ≡ toℕ (inject+ k (fromℕ m))
99
 
inject+-lemma zero    k = refl
100
 
inject+-lemma (suc m) k = cong suc (inject+-lemma m k)
 
98
inject+-lemma : ∀ {m} n (i : Fin m) → toℕ i ≡ toℕ (inject+ n i)
 
99
inject+-lemma n zero    = refl
 
100
inject+-lemma n (suc i) = cong suc (inject+-lemma n i)
101
101
 
102
102
inject₁-lemma : ∀ {m} (i : Fin m) → toℕ (inject₁ i) ≡ toℕ i
103
103
inject₁-lemma zero    = refl
118
118
<′⇒≺ (N.≤′-step m≤′n) | n ≻toℕ i =
119
119
  subst (λ i → i ≺ suc n) (inject₁-lemma i) (suc n ≻toℕ (inject₁ i))
120
120
 
 
121
toℕ-raise : ∀ {m} n (i : Fin m) → toℕ (raise n i) ≡ n ℕ+ toℕ i
 
122
toℕ-raise zero    i = refl
 
123
toℕ-raise (suc n) i = cong suc (toℕ-raise n i)
 
124
 
 
125
fromℕ≤-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i ℕ< m) → fromℕ≤ i<m ≡ i
 
126
fromℕ≤-toℕ zero    (s≤s z≤n)       = refl
 
127
fromℕ≤-toℕ (suc i) (s≤s (s≤s m≤n)) = cong suc (fromℕ≤-toℕ i (s≤s m≤n))
 
128
 
 
129
toℕ-fromℕ≤ : ∀ {m n} (m<n : m ℕ< n) → toℕ (fromℕ≤ m<n) ≡ m
 
130
toℕ-fromℕ≤ (s≤s z≤n)       = refl
 
131
toℕ-fromℕ≤ (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ≤ (s≤s m<n))
 
132
 
121
133
------------------------------------------------------------------------
122
134
-- Operations
123
135