Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/derive.agda @ 402:093e386c10a2

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, 10 Aug 2023 09:59:47 +0900
parents 62a4d1a2c48d
children c298981108c1
comparison
equal deleted inserted replaced
401:62a4d1a2c48d 402:093e386c10a2
338 rg00 x (z ∷ y) record { state = φ ; is-derived = isd } refl = rg00 z y record { state = φ ; is-derived = derive isd z refl } refl 338 rg00 x (z ∷ y) record { state = φ ; is-derived = isd } refl = rg00 z y record { state = φ ; is-derived = derive isd z refl } refl
339 339
340 derive-ε : (r : Regex Σ) → (s : Σ) → r ≡ ε → derivative r s ≡ φ 340 derive-ε : (r : Regex Σ) → (s : Σ) → r ≡ ε → derivative r s ≡ φ
341 derive-ε r s refl = refl 341 derive-ε r s refl = refl
342 342
343 rg03-or : (x s : Σ) → {r r₁ : Regex Σ} → (derivative (r || r₁) s ≡ derivative r s ) ∨ (derivative (r || r₁) s ≡ derivative r₁ s )
344 ∨ (derivative (r || r₁) s ≡ derivative r s || derivative r₁ s )
345 rg03-or x s {r} {r₁} with derivative r s | derivative r₁ s
346 ... | φ | rr = case2 (case1 refl)
347 ... | ε | φ = case1 refl
348 ... | rr * | φ = case1 refl
349 ... | rr & rr₁ | φ = case1 refl
350 ... | rr || rr₁ | φ = case1 refl
351 ... | < x₁ > | φ = case1 refl
352 ... | ε | ε = case2 (case2 refl)
353 ... | rr * | ε = case2 (case2 refl)
354 ... | rr & rr₁ | ε = case2 (case2 refl)
355 ... | rr || rr₁ | ε = case2 (case2 refl)
356 ... | < x₁ > | ε = case2 (case2 refl)
357 ... | ε | rr₁ * = case2 (case2 refl)
358 ... | rr * | rr₁ * = case2 (case2 refl)
359 ... | rr & rr₂ | rr₁ * = case2 (case2 refl)
360 ... | rr || rr₂ | rr₁ * = case2 (case2 refl)
361 ... | < x₁ > | rr₁ * = case2 (case2 refl)
362 ... | rr | rr₁ & rr₂ = case2 (case2 ?)
363 ... | rr | rr₁ || rr₂ = case2 (case2 ?)
364 ... | rr | < x₁ > = case2 (case2 ?)
365
343 derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match r x 366 derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match r x
344 derive-is-regex-language ε [] = refl 367 derive-is-regex-language ε [] = refl
345 derive-is-regex-language ε (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) 368 derive-is-regex-language ε (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl)
346 derive-is-regex-language φ [] = refl 369 derive-is-regex-language φ [] = refl
347 derive-is-regex-language φ (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) 370 derive-is-regex-language φ (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl)
351 derive-is-regex-language (r *) (h ∷ x) = ? where 374 derive-is-regex-language (r *) (h ∷ x) = ? where
352 rg03 : (x s : Σ) → ? 375 rg03 : (x s : Σ) → ?
353 rg03 = ? 376 rg03 = ?
354 derive-is-regex-language (r & r₁) x = ? 377 derive-is-regex-language (r & r₁) x = ?
355 derive-is-regex-language (r || r₁) [] = cong₂ (λ j k → j \/ k ) (derive-is-regex-language r []) (derive-is-regex-language r₁ []) 378 derive-is-regex-language (r || r₁) [] = cong₂ (λ j k → j \/ k ) (derive-is-regex-language r []) (derive-is-regex-language r₁ [])
356 derive-is-regex-language (r || r₁) (x ∷ x₁) = ? 379 derive-is-regex-language (r || r₁) (x ∷ x₁) = ?
357 derive-is-regex-language < x₁ > [] = refl 380 derive-is-regex-language < x₁ > [] = refl
358 derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x 381 derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x
359 ... | yes _ = refl 382 ... | yes _ = refl
360 ... | no _ = refl 383 ... | no _ = refl
361 derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = sym rg02 where 384 derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = sym rg02 where
367 rg02 with rg03 x₁ x 390 rg02 with rg03 x₁ x
368 ... | case2 eq = rg00 x (x₂ ∷ x₃) record { state = _ ; is-derived = derive (unit refl) _ refl} eq 391 ... | case2 eq = rg00 x (x₂ ∷ x₃) record { state = _ ; is-derived = derive (unit refl) _ refl} eq
369 ... | case1 eq = rg00 x₂ x₃ record { state = _ ; is-derived = derive (derive (unit refl) _ refl) _ refl } (derive-ε _ _ eq ) 392 ... | case1 eq = rg00 x₂ x₃ record { state = _ ; is-derived = derive (derive (unit refl) _ refl) _ refl } (derive-ε _ _ eq )
370 -- immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b) 393 -- immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b)
371 394
372 derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-match r x ≡ regex-match1 r x 395 derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match1 r x
373 derive=ISB ε [] = refl 396 derive=ISB ε [] = refl
374 derive=ISB ε (x ∷ x₁) = ? 397 derive=ISB ε (x ∷ x₁) = ?
375 derive=ISB φ [] = refl 398 derive=ISB φ [] = refl
376 derive=ISB φ (x ∷ x₁) = ? 399 derive=ISB φ (x ∷ x₁) = ?
377 derive=ISB (r *) x = ? 400 derive=ISB (r *) x = ?
381 derive=ISB < x₁ > (x ∷ []) with eq? x₁ x 404 derive=ISB < x₁ > (x ∷ []) with eq? x₁ x
382 ... | yes _ = refl 405 ... | yes _ = refl
383 ... | no _ = refl 406 ... | no _ = refl
384 derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ? 407 derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ?
385 408
386 ISB-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡ regex-match1 r x 409
387 ISB-is-regex-language r x = trans ( derive-is-regex-language r x ) (derive=ISB r x) 410
388 411
389
390