# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1690139692 -32400
# Node ID 1feaa053e8d7fc7e45dd24497df6cc50e3045db5
# Parent  d2bc08d03e9941a33a4df876c0670c8fa9d0c03c
.. another one

diff -r d2bc08d03e99 -r 1feaa053e8d7 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Sun Jul 23 11:05:31 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 04:14:52 2023 +0900
@@ -88,6 +88,68 @@
 
 open import Relation.Binary.Definitions
 
+open _∧_ 
+
+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 ⟫
+
+rg-eq? : (r s : Regex Σ) → Dec ( r ≡ s )
+rg-eq? ε ε = yes refl
+rg-eq? ε φ = no (λ ())
+rg-eq? ε (s *) = no (λ ())
+rg-eq? ε (s & s₁) = no (λ ())
+rg-eq? ε (s || s₁) = no (λ ())
+rg-eq? ε < x > = no (λ ())
+rg-eq? φ ε = no (λ ())
+rg-eq? φ φ = yes refl
+rg-eq? φ (s *) = no (λ ())
+rg-eq? φ (s & s₁) = no (λ ())
+rg-eq? φ (s || s₁) = no (λ ())
+rg-eq? φ < x > = no (λ ())
+rg-eq? (r *) ε = no (λ ())
+rg-eq? (r *) φ = no (λ ())
+rg-eq? (r *) (s *) with rg-eq? r s
+... | yes eq = yes ( cong (_*) eq)
+... | no ne = no (λ eq → ne (fb10 eq) ) where
+     fb10 : {r s : Regex Σ} → (r *) ≡ (s *) → r ≡ s 
+     fb10  refl = refl
+rg-eq? (r *) (s & s₁) = no (λ ())
+rg-eq? (r *) (s || s₁) = no (λ ())
+rg-eq? (r *) < x > = no (λ ())
+rg-eq? (r & r₁) ε = no (λ ())
+rg-eq? (r & r₁) φ = no (λ ())
+rg-eq? (r & r₁) (s *) = no (λ ())
+rg-eq? (r & r₁) (s & s₁) with rg-eq? r s | rg-eq? 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) ))
+rg-eq? (r & r₁) (s || s₁) = no (λ ())
+rg-eq? (r & r₁) < x > = no (λ ())
+rg-eq? (r || r₁) ε = no (λ ())
+rg-eq? (r || r₁) φ = no (λ ())
+rg-eq? (r || r₁) (s *) = no (λ ())
+rg-eq? (r || r₁) (s & s₁) = no (λ ())
+rg-eq? (r || r₁) (s || s₁) with rg-eq? r s | rg-eq? 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) ))
+rg-eq? (r || r₁) < x > = no (λ ())
+rg-eq? < x > ε = no (λ ())
+rg-eq? < x > φ = no (λ ())
+rg-eq? < x > (s *) = no (λ ())
+rg-eq? < x > (s & s₁) = no (λ ())
+rg-eq? < x > (s || s₁) = no (λ ())
+rg-eq? < 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
+
 rank : (r : Regex Σ) → ℕ
 rank ε = 0
 rank φ = 0
@@ -96,151 +158,45 @@
 rank (r || r₁) = max (rank r) (rank r₁)
 rank < x > = 0
 
-data SB : (r : Regex Σ) → (rn : ℕ) → Set where
-    sbε : SB ε 0
-    sbφ : SB φ 0
-    sb<> : (s : Σ) → SB < s > 0
-    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)
+data SB : (r s : Regex Σ) → Set where
+    sunit  : {r : Regex Σ} → SB r r
+    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
+    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 Σ) → rank x < rank y  → SB x y → SB y (x & y) 
+
+record ISB (r : Regex Σ) : Set where
+    field
+        s : Regex Σ
+        is-sub : SB r s
 
 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 ε 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 φ 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₁) 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 *) 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 (λ ())
-dec-regex ε (s *) = no (λ ())
-dec-regex ε (s & s₁) = no (λ ())
-dec-regex ε (s || s₁) = no (λ ())
-dec-regex ε < x > = no (λ ())
-dec-regex φ ε = no (λ ())
-dec-regex φ φ = yes refl
-dec-regex φ (s *) = no (λ ())
-dec-regex φ (s & s₁) = no (λ ())
-dec-regex φ (s || s₁) = no (λ ())
-dec-regex φ < x > = no (λ ())
-dec-regex (r *) ε = no (λ ())
-dec-regex (r *) φ = no (λ ())
-dec-regex (r *) (s *) with dec-regex r s
-... | yes eq = yes ( cong (_*) eq)
-... | no ne = no (λ eq → ne (fb10 eq) ) where
-     fb10 : {r s : Regex Σ} → (r *) ≡ (s *) → r ≡ s 
-     fb10  refl = refl
-dec-regex (r *) (s & s₁) = no (λ ())
-dec-regex (r *) (s || s₁) = no (λ ())
-dec-regex (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₁) 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
+finSB : (r : Regex Σ) → FiniteSet (ISB r)
+finSB = ?
 
 
-toSB : (r : Regex   Σ) →  SB r (rank r) → Bool
-toSB ε sbε = true
-toSB φ sbφ = true
-toSB (r *) (sb* .r .(rank r) x) = toSB r x
-toSB (r & r₁) (sb& .r .r₁ xn .(max (rank r) (rank r₁)) x<m x₁ x₂) = toSB r ?  /\ toSB r₁ ?
-toSB (r || r₁) x = toSB r ?  \/ toSB r₁ ?
-toSB < x₁ > (sb<> .x₁) = true
+toSB : (r : Regex   Σ) →  ISB r → Bool
+toSB r isb with rg-eq? r (ISB.s isb)
+... | yes _ = true
+... | no _ = false
+
+sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
+sbempty? r = ?
 
-sbempty? : (r : Regex Σ) → SB r (rank r) → Bool
-sbempty? .ε sbε = true
-sbempty? .φ sbφ = false
-sbempty? .(< s >) (sb<> s) = false
-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 Σ) →  (ISB r → Bool) → Σ → ISB r  → Bool
+sbderive = ?
+
+-- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
+--    this is not correct because it contains s || s || s || .....
 
-sbderive : (r : Regex Σ) →  (SB r (rank r) → Bool) → Σ → SB r (rank r) → Bool
-sbderive ε f s sbε = f sbε
-sbderive φ f s sbφ = false
-sbderive (r *) f s (sb* .r .(rank r) sb) = ?
-sbderive (r & r₁) f s sb = ?
-sbderive (r || r₁) f s sb = ?
-sbderive < x > f s sb = ?
+finSBTA : (r : Regex Σ) → FiniteSet (ISB r → Bool)
+finSBTA r = fin→ ( finSB r )
 
-regex→automaton1 : (r : Regex   Σ) → Automaton (SB r (rank r) → Bool) Σ
-regex→automaton1 r = record { δ = sbderive r ; aend = λ d → ? }  
+regex→automaton1 : (r : Regex   Σ) → Automaton (ISB r  → Bool) Σ
+regex→automaton1 r = record { δ = sbderive r ; aend = sbempty? r }
 
 regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool
 regex-match1 r is = accept ( regex→automaton1 r ) (λ sb → toSB r sb) is