Mercurial > hg > Members > kono > Proof > automaton

changeset 397:2e22a1f3a55a

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 Thu, 03 Aug 2023 18:13:59 +0900
parents f26444eb0275
children d7ea37e49f35
files automaton-in-agda/src/derive.agda automaton-in-agda/src/non-regular.agda
diffstat 2 files changed, 43 insertions(+), 98 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Thu Aug 03 17:32:50 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Thu Aug 03 18:13:59 2023 +0900
@@ -159,7 +159,9 @@
 rank < x > = 0
 
 data SB : (r s : Regex Σ) → Set where
-    sunit  : {r : Regex Σ} → SB r r
+    sε  : SB ε ε
+    sφ  : SB φ φ
+    s<> : {s : Σ} → SB < s >  < s > 
     sub|1  : {x y z : Regex Σ} → SB x z → SB (x || y) z
     sub|2  : {x y z : Regex Σ} → SB y z → SB (x || y) z
     sub*   : {x y : Regex Σ} → SB x y  → SB (x *) y
@@ -176,34 +178,31 @@
 open import bijection using ( InjectiveF ; Is )  
 
 finISB : (r : Regex Σ) → FiniteSet (ISB r)
-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 φ = 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 ε = record { finite = 1 ;  Q←F = λ _ → record { s = ε ; is-sub = sε } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
+    fb00 : (q : ISB ε) → record { s = ε ; is-sub = sε } ≡ q
+    fb00 record { s = .ε ; is-sub = sε } = refl
+    fb01 : (q : ISB ε) → record { s = ε ; is-sub = sε } ≡ q
+    fb01 record { s = .ε ; is-sub = sε } = refl
+finISB φ = record { finite = 1 ;  Q←F = λ _ → record { s = φ ; is-sub = sφ } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
+    fb00 : (q : ISB φ) → record { s = φ ; is-sub = sφ } ≡ q
+    fb00 record { s = .φ ; is-sub = sφ } = refl
+    fb01 : (q : ISB φ) → record { s = φ ; is-sub = sφ } ≡ q
+    fb01 record { s = .φ ; is-sub = sφ } = refl
+finISB < s > = record { finite = 1 ;  Q←F = λ _ → record { s = < s > ; is-sub = s<> } ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
+    fb00 : (q : ISB < s >) → record { s = < s > ; is-sub = s<> } ≡ q
+    fb00 record { s = < s > ; is-sub = s<> } = refl
+    fb01 : (q : ISB < s >) → record { s = < s > ; is-sub = s<> } ≡ q
+    fb01 record { s = < s > ; is-sub = s<> } = refl
+finISB (x || y) = iso-fin (fin-∨ (finISB x) (finISB y)) record { fun← = fb00 ; fun→ = fb01 ; fiso← = {!!} ; fiso→ = {!!} } where
+     fb00 : ISB (x || y) → ISB x ∨ ISB y
+     fb00 record { s = s ; is-sub = (sub|1 is-sub) } = case1 record { s = s ; is-sub = is-sub } 
+     fb00 record { s = s ; is-sub = (sub|2 is-sub) } = case2 record { s = s ; is-sub = is-sub } 
+     fb01 : ISB x ∨ ISB y → ISB (x || y)
+     fb01 (case1 record { s = s ; is-sub = is-sub }) = record { s = s ; is-sub = sub|1 is-sub  }
+     fb01 (case2 record { s = s ; is-sub = is-sub }) = record { s = s ; is-sub = sub|2 is-sub  }
+     fb02 : (x : ISB x ∨ ISB y) → fb00 (fb01 x) ≡ x
+     fb02 (case1 record { s = s ; is-sub = is-sub }) = refl
+     fb02 (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 
@@ -211,7 +210,6 @@
           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) } = {!!}
@@ -230,7 +228,6 @@
         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 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }
 
@@ -240,29 +237,31 @@
 ... | no _ = false
 
 sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
-sbempty? ε f with f record { s = ε ; is-sub = sunit  }
+sbempty? ε f with f record { s = ε ; is-sub = sε  }
 ... | true = true
 ... | false = false
 sbempty? φ f = false
-sbempty? (r *) f with f record { s = r * ; is-sub = sunit  }
+sbempty? (r *) f with f record { s = r * ; is-sub = sub* ?  }
 ... | true = true 
 ... | false = false 
-sbempty? (r & r₁) f with f record { s = r & r₁ ; is-sub = sunit  }
+sbempty? (r & r₁) f with f record { s = r & r₁ ; is-sub = sub&& ? ? ? ? ? }
 ... | false = false
 ... | true = empty? r /\ empty? r₁
-sbempty? (r || r₁) f with f record { s = r || r₁ ; is-sub = sunit  }
+sbempty? (r || r₁) f with f record { s = r || r₁ ; is-sub = ? }
 ... | false = false
 ... | true = empty? r \/ empty? r₁ 
 sbempty? < x > f = false
 
 sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
-sbderive ε f s record { s = .ε ; is-sub = sunit } = false
-sbderive φ f s record { s = t ; is-sub = is-sub } = false
-sbderive (r *) f s record { s = t ; is-sub = is-sub } = ?
-sbderive (r & r₁) f s record { s = t ; is-sub = is-sub } = ?
-sbderive (r || r₁) f s record { s = .(r || r₁) ; is-sub = sunit } = ?
-sbderive (r || r₁) f s record { s = t ; is-sub = (sub|1 is-sub) } = ?
-sbderive (r || r₁) f s record { s = t ; is-sub = (sub|2 is-sub) } = ?
+sbderive ε f s record { s = .ε ; is-sub = sε } = false
+sbderive φ f s record { s = t ; is-sub = sφ } = false
+sbderive (r *) f s record { s = t ; is-sub = (sub* is-sub) } = ?
+sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = (sub*& x .r x₁ is-sub) } = ?
+sbderive (r & r₁) f s record { s = t ; is-sub = (sub&1 .r .r₁ .t is-sub) } = ?
+sbderive (r & r₁) f s record { s = t ; is-sub = (sub&2 .r .r₁ .t is-sub) } = ?
+sbderive (r & r₁) f s record { s = .(z & r₁) ; is-sub = (sub&& .r .r₁ z x is-sub) } = ?
+sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|1 is-sub) } = ?
+sbderive (r || r₁) f s₁ record { s = s ; is-sub = (sub|2 is-sub) } = ?
 sbderive < x > f s record { s = t ; is-sub = is-sub } = ?
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
--- a/automaton-in-agda/src/non-regular.agda	Thu Aug 03 17:32:50 2023 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Thu Aug 03 18:13:59 2023 +0900
@@ -122,62 +122,8 @@
 top-is-i0 (i0 ∷ _) = true
 top-is-i0 (i1 ∷ _) = false
 
-nn02  : (x : List In2) → inputnn1 x ≡ true → x ≡ inputnn0 (half x)
-nn02 x eq  = nn08 x eq where
-     nn07 : (i : ℕ) → (x : List In2) → inputnn1-i1 i x ≡ true → x ≡ input-addi1 i
-     nn07 zero [] eq = refl
-     nn07 zero (i0 ∷ x₁) ()
-     nn07 zero (i1 ∷ x₁) ()
-     nn07 (suc i) (i1 ∷ x₁) eq = cong (λ k → i1 ∷ k) (nn07 i x₁ eq)
-     nn08 : (x : List In2 ) →  inputnn1-i1 (proj1 (inputnn1-i0 0 x)) (proj2 (inputnn1-i0 0 x)) ≡ true
-        → x ≡ input-addi0 (half x) (input-addi1 (half x))
-     nn08 [] eq = ? 
-     nn08 (i1 ∷ t) eq = ? 
-     nn08 (i0 ∷ []) eq = ?  
-     nn08 (i0 ∷ i1 ∷ t) eq = ?  
-     nn08 (i0 ∷ t @ (i0 ∷ _)) eq = ?  where
-         nn20 : top-is-i0 t ≡ true
-         nn20 = refl
-         y : List In2 → List In2
-         y [] = []
-         y (x ∷ [])  = []
-         y (x ∷ t ∷ z )  = x ∷ y (t ∷ z)
-         nn15 : ( x y : List In2) → length x ≡ suc (suc (length y)) → half x ≡ suc (half y)
-         nn15 (x ∷ x₁ ∷ []) [] eq = refl
-         nn15 (x ∷ x₁ ∷ x₃ ∷ []) (x₂ ∷ []) eq = refl
-         nn15 (x ∷ x₁ ∷ x₃ ∷ x₅ ∷ []) (x₂ ∷ x₄ ∷ []) eq = refl
-         nn15 (x ∷ x₁ ∷ x₃ ∷ x₅) (x₂ ∷ x₄ ∷ x₆ ∷ y₁) eq = cong suc (nn15 (x₃ ∷ x₅) (x₆ ∷ y₁) (cong pred (cong pred eq)) )
-         nn13 : (z : List In2) → half (i0 ∷ i0 ∷ z) ≡ suc (half (y (i0 ∷ z)))
-         nn13 z = nn15 (i0 ∷ i0 ∷ z) (y (i0 ∷ z)) ? where
-             nn17 : {x : In2} (z : List In2) →  length (y (i0 ∷ z)) ≡ length (y (x ∷ z))
-             nn17 [] = refl
-             nn17 (x ∷ []) = refl
-             nn17 (x ∷ x₁ ∷ z) = cong suc ( nn17 {x} (x₁ ∷ z)) 
-             nn16 : (z : List In2 ) → length (i0 ∷ i0 ∷ z) ≡ suc (suc (length (y (i0 ∷ z))))
-             nn16 [] = refl
-             nn16 (x ∷ z) = begin
-               length (i0 ∷ i0 ∷ x ∷ z) ≡⟨ refl ⟩
-               suc (length (i0 ∷ i0 ∷ z)) ≡⟨ cong suc (nn16 z) ⟩
-               suc (suc (suc (length (y (i0 ∷ z))))) ≡⟨ cong suc (cong suc ( cong suc (nn17 z))) ⟩
-               suc (suc (suc (length (y (x ∷ z))))) ≡⟨ refl ⟩
-               suc (suc (length (i0 ∷ y (x ∷ z)))) ∎ where open ≡-Reasoning
-         nn11 : (t : List In2) → inputnn1-i1 (proj1 (inputnn1-i0 0 t)) (proj2 (inputnn1-i0 0 t)) ≡ true
-            → top-is-i0 t ≡ true
-            → y t ++ (i1 ∷ []) ≡  t
-         nn11 [] eq ne = ?
-         nn11 (i0 ∷ t) eq ne = ?
-         nn11 (i1 ∷ []) eq ne = ?
-         nn11 (i1 ∷ i0 ∷ t) eq ne = ?
-         nn11 (i1 ∷ i1 ∷ t) eq ne = cong (i1 ∷_ ) (nn11 (i1 ∷ t) eq ? )
-         nn10  : (y : List In2 ) 
-            → inputnn1-i1 (proj1 (inputnn1-i0 0 y)) (proj2 (inputnn1-i0 0 y)) ≡ true
-            →  y ≡ input-addi0 (half y) (input-addi1 (half y))
-         nn10 y eq = nn08 y eq
-         nn14 :  inputnn1-i1 (proj1 (inputnn1-i0 0 (y t))) (proj2 (inputnn1-i0 0 (y t))) ≡ true
-         nn14 = ?
-         nn12 : i0 ∷ t ≡ input-addi0 (half (i0 ∷ t)) (input-addi1 (half (i0 ∷ t)))
-         nn12 = ?
-        
+-- if this is easy, we may have an easy proof
+-- nn02  : (x : List In2) → inputnn1 x ≡ true → x ≡ inputnn0 (half x)
 
 --
 --  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.