Mercurial > hg > Members > kono > Proof > automaton

changeset 26:7ce76b3acc62

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
improve finite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Nov 2018 10:47:12 +0900
parents 256b7a6de863
children caf9b6aebd24
files agda/nfa.agda
diffstat 1 files changed, 27 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/agda/nfa.agda	Mon Nov 05 08:59:31 2018 +0900
+++ b/agda/nfa.agda	Mon Nov 05 10:47:12 2018 +0900
@@ -37,31 +37,45 @@
         : Set  where
      field
         fin : Fin n
-        Q←F : {n : ℕ } → Fin n → Q
-        F←Q : {n : ℕ } → Q → Fin n 
-        finiso→ : {n : ℕ } → (q : Q) → Q←F {n} ( F←Q q ) ≡ q
-        finiso← : {n : ℕ } → (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+        Q←F : {n : ℕ} → Fin n → Q
+        F←Q : Q → Fin n 
+        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
+        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
      exists : ( Q → Bool ) → Bool
      exists p = exists1 fin p where
-         exists1 : {n : ℕ } → (f : Fin n ) → ( Q → Bool ) → Bool
+         exists1 : {n : ℕ} → Fin n → ( Q → Bool ) → Bool
          exists1 ( Fin.zero ) _ = false
          exists1 ( Fin.suc f ) p = p (Q←F f) ∧ exists1 f p
 
 finState1 : FiniteSet States1 3
 finState1 = record {
         fin = fromℕ 2
-      ; Q←F = {!!}
-      ; F←Q  = {!!}
-      ; finiso→ = {!!}
-      ; finiso← = {!!}
+      ; Q←F = Q←F
+      ; F←Q  = F←Q
+      ; finiso→ = finiso→
+      ; finiso← = finiso←
    } where
-       Q←F : {n : ℕ } → Fin n → States1
+       less : {n : ℕ} → Fin n → 
+       less = ?
+       Q←F : {n : ℕ} → Fin n → States1
        Q←F zero = sr
        Q←F (suc zero) = ss
        Q←F (suc (suc zero)) = st
-       Q←F (suc (suc (suc _)))  = {!!}
-       F←Q : {n : ℕ } → States1 → Fin n
-       F←Q = {!!}
+       Q←F (suc (suc (suc _))) = st
+       F←Q : States1 → Fin 3
+       F←Q sr = zero
+       F←Q ss = suc (zero)
+       F←Q st = suc ( suc zero )
+       finiso→ : (q : States1) → Q←F (F←Q q) ≡ q
+       finiso→ sr = refl
+       finiso→ ss = refl
+       finiso→ st = refl
+       finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
+       finiso← zero = refl
+       finiso← (suc zero) = refl
+       finiso← (suc (suc zero)) = refl
+       finiso← (suc (suc (suc f))) = {!!}
+
 
 open FiniteSet