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

Question

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?

Answer 1

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.