Определение отношения подтипа в Coq

В Coq нет настоящего подтипа (за исключением подтипа юниверса, который, вероятно, не то, что вам нужно). Ближайшей альтернативой является использование приведения, представляющего собой функции, которые средство проверки типов Coq вставляет автоматически всякий раз, когда оно ожидает элемент одного типа, но вместо этого находит элемент другого типа. Например, рассмотрим следующее приведение логических значений к натуральным числам:

Definition nat_of_bool (b : bool) : nat :=
  if b then 1 else 0.

Coercion nat_of_bool : bool >-> nat.

После запуска этого фрагмента Coq использует nat_of_bool для преобразования bool в nat, как показано здесь:

Check true + 3.
(* true + 3 : nat *)

Таким образом, bool начинает вести себя почти так, как если бы он был подтипом nat.

Хотя nat_of_bool здесь не появляется, он просто скрыт принтером Coq. Этот терм на самом деле то же самое, что и nat_of_bool true + 3, в чем мы можем убедиться, попросив Coq вывести все приведения:

Set Printing Coercions.
Check true + 3.
(* nat_of_bool true + 3 : nat *)

Символ :> о котором вы спрашивали ранее при использовании в объявлении записи делает то же самое. Например, код

Record foo := Foo {
  sort :> Type
}.

эквивалентно

Record foo := Foo {
  sort : Type
}.

Coercion sort : foo >-> Sortclass.

где Sortclass — это специальная цель принуждения для Type, Prop и Set.

руководство пользователя Coq более подробно описывает приведение.