CODEWITHSUNDEEP
listtypescoqcoercion
Sambo
Sambo

Reputation: 199

Coq - Coercion of list nat

I would like to do a coercion from the type list nat to the type list bool. I would think that this could be done in the following way:

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.

However, this doesn't work. It seems like there is a fundamental issue with using coercion on something of the form list nat. Why does this not work?

Upvotes: 0

Views: 274

Answers (1)

M Soegtrop
M Soegtrop

Reputation: 1456

The documentation states that a class name must be a defined name. Neither list nat nor list bool are defined names - they are both applications. You must give the types between you want to define coercions a name as in:

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.

Please note that the coercion function must use these names - you can't write list nat instead of list_nat. Also the applications of the coercion must use the defined names as in:

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

I guess this is so because coercions might be done at the syntactic level where type unifications would be difficult.

Upvotes: 3

Related Questions