Mercurial > hg > Members > kono > Proof > automaton

changeset 341:9120a5872a5b

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 Tue, 11 Jul 2023 11:04:00 +0900
parents b818fbd86d0b
children ab3b3a06d019
files automaton-in-agda/src/derive.agda automaton-in-agda/src/fin.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/halt.agda
diffstat 4 files changed, 70 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Mon Jul 10 14:28:39 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Tue Jul 11 11:04:00 2023 +0900
@@ -94,12 +94,24 @@
 rank < x > = 0
 
 data SB : (r : Regex Σ) → (rn : ℕ) → Set where
-    sbε : (r : Regex Σ) → SB ε 0
-    sbφ : (r : Regex Σ) → SB φ 0
+    sbε : SB ε 0
+    sbφ : SB φ 0
     sb<> : (s : Σ) → SB < s > 0
     sb| : (x y : Regex Σ) → (xn yn xy : ℕ) → SB x xn → SB y yn → xy ≡  max xn yn  → SB (x || y)  xy
-    sb* : (x : Regex Σ) → (xn : ℕ) → SB (x & (x *)) (suc xn)
-    sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn  → SB (x & y) (suc yn)
+    sb* : (x : Regex Σ) → (xn : ℕ) → SB x xn  → SB (x *) (suc xn)
+    sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn  → ( sx : SB x xn ) (sy : SB y yn ) → SB (x & y) (suc yn)
+
+sb-id : (r : Regex Σ) → SB r (rank r) → Bool
+sb-id r sb with rank r | inspect rank r
+sb-id ε sbε | zero | _ = true
+sb-id φ sbφ | zero | _ = true
+sb-id < t > (sb<> s) | zero | _ with eq? t s
+... | yes _ = true
+... | no _  = false
+sb-id (x0 || y0) (sb| x y xn yn .zero sb sb₁ x₁) | zero | record { eq = eq1 } = sb-id x0 ?  /\ sb-id y0 ?  
+sb-id _ (sb| x y xn yn .(suc k) sb sb₁ x₁) | suc k | record { eq = eq1 } = sb-id x ?  /\ sb-id y ?  
+sb-id (y *) (sb* x t u) | suc k | record{ eq = eq1 } = sb-id y ?
+sb-id (x0 & y0) (sb& .x0 .y0 xn .k x z z₁) | suc k | record { eq = eq1 } = sb-id x0 ? /\ sb-id y0 ?
 
 SBTA : (r : Regex Σ) → Automaton (SB r (rank r) → Bool) Σ
 SBTA = ?
@@ -117,21 +129,31 @@
     fb00 (suc n) (r & r₁) eq = ?
     fb00 (suc n) (r || r₁) eq = ?
 
+fb01 : (n : ℕ ) →  (r : Regex Σ) →  rank r ≡ n →  Derivative r → SB r (rank r) → Bool
+fb01 n r eq d sb with is-derived d 
+fb01 n r eq d sb | unit = sb-id r sb
+fb01 zero .ε eq d sbε  | derive {y} ss i = true
+fb01 zero .φ eq d sbφ | derive {y} ss i = true
+fb01 zero .(< s >) eq d (sb<> s) | derive {y} ss i with eq? s i
+... | yes _ = true
+... | no _  = false
+fb01 zero .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
+fb01 (suc n) .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
+fb01 (suc n) .(x *) eq d (sb* x xn u ) | derive {y₂} ss i = ?
+fb01 (suc n) t eq d z | derive {y₂} ss i = ?
+
 injSB : (r : Regex   Σ) → InjectiveF (Derivative r) (SB r (rank r) → Bool)
 injSB r = record { f = fb01 (rank r) r refl ; inject = ? } where
-     fb01 : (n : ℕ ) →  (r : Regex Σ) →  rank r ≡ n →  Derivative r → SB r (rank r) → Bool
-     fb01 n r eq d sb with is-derived d 
-     fb01 n r eq d sb | unit = true
-     fb01 zero .ε eq d (sbε r) | derive {y} ss i = true
-     fb01 zero .φ eq d (sbφ r) | derive {y} ss i = false
-     fb01 zero .(< s >) eq d (sb<> s) | derive {y} ss i = ?
-     fb01 zero .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
-     fb01 (suc n) .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
-     fb01 (suc n) .(x & (x *)) eq d (sb* x .(max (rank x) (rank (x *)))) | derive {y₂} ss i = ?
-     fb01 (suc n) .(x & y) eq d (sb& x y xn .(max (rank x) (rank y)) x₁) | derive {y₂} ss i = ?
+     fb02 : (x y : Derivative r) → fb01 (rank r) r refl x ≡ fb01 (rank r) r refl y → x ≡ y
+     fb02 = ?
+
+decdb : (r : Regex   Σ) →  (a : SB r (rank r) → Bool) 
+    → Dec (Is (Derivative r) (SB r (rank r) → Bool) (InjectiveF.f (injSB r)) a )
+decdb r a with fb01 (rank r) r refl record { state = r ; is-derived = ? }
+... | t = ?
 
 finite-derivative : (r : Regex   Σ) → FiniteSet (Derivative r) 
-finite-derivative r = inject-fin (finSBTA r) (injSB r) ?
+finite-derivative r = inject-fin (finSBTA r) (injSB r) (decdb r)
 
 
 
--- a/automaton-in-agda/src/fin.agda	Mon Jul 10 14:28:39 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Tue Jul 11 11:04:00 2023 +0900
@@ -3,7 +3,7 @@
 module fin where
 
 open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ )
-open import Data.Fin.Properties hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties as DFP hiding (≤-trans ;  <-trans ;  ≤-refl  ) renaming ( <-cmp to <-fcmp )
 open import Data.Nat
 open import Data.Nat.Properties
 open import logic
@@ -132,7 +132,6 @@
 open import Data.List
 open import Relation.Binary.Definitions
 
-
 -----
 --
 -- find duplicate element in a List (Fin n)
@@ -140,6 +139,28 @@
 --    if the length is longer than n, we can find duplicate element as FDup-in-list 
 --
 
+record fDUP {n m : ℕ} (n<m :  n < m) ( f : Fin m → Fin n )  : Set where
+    field 
+      i j   : Fin m
+      dup : f i ≡ f j
+
+f-1 : (n m : ℕ) → (n<m : n < suc m ) → ( f : Fin (suc m) → Fin n ) → Fin m → Fin n 
+f-1 = ?
+
+n<m→fDUP : (n m : ℕ) → (n<m : n < m ) → ( f : Fin m → Fin n ) → fDUP n<m f
+n<m→fDUP n (suc m) (s≤s n≤m) f with ≤-∨ n≤m
+... | case1 eq = ?
+... | case2 n<m with n<m→fDUP n m ? (f-1 _ _ ? f )
+... | t = ?
+
+n<m→¬dup : {n m : ℕ} → n < m → ( f : Fin m → Fin n ) 
+   → ¬ ( (i j : Fin m)  → f i ≡ f j → i ≡ j )
+n<m→¬dup = ?
+
+list2func : (n : ℕ) → (x : List (Fin n)) → suc n < length x → Fin (length x) → Fin n
+list2func n (x ∷ t) n<x zero = x
+list2func n (x ∷ t) (s≤s n<x) (suc fx) = list2func n t ? fx
+
 -- fin-count : { n : ℕ }  (q : Fin n) (qs : List (Fin n) ) → ℕ
 -- fin-count q p[ = 0
 -- fin-count q (q0 ∷ qs ) with <-fcmp q q0 
@@ -181,11 +202,6 @@
 ... | tri≈ ¬a b ¬c = list-less ls
 ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls
 
-fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x
-fin010 {_} {_} {x} c = begin 
-           toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa))))  ≡⟨ toℕ-fromℕ< _ ⟩
-           toℕ x  ∎   where open ≡-Reasoning
-
 ---
 ---  if List (Fin n) is longer than n, there is at most one duplication
 ---
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 10 14:28:39 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 11 11:04:00 2023 +0900
@@ -609,7 +609,7 @@
    ... | yes isb = record {
         finite = suc (finite bp)
         ; Q←F =  info05
-        ; F←Q =  ?
+        ; F←Q =  info06
         ; finiso→ = ?
         ; finiso← = ?
         } where
@@ -631,10 +631,16 @@
           ... | tri> ¬a ¬b c = ?
    ... | no nisb = record {
         finite = finite bp
-        ; Q←F =  λ x → record { b = B<n.b ( Q←F ? x) ; b<n = ? }
-        ; F←Q =  ?
+        ; Q←F =  λ x → record { b = B<n.b ( Q←F bp x) ; b<n = ? }
+        ; F←Q =  info07
         ; finiso→ = ?
         ; finiso← = ?
         } where
           bp : FiniteSet (B<n n)
           bp = inf00 n (NP.≤-trans a≤sa le )
+          info07 : B<n (suc n) → Fin (finite bp)
+          info07 x with <-cmp (toℕ (F←Q fa (f (B<n.b x)))) n
+          ... | t = ?
+
+
+
--- a/automaton-in-agda/src/halt.agda	Mon Jul 10 14:28:39 2023 +0900
+++ b/automaton-in-agda/src/halt.agda	Tue Jul 11 11:04:00 2023 +0900
@@ -36,7 +36,7 @@
     diagn1 n dn = ¬t=f (diag b n ) ( begin
            not (diag b n)
         ≡⟨⟩
-           not (not fun← b n n)
+           not (not (fun← b n n))
         ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
            not (fun← b (fun→ b (diag b))  n)
         ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩