Coq-强制列表nat

Question

我想执行从类型list nat到类型list bool的强制。我认为这可以通过以下方式实现：

From Coq Require Import Lists.List.
Definition nat_to_bool (n : nat) : bool :=
match n with
| 0 => true
| _ => false
end.
Definition list_nat_to_list_bool (l : list nat) : list bool :=
map (fun n => (nat_to_bool n)) l.
Coercion list_nat_to_list_bool : list nat >-> list bool.

然而，这不起作用。对list nat形式的东西使用强制似乎存在一个根本问题。为什么这不起作用？

Answer 1

文档规定类名必须是已定义的名称。list nat和list bool都不是定义的名称，它们都是应用程序。您必须为要定义强制的类型之间的类型指定一个名称，如：

From Coq Require Import Lists.List.
Definition nat_to_bool (n : nat) : bool :=
match n with
| 0 => true
| _ => false
end.
Definition list_nat := list nat.
Definition list_bool := list bool.
Definition list_nat_to_list_bool (l : list_nat) : list_bool :=
map (fun n => (nat_to_bool n)) l.
Coercion list_nat_to_list_bool : list_nat >-> list_bool.

请注意，强制函数必须使用这些名称——不能用list nat代替list_nat。此外，强制的应用程序必须使用以下定义的名称：

Definition test : list_bool := (1 :: nil) : list_nat.

我猜测这是因为强制可能在语法级别进行，而在语法级别，类型统一将很困难。