Coq

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

documentation 声明 class 名称必须是定义的名称。 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.

我猜测之所以如此，是因为强制转换可能会在类型统一很困难的句法级别完成。

Coq - 列表 nat 的强制转换

Coq - Coercion of list nat

types

list

coercion