Доказательство конкатенации языка ассоциативно в Агде

Question

Я новичок в языке Agda, и я работаю над формальными языками, используя Agda.

У меня есть некоторые проблемы, когда доказательство объединения языков является ассоциативным. Доказательство будет выделено желтым цветом, так как Agda не смогла найти слова для "++Assoc" в следующем коде:

LangAssoc : ∀{Σ}{l1 l2 l3 : Language Σ}{w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w
LangAssoc {l1 = l1} (conc x (conc y z)) = conc (conc (subst l1 (++Assoc _ _ _) x) y) z

Где "++Assoc" является доказательством ассоциативности конкатенации списков.

Язык и конкатенация определяются следующим образом:

Language : ℕ → Set₁
Language a = Word a → Set

data LangConc {Σ} (l1 l2 : Language Σ) : Language Σ where
  conc : ∀{w1 w2} → l1 w1 → l2 w2 → (LangConc l1 l2) (w1 ++ w2)

Поэтому я хотел бы спросить, может ли кто-нибудь объяснить, что я делаю не так в этой ситуации, и дать мне подсказку, как решить проблему.

Редактировать 1: я пробовал другой способ, используя subst вне конкатенации, но я застрял в этой ситуации:

LangAssoc : ∀{Σ} {l1 l2 l3 : Language Σ} {w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w
LangAssoc {Σ} {l1 = l1} {l2 = l2} {l3 = l3} (conc x (conc y z)) = subst {!!} (++Assoc {Σ} _ _ _) (conc {Σ} (conc {Σ} x y) z)

Редактировать 2: я только что попробовал следующий код и приводит к сообщению об ошибке.

LangAssoc : ∀{Σ} {l1 l2 l3 : Language Σ} {w : Word Σ} → (LangConc l1 (LangConc l2 l3)) w → (LangConc (LangConc l1 l2) l3) w
LangAssoc {l1 = l1} {w = w} (conc x (conc y z)) =  ?

---

w1 ++ w2 != w of type List (Fin Σ)
when checking that the pattern conc x (conc y z) has type
LangConc l1 (LangConc l2 l3) w

---

Изменить 3: Просто еще одна попытка, разбив слово w на три части, как предложено.

LangAssoc : ∀{Σ : ℕ}{l1 l2 l3 : Language Σ}{w1 w2 w3 : Word Σ} 
             → (LangConc l1 (LangConc l2 l3)) (w1 ++ w2 ++ w3)
             → (LangConc (LangConc l1 l2) l3) ((w1 ++ w2) ++ w3)
LangAssoc (conc {w1} x (conc {w2} {w3} y z))
   = subst (LangConc (LangConc _ _) _) (++Assoc w1 w2 w3) (conc (conc x y) z)

---

Сообщение об ошибке:

w4 != w1 of type List (Fin Σ)
when checking that the pattern conc {w1} x (conc {w2} {w3} y z) has
type LangConc l1 (LangConc l2 l3) (w1 ++ w2 ++ w3)

где List (Fin Σ) - определение слова Σ.

Answer 1

Проблема в том, что ++ не является инъективным (и даже если бы Агда не знала об этом), поэтому при попытке решить x ++ (y ++ z) ?= _1 ++ (_2 ++ _3)Агда не может найти наиболее общего решения.

Например, говоря _1 = [], _2 = x, _3 = y ++ z должно сработать.

Изменить: не имеет смысла вводить w после сопоставления с шаблоном LangConc l1 (LangConc l2 l3) w: w был разбит на 3 части (те, которые соответствуют l1, l2 а также l3). Гораздо интереснее представить эти части:

LangAssoc (conc {w1} x (conc {w2} {w3} y z)) =
  subst (LangConc (LangConc _ _) _) (++Assoc w1 w2 w3) (conc (conc x y) z)