Mercurial > hg > Members > kono > Proof > automaton
annotate agda/finiteSet.agda @ 104:fba1cd54581d
use exists in cond, nfa example
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 14 Nov 2019 05:13:49 +0900 |
parents | 86d390666078 |
children | ed0a2dad62f4 |
rev | line source |
---|---|
44 | 1 module finiteSet where |
2 | |
69 | 3 open import Data.Nat hiding ( _≟_ ) |
83 | 4 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_) |
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 ( _≟_ ) | |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
13 open import Data.List |
44 | 14 |
79 | 15 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
16 | |
85 | 17 record Found ( Q : Set ) (p : Q → Bool ) : Set where |
18 field | |
92 | 19 found-q : Q |
20 found-p : p found-q ≡ true | |
79 | 21 |
85 | 22 record FiniteSet ( Q : Set ) { n : ℕ } : Set where |
44 | 23 field |
24 Q←F : Fin n → Q | |
25 F←Q : Q → Fin n | |
26 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q | |
27 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f | |
70 | 28 finℕ : ℕ |
29 finℕ = n | |
44 | 30 lt0 : (n : ℕ) → n Data.Nat.≤ n |
31 lt0 zero = z≤n | |
32 lt0 (suc n) = s≤s (lt0 n) | |
33 lt2 : {m n : ℕ} → m < n → m Data.Nat.≤ n | |
34 lt2 {zero} lt = z≤n | |
35 lt2 {suc m} {zero} () | |
36 lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt) | |
76 | 37 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool |
38 exists1 zero _ _ = false | |
39 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p | |
44 | 40 exists : ( Q → Bool ) → Bool |
76 | 41 exists p = exists1 n (lt0 n) p |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
42 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
43 list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
44 list1 zero _ _ = [] |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
45 list1 ( suc m ) m<n p with bool-≡-? (p (Q←F (fromℕ≤ {m} {n} m<n))) true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
46 ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
47 ... | no _ = list1 m (lt2 m<n) p |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
48 to-list : ( Q → Bool ) → List Q |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
49 to-list p = list1 n (lt0 n) p |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
50 |
69 | 51 equal? : Q → Q → Bool |
52 equal? q0 q1 with F←Q q0 ≟ F←Q q1 | |
53 ... | yes p = true | |
54 ... | no ¬p = false | |
95 | 55 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y |
56 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 | |
57 equal→refl {q0} {q1} refl | yes eq = begin | |
58 q0 | |
59 ≡⟨ sym ( finiso→ q0) ⟩ | |
60 Q←F (F←Q q0) | |
61 ≡⟨ cong (λ k → Q←F k ) eq ⟩ | |
62 Q←F (F←Q q1) | |
63 ≡⟨ finiso→ q1 ⟩ | |
64 q1 | |
65 ∎ where open ≡-Reasoning | |
66 equal→refl {q0} {q1} () | no ne | |
87 | 67 equal?-refl : {q : Q} → equal? q q ≡ true |
68 equal?-refl {q} with F←Q q ≟ F←Q q | |
69 ... | yes p = refl | |
70 ... | no ne = ⊥-elim (ne refl) | |
77 | 71 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n |
72 fin<n {_} {zero} = s≤s z≤n | |
73 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f}) | |
84 | 74 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j |
75 i=j {suc n} zero zero refl = refl | |
76 i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) ) | |
85 | 77 -- ¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P → ¬ (∀ i → P i) → (∃ λ i → ¬ P i) |
78 End : (m : ℕ ) → (p : Q → Bool ) → Set | |
79 End m p = (i : Fin n) → m ≤ toℕ i → p (Q←F i ) ≡ false | |
80 next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p | |
83 | 81 → (m<n : m < n ) → p (Q←F (fromℕ≤ m<n )) ≡ false |
85 | 82 → End m p |
83 next-end {m} p prev m<n np i m<i with Data.Nat.Properties.<-cmp m (toℕ i) | |
84 next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a | |
85 next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c ) | |
86 next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where | |
83 | 87 m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ≤ m<n ≡ i |
84 | 88 m<n=i i eq m<n = i=j (fromℕ≤ m<n) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq ) |
85 | 89 first-end : ( p : Q → Bool ) → End n p |
90 first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {n} {i}) ) | |
88 | 91 found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true |
92 found {p} q pt = found1 n (lt0 n) ( first-end p ) where | |
83 | 93 found1 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → ((i : Fin n) → m ≤ toℕ i → p (Q←F i ) ≡ false ) → exists1 m m<n p ≡ true |
94 found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt ) | |
84 | 95 found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true |
96 found1 (suc m) m<n end | yes eq = subst (λ k → k \/ exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p} ) | |
97 found1 (suc m) m<n end | no np = begin | |
82 | 98 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p |
85 | 99 ≡⟨ bool-or-1 (¬-bool-t np ) ⟩ |
82 | 100 exists1 m (lt2 m<n) p |
85 | 101 ≡⟨ found1 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ⟩ |
82 | 102 true |
103 ∎ where open ≡-Reasoning | |
83 | 104 not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false |
105 not-found {p} pn = not-found2 n (lt0 n) where | |
106 not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false | |
107 not-found2 zero _ = refl | |
108 not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n)) | |
109 not-found2 (suc m) m<n | eq = begin | |
110 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p | |
85 | 111 ≡⟨ bool-or-1 eq ⟩ |
83 | 112 exists1 m (lt2 m<n) p |
113 ≡⟨ not-found2 m (lt2 m<n) ⟩ | |
114 false | |
115 ∎ where open ≡-Reasoning | |
85 | 116 open import Level |
117 postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) | |
118 found← : { p : Q → Bool } → exists p ≡ true → Found Q p | |
119 found← {p} exst = found2 n (lt0 n) (first-end p ) where | |
120 found2 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p → Found Q p | |
121 found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q) z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where | |
122 lemma : (λ z → p (Q←F (F←Q z))) ≡ p | |
123 lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl ) | |
124 found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true | |
92 | 125 found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ≤ m<n) ; found-p = eq } |
85 | 126 found2 (suc m) m<n end | no np = |
127 found2 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) | |
128 not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false | |
88 | 129 not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) ) |
44 | 130 |