證明語言連接在Agda中是關聯的

Question

我是Agda語言的新手，我正在使用Agda正式語言。

當證明語言連接是關聯時，我遇到了一些問題。該證明將是黃色突出顯示爲阿格達不能在下面的代碼中找到了「++副教授」的話來說：

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 

凡「++副教授」是列表的級聯的關聯性的證據。

語言和連接定義如下：

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) 

其中列表（鰭Σ）是字Σ的定義。

Answer 1

問題是，++是不是內射的（即使它是，Agda不知道它），所以當試圖解決x ++ (y ++ z) ?= _1 ++ (_2 ++ _3)時，沒有最通用的解決方案Agda可以挑選。

例如說，說_1 = [],_2 = x,_3 = y ++ z將工作。

編輯：這並沒有真正有意義給在LangConc l1 (LangConc l2 l3) w匹配模式之後推出w：w已在3個部分（那些correponding到l1，l2和l3）被打破了。引入這些零件更有趣：

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