Mercurial > hg > Members > kono > Proof > automaton

annotate agda/sbconst1.agda @ 13:02b4ecc9972c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
start exp version of subset construction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Aug 2018 17:03:40 +0900
parents
children 7eb71391088c
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module sbconst1 where
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level renaming ( suc to succ ; zero to Zero )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.List
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Maybe
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Data.Bool using ( Bool ; true ; false )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary using (¬_; Dec; yes; no)
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Data.Product
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 -- open import Data.Nat.DivMod
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 -- open import Data.Fin using ( toℕ )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import automaton
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open Automaton
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open NAutomaton
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 -- record Automaton ( Q : Set ) ( Σ : Set )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 -- : Set where
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 -- field
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 -- δ : Q → Σ → Q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 -- astart : Q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 -- aend : Q → Bool
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 --
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 -- record NAutomaton ( Q : Set ) ( Σ : Set )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 -- : Set where
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 -- field
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 -- nδ : Q → Σ → List Q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 -- sid : Q → ℕ
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 -- nstart : Q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 -- nend : Q → Bool
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 record FiniteSet ( Q : Set ) ( max : ℕ )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 : Set where
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 field
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 not-zero : max > 0
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ←ℕ : ℕ → Q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ←Q : Q → ℕ
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 finite : (q : Q) → ←Q q < max
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 finiso→ :(q : Q) → ←ℕ ( ←Q q ) ≡ q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 finiso← :(n : ℕ) → ←Q ( ←ℕ n ) ≡ n
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 open FiniteSet
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 _div_ : ℕ → ℕ → Maybe ℕ
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 _div_ x zero = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 _div_ x (suc y) = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 _mod_ : ℕ → ℕ → Maybe ℕ
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 _mod_ = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 lemma1 : { Q R : Set} {n m : ℕ } → FiniteSet Q n → FiniteSet R m → FiniteSet (Q × R) ( n * m )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 lemma1 {Q} {R} {zero} {_} N M = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 lemma1 {Q} {R} {n} {zero} N M = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 lemma1 {Q} {R} {n} {m} N M = record {
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 not-zero = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 ; ←ℕ = λ i → ( ←ℕ N {!!} , ←ℕ M {!!})
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 ; ←Q = λ q → ( ←Q N ( proj₁ q ) * ( ←Q M (proj₂ q )))
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 ; finite = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 ; finiso→ = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 ; finiso← = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 }
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 _exp_ : ℕ → ℕ → ℕ
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 _exp_ = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 sbstFin : { Q : Set} {n : ℕ } → FiniteSet Q n → FiniteSet (Q → Bool) {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 sbstFin = {!!}
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 list2sbst : {Q : Set} { n : ℕ } → FiniteSet Q n → List Q → Q → Bool
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 list2sbst N [] _ = false
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 list2sbst N ( h ∷ t ) q with ←Q N q ≟ ←Q N h
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 ... | yes _ = true
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 ... | no _ = list2sbst N t q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77