open import lib open import sum module grammar (form : Set)(_eq_ : form β†’ form β†’ 𝔹)(drop-form : (x y : form) β†’ x ≑ y β†’ x eq y ≑ tt)(rise-form : (x y : form) β†’ x eq y ≑ tt β†’ x ≑ y) where infix 7 _β‡’_ data production : Set where _β‡’_ : form β†’ 𝕃 (form ⊎ char) β†’ production record grammar {numprods : β„•} : Set where constructor _,_ field start : form prods : 𝕍 production numprods open grammar splice : β„• β†’ 𝕃 (form ⊎ char) β†’ form β†’ 𝕃 (form ⊎ char) β†’ 𝕃 (form ⊎ char) splice x [] _ _ = [] splice 0 ((inj₁ s) :: ss) s' ss' with s eq s' ... | tt = ss' ++ ss ... | ff = (inj₁ s) :: ss splice 0 (x :: ss) s' ss' = x :: ss splice (suc n) (s :: ss) s' ss' = s :: splice n ss s' ss' 𝕃injβ‚‚ : βˆ€{β„“ β„“'}{B : Set β„“}{A : Set β„“'} β†’ 𝕃 A β†’ 𝕃 (B ⊎ A) 𝕃injβ‚‚ (x :: xs) = (injβ‚‚ x) :: 𝕃injβ‚‚ xs 𝕃injβ‚‚ [] = [] 𝕃inj₁ : βˆ€{β„“ β„“'}{B : Set β„“}{A : Set β„“'} β†’ 𝕃 A β†’ 𝕃 (A ⊎ B) 𝕃inj₁ (x :: xs) = (inj₁ x) :: 𝕃inj₁ xs 𝕃inj₁ [] = [] data derivation{numprods : β„•} {g : grammar{numprods}} : 𝕃 (form ⊎ char) β†’ 𝕃 char β†’ Set where end : {ss : 𝕃 char} β†’ derivation (𝕃injβ‚‚ ss) ss step : βˆ€ {ss1 ss1' : 𝕃 (form ⊎ char)}{ss2 : 𝕃 char}{s : form}{ss : 𝕃 (form ⊎ char)} β†’ (m n : β„•) β†’ (p : n < numprods ≑ tt) β†’ nth𝕍 n p (prods g) ≑ (s β‡’ ss) β†’ m < length ss1 ≑ tt β†’ splice m ss1 s ss ≑ ss1' β†’ derivation {g = g} ss1' ss2 β†’ derivation ss1 ss2 splice-concat : βˆ€{l1 l2 target final : 𝕃 (form ⊎ char)}{n : β„•}{slice : form} β†’ splice n l1 slice target ≑ final β†’ splice (n + (length l2)) (l2 ++ l1) slice target ≑ l2 ++ final splice-concat{l2 = []}{n = n} pr rewrite +0 n = pr splice-concat{l1}{x :: xs}{n = n} pr rewrite +suc n (length xs) | splice-concat{l1}{l2 = xs} pr = refl _=form⊎char_ : (x y : form ⊎ char) β†’ 𝔹 _=form⊎char_ = =⊎ _eq_ _=char_ form⊎char-drop : (x y : form ⊎ char) β†’ x ≑ y β†’ x =form⊎char y ≑ tt form⊎char-drop = β‰‘βŠŽ-to-= _eq_ _=char_ drop-form ≑char-to-= form⊎char-rise : (x y : form ⊎ char) β†’ x =form⊎char y ≑ tt β†’ x ≑ y form⊎char-rise = =⊎-to-≑ _eq_ _=char_ rise-form =char-to-≑ splice-concat2 : βˆ€{l1 l2 target final : 𝕃 (form ⊎ char)}{n : β„•}{slice : form} β†’ splice n l1 slice target ≑ final β†’ n < length l1 ≑ tt β†’ splice n (l1 ++ l2) slice target ≑ final ++ l2 splice-concat2{[]}{n = n} pr1 pr2 rewrite <-0 n = 𝔹-contra pr2 splice-concat2{inj₁ x :: xs}{l2}{target}{n = 0}{slice} pr1 pr2 with x eq slice ...| tt rewrite (sym pr1) | ++[] target | ++-assoc target xs l2 = refl ...| ff rewrite (sym pr1) = refl splice-concat2{injβ‚‚ x :: xs}{l2}{target}{n = 0}{slice} pr1 pr2 rewrite (sym pr1) = refl splice-concat2{x :: xs}{l2}{target}{[]}{suc n} pr1 pr2 with pr1 ...| () splice-concat2{x :: xs}{l2}{target}{f :: fs}{suc n}{slice} pr1 pr2 with =𝕃-from-≑ _=form⊎char_ form⊎char-drop pr1 ...| s1 rewrite splice-concat2{xs}{l2}{target}{fs}{n}{slice} (≑𝕃-from-={l1 = splice n xs slice target}{fs} _=form⊎char_ form⊎char-rise (&&-snd{x =form⊎char f} s1)) pr2 | form⊎char-rise x f (&&-fst{x =form⊎char f} s1) = refl length+ : βˆ€{β„“}{A : Set β„“}(l1 l2 : 𝕃 A) β†’ length (l1 ++ l2) ≑ length l1 + length l2 length+ [] l2 = refl length+ (x :: xs) l2 rewrite length+ xs l2 = refl <-h1 : βˆ€{x y a : β„•} β†’ x < y ≑ tt β†’ x + a < y + a ≑ tt <-h1{x}{y}{0} p rewrite +0 x | +0 y = p <-h1{x}{y}{suc n} p rewrite +suc y n | +suc x n = <-h1{x}{y}{n} p <-h2 : βˆ€{a x y : β„•} β†’ a < x ≑ tt β†’ a < x + y ≑ tt <-h2{a}{x}{0} p rewrite +0 x = p <-h2{a}{x}{suc y} p rewrite +suc x y with <-h2{a}{x}{y} p | <-suc (x + y) ...| pr1 | pr2 = <-trans{a}{x + y}{suc (x + y)} pr1 pr2 length𝕃injβ‚‚ : βˆ€{β„“ β„“'}{A : Set β„“}{B : Set β„“'} β†’ (l : 𝕃 A) β†’ length (𝕃injβ‚‚{B = B} l) ≑ length l length𝕃injβ‚‚{B = B} (x :: xs) rewrite length𝕃injβ‚‚{B = B} xs = refl length𝕃injβ‚‚ [] = refl 𝕃injβ‚‚++ : βˆ€{β„“ β„“'}{A : Set β„“}{B : Set β„“'} β†’ (l1 l2 : 𝕃 A) β†’ 𝕃injβ‚‚{B = B} (l1 ++ l2) ≑ 𝕃injβ‚‚ l1 ++ 𝕃injβ‚‚ l2 𝕃injβ‚‚++ [] l2 = refl 𝕃injβ‚‚++{B = B} (x :: xs) l2 rewrite 𝕃injβ‚‚++{B = B} xs l2 = refl infixr 10 _deriv++_ _deriv++_ : {l2 l4 : 𝕃 char}{l1 l3 : 𝕃 (form ⊎ char)}{n : β„•}{gr : grammar{n}} β†’ derivation{g = gr} l1 l2 β†’ derivation{g = gr} l3 l4 β†’ derivation{g = gr} (l1 ++ l3) (l2 ++ l4) _deriv++_{l2}{l4} end end rewrite sym (𝕃injβ‚‚++{B = form} l2 l4) = end _deriv++_{l2}{l4}{l1}{l3} f (step{ss1' = ss1'}{s = s}{ss} a b pr1 pr2 pr3 pr4 next) with <-h1{a}{length l3}{length l1} pr3 ...| pr5 rewrite +comm (length l3) (length l1) | (sym (length+ l1 l3)) = step{ss1 = l1 ++ l3}{l1 ++ ss1'}{l2 ++ l4} (a + (length l1)) b pr1 pr2 pr5 (splice-concat{l3}{l1} pr4) (_deriv++_ f next) _deriv++_{l2}{l4}{l1} (step{ss1' = ss1'}{s = s}{ss} a b pr1 pr2 pr3 pr4 next) end with <-h2{a}{length l1}{length (𝕃injβ‚‚{B = form} l4)} pr3 ...| pr5 rewrite sym (length+ l1 (𝕃injβ‚‚ l4)) = step{ss1 = l1 ++ 𝕃injβ‚‚ l4}{ss1' ++ 𝕃injβ‚‚ l4}{l2 ++ l4} a b pr1 pr2 pr5 (splice-concat2{l1}{𝕃injβ‚‚ l4} pr4 pr3) (_deriv++_ next end)