Mercurial > hg > Members > kono > Proof > automaton

changeset 382:9fba498b0a7a

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, 24 Jul 2023 19:01:09 +0900
parents 113330c6e896
children 708570e55a91
files automaton-in-agda/src/derive.agda automaton-in-agda/src/regex1.agda
diffstat 2 files changed, 85 insertions(+), 44 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 15:49:41 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 19:01:09 2023 +0900
@@ -175,39 +175,64 @@
 
 open import bijection using ( InjectiveF ; Is )  
 
-finISB2 : {r z : Regex Σ} → FiniteSet (ISB z) → FiniteSet (SB r z)
-finISB2 = ?
-
 finISB : (r : Regex Σ) → FiniteSet (ISB r)
-finISB ε = record { finite = 1 ;  Q←F = λ _ → record { s = ε ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = fin1≡0  } where
+finISB ε = record { finite = 1 ;  Q←F = λ _ → record { s = ε ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
     fb00 : (q : ISB ε) → record { s = ε ; is-sub = sunit } ≡ q
     fb00 record { s = .ε ; is-sub = sunit } = refl
-finISB φ = ?
-finISB < x > = ?
-finISB (x || y) = iso-fin (fin-∨1 (fin-∨ (finISB x) (finISB y))) ? where
-     fb00 : ISB (x || y) → ?
-     fb00 record { s = .(x || y) ; is-sub = sunit } = ?
-     fb00 record { s = s ; is-sub = (sub|1 is-sub) } = ?
-     fb00 record { s = s ; is-sub = (sub|2 is-sub) } = ?
-finISB (x & y) = iso-fin (fin-∨ (inject-fin (finISB y) ? ?) (fin-∨1 (fin-∨ (finISB x) (finISB y)))) ? where
-     fb00 : ISB (x & y) → ?
-     fb00 record { s = .(x & y) ; is-sub = sunit } = ?
-     fb00 record { s = s ; is-sub = (sub&1 .x .y .s is-sub) } = ?
-     fb00 record { s = s ; is-sub = (sub&2 .x .y .s is-sub) } = ?
-     fb00 record { s = (z & y) ; is-sub = (sub&& x y z lt is-sub) } = ?
-finISB (x *) = iso-fin (fin-∨ (inject-fin (finISB x) fi ? ) (fin-∨1 (finISB x) )) record { fun← = fb00 } where
+    fb01 : (q : ISB ε) → record { s = ε ; is-sub = sunit } ≡ q
+    fb01 record { s = .ε ; is-sub = sunit } = refl
+finISB φ = record { finite = 1 ;  Q←F = λ _ → record { s = φ ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
+    fb00 : (q : ISB φ) → record { s = φ ; is-sub = sunit } ≡ q
+    fb00 record { s = .φ ; is-sub = sunit } = refl
+    fb01 : (q : ISB φ) → record { s = φ ; is-sub = sunit } ≡ q
+    fb01 record { s = .φ ; is-sub = sunit } = refl
+finISB < s > = record { finite = 1 ;  Q←F = λ _ → record { s = < s > ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
+    fb00 : (q : ISB < s >) → record { s = < s > ; is-sub = sunit } ≡ q
+    fb00 record { s = < s > ; is-sub = sunit } = refl
+    fb01 : (q : ISB < s >) → record { s = < s > ; is-sub = sunit } ≡ q
+    fb01 record { s = < s > ; is-sub = sunit } = refl
+finISB (x || y) = iso-fin (fin-∨1 (fin-∨ (finISB x) (finISB y))) record { fun← = fb00 ; fun→ = fb01 ; fiso← = {!!} ; fiso→ = {!!} } where
+     fb00 : ISB (x || y) → One ∨ ISB x ∨ ISB y
+     fb00 record { s = .(x || y) ; is-sub = sunit } = case1 one
+     fb00 record { s = s ; is-sub = (sub|1 is-sub) } = case2 (case1 record { s = s ; is-sub = is-sub } )
+     fb00 record { s = s ; is-sub = (sub|2 is-sub) } = case2 (case2 record { s = s ; is-sub = is-sub } )
+     fb01 : One ∨ ISB x ∨ ISB y → ISB (x || y)
+     fb01 (case1 one) = record { s = (x || y) ; is-sub = sunit } 
+     fb01 (case2 (case1 record { s = s ; is-sub = is-sub })) = record { s = s ; is-sub = sub|1 is-sub  }
+     fb01 (case2 (case2 record { s = s ; is-sub = is-sub })) = record { s = s ; is-sub = sub|2 is-sub  }
+     fb02 : (x : One ∨ ISB x ∨ ISB y) → fb00 (fb01 x) ≡ x
+     fb02 (case1 one) = refl
+     fb02 (case2 (case1 record { s = s ; is-sub = is-sub })) = refl
+     fb02 (case2 (case2 record { s = s ; is-sub = is-sub })) = refl
+
+finISB (x & y) = iso-fin (fin-∨ (inject-fin (fin-∧ (finISB x) (finISB y)) fi {!!}) (fin-∨1 (fin-∨ (finISB x) (finISB y)))) {!!} where
+     record Z : Set where
+        field 
+          x1 y1 z : Regex Σ
+          lt : rank z < suc (max (rank x1) (rank z))
+          is-sub : SB x1 z
+     fb00 : ISB (x & y) → {!!}
+     fb00 record { s = .(x & y) ; is-sub = sunit } = {!!}
+     fb00 record { s = s ; is-sub = (sub&1 .x .y .s is-sub) } = {!!}
+     fb00 record { s = s ; is-sub = (sub&2 .x .y .s is-sub) } = {!!}
+     fb00 record { s = (z & y) ; is-sub = (sub&& x y z lt is-sub) } = {!!}
+     fi : InjectiveF Z (ISB x ∧ ISB y)
+     fi = record { f = f ; inject = {!!} } where
+        f : Z → ISB x ∧ ISB y
+        f z = ⟪ record { s = Z.x1 z ; is-sub = {!!} }  , {!!} ⟫
+finISB (x *) = iso-fin (fin-∨ (inject-fin (finISB x) fi {!!} ) (fin-∨1 (finISB x) )) record { fun← = fb00 } where
      record Z : Set where
         field 
           z : Regex Σ
           lt : rank z < rank x
           is-sub : SB x z
      fi : InjectiveF Z (ISB x) 
-     fi = record { f = f ; inject = ? } where
+     fi = record { f = f ; inject = {!!} } where
         f : Z → ISB x
         f z = record { s = Z.z z ; is-sub = Z.is-sub z }
-     fb00 : ISB (x *) → ?
-     fb00 record { s = .(x *) ; is-sub = sunit } = ?
-     fb00 record { s = s ; is-sub = (sub* is-sub) } = ?
+     fb00 : ISB (x *) → {!!}
+     fb00 record { s = .(x *) ; is-sub = sunit } = {!!}
+     fb00 record { s = s ; is-sub = (sub* is-sub) } = {!!}
      fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }
 
 toSB : (r : Regex   Σ) →  ISB r → Bool
@@ -231,13 +256,29 @@
 ... | true = empty? r \/ empty? r₁ 
 sbempty? < x > f = false
 
-sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r  → Bool
+sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
 sbderive r f s record { s = t ; is-sub = is-sub } with rg-eq? (derivative r s) t | f record { s = r ; is-sub = sunit  }
 ... | yes _ | true = true
 ... | no _ | true = false
 ... | yes _ | false = false
 ... | no _ | false = false
 
+open import regex1
+
+ISB→Regex : (r : Regex Σ) →  (ISB r → Bool) → Regex Σ
+ISB→Regex ε f with f record { s = ε ; is-sub = sunit  }
+... | true = ε
+... | false = φ
+ISB→Regex φ f = φ
+ISB→Regex (r *) f = {!!}
+ISB→Regex (r & r₁) f = {!!}
+ISB→Regex (r || r₁) f = {!!}
+ISB→Regex < x > f = {!!}
+
+lem00 : (r : Regex Σ) → (z : Σ) (x : List Σ )→ regex-language r eq? (z ∷ x ) ≡  
+                                               regex-language (ISB→Regex r (λ isb → (sbderive r (toSB r ) z isb)))  eq? x  
+lem00 r z x = {!!}
+
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
 
--- a/automaton-in-agda/src/regex1.agda	Mon Jul 24 15:49:41 2023 +0900
+++ b/automaton-in-agda/src/regex1.agda	Mon Jul 24 19:01:09 2023 +0900
@@ -75,18 +75,18 @@
 
 -- Meaning of regular expression
 
-regular-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y))  →  List Σ → Bool
-regular-language φ cmp _ = false
-regular-language ε cmp [] = true
-regular-language ε cmp (_ ∷ _) = false
-regular-language (x *) cmp = repeat ( regular-language x cmp  )
-regular-language (x & y) cmp  = split ( λ z → regular-language x  cmp z ) (λ z →  regular-language y  cmp z )
-regular-language (x || y) cmp  = λ s → ( regular-language x  cmp s )  \/  ( regular-language y  cmp s)
-regular-language < h > cmp  [] = false
-regular-language < h > cmp  (h1  ∷ [] ) with cmp h h1
+regex-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y))  →  List Σ → Bool
+regex-language φ cmp _ = false
+regex-language ε cmp [] = true
+regex-language ε cmp (_ ∷ _) = false
+regex-language (x *) cmp = repeat ( regex-language x cmp  )
+regex-language (x & y) cmp  = split ( λ z → regex-language x  cmp z ) (λ z →  regex-language y  cmp z )
+regex-language (x || y) cmp  = λ s → ( regex-language x  cmp s )  \/  ( regex-language y  cmp s)
+regex-language < h > cmp  [] = false
+regex-language < h > cmp  (h1  ∷ [] ) with cmp h h1
 ... | yes _ = true
 ... | no _  = false
-regular-language < h >  _ (_ ∷ _ ∷ _)  = false
+regex-language < h >  _ (_ ∷ _ ∷ _)  = false
 
 cmpi : (x y : In ) → Dec (x ≡ y)
 cmpi a a = yes refl
@@ -106,13 +106,13 @@
 cmpi d b = no (λ ()) 
 cmpi d c = no (λ ()) 
 
-test-regex : regular-language r1' cmpi ( a ∷ [] ) ≡ false
+test-regex : regex-language r1' cmpi ( a ∷ [] ) ≡ false
 test-regex = refl
 
--- test-regex2 : regular-language r2 cmpi ( b ∷ c ∷ a ∷ b ∷ [] ) ≡ false
+-- test-regex2 : regex-language r2 cmpi ( b ∷ c ∷ a ∷ b ∷ [] ) ≡ false
 -- test-regex2 = refl
 
-test-regex1 : regular-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true
+test-regex1 : regex-language r2 cmpi ( a ∷ a ∷ b ∷ c ∷ [] ) ≡ true
 test-regex1 = refl
 
                                                                                                                     
@@ -138,10 +138,10 @@
 -- from example 1.53 1
 
 ex53-1 : Set 
-ex53-1 = (s : List In ) → regular-language ( (< a > *) & < b > & (< a > *) ) cmpi s ≡ true → {!!} -- contains exact one b
+ex53-1 = (s : List In ) → regex-language ( (< a > *) & < b > & (< a > *) ) cmpi s ≡ true → {!!} -- contains exact one b
 
 ex53-2 : Set 
-ex53-2 = (s : List In ) → regular-language ( (any * ) & < b > & (any *) ) cmpi s ≡ true → {!!} -- contains at lease one b
+ex53-2 = (s : List In ) → regex-language ( (any * ) & < b > & (any *) ) cmpi s ≡ true → {!!} -- contains at lease one b
 
 evenp : {Σ : Set} →  List Σ → Bool
 oddp : {Σ : Set} →  List Σ → Bool
@@ -153,10 +153,10 @@
 
 -- from example 1.53 5
 egex-even : Set
-egex-even = (s : List In ) → regular-language ( ( any & any ) * ) cmpi s ≡ true → evenp s ≡ true
+egex-even = (s : List In ) → regex-language ( ( any & any ) * ) cmpi s ≡ true → evenp s ≡ true
 
-test11 =  regular-language ( ( any & any ) * ) cmpi (a ∷ [])
-test12 =  regular-language ( ( any & any ) * ) cmpi (a ∷ b ∷ [])
+test11 =  regex-language ( ( any & any ) * ) cmpi (a ∷ [])
+test12 =  regex-language ( ( any & any ) * ) cmpi (a ∷ b ∷ [])
 
 -- proof-egex-even : egex-even 
 -- proof-egex-even [] _ = refl
@@ -199,8 +199,8 @@
      finiso←0 (suc (suc (suc zero))) = refl
 
 
-open import derive In iFin
-open import automaton
+-- open import derive In iFin
+-- open import automaton
 
-ra-ex = trace (regex→automaton cmpi r2) (record { state = r2 ; is-derived = unit }) ( a ∷ b ∷ c ∷ [])
+-- ra-ex = trace (regex→automaton cmpi r2) (record { state = r2 ; is-derived = unit refl }) ( a ∷ b ∷ c ∷ [])