Agdaで言語の連結が証明されている

Question

私はAgdaという言葉が初めてです。私は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：ちょうど提案として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) 

一覧（フィンΣ）はWordのΣの定義です。

Answer 1

問題は、x ++ (y ++ z) ?= _1 ++ (_2 ++ _3)を解決しようとすると、Agdaが選ぶことのできる最も一般的な解決法はないということです。問題は、++は注入型ではありません（Agdaはそれについて知りませんでした）。

たとえば、_1 = [],_2 = x、_3 = y ++ zと表示されます。

編集：それは本当にLangConc l1 (LangConc l2 l3) wにマッチしたパターンを有する後wを導入することは理にかなっていません：wは3部（l1、l2とl3にcorrepondingもの）に分割されています。これらのパーツを紹介するのははるかに面白いです：

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