Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/regex1-ex.agda @ 411:207e6c4e155c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 Nov 2023 17:40:55 +0900 |
| parents | a5c874396cc4 |
| children |
| rev | line source |
|---|---|
| 44 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 384 | 2 module regex1-ex where |
| 0 | 3 |
| 4 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 330 | 5 open import Data.Fin hiding ( pred ) |
| 34 | 6 open import Data.Nat hiding ( _≟_ ) |
| 44 | 7 open import Data.List hiding ( any ; [_] ) |
| 274 | 8 -- import Data.Bool using ( Bool ; true ; false ; _∧_ ) |
| 9 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ ) | |
| 34 | 10 open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) |
| 1 | 11 open import Relation.Nullary using (¬_; Dec; yes; no) |
| 141 | 12 open import regex |
| 274 | 13 open import logic |
|
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
14 open import regular-language |
| 1 | 15 |
| 36 | 16 -- postulate a b c d : Set |
| 17 | |
| 141 | 18 data In : Set where |
| 19 a : In | |
| 20 b : In | |
| 21 c : In | |
| 22 d : In | |
| 36 | 23 |
| 274 | 24 -- infixr 40 _&_ _||_ |
| 25 | |
| 26 r1' = (< a > & < b >) & < c > --- abc | |
| 27 r1 = < a > & < b > & < c > --- abc | |
| 28 r0 : ¬ (r1' ≡ r1) | |
| 29 r0 () | |
| 30 any = < a > || < b > || < c > || < d > --- a|b|c|d | |
| 31 r2 = ( any * ) & ( < a > & < b > & < c > ) -- .*abc | |
| 32 r3 = ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > ) | |
| 33 r4 = ( < a > & < b > & < c > ) || ( < b > & < c > & < d > ) | |
| 34 r5 = ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > ) | |
| 35 | |
| 36 open import nfa | |
| 37 | |
| 411 | 38 tt1 : {Σ : Set} → ( P Q : List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] ) ≡ |
| 39 P [] /\ Q (a ∷ b ∷ c ∷ []) \/ | |
| 40 P (a ∷ []) /\ Q (b ∷ c ∷ []) \/ | |
| 41 P (a ∷ b ∷ []) /\ Q (c ∷ []) \/ P (a ∷ b ∷ c ∷ []) /\ Q [] | |
| 42 tt1 P Q = refl | |
| 330 | 43 |
| 411 | 44 test-AB→repeat3 : {Σ : Set} → {A : List In → Bool} → repeat A [] ( a ∷ [] ) ≡ A (a ∷ [] ) |
| 45 test-AB→repeat3 {_} {A} = refl | |
| 330 | 46 |
| 411 | 47 test-AB→repeat2 : {Σ : Set} → {A : List In → Bool} → repeat A [] ( a ∷ b ∷ [] ) ≡ A (a ∷ []) /\ A (b ∷ []) \/ A (a ∷ b ∷ []) |
| 48 test-AB→repeat2 {_} {A} = refl | |
| 49 | |
| 50 test-AB→repeat1 : {Σ : Set} → {A : List In → Bool} → repeat A [] ( a ∷ b ∷ c ∷ [] ) ≡ | |
| 51 A (a ∷ []) /\ ((A (b ∷ []) /\ A (c ∷ [])) \/ A (b ∷ c ∷ [])) | |
| 52 \/ A (a ∷ b ∷ []) /\ A (c ∷ []) -- ok | |
| 53 \/ A (a ∷ b ∷ c ∷ []) -- ok | |
| 330 | 54 test-AB→repeat1 {_} {A} = refl |
| 55 | |
| 141 | 56 cmpi : (x y : In ) → Dec (x ≡ y) |
| 57 cmpi a a = yes refl | |
| 58 cmpi b b = yes refl | |
| 59 cmpi c c = yes refl | |
| 60 cmpi d d = yes refl | |
| 61 cmpi a b = no (λ ()) | |
| 62 cmpi a c = no (λ ()) | |
| 63 cmpi a d = no (λ ()) | |
| 64 cmpi b a = no (λ ()) | |
| 65 cmpi b c = no (λ ()) | |
| 66 cmpi b d = no (λ ()) | |
| 67 cmpi c a = no (λ ()) | |
| 68 cmpi c b = no (λ ()) | |
| 69 cmpi c d = no (λ ()) | |
| 70 cmpi d a = no (λ ()) | |
| 71 cmpi d b = no (λ ()) | |
| 72 cmpi d c = no (λ ()) | |
| 36 | 73 |
| 411 | 74 test-regex : regex-language r1' cmpi ( a ∷ b ∷ c ∷ [] ) ≡ true |
| 138 | 75 test-regex = refl |
| 76 | |
| 382 | 77 -- test-regex2 : regex-language r2 cmpi ( b ∷ c ∷ a ∷ b ∷ [] ) ≡ false |
| 330 | 78 -- test-regex2 = refl |
| 79 | |
| 382 | 80 test-regex1 : regex-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true |
| 138 | 81 test-regex1 = refl |
| 82 | |
| 141 | 83 |
|
383
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
84 --test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ ( |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
85 -- ( A [] /\ B ( a ∷ b ∷ a ∷ [] ) ) \/ |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
86 -- ( A ( a ∷ [] ) /\ B ( b ∷ a ∷ [] ) ) \/ |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
87 -- ( A ( a ∷ b ∷ [] ) /\ B ( a ∷ [] ) ) \/ |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
88 -- ( A ( a ∷ b ∷ a ∷ [] ) /\ B [] ) |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
89 -- ) |
|
708570e55a91
add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
382
diff
changeset
|
90 -- test-AB→split {_} {A} {B} = refl |
| 138 | 91 |
| 274 | 92 list-eq : {Σ : Set} → (cmpi : (s t : Σ) → Dec (s ≡ t )) → (s t : List Σ ) → Bool |
| 93 list-eq cmpi [] [] = true | |
| 94 list-eq cmpi [] (x ∷ t) = false | |
| 95 list-eq cmpi (x ∷ s) [] = false | |
| 96 list-eq cmpi (x ∷ s) (y ∷ t) with cmpi x y | |
| 97 ... | yes _ = list-eq cmpi s t | |
| 98 ... | no _ = false | |
| 99 | |
| 100 -- split-spec-01 : {s t u : List In } → s ++ t ≡ u → split (list-eq cmpi s) (list-eq cmpi t) u ≡ true | |
| 101 -- split-spec-01 = {!!} | |
| 102 | |
| 141 | 103 -- from example 1.53 1 |
| 104 | |
| 105 ex53-1 : Set | |
| 382 | 106 ex53-1 = (s : List In ) → regex-language ( (< a > *) & < b > & (< a > *) ) cmpi s ≡ true → {!!} -- contains exact one b |
| 141 | 107 |
| 108 ex53-2 : Set | |
| 382 | 109 ex53-2 = (s : List In ) → regex-language ( (any * ) & < b > & (any *) ) cmpi s ≡ true → {!!} -- contains at lease one b |
| 141 | 110 |
| 111 evenp : {Σ : Set} → List Σ → Bool | |
| 112 oddp : {Σ : Set} → List Σ → Bool | |
| 113 oddp [] = false | |
| 114 oddp (_ ∷ t) = evenp t | |
| 138 | 115 |
| 141 | 116 evenp [] = true |
| 117 evenp (_ ∷ t) = oddp t | |
| 118 | |
| 119 -- from example 1.53 5 | |
| 120 egex-even : Set | |
| 382 | 121 egex-even = (s : List In ) → regex-language ( ( any & any ) * ) cmpi s ≡ true → evenp s ≡ true |
| 141 | 122 |
| 382 | 123 test11 = regex-language ( ( any & any ) * ) cmpi (a ∷ []) |
| 124 test12 = regex-language ( ( any & any ) * ) cmpi (a ∷ b ∷ []) | |
| 141 | 125 |
| 126 -- proof-egex-even : egex-even | |
| 127 -- proof-egex-even [] _ = refl | |
| 128 -- proof-egex-even (a ∷ []) () | |
| 129 -- proof-egex-even (b ∷ []) () | |
| 130 -- proof-egex-even (c ∷ []) () | |
| 131 -- proof-egex-even (x ∷ x₁ ∷ s) y = proof-egex-even s {!!} | |
| 132 | |
| 274 | 133 open import finiteSet |
| 134 | |
| 135 iFin : FiniteSet In | |
| 136 iFin = record { | |
| 137 finite = finite0 | |
| 138 ; Q←F = Q←F0 | |
| 139 ; F←Q = F←Q0 | |
| 140 ; finiso→ = finiso→0 | |
| 141 ; finiso← = finiso←0 | |
| 142 } where | |
| 143 finite0 : ℕ | |
| 144 finite0 = 4 | |
| 145 Q←F0 : Fin finite0 → In | |
| 146 Q←F0 zero = a | |
| 147 Q←F0 (suc zero) = b | |
| 148 Q←F0 (suc (suc zero)) = c | |
| 149 Q←F0 (suc (suc (suc zero))) = d | |
| 150 F←Q0 : In → Fin finite0 | |
| 151 F←Q0 a = # 0 | |
| 152 F←Q0 b = # 1 | |
| 153 F←Q0 c = # 2 | |
| 154 F←Q0 d = # 3 | |
| 155 finiso→0 : (q : In) → Q←F0 ( F←Q0 q ) ≡ q | |
| 156 finiso→0 a = refl | |
| 157 finiso→0 b = refl | |
| 158 finiso→0 c = refl | |
| 159 finiso→0 d = refl | |
| 160 finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f | |
| 161 finiso←0 zero = refl | |
| 162 finiso←0 (suc zero) = refl | |
| 163 finiso←0 (suc (suc zero)) = refl | |
| 164 finiso←0 (suc (suc (suc zero))) = refl | |
| 165 | |
| 166 | |
| 382 | 167 -- open import derive In iFin |
| 168 -- open import automaton | |
| 141 | 169 |
| 382 | 170 -- ra-ex = trace (regex→automaton cmpi r2) (record { state = r2 ; is-derived = unit refl }) ( a ∷ b ∷ c ∷ []) |
| 141 | 171 |