Конвертация из разных типов

Question

 Inductive color: Type :=
 | red 
 | green
 | blue.
Inductive listw : Type :=
  | nil : listw
  | cons : web -> listw -> listw.
Definition colorlist (c:color) : listw :=
  match w with 
  | red => (cons red nil)
  | green => (cons green nil)
  | blue => (cons blue nil)
end.
Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).
Definition bag:=listw.
Definition bag:=((cons red nil)++(cons green nil)++(cons blue nil)).
Bag = cons red (cons green (cons blue nil)).

Я определил список цветов (индуктивный тип). Хотите заменить каждый цвет на конкретное натуральное число. У меня проблема с присвоением натурального номера другому списку индуктивных типов.

Answer 1

Мне трудно понять, что именно вы хотите, поэтому я постараюсь написать ответ на то, что я делаю.

У вас есть тип цвета:

Inductive color := 
| red
| green
| blue.

Затем вы хотите получить список натуральных чисел из него. Таким образом, вы связываете число с каждым цветом:

Definition nat_of_color (c : color) : nat :=
  match c with
  | red => 0
  | green => 1
  | blue => 2
  end.

Теперь, если вы должны использовать тип list, предоставленный coq, вам нужна следующая функция:

Definition nat_list_of_color_list (l : list color) : list nat :=
  List.map nat_of_color l.

InДругими словами, List.map nat_of_color - это функция, которую вы, похоже, желаете.

Обратите внимание, что алгоритм сортировки и счетчик совпадений, вероятно, можно сделать более универсальным для работы с цветами сразу же.