Mercurial > hg > Members > kono > Proof > automaton
changeset 402:093e386c10a2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 10 Aug 2023 09:59:47 +0900 |
| parents | 62a4d1a2c48d |
| children | c298981108c1 |
| files | automaton-in-agda/src/derive.agda |
| diffstat | 1 files changed, 25 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/derive.agda Thu Aug 10 09:29:03 2023 +0900 +++ b/automaton-in-agda/src/derive.agda Thu Aug 10 09:59:47 2023 +0900 @@ -340,6 +340,29 @@ derive-ε : (r : Regex Σ) → (s : Σ) → r ≡ ε → derivative r s ≡ φ derive-ε r s refl = refl +rg03-or : (x s : Σ) → {r r₁ : Regex Σ} → (derivative (r || r₁) s ≡ derivative r s ) ∨ (derivative (r || r₁) s ≡ derivative r₁ s ) + ∨ (derivative (r || r₁) s ≡ derivative r s || derivative r₁ s ) +rg03-or x s {r} {r₁} with derivative r s | derivative r₁ s +... | φ | rr = case2 (case1 refl) +... | ε | φ = case1 refl +... | rr * | φ = case1 refl +... | rr & rr₁ | φ = case1 refl +... | rr || rr₁ | φ = case1 refl +... | < x₁ > | φ = case1 refl +... | ε | ε = case2 (case2 refl) +... | rr * | ε = case2 (case2 refl) +... | rr & rr₁ | ε = case2 (case2 refl) +... | rr || rr₁ | ε = case2 (case2 refl) +... | < x₁ > | ε = case2 (case2 refl) +... | ε | rr₁ * = case2 (case2 refl) +... | rr * | rr₁ * = case2 (case2 refl) +... | rr & rr₂ | rr₁ * = case2 (case2 refl) +... | rr || rr₂ | rr₁ * = case2 (case2 refl) +... | < x₁ > | rr₁ * = case2 (case2 refl) +... | rr | rr₁ & rr₂ = case2 (case2 ?) +... | rr | rr₁ || rr₂ = case2 (case2 ?) +... | rr | < x₁ > = case2 (case2 ?) + derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match r x derive-is-regex-language ε [] = refl derive-is-regex-language ε (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) @@ -353,7 +376,7 @@ rg03 = ? derive-is-regex-language (r & r₁) x = ? derive-is-regex-language (r || r₁) [] = cong₂ (λ j k → j \/ k ) (derive-is-regex-language r []) (derive-is-regex-language r₁ []) -derive-is-regex-language (r || r₁) (x ∷ x₁) = ? +derive-is-regex-language (r || r₁) (x ∷ x₁) = ? derive-is-regex-language < x₁ > [] = refl derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x ... | yes _ = refl @@ -369,7 +392,7 @@ ... | case1 eq = rg00 x₂ x₃ record { state = _ ; is-derived = derive (derive (unit refl) _ refl) _ refl } (derive-ε _ _ eq ) -- immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b) -derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-match r x ≡ regex-match1 r x +derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match1 r x derive=ISB ε [] = refl derive=ISB ε (x ∷ x₁) = ? derive=ISB φ [] = refl @@ -383,8 +406,6 @@ ... | no _ = refl derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ? -ISB-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match1 r x -ISB-is-regex-language r x = trans ( derive-is-regex-language r x ) (derive=ISB r x)