|
44
|
1 module finiteSet where
|
|
|
2
|
|
69
|
3 open import Data.Nat hiding ( _≟_ )
|
|
44
|
4 open import Data.Fin renaming ( _<_ to _<<_ )
|
|
69
|
5 open import Data.Fin.Properties
|
|
|
6 open import Relation.Nullary
|
|
44
|
7 open import Relation.Binary.Core
|
|
46
|
8 open import Relation.Binary.PropositionalEquality
|
|
69
|
9 open import logic
|
|
44
|
10
|
|
|
11 record FiniteSet ( Q : Set ) { n : ℕ }
|
|
|
12 : Set where
|
|
|
13 field
|
|
|
14 Q←F : Fin n → Q
|
|
|
15 F←Q : Q → Fin n
|
|
|
16 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
|
|
|
17 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
|
|
70
|
18 finℕ : ℕ
|
|
|
19 finℕ = n
|
|
44
|
20 lt0 : (n : ℕ) → n Data.Nat.≤ n
|
|
|
21 lt0 zero = z≤n
|
|
|
22 lt0 (suc n) = s≤s (lt0 n)
|
|
|
23 lt2 : {m n : ℕ} → m < n → m Data.Nat.≤ n
|
|
|
24 lt2 {zero} lt = z≤n
|
|
|
25 lt2 {suc m} {zero} ()
|
|
|
26 lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
|
|
|
27 exists : ( Q → Bool ) → Bool
|
|
|
28 exists p = exists1 n (lt0 n) p where
|
|
|
29 exists1 : (m : ℕ ) → m Data.Nat.≤ n → ( Q → Bool ) → Bool
|
|
|
30 exists1 zero _ _ = false
|
|
69
|
31 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
|
|
|
32 equal? : Q → Q → Bool
|
|
|
33 equal? q0 q1 with F←Q q0 ≟ F←Q q1
|
|
|
34 ... | yes p = true
|
|
|
35 ... | no ¬p = false
|
|
44
|
36
|
|
|
37 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
|
|
|
38 fless zero = s≤s z≤n
|
|
|
39 fless (suc f) = s≤s ( fless f )
|
|
69
|
40
|
