Proving concatenation of language is associative in Agda

Question

I am new to the language Agda, and I am working on formal languages using Agda.

I've got some problems when proving the concatenation of languages is associative. The proof will be yellow highlighted as Agda could not find the words for "++Assoc" in the following code:

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

Where the "++Assoc" is the proof of the associativity of the concatenation of the lists.

The language and concatenation is defined as following:

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)

So I would like to ask if anyone can explain on what am I doing wrong in this situation and give me some hint on how to solve the problem.

Edit 1: I've tried another way by using subst outside the concatenation, but I got stuck in this situation:

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)

Edit 2: I've just tried with the following code and results in a error message.

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

---

Edit 3: Just had another try by breaking the word w into three pieces as suggested.

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)

---

Error message:

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)

where List (Fin Σ) is the definition of Word Σ.

Answer 1

The problem is that ++ is not injective (and even if it were, Agda wouldn't know about it) so when trying to solve x ++ (y ++ z) ?= _1 ++ (_2 ++ _3), there is no most general solution Agda could pick.

For instance saying _1 = [], _2 = x, _3 = y ++ z would work.

Edit: It does not really makes sense to introduce w after having pattern matched on LangConc l1 (LangConc l2 l3) w: w has been broken up in 3 parts (the ones correponding to l1, l2 and l3). It is much more interesting to introduce these parts:

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