Mercurial > hg > Members > kono > Proof > automaton
annotate agda/finiteSet.agda @ 114:a7364dfcc51e
finite-or
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 18 Nov 2019 23:53:47 +0900 |
| parents | 58b009043733 |
| children | 1b54c0623d01 |
| rev | line source |
|---|---|
| 111 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 44 | 2 module finiteSet where |
| 3 | |
| 69 | 4 open import Data.Nat hiding ( _≟_ ) |
| 83 | 5 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_) |
| 69 | 6 open import Data.Fin.Properties |
| 76 | 7 open import Data.Empty |
| 69 | 8 open import Relation.Nullary |
| 44 | 9 open import Relation.Binary.Core |
| 46 | 10 open import Relation.Binary.PropositionalEquality |
| 69 | 11 open import logic |
| 78 | 12 open import nat |
| 13 open import Data.Nat.Properties hiding ( _≟_ ) | |
| 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 |
| 114 | 43 open import Data.List |
| 44 list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
45 list1 zero _ _ = [] |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
46 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
|
47 ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p |
| 114 | 48 ... | no _ = list1 m (lt2 m<n) p |
| 49 to-list : ( Q → Bool ) → List Q | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
50 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
|
51 |
| 69 | 52 equal? : Q → Q → Bool |
| 53 equal? q0 q1 with F←Q q0 ≟ F←Q q1 | |
| 54 ... | yes p = true | |
| 55 ... | no ¬p = false | |
| 95 | 56 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y |
| 57 equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 | |
| 58 equal→refl {q0} {q1} refl | yes eq = begin | |
| 59 q0 | |
| 60 ≡⟨ sym ( finiso→ q0) ⟩ | |
| 61 Q←F (F←Q q0) | |
| 62 ≡⟨ cong (λ k → Q←F k ) eq ⟩ | |
| 63 Q←F (F←Q q1) | |
| 64 ≡⟨ finiso→ q1 ⟩ | |
| 65 q1 | |
| 66 ∎ where open ≡-Reasoning | |
| 67 equal→refl {q0} {q1} () | no ne | |
| 87 | 68 equal?-refl : {q : Q} → equal? q q ≡ true |
| 69 equal?-refl {q} with F←Q q ≟ F←Q q | |
| 70 ... | yes p = refl | |
| 71 ... | no ne = ⊥-elim (ne refl) | |
| 77 | 72 fin<n : {n : ℕ} {f : Fin n} → toℕ f < n |
| 73 fin<n {_} {zero} = s≤s z≤n | |
| 74 fin<n {suc n} {suc f} = s≤s (fin<n {n} {f}) | |
| 84 | 75 i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j |
| 76 i=j {suc n} zero zero refl = refl | |
| 77 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 | 78 -- ¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P → ¬ (∀ i → P i) → (∃ λ i → ¬ P i) |
| 79 End : (m : ℕ ) → (p : Q → Bool ) → Set | |
| 80 End m p = (i : Fin n) → m ≤ toℕ i → p (Q←F i ) ≡ false | |
| 81 next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p | |
| 83 | 82 → (m<n : m < n ) → p (Q←F (fromℕ≤ m<n )) ≡ false |
| 85 | 83 → End m p |
| 84 next-end {m} p prev m<n np i m<i with Data.Nat.Properties.<-cmp m (toℕ i) | |
| 85 next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a | |
| 86 next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c ) | |
| 87 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 | 88 m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ≤ m<n ≡ i |
| 84 | 89 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 | 90 first-end : ( p : Q → Bool ) → End n p |
| 91 first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {n} {i}) ) | |
| 88 | 92 found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true |
| 93 found {p} q pt = found1 n (lt0 n) ( first-end p ) where | |
| 83 | 94 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 |
| 95 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 | 96 found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true |
| 97 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} ) | |
| 98 found1 (suc m) m<n end | no np = begin | |
| 82 | 99 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p |
| 85 | 100 ≡⟨ bool-or-1 (¬-bool-t np ) ⟩ |
| 82 | 101 exists1 m (lt2 m<n) p |
| 85 | 102 ≡⟨ found1 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ⟩ |
| 82 | 103 true |
| 104 ∎ where open ≡-Reasoning | |
| 83 | 105 not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false |
| 106 not-found {p} pn = not-found2 n (lt0 n) where | |
| 107 not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false | |
| 108 not-found2 zero _ = refl | |
| 109 not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n)) | |
| 110 not-found2 (suc m) m<n | eq = begin | |
| 111 p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p | |
| 85 | 112 ≡⟨ bool-or-1 eq ⟩ |
| 83 | 113 exists1 m (lt2 m<n) p |
| 114 ≡⟨ not-found2 m (lt2 m<n) ⟩ | |
| 115 false | |
| 116 ∎ where open ≡-Reasoning | |
| 85 | 117 open import Level |
| 118 postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) | |
| 119 found← : { p : Q → Bool } → exists p ≡ true → Found Q p | |
| 120 found← {p} exst = found2 n (lt0 n) (first-end p ) where | |
| 121 found2 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p → Found Q p | |
| 122 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 | |
| 123 lemma : (λ z → p (Q←F (F←Q z))) ≡ p | |
| 124 lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl ) | |
| 125 found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true | |
| 92 | 126 found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ≤ m<n) ; found-p = eq } |
| 85 | 127 found2 (suc m) m<n end | no np = |
| 128 found2 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) | |
| 129 not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false | |
| 88 | 130 not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) ) |
| 44 | 131 |
| 111 | 132 fin-∨' : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a Data.Nat.+ b} |
| 133 fin-∨' {A} {B} {a} {b} fa fb = record { | |
| 134 Q←F = Q←F | |
| 135 ; F←Q = F←Q | |
| 136 ; finiso→ = finiso→ | |
| 137 ; finiso← = finiso← | |
| 138 } where | |
| 139 n : ℕ | |
| 140 n = a Data.Nat.+ b | |
| 141 Q : Set | |
| 142 Q = A ∨ B | |
| 113 | 143 f-a : ∀{i} → (f : Fin i ) → (a : ℕ ) → toℕ f > a → toℕ f < a Data.Nat.+ b → Fin b |
| 144 f-a {i} f zero lt lt2 = fromℕ≤ lt2 | |
| 145 f-a {suc i} (suc f) (suc a) (s≤s lt) (s≤s lt2) = f-a f a lt lt2 | |
| 146 f-a zero (suc x) () _ | |
| 111 | 147 Q←F : Fin n → Q |
| 148 Q←F f with Data.Nat.Properties.<-cmp (toℕ f) a | |
| 149 Q←F f | tri< lt ¬b ¬c = case1 (FiniteSet.Q←F fa (fromℕ≤ lt )) | |
| 113 | 150 Q←F f | tri≈ ¬a eq ¬c = case2 (FiniteSet.Q←F fb (fromℕ≤ (0<b a (a<a+b eq ) ))) where |
| 151 a<a+b : toℕ f ≡ a → a < a Data.Nat.+ b | |
| 152 a<a+b eq = subst (λ k → k < a Data.Nat.+ b) eq ( toℕ<n f ) | |
| 153 0<b : (a : ℕ ) → a < a Data.Nat.+ b → 0 < b | |
| 154 0<b zero a<a+b = a<a+b | |
| 155 0<b (suc a) (s≤s a<a+b) = 0<b a a<a+b | |
| 156 Q←F f | tri> ¬a ¬b c = case2 (FiniteSet.Q←F fb (f-a f a c (toℕ<n f) )) | |
| 111 | 157 F←Q : Q → Fin n |
| 158 F←Q (case1 qa) = inject+ b (FiniteSet.F←Q fa qa) | |
| 159 F←Q (case2 qb) = raise a (FiniteSet.F←Q fb qb) | |
| 160 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q | |
| 114 | 161 finiso→ (case1 qa) = {!!} |
| 162 finiso→ (case2 qb) = {!!} | |
| 111 | 163 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f |
| 114 | 164 finiso← f with Data.Nat.Properties.<-cmp (toℕ f) a |
| 165 finiso← f | tri< lt ¬b ¬c = lemma11 where | |
| 166 lemma11 : inject+ b (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ lt ) )) ≡ f | |
| 167 lemma11 = {!!} | |
| 168 finiso← f | tri≈ ¬a eq ¬c = lemma12 where | |
| 169 lemma12 : raise a (FiniteSet.F←Q fb (FiniteSet.Q←F fb (fromℕ≤ {!!} ))) ≡ f | |
| 170 lemma12 = {!!} | |
| 171 finiso← f | tri> ¬a ¬b c = lemma13 where | |
| 172 lemma13 : raise a (FiniteSet.F←Q fb ((FiniteSet.Q←F fb (f-a f a c (toℕ<n f))))) ≡ f | |
| 173 lemma13 = {!!} | |
| 111 | 174 |
| 175 import Data.Nat.DivMod | |
| 176 import Data.Nat.Properties | |
| 177 | |
| 112 | 178 open _∧_ |
| 179 | |
| 114 | 180 open import Data.Vec |
| 181 import Data.Product | |
| 182 | |
| 183 exp2 : (n : ℕ ) → exp 2 (suc n) ≡ exp 2 n Data.Nat.+ exp 2 n | |
| 184 exp2 n = begin | |
| 185 exp 2 (suc n) | |
| 186 ≡⟨⟩ | |
| 187 2 * ( exp 2 n ) | |
| 188 ≡⟨ *-comm 2 (exp 2 n) ⟩ | |
| 189 ( exp 2 n ) * 2 | |
| 190 ≡⟨ +-*-suc ( exp 2 n ) 1 ⟩ | |
| 191 (exp 2 n ) Data.Nat.+ ( exp 2 n ) * 1 | |
| 192 ≡⟨ cong ( λ k → (exp 2 n ) Data.Nat.+ k ) (proj₂ *-identity (exp 2 n) ) ⟩ | |
| 193 exp 2 n Data.Nat.+ exp 2 n | |
| 194 ∎ where | |
| 195 open ≡-Reasoning | |
| 196 open Data.Product | |
| 197 | |
| 198 cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f | |
| 199 cast-iso refl zero = refl | |
| 200 cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) | |
| 201 | |
| 202 | |
| 203 fin2List : {n : ℕ } → FiniteSet (Vec Bool n) {exp 2 n } | |
| 204 fin2List {zero} = record { | |
| 205 Q←F = λ _ → Vec.[] | |
| 206 ; F←Q = λ _ → # 0 | |
| 111 | 207 ; finiso→ = finiso→ |
| 208 ; finiso← = finiso← | |
| 209 } where | |
| 114 | 210 Q = Vec Bool zero |
| 211 finiso→ : (q : Q) → [] ≡ q | |
| 212 finiso→ [] = refl | |
| 213 finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f | |
| 214 finiso← zero = refl | |
| 215 fin2List {suc n} = record { | |
| 216 Q←F = Q←F | |
| 217 ; F←Q = F←Q | |
| 218 ; finiso→ = finiso→ | |
| 219 ; finiso← = finiso← | |
| 220 } where | |
| 111 | 221 Q : Set |
| 114 | 222 Q = Vec Bool (suc n) |
| 223 QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n | |
| 224 QtoR ( true ∷ x ) = case1 x | |
| 225 QtoR ( false ∷ x ) = case2 x | |
| 226 RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n) | |
| 227 RtoQ ( case1 x ) = true ∷ x | |
| 228 RtoQ ( case2 x ) = false ∷ x | |
| 229 isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x | |
| 230 isoRQ (true ∷ _ ) = refl | |
| 231 isoRQ (false ∷ _ ) = refl | |
| 232 isoQR : (x : Vec Bool n ∨ Vec Bool n ) → QtoR ( RtoQ x ) ≡ x | |
| 233 isoQR (case1 x) = refl | |
| 234 isoQR (case2 x) = refl | |
| 235 fin∨ = fin-∨' (fin2List {n}) (fin2List {n}) | |
| 236 Q←F : Fin (exp 2 (suc n)) → Q | |
| 237 Q←F f = RtoQ ( FiniteSet.Q←F fin∨ (cast (exp2 n) f )) | |
| 238 F←Q : Q → Fin (exp 2 (suc n)) | |
| 239 F←Q q = cast (sym (exp2 n)) ( FiniteSet.F←Q fin∨ ( QtoR q ) ) | |
| 111 | 240 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q |
| 114 | 241 finiso→ q = begin |
| 242 RtoQ ( FiniteSet.Q←F fin∨ (cast (exp2 n) (cast (sym (exp2 n)) ( FiniteSet.F←Q fin∨ (QtoR q) )) )) | |
| 243 ≡⟨ cong (λ k → RtoQ ( FiniteSet.Q←F fin∨ k)) (cast-iso (exp2 n) _ ) ⟩ | |
| 244 RtoQ ( FiniteSet.Q←F fin∨ ( FiniteSet.F←Q fin∨ (QtoR q) )) | |
| 245 ≡⟨ cong ( λ k → RtoQ k ) ( FiniteSet.finiso→ fin∨ _ ) ⟩ | |
| 246 RtoQ (QtoR _) | |
| 247 ≡⟨ isoRQ q ⟩ | |
| 248 q | |
| 249 ∎ where open ≡-Reasoning | |
| 250 finiso← : (f : Fin (exp 2 (suc n) )) → F←Q ( Q←F f ) ≡ f | |
| 251 finiso← f = begin | |
| 252 cast _ (FiniteSet.F←Q fin∨ (QtoR (RtoQ (FiniteSet.Q←F fin∨ (cast _ f )) ) )) | |
| 253 ≡⟨ cong (λ k → cast (sym (exp2 n)) (FiniteSet.F←Q fin∨ k )) (isoQR (FiniteSet.Q←F fin∨ (cast _ f))) ⟩ | |
| 254 cast (sym (exp2 n)) (FiniteSet.F←Q fin∨ (FiniteSet.Q←F fin∨ (cast (exp2 n) f ))) | |
| 255 ≡⟨ cong (λ k → cast (sym (exp2 n)) k ) ( FiniteSet.finiso← fin∨ _ ) ⟩ | |
| 256 cast _ (cast (exp2 n) f ) | |
| 257 ≡⟨ cast-iso (sym (exp2 n)) _ ⟩ | |
| 258 f | |
| 259 ∎ where open ≡-Reasoning | |
| 111 | 260 |
| 114 | 261 Func2List : { Q : Set } → {n : ℕ } → FiniteSet Q {n} → ( Q → Bool ) → Vec Bool n |
| 262 Func2List = {!!} | |
| 111 | 263 |
| 114 | 264 List2Func : { Q : Set } → {n : ℕ } → FiniteSet Q {n} → Vec Bool n → ( Q → Bool ) |
| 265 List2Func = {!!} |