在预计列表的构造函数的同时，找到了一个归纳类型bool的构造函数

发布于 2025-01-21 22:43:04 字数 330 浏览 4 评论 0原文

我有以下问题：定义fonction值：list bool - ＆gt;返回由布尔值列表表示的值（二进制号为十进制数字）的NAT。例如，值[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的构造函数而列表的构造函数期望

。但这仍然行不通...我该怎么办？

原文

I have the following question : Define the fonction value : list bool -> nat that return the value represented by a list of booleans(binary number to decimal number). For example, value [false;true;false;true] = 10.
I wrote this:

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

but I get this error : "Found a constructor of inductive type bool
while a constructor of list
is expected."

I have tried to put false and true as bool list : [false] [true]
but it still doesn't work... What should I do?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

傲娇萝莉攻 2025-01-28 22:43:04

实际上，Coq正确地抱怨您应该使用构造函数进行列表，true和false是布尔值，而不是布尔值列表。您是对的，应该使用[true]和[false]。

然后，COQ仍然应该抱怨您没有在空列表上指定您的功能，因此您需要为此添加一个案例：

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.

Indeed, Coq rightfully complains that you should use a constructor for list, and true and false are booleans, not lists of booleans. You are right that [true] and [false] should be used.

Then after this, Coq should still complain that you did not specify your function on the empty list, so you need to add a case for it like so:

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

This time Coq will still complain but for another reason: it doesn't know that [x] is smaller than x :: r. Because it isn't the case syntactically.
To fix it, I suggest to simply deal with the two cases: true and false. This yields something simpler in any case:

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.

回复收藏 0 原文

~没有更多了~