regular-language - 证明语言的连接在 Agda 中是关联的

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 Σ) 是 Word Σ 的定义。

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 个部分(对应于 l1、l2 和 l3)。介绍这些部分更有趣:

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