Agda 统一超过一个列表

Question

我正在做一个项目来证明正则表达式的一些属性。 这是我的部分代码

⇨这里表示派生，Regexp ⇨ word表示正则表达式可以派生一个词

Σ : Set
Σ* : List Σ

如果e₁ ⇨ w₁、e₂ ⇨ w₂和w ≡ w₁ ++ w₂，则下面定义了串联e₁ ∙ e₂可以派生单词w的情况

data _⇨_ : RegExp Σ → Σ* → Set where
 con : {e₁ e₂ : RegExp Σ}{w w₁ w₂ : Σ*} → w ≡ w₁ ++ w₂ → e₁ ⇨ w₁ → e₂ ⇨ w₂ → e₁ ∙ e₂ ⇨ w

这证明如果w ≡ w₁ ++ [] 和 (e₁ 不能推导出 w₁) 比 (e₁.e₂ 不能推导出 w)

¬e₁∙e₂⇨xs[]ˡ : {e₁ e₂ : RegExp Σ}{w w₁ : Σ*} → w ≡ w₁ ++ [] → ¬ (e₁ ⇨ w₁) → ¬ (e₁ ∙ e₂ ⇨ w)
¬e₁∙e₂⇨xs[]ˡ refl ¬e₁⇨w₁ (con {w₂ = []} refl e₁⇨w₁ e₂⇨[]) = ¬e₁⇨w₁ e₁⇨w₁

但是con refl e₁⇨w₁ e₂⇨[]中的refl不进行类型检查，因为Agda无法将¬e₁∙e₂⇨xs[]ˡ中的w₁与¬ (e₁ ∙ e₂ ⇨ w)中的w₁统一起来，错误信息就在这里：

w₁ != w₂ of type List Σ
when checking that the pattern refl has type w₁ ++ [] ≡ w₂ ++ []

任何帮助将不胜感激！

Answer 1

在您对w ≡ w₁ ++ [] 进行模式匹配后，您注定要失败，因为w 与w₁ ++ [] 统一，e₁ ∙ e₂ ⇨ w 变为e₁ ∙ e₂ ⇨ w₁ ++ []，您无法对其进行模式匹配。

_++_ 不是单射的，w₁ ++ [] ≡ w₁' ++ w₂' 不包含w₁ ≡ w₁' × [] ≡ w₂' — 通常还有其他方法可以统一这两个表达式。

你的引理同构于

¬e₁∙e₂⇨xs[]ˡ : {e₁ e₂ : RegExp Σ}{w : Σ*} → ¬ (e₁ ⇨ w) → ¬ (e₁ ∙ e₂ ⇨ w)

在我看来是假的。

请参阅here 了解类似问题。