Mercurial > hg > Members > kono > Proof > automaton

changeset 27:caf9b6aebd24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Nov 2018 11:16:29 +0900
parents 7ce76b3acc62
children 950d08ec1885
files agda/nfa.agda
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/agda/nfa.agda	Mon Nov 05 10:47:12 2018 +0900
+++ b/agda/nfa.agda	Mon Nov 05 11:16:29 2018 +0900
@@ -3,8 +3,10 @@
 -- open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Nat
 open import Data.List
-open import Data.Fin
+open import Data.Fin hiding ( _<_ )
 open import Data.Maybe
+open import Relation.Nullary
+open import Data.Empty
 open import Data.Bool using ( Bool ; true ; false ; _∧_ )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -37,15 +39,19 @@
         : Set  where
      field
         fin : Fin n
-        Q←F : {n : ℕ} → Fin n → Q
+        Q←F : 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 : ℕ} → Fin n → ( Q → Bool ) → Bool
-         exists1 ( Fin.zero ) _ = false
-         exists1 ( Fin.suc f ) p = p (Q←F f) ∧ exists1 f p
+         exists1 ( zero ) _ = false
+         exists1 ( suc f ) p = p (Q←F {!!}) ∧ exists1 f p
+
+fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
+fless zero = s≤s z≤n
+fless (suc f) = s≤s ( fless f )
 
 finState1 : FiniteSet States1 3
 finState1 = record {
@@ -55,13 +61,11 @@
       ; finiso→ = finiso→
       ; finiso← = finiso←
    } where
-       less : {n : ℕ} → Fin n → 
-       less = ?
-       Q←F : {n : ℕ} → Fin n → States1
+       Q←F : Fin 3 → States1
        Q←F zero = sr
        Q←F (suc zero) = ss
        Q←F (suc (suc zero)) = st
-       Q←F (suc (suc (suc _))) = st
+       Q←F (suc (suc (suc ()))) 
        F←Q : States1 → Fin 3
        F←Q sr = zero
        F←Q ss = suc (zero)
@@ -74,7 +78,7 @@
        finiso← zero = refl
        finiso← (suc zero) = refl
        finiso← (suc (suc zero)) = refl
-       finiso← (suc (suc (suc f))) = {!!}
+       finiso← (suc (suc (suc ()))) 
 
 
 open FiniteSet