为什么模式匹配有时在 Agda 中是“必不可少的”？

Question

为什么在 Agda 中模式匹配有时是“必不可少的”？

我从Programming Language Foundations in 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 进行大小写拆分，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 文本说：

左边的模式匹配是必不可少的，因为 用⟨ x , y ⟩ 替换w 允许两边 命题等式简化为同一项。

但这并没有说明为什么模式匹配有助于简化，或者我们什么时候可以看到这种效果。

Answer 1

以这种方式构造的相等的含义可以看作是两个函数存在的证明：∀ {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₁，它们是定义等式。