找到了一个归纳类型 bool 的构造函数，而期望是一个列表的构造函数

Question

我有以下问题：定义函数值：list bool -> nat return 由布尔值列表（二进制数到十进制数）表示的值。例如，值 [false;true;false;true] = 10。我写了这个：

Fixpoint value (l: list bool) := match l with
|true=> 1
|false=> 0
|x::r => (value [x])+2*(value r)
end.

但我收到此错误：“找到了归纳类型 bool 的构造函数而列表的构造函数是预期的。

我尝试将 false 和 true 作为布尔列表：[false] [true] 但是还是不行。。。怎么办？

Answer 1

事实上，Coq 理所当然地抱怨你应该为列表使用构造函数，并且 true 和 false 是布尔值，而不是布尔值列表。你是对的，应该使用 [true] 和 [false]。

那么在这之后，Coq 应该仍然抱怨你没有在空列表上指定你的函数，所以你需要像这样为它添加一个 case:

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | [ true ] => 1
  | [ false ] => 0
  | x :: r => value [x] + 2 * value r
  end.

这次 Coq 仍然会报错，但有另一个原因：它不知道 [x] 小于 x :: r。因为语法上不是这样的。要修复它，我建议简单地处理这两种情况：true 和 false。这在任何情况下都会产生更简单的东西：

From Coq Require Import List.
Import ListNotations.

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: r => 1 + 2 * value r
  | false :: r => 2 * value r
  end.

找到了一个归纳类型 bool 的构造函数，而期望是一个列表的构造函数

Found a constructor of inductive type bool while a constructor of list is expected

coq

inductive-logic-programming