Mercurial > hg > Members > kono > Proof > automaton

comparison agda/lang-text.agda @ 141:b3f05cd08d24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 27 Dec 2020 13:26:44 +0900
parents
children
comparison
equal deleted inserted replaced
140:4c3fbfde1bc2 141:b3f05cd08d24
1 module lang-text where
2
3 open import Data.List
4 open import Data.String
5 open import Data.Char
6 open import Data.Char.Unsafe
7 open import Relation.Binary.PropositionalEquality
8 open import Relation.Nullary
9 open import logic
10
11 split : {Σ : Set} → (List Σ → Bool)
12 → ( List Σ → Bool) → List Σ → Bool
13 split x y [] = x [] /\ y []
14 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
15 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
16
17 contains : String → String → Bool
18 contains x y = contains1 (toList x ) ( toList y ) where
19 contains1 : List Char → List Char → Bool
20 contains1 [] [] = false
21 contains1 [] ( cx ∷ ly ) = false
22 contains1 (cx ∷ lx) [] = true
23 contains1 (cx ∷ lx ) ( cy ∷ ly ) with cx ≟ cy
24 ... | yes refl = contains1 lx ly
25 ... | no n = false
26
27 -- w does not contain the substring ab
28 ex15a : Set
29 ex15a = (w : String ) → ¬ (contains w "ab" ≡ true )
30
31 -- w does not contains substring baba
32 ex15b : Set
33 ex15b = (w : String ) → ¬ (contains w "baba" ≡ true )
34
35 -- w contains neither the substing ab nor ba
36 ex15c : Set
37
38 -- w is any string not in a*b*
39 ex15c = (w : String ) → ( ¬ (contains w "ab" ≡ true ) /\ ( ¬ (contains w "ba" ≡ true )
40
41 ex15d : {!!}
42 ex15d = {!!}
43
44 ex15e : {!!}
45 ex15e = {!!}
46
47 ex15f : {!!}
48 ex15f = {!!}
49
50 ex15g : {!!}
51 ex15g = {!!}
52
53 ex15h : {!!}
54 ex15h = {!!}