时间戳

首页 > 解决方案 > 如何在 Coq 的函数式编程语言中执行 else 语句？

coq - 如何在 Coq 的函数式编程语言中执行 else 语句？

问题描述

我正在尝试计算Coqv中 a中某个元素的出现次数。natlist/bag我试过了：

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match h with
               | v => 1 + (count v tl)
               end
  end.

但是我的证明不起作用：

Example test_count1:              count 1 [1;2;3;1;4;1] = 3.
Proof. simpl. reflexivity. Qed.

为什么第一段代码不起作用？v不匹配时它在做什么？

我也试过：

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match h with
               | v => 1 + (count v tl)
               | _ => count v tl
               end
  end.

但这也会在 Coq 中产生错误，我什至无法运行它。

函数式编程对我来说有点陌生，所以我不知道如何在 Coq 中实际表达这一点。我真的只想说如果h匹配v然后执行 +1 并递归，否则仅递归（即我猜加零）。

有没有一种简单的方法可以用 Coq 的函数式编程语言来表达这一点？

我问的原因是因为我觉得 match 的东西与“普通”Python 编程中的 if else 语句非常相似。所以要么我错过了函数式编程的重点或其他东西。这是我隐含地担心的主要问题。

标签： coq

解决方案

（这类似于丹尼尔的回答，但我已经写了大部分）

你的问题是在这段代码中：

match h with
| v => 1 + (count v tl)
end

匹配v绑定一个新变量v。要测试是否h等于v，您必须使用一些决策程序来测试自然数的相等性。

例如，您可以使用Nat.eqb，它接受两个自然数并返回一个bool指示它们是否相等的值。

Require Import Nat.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => if (eqb h v) then (1 + count v t1) else (count v t1)
  end.

为什么我们不能简单地匹配我们想要的术语？模式匹配总是匹配该类型的构造函数。在这段代码中，外部匹配语句与niland匹配h :: t1（这是一个符号cons h t1或类似的东西，取决于 的精确定义bag）。在匹配语句中

match n with
| 0 => (* something *)
| S n => (* something else *)
end.

我们匹配nat:0和S _.

在您的原始代码中，您尝试匹配 on v，它不是构造函数，因此 Coq 只需绑定一个新变量并调用它v。

推荐阅读