为什么模式匹配有时在 Agda 中是“必不可少的”？
当没有模式匹配时，Agda 给出了不允许refl的洞：
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× x = ?
它报告了这个目标和假设：
Goal: ⟨ proj₁ x , proj₂ x ⟩ ≡ x
————————————————————————————————————————————————————————————
x : A × B
但是如果我告诉它进行大小写拆分，Agda 可以弄清楚发生了什么（ctrl-c ctrl-c x Ret)
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , x₁ ⟩ = ?
Goal: ⟨ x , x₁ ⟩ ≡ ⟨ x , x₁ ⟩
然后 Agda 让我用refl.
这是怎么回事？模式匹配如何为 Agda 提供更多信息？
PLFA 文本说：
左侧的模式匹配是必不可少的，因为替换
w为⟨ x , y ⟩允许命题等式的两边都简化为相同的项。
但这并没有说明为什么模式匹配有助于简化，或者我们何时可以看到这种效果。
以这种方式构建的等式的含义可以看作是两个函数存在的证明：∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩和∀ {A B : Set} (w : A × B) → w，必须证明它们对相同的输入产生相等的输出。
在第一种情况下，该语句需要证明\ w -> ⟨ proj₁ w , proj₂ w ⟩ ≡ \ w -> w。Agda 告诉你没有定义的等式可以得出这个结论。有人可能会争辩说，对于单构造函数类型，可以自动计算，但是您可以看到这通常并不那么简单。
在第二种情况下，假设模式匹配证明w ≡ ⟨ x , x₁ ⟩，您只需要证明proj₁ ≡ \ ⟨ x , x₁ ⟩ -> x和proj₂ ≡ \ ⟨ x , x₁ ⟩ -> x₁，它们是定义相等的。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句