Mercurial > hg > Members > kono > Proof > automaton

changeset 373:d2bc08d03e99

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 Sun, 23 Jul 2023 11:05:31 +0900
parents cf98055f71b3
children 1feaa053e8d7
files automaton-in-agda/src/derive.agda
diffstat 1 files changed, 73 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda	Sat Jul 22 15:37:44 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Jul 23 11:05:31 2023 +0900
@@ -74,7 +74,7 @@
 
 -- open import nfa
 open import Data.Nat
-open import Data.Nat.Properties
+open import Data.Nat.Properties hiding ( eq? )
 open import nat
 open import finiteSetUtil
 open FiniteSet
@@ -100,33 +100,65 @@
     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|1 : (x y : Regex Σ) → (xn : ℕ) → SB x xn → SB (x || y)  (max (rank x) (rank y))
+    sb|2 : (x y : Regex Σ) → (yn : ℕ) → SB y yn → SB (x || y)  (max (rank x) (rank y))
     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)
 
 open import bijection using ( InjectiveF ; Is )  
 
+rank-eq : {r : Regex Σ} → {i : ℕ} → (a : SB r i)  → i ≡ rank r 
+rank-eq sbε = refl
+rank-eq sbφ = refl
+rank-eq (sb<> s) = refl
+rank-eq (sb|1 x y xn sb) = refl
+rank-eq (sb|2 x y yn sb) = refl
+rank-eq (sb* x xn sb) = cong suc ( rank-eq sb )
+rank-eq (sb& x y xn yn x₁ sb sb₁) = cong suc (trans (rank-eq sb₁) (sym ( x≤y→max=y _ _ (
+   begin
+   rank x ≡⟨ sym ( rank-eq sb) ⟩ 
+   xn <⟨ x₁ ⟩ 
+   yn ≡⟨ rank-eq sb₁ ⟩ 
+   rank y ∎ ) ))) where open ≤-Reasoning
+
+regex∨ : {r r₁ : Regex Σ} →  Bijection (SB r (rank r) ∨ SB r₁ (rank r₁)) (SB (r || r₁) (max (rank r) (rank r₁)))
+regex∨ {r} {r₁} =  record {  fun← = f1 ; fun→  = f2 ; fiso← = ? ;  fiso→ = ? } where
+     f1 : SB (r || r₁) (max (rank r) (rank r₁)) → SB r (rank r) ∨ SB r₁ (rank r₁)
+     f1 (sb|1 .r .r₁ xn x) = case1 ( subst (λ k → SB r k  ) (rank-eq x) x)
+     f1 (sb|2 .r .r₁ yn x) = case2 ( subst (λ k → SB r₁ k ) (rank-eq x) x)
+     f2 :  SB r (rank r) ∨ SB r₁ (rank r₁) → SB (r || r₁) (max (rank r) (rank r₁)) 
+     f2 (case1 sb) = sb|1 r r₁ (rank r ) sb
+     f2 (case2 sb) = sb|2 r r₁ (rank r₁) sb
+
 finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool)
 finSBTA r = fin→ ( fb00 (rank r) r ≤-refl ) where
     fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≤ n → FiniteSet (SB r (rank r))
-    fb00 n ε eq = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
+    fb00 n ε le = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
         fb01 :  (q : SB ε 0) → sbε ≡ q
         fb01 sbε = refl
-    fb00 zero φ eq = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
+    fb00 zero φ le = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
         fb01 :  (q : SB φ 0) → sbφ ≡ q
         fb01 sbφ = refl
-    fb00 zero (r || r₁) eq = iso-fin (fin-∨ (fb00 zero r ?) (fb00 zero r₁ ?)) ?
-    fb00 zero < x > eq = record { finite = 1 ; Q←F = λ _ → sb<> x ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
+    fb00 zero (r || r₁) le = iso-fin (fin-∨ (fb00 zero r (≤-trans (x≤max _ _) le)) (fb00 zero r₁ (≤-trans (y≤max _ _) le)))  regex∨
+    fb00 zero < x > le = record { finite = 1 ; Q←F = λ _ → sb<> x ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
         fb01 : (q : SB < x > 0) → sb<> x ≡ q
         fb01 (sb<> x) = refl
-    fb00 (suc n) (r *) eq = iso-fin (fb00 n r ?) ?
-    fb00 (suc n) (r & r₁) eq = iso-fin (fin-∧ (fb00 n r ?) (fb00 n r₁ ?)) ?
-    fb00 (suc n) (r || r₁) eq = iso-fin (fin-∨ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) ?
+    fb00 (suc n) (r *) le = iso-fin (fb00 n r ?) ?
+    fb00 (suc n) (r & r₁) le = iso-fin (fin-∧ (fb00 n r ?) (fb00 n r₁ ?)) ?
+    fb00 (suc n) (r || r₁) le = iso-fin (fin-∨ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) regex∨
     fb00 zero (x *) ()
     fb00 zero (x & x₁) ()
     fb00 (suc n) φ z≤n =  fb00 n φ z≤n 
     fb00 (suc n) < x > z≤n = fb00 n < x > z≤n 
 
+fb20 : {r s r₁ s₁ : Regex Σ} → r & r₁ ≡ s & s₁ → (r ≡ s ) ∧  (r₁ ≡ s₁ )
+fb20  refl = ⟪ refl , refl ⟫
+
+fb21 : {r s r₁ s₁ : Regex Σ} → r || r₁ ≡ s || s₁ → (r ≡ s ) ∧  (r₁ ≡ s₁ )
+fb21  refl = ⟪ refl , refl ⟫
+
+open _∧_ 
+
 dec-regex : (r s : Regex Σ) → Dec ( r ≡ s )
 dec-regex ε ε = yes refl
 dec-regex ε φ = no (λ ())
@@ -150,9 +182,36 @@
 dec-regex (r *) (s & s₁) = no (λ ())
 dec-regex (r *) (s || s₁) = no (λ ())
 dec-regex (r *) < x > = no (λ ())
-dec-regex (r & r₁) s = ?
-dec-regex (r || r₁) s = ?
-dec-regex < x > s = ?
+dec-regex (r & r₁) ε = no (λ ())
+dec-regex (r & r₁) φ = no (λ ())
+dec-regex (r & r₁) (s *) = no (λ ())
+dec-regex (r & r₁) (s & s₁) with dec-regex r s | dec-regex r₁ s₁
+... | yes y | yes y₁ = yes ( cong₂ _&_ y y₁)
+... | yes y | no n  = no (λ eq → n (proj2 (fb20 eq) ))
+... | no n  | yes y = no (λ eq → n (proj1 (fb20 eq) ))
+... | no n  | no n₁ = no (λ eq → n (proj1 (fb20 eq) ))
+dec-regex (r & r₁) (s || s₁) = no (λ ())
+dec-regex (r & r₁) < x > = no (λ ())
+dec-regex (r || r₁) ε = no (λ ())
+dec-regex (r || r₁) φ = no (λ ())
+dec-regex (r || r₁) (s *) = no (λ ())
+dec-regex (r || r₁) (s & s₁) = no (λ ())
+dec-regex (r || r₁) (s || s₁) with dec-regex r s | dec-regex r₁ s₁
+... | yes y | yes y₁ = yes ( cong₂ _||_ y y₁)
+... | yes y | no n  = no (λ eq → n (proj2 (fb21 eq) ))
+... | no n  | yes y = no (λ eq → n (proj1 (fb21 eq) ))
+... | no n  | no n₁ = no (λ eq → n (proj1 (fb21 eq) ))
+dec-regex (r || r₁) < x > = no (λ ())
+dec-regex < x > ε = no (λ ())
+dec-regex < x > φ = no (λ ())
+dec-regex < x > (s *) = no (λ ())
+dec-regex < x > (s & s₁) = no (λ ())
+dec-regex < x > (s || s₁) = no (λ ())
+dec-regex < x > < x₁ > with eq? x x₁
+... | yes y = yes (cong <_> y)
+... | no n = no (λ eq → n (fb11 eq))   where
+     fb11 : < x > ≡ < x₁ > → x ≡ x₁
+     fb11 refl = refl
 
 
 toSB : (r : Regex   Σ) →  SB r (rank r) → Bool
@@ -167,9 +226,10 @@
 sbempty? .ε sbε = true
 sbempty? .φ sbφ = false
 sbempty? .(< s >) (sb<> s) = false
-sbempty? .(x || y) (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) = sbempty? ? ? \/ sbempty? ? ?
 sbempty? .(x *) (sb* x .(rank x) sb) = true
 sbempty? .(x & y) (sb& x y xn .(max (rank x) (rank y)) x₁ sb sb₁) = sbempty? ? ? /\ sbempty? ? ?
+sbempty? .(x || y) (sb|1 x y xn sb) = ?
+sbempty? .(x || y) (sb|2 x y yn sb) = ?
 
 sbderive : (r : Regex Σ) →  (SB r (rank r) → Bool) → Σ → SB r (rank r) → Bool
 sbderive ε f s sbε = f sbε