Mercurial > hg > Members > kono > Proof > automaton

comparison agda/finiteSet.agda @ 104:fba1cd54581d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use exists in cond, nfa example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 14 Nov 2019 05:13:49 +0900
parents 86d390666078
children ed0a2dad62f4
comparison
equal deleted inserted replaced
103:a46e0a2a3543 104:fba1cd54581d
8 open import Relation.Binary.Core 8 open import Relation.Binary.Core
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open import logic 10 open import logic
11 open import nat 11 open import nat
12 open import Data.Nat.Properties hiding ( _≟_ ) 12 open import Data.Nat.Properties hiding ( _≟_ )
13 open import Data.List
13 14
14 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 15 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
15 16
16 record Found ( Q : Set ) (p : Q → Bool ) : Set where 17 record Found ( Q : Set ) (p : Q → Bool ) : Set where
17 field 18 field
36 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool 37 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
37 exists1 zero _ _ = false 38 exists1 zero _ _ = false
38 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p 39 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
39 exists : ( Q → Bool ) → Bool 40 exists : ( Q → Bool ) → Bool
40 exists p = exists1 n (lt0 n) p 41 exists p = exists1 n (lt0 n) p
42
43 list1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → List Q
44 list1 zero _ _ = []
45 list1 ( suc m ) m<n p with bool-≡-? (p (Q←F (fromℕ≤ {m} {n} m<n))) true
46 ... | yes _ = Q←F (fromℕ≤ {m} {n} m<n) ∷ list1 m (lt2 m<n) p
47 ... | no _ = list1 m (lt2 m<n) p
48 to-list : ( Q → Bool ) → List Q
49 to-list p = list1 n (lt0 n) p
50
41 equal? : Q → Q → Bool 51 equal? : Q → Q → Bool
42 equal? q0 q1 with F←Q q0 ≟ F←Q q1 52 equal? q0 q1 with F←Q q0 ≟ F←Q q1
43 ... | yes p = true 53 ... | yes p = true
44 ... | no ¬p = false 54 ... | no ¬p = false
45 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y 55 equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y