我正在尝试实现一个函数，该函数可以简单地计算包中某些 nat 的出现次数（只是列表的同义词）。
这就是我想做的，但它不起作用：
Require Import Coq.Lists.List.
Import ListNotations.
Definition bag := list nat.
Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil => O
| v :: t => S (count v t)
| _ :: t => count v t
end.
Coq 说最后一个子句是多余的，即它只处理v作为头部的名称而不是特定的名称v它被传递给 count 的调用。有什么方法可以对作为函数参数传递的值进行模式匹配吗？如果没有，我应该如何编写该函数？
我让这个工作：
Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil => O
| h :: t => if (beq_nat v h) then S (count v t) else count v t
end.
但我不喜欢它。如果可能的话，我宁愿模式匹配。
模式匹配是与相等不同的结构，旨在区分以“归纳”形式编码的数据，作为函数式编程的标准。
特别是，模式匹配在许多情况下都存在不足，例如当您需要潜在无限的模式时。
话虽这么说，一种更合理的计数类型是 math-comp 库中提供的类型：
count : forall T : Type, pred T -> seq T -> nat
Fixpoint count s := if s is x :: s' then a x + count s' else 0.
然后你可以将你的函数构建为count (pred1 x) where pred1 : forall T : eqType, T -> pred T，也就是说，具有可判定（可计算）相等性的类型的固定元素的一元相等谓词；pred1 x y <-> x = y.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
