了解 Coq 中模式匹配的工作原理

Question

我目前正在关注《软件基础》一书，目前正在阅读“列表”章节。 然而，我很难理解模式匹配的具体情况，并且由于是 Coq 的初学者，我不确定如何找到这个问题的答案。

因此，练习是创建一个来计算列表（更具体地说是一个包）中有Fixpoint多少 nat 。vs

我决定为此使用模式匹配，但如果我尝试定义这样的函数：

Fixpoint count' (v: nat) (s: bag) : nat :=
  match s with
  | nil => O
  | h :: t => match h with
              | v => S (count' v t)
              end
  end.

并尝试将此功能应用于，比方说，

Example test_count1: count' 1 [1;2;3;1;4;1] = 3.

我最终会得到6 = 3。我的理解是，匹配h始终v是“true”，因此它最终会计算列表中的每个元素。

但为什么会发生这种情况呢？h我们如何使用模式匹配来比较和的值v？

PS：我已经使用比较 ifh和vequal 的辅助函数解决了这个练习，但我想知道这是否只能使用内置模式匹配来实现。

Answer 1

图案

match h with
| v => S (count' v t)
end

v引入了一个绑定到 的新变量h，遮盖了现有的v. 它相当于一个let表达式：

let v := h in S (count' v t)
(* or, without shadowing *)
let v1 := h in S (count' v1 t)

相反，要比较h和v，请使用比较函数：

if h =? v then ... else ...