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
|
76
|
6 open import Data.Empty
|
69
|
7 open import Relation.Nullary
|
44
|
8 open import Relation.Binary.Core
|
46
|
9 open import Relation.Binary.PropositionalEquality
|
69
|
10 open import logic
|
78
|
11 open import nat
|
|
12 open import Data.Nat.Properties hiding ( _≟_ )
|
44
|
13
|
79
|
14 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
15
|
|
16
|
44
|
17 record FiniteSet ( Q : Set ) { n : ℕ }
|
|
18 : Set where
|
|
19 field
|
|
20 Q←F : Fin n → Q
|
|
21 F←Q : Q → Fin n
|
|
22 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
|
|
23 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
|
70
|
24 finℕ : ℕ
|
|
25 finℕ = n
|
44
|
26 lt0 : (n : ℕ) → n Data.Nat.≤ n
|
|
27 lt0 zero = z≤n
|
|
28 lt0 (suc n) = s≤s (lt0 n)
|
|
29 lt2 : {m n : ℕ} → m < n → m Data.Nat.≤ n
|
|
30 lt2 {zero} lt = z≤n
|
|
31 lt2 {suc m} {zero} ()
|
|
32 lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
|
76
|
33 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
|
|
34 exists1 zero _ _ = false
|
|
35 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
|
44
|
36 exists : ( Q → Bool ) → Bool
|
76
|
37 exists p = exists1 n (lt0 n) p
|
69
|
38 equal? : Q → Q → Bool
|
|
39 equal? q0 q1 with F←Q q0 ≟ F←Q q1
|
|
40 ... | yes p = true
|
|
41 ... | no ¬p = false
|
76
|
42 not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
|
|
43 not-found {p} pn = not-found2 n (lt0 n) where
|
|
44 not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false
|
|
45 not-found2 zero _ = refl
|
|
46 not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n))
|
|
47 not-found2 (suc m) m<n | eq = begin
|
|
48 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p
|
|
49 ≡⟨ cong (λ k → k \/ exists1 m (lt2 m<n) p ) eq ⟩
|
|
50 false \/ exists1 m (lt2 m<n) p
|
|
51 ≡⟨ bool-or-1 refl ⟩
|
|
52 exists1 m (lt2 m<n) p
|
|
53 ≡⟨ not-found2 m (lt2 m<n) ⟩
|
|
54 false
|
|
55 ∎ where open ≡-Reasoning
|
77
|
56 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
|
|
57 fin<n {_} {zero} = s≤s z≤n
|
|
58 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
|
76
|
59 found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
|
80
|
60 found {p} {q} pt = found1 n (fin<n {n} {F←Q q}) (lt0 n) where
|
|
61 found1 : (m : ℕ ) {i : ℕ} (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ true
|
81
|
62 found1 0 ()
|
|
63 found1 (suc m) lt m<n with fromℕ≤ m<n ≟ F←Q q
|
|
64 found1 (suc m) lt m<n | yes eq = begin
|
78
|
65 p (Q←F (fromℕ≤ m<n )) \/ exists1 m (lt2 m<n ) p
|
81
|
66 ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (
|
|
67 begin
|
|
68 Q←F (fromℕ≤ m<n)
|
|
69 ≡⟨ cong ( λ k → Q←F k ) eq ⟩
|
|
70 Q←F (F←Q q)
|
|
71 ≡⟨ finiso→ q ⟩
|
|
72 q
|
|
73 ∎ ) ⟩
|
78
|
74 p q \/ exists1 m (lt2 m<n ) p
|
|
75 ≡⟨ cong (λ k → ( k \/ exists1 m (lt2 m<n ) p )) pt ⟩
|
|
76 true \/ exists1 m (lt2 m<n ) p
|
|
77 ≡⟨⟩
|
|
78 true
|
77
|
79 ∎ where open ≡-Reasoning
|
80
|
80 found1 (suc m) lt m<n | no ¬p = {!!}
|
78
|
81
|
44
|
82
|
|
83 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
|
|
84 fless zero = s≤s z≤n
|
|
85 fless (suc f) = s≤s ( fless f )
|
69
|
86
|