|
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
|
|
44
|
11
|
|
|
12 record FiniteSet ( Q : Set ) { n : ℕ }
|
|
|
13 : Set where
|
|
|
14 field
|
|
|
15 Q←F : Fin n → Q
|
|
|
16 F←Q : Q → Fin n
|
|
|
17 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
|
|
|
18 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
|
|
70
|
19 finℕ : ℕ
|
|
|
20 finℕ = n
|
|
44
|
21 lt0 : (n : ℕ) → n Data.Nat.≤ n
|
|
|
22 lt0 zero = z≤n
|
|
|
23 lt0 (suc n) = s≤s (lt0 n)
|
|
|
24 lt2 : {m n : ℕ} → m < n → m Data.Nat.≤ n
|
|
|
25 lt2 {zero} lt = z≤n
|
|
|
26 lt2 {suc m} {zero} ()
|
|
|
27 lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
|
|
76
|
28 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
|
|
|
29 exists1 zero _ _ = false
|
|
|
30 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
|
|
44
|
31 exists : ( Q → Bool ) → Bool
|
|
76
|
32 exists p = exists1 n (lt0 n) p
|
|
69
|
33 equal? : Q → Q → Bool
|
|
|
34 equal? q0 q1 with F←Q q0 ≟ F←Q q1
|
|
|
35 ... | yes p = true
|
|
|
36 ... | no ¬p = false
|
|
76
|
37 not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
|
|
|
38 not-found {p} pn = not-found2 n (lt0 n) where
|
|
|
39 not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false
|
|
|
40 not-found2 zero _ = refl
|
|
|
41 not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n))
|
|
|
42 not-found2 (suc m) m<n | eq = begin
|
|
|
43 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p
|
|
|
44 ≡⟨ cong (λ k → k \/ exists1 m (lt2 m<n) p ) eq ⟩
|
|
|
45 false \/ exists1 m (lt2 m<n) p
|
|
|
46 ≡⟨ bool-or-1 refl ⟩
|
|
|
47 exists1 m (lt2 m<n) p
|
|
|
48 ≡⟨ not-found2 m (lt2 m<n) ⟩
|
|
|
49 false
|
|
|
50 ∎ where open ≡-Reasoning
|
|
|
51 not-found1 : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false
|
|
|
52 not-found1 {p} ne q = not-found3 n (lt0 n) where
|
|
|
53 not-found3 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → p q ≡ false
|
|
|
54 not-found3 zero _ = {!!}
|
|
|
55 not-found3 ( suc m ) m<n = {!!}
|
|
|
56 found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
|
|
|
57 found {p} {q} pt with bool-≡-? (exists p) true
|
|
|
58 ... | yes eq1 = eq1
|
|
|
59 ... | no ne = ⊥-elim ( contra-position not-found1 notall (¬-bool-t ne) ) where
|
|
|
60 notall : ¬ ((q1 : Q) → p q1 ≡ false)
|
|
|
61 notall ne = ¬-bool (ne q) pt
|
|
44
|
62
|
|
|
63 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
|
|
|
64 fless zero = s≤s z≤n
|
|
|
65 fless (suc f) = s≤s ( fless f )
|
|
69
|
66
|
