8
8
module Data.Fin.Props where
10
11
open import Data.Fin
11
12
open import Data.Nat as N
12
using (ℕ; zero; suc; s≤s; z≤n)
13
using (ℕ; zero; suc; s≤s; z≤n; _∸_)
13
14
renaming (_≤_ to _ℕ≤_; _<_ to _ℕ<_; _+_ to _ℕ+_)
15
15
import Data.Nat.Properties as N
16
open import Data.Product
16
17
open import Function
17
18
open import Function.Equality as FunS using (_⟨$⟩_)
18
19
open import Function.Injection
19
20
using (Injection; module Injection)
21
open import Algebra.FunctionProperties
20
22
open import Relation.Nullary
21
23
open import Relation.Binary
22
open import Relation.Binary.PropositionalEquality as PropEq
24
open import Relation.Binary.PropositionalEquality as P
23
25
using (_≡_; refl; cong; subst)
24
26
open import Category.Functor
25
27
open import Category.Applicative
31
drop-suc : ∀ {o} {m n : Fin o} →
32
suc m ≡ (suc n ∶ Fin (suc o)) → m ≡ n
33
drop-suc : ∀ {o} {m n : Fin o} → Fin.suc m ≡ suc n → m ≡ n
33
34
drop-suc refl = refl
35
36
preorder : ℕ → Preorder _ _ _
36
preorder n = PropEq.preorder (Fin n)
37
preorder n = P.preorder (Fin n)
38
39
setoid : ℕ → Setoid _ _
39
setoid n = PropEq.setoid (Fin n)
40
setoid n = P.setoid (Fin n)
41
42
strictTotalOrder : ℕ → StrictTotalOrder _ _ _
42
43
strictTotalOrder n = record
72
73
to-from zero = refl
73
74
to-from (suc n) = cong suc (to-from n)
76
toℕ-injective : ∀ {n} {i j : Fin n} → toℕ i ≡ toℕ j → i ≡ j
77
toℕ-injective {zero} {} {} _
78
toℕ-injective {suc n} {zero} {zero} eq = refl
79
toℕ-injective {suc n} {zero} {suc j} ()
80
toℕ-injective {suc n} {suc i} {zero} ()
81
toℕ-injective {suc n} {suc i} {suc j} eq =
82
cong suc (toℕ-injective (cong N.pred eq))
75
84
bounded : ∀ {n} (i : Fin n) → toℕ i ℕ< n
76
85
bounded zero = s≤s z≤n
77
86
bounded (suc i) = s≤s (bounded i)
145
156
reverse {zero} ()
146
157
reverse {suc n} i = inject≤ (n ℕ- i) (N.n∸m≤n (toℕ i) (suc n))
159
reverse-prop : ∀ {n} → (i : Fin n) → toℕ (reverse i) ≡ n ∸ suc (toℕ i)
160
reverse-prop {zero} ()
161
reverse-prop {suc n} i = begin
162
toℕ (inject≤ (n ℕ- i) _) ≡⟨ inject≤-lemma _ _ ⟩
163
toℕ (n ℕ- i) ≡⟨ toℕ‿ℕ- n i ⟩
168
toℕ‿ℕ- : ∀ n i → toℕ (n ℕ- i) ≡ n ∸ toℕ i
169
toℕ‿ℕ- n zero = to-from n
171
toℕ‿ℕ- (suc n) (suc i) = toℕ‿ℕ- n i
173
reverse-involutive : ∀ {n} → Involutive _≡_ reverse
174
reverse-involutive {n} i = toℕ-injective (begin
175
toℕ (reverse (reverse i)) ≡⟨ reverse-prop _ ⟩
176
n ∸ suc (toℕ (reverse i)) ≡⟨ eq ⟩
180
open CommutativeSemiring N.commutativeSemiring using (+-comm)
182
lem₁ : ∀ m n → (m ℕ+ n) ∸ (m ℕ+ n ∸ m) ≡ m
184
m ℕ+ n ∸ (m ℕ+ n ∸ m) ≡⟨ cong (λ ξ → m ℕ+ n ∸ (ξ ∸ m)) (+-comm m n) ⟩
185
m ℕ+ n ∸ (n ℕ+ m ∸ m) ≡⟨ cong (λ ξ → m ℕ+ n ∸ ξ) (N.m+n∸n≡m n m) ⟩
186
m ℕ+ n ∸ n ≡⟨ N.m+n∸n≡m m n ⟩
189
lem₂ : ∀ n → (i : Fin n) → n ∸ suc (n ∸ suc (toℕ i)) ≡ toℕ i
191
lem₂ (suc n) i = begin
192
n ∸ (n ∸ toℕ i) ≡⟨ cong (λ ξ → ξ ∸ (ξ ∸ toℕ i)) i+j≡k ⟩
193
(toℕ i ℕ+ j) ∸ (toℕ i ℕ+ j ∸ toℕ i) ≡⟨ lem₁ (toℕ i) j ⟩
196
decompose-n : ∃ λ j → n ≡ toℕ i ℕ+ j
197
decompose-n = n ∸ toℕ i , P.sym (N.m+n∸m≡n (prop-toℕ-≤ i))
199
j = proj₁ decompose-n
200
i+j≡k = proj₂ decompose-n
202
eq : n ∸ suc (toℕ (reverse i)) ≡ toℕ i
204
n ∸ suc (toℕ (reverse i)) ≡⟨ cong (λ ξ → n ∸ suc ξ) (reverse-prop i) ⟩
205
n ∸ suc (n ∸ suc (toℕ i)) ≡⟨ lem₂ n i ⟩
148
208
-- If there is an injection from a set to a finite set, then equality
149
209
-- of the set can be decided.
151
211
eq? : ∀ {s₁ s₂ n} {S : Setoid s₁ s₂} →
152
Injection S (PropEq.setoid (Fin n)) → Decidable (Setoid._≈_ S)
212
Injection S (P.setoid (Fin n)) → Decidable (Setoid._≈_ S)
153
213
eq? inj x y with to ⟨$⟩ x ≟ to ⟨$⟩ y where open Injection inj
154
214
... | yes tox≡toy = yes (Injection.injective inj tox≡toy)
155
215
... | no tox≢toy = no (tox≢toy ∘ FunS.cong (Injection.to inj))
added
removed
src/Data/Fin/Props.agda
