Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/finiteSet.agda @ 346:4456eebbd1bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
copying countable bijection may not easy
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 17 Jul 2023 11:00:19 +0900
parents 91781b7c65a8
children c298981108c1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
111
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
1 {-# OPTIONS --allow-unsolved-metas #-}
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 module finiteSet where
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
4 open import Data.Nat hiding ( _≟_ )
83
92f396c3a1d7 add end function
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 82
diff changeset
5 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
318
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 264
diff changeset
6 -- open import Data.Fin.Properties hiding ( ≤-refl )
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
7 open import Data.Empty
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
8 open import Relation.Nullary
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
9 open import Relation.Binary.Definitions
46
964e4bd0272a add coinduction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
10 open import Relation.Binary.PropositionalEquality
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
11 open import logic
78
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
12 open import nat
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
13 open import Data.Nat.Properties hiding ( _≟_ )
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
79
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
15 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 78
diff changeset
16
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
17 record FiniteSet ( Q : Set ) : Set where
85
9911911b77cb all foundables
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
18 field
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
19 finite : ℕ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
20 Q←F : Fin finite → Q
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
21 F←Q : Q → Fin finite
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
23 finiso← : (f : Fin finite ) → F←Q ( Q←F f ) ≡ f
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
24 exists1 : (m : ℕ ) → m Data.Nat.≤ finite → (Q → Bool) → Bool
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
25 exists1 zero _ _ = false
264
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
26 exists1 ( suc m ) m<n p = p (Q←F (fromℕ< {m} {finite} m<n)) \/ exists1 m (<to≤ m<n) p
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 exists : ( Q → Bool ) → Bool
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
28 exists p = exists1 finite ≤-refl p
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
29
114
a7364dfcc51e finite-or
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
30 open import Data.List
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
31 list1 : (m : ℕ ) → m Data.Nat.≤ finite → (Q → Bool) → List Q
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
32 list1 zero _ _ = []
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
33 list1 ( suc m ) m<n p with bool-≡-? (p (Q←F (fromℕ< {m} {finite} m<n))) true
264
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
34 ... | yes _ = Q←F (fromℕ< {m} {finite} m<n) ∷ list1 m (<to≤ m<n) p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
35 ... | no _ = list1 m (<to≤ m<n) p
114
a7364dfcc51e finite-or
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
36 to-list : ( Q → Bool ) → List Q
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
37 to-list p = list1 finite ≤-refl p
104
fba1cd54581d use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
38
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
39 equal? : Q → Q → Bool
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
40 equal? q0 q1 with F←Q q0 ≟ F←Q q1
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
41 ... | yes p = true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 46
diff changeset
42 ... | no ¬p = false