Coq中模式匹配工作原理及等值比较实现问题

错误原因 #

你的代码bug来自Coq模式匹配的变量遮蔽规则：
Coq模式匹配中，分支里出现的非构造子小写标识符，会被识别为新绑定的局部变量，匹配任意输入值，不会自动和上下文中的同名变量做等值比较。
你写的match h with | v => S (count' v t)分支中，|后的v是接收h值的新局部变量，直接遮蔽了外层传入的参数v。这就导致无论h取什么值，都会走计数加1的分支，长度为6的测试列表最终返回6，和你观测到的错误结果完全吻合。

纯模式匹配实现可行性 #

可以实现，但不存在“仅靠单层非递归模式匹配完成两个自然数比较”的写法。自然数是递归归纳类型，等值判断需要沿着O/S构造子逐层解构，本身就是递归逻辑：你不需要额外定义全局辅助函数，但必须把这部分递归判断逻辑内嵌在count函数中。
无全局辅助函数、完全依赖内置模式匹配的实现参考：

Fixpoint count' (v: nat) (s: bag) : nat :=
  match s with
  | nil => O
  | h :: t =>
    match
      (* 局部内嵌自然数等值判断，不定义全局辅助函数 *)
      (fix eq_nat (a b : nat) : bool :=
        match a, b with
        | O, O => true
        | S a', S b' => eq_nat a' b'
        | _, _ => false
        end) v h
    with
    | true => S (count' v t)
    | false => count' v t
    end
  end.

上述代码可以正确通过计数测试，没有调用任何自定义全局函数，所有逻辑都通过内置的fix递归和模式匹配完成。
注意：永远不要试图在模式分支中写和外层参数同名的变量来实现“匹配相等”，这种写法只会触发变量遮蔽，是Coq初学者最容易踩的模式匹配坑点之一。

内容的提问来源于stack exchange，提问作者wrongbyte