如何匹配Coq中的特定值？ [英] How can I match on a specific value in Coq?

问题描述

我正在尝试实现一个功能，该功能仅计算袋子中某些nat的出现次数（只是列表的同义词）。

I'm trying to implement a function that simply counts the number of occurrences of some nat in a bag (just a synonym for a list).

这是我想做的，但是不起作用：

This is what I want to do, but it doesn't work:

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 作为头的名称，而不是传递给count调用的特定 v 。有什么方法可以对作为函数参数传递的值进行模式匹配？如果没有，我该怎么写该函数？

Coq says that the final clause is redundant, i.e., it just treats v as a name for the head instead of the specific v that is passed to the call of count. Is there any way to pattern match on values passed as function arguments? If not, how should I instead write the function?

我使它起作用：

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. 

但我不喜欢它。如果可能的话，我宁愿进行模式匹配。

But I don't like it. I'd rather pattern match if possible.

推荐答案

模式匹配与等式是一种不同的构造，旨在区分以形式编码的数据

Pattern matching is a different construction from equality, meant to discriminate data encoded in form of "inductives", as standard in functional programming.

特别是，在许多情况下，例如当您需要潜在的无限模式时，模式匹配不足。

In particular, pattern matching falls short in many cases, such as when you need potentially infinite patterns.

话虽如此，一种更明智的计数类型是math-comp库中可用的类型：

That being said, a more sensible type for count is the one available in the math-comp library:

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），其中 pred1：forall T：eqType，T-> pred T ，也就是说，具有可判定（可计算）相等类型的固定元素的一元相等谓词； pred1 x y<-> x = y 。

You can then build your function as count (pred1 x) where pred1 : forall T : eqType, T -> pred T , that is to say, the unary equality predicate for a fixed element of a type with decidable (computable) equality; pred1 x y <-> x = y.

这篇关于如何匹配Coq中的特定值？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！