Как построить тип данных со указанными свойствами?

Question

[zm_sansan]

Необходимо построить тип данных на некотором функциональном языке.
Это тип данных должен содержать параметр - количество его элементов.
Эти элементы соответственно должны быть различными.
Они должны быть линейно упорядочены, должен быть наименьшей и наибольший элемент.
На таком типе данных будут строиться функции для перехода к следующему и предыдущему элементу, доступу к наименьшему и наибольшему элементу.

В общем так сказать список цифр или алфавит.

На Coq я построил такой тип данных:

Definition SS n := {m : nat | m < n}.

Т.е. вроде множества из натуральных чисел меньше заданного n.
Проблема в том, что, доказательство того, что то или иное натуральное число входит в это множество, предвещает сравнение чисел, которое жутко громоздкое, и его даже не получается обобщить на любое число.

Вот например доказательство, что 0 входит в это множество:

OelSS10 =
exist (fun m : nat => m < 10) 0
(le_S 1 9
(le_S 1 8
(le_S 1 7
(le_S 1 6
(le_S 1 5
(le_S 1 4
(le_S 1 3
(le_S 1 2
(le_S 1 1 (le_n 1))))))))))
: SS 10
Можно конечно задать просто тип вручную Iductive SS := c0 | c1 | c2 | c3 | c4.

Но тут как минимум отсутствует упорядоченность, а вручную запаришься её описывать.

Прошу помочь, долго уже бьюсь над этой проблемой.

Answer 1

[zm_sansan]

На одном форуме предложили такой вариант для описания конечного множества.

Inductive Fin : nat -> Type :=
| FZ : forall k:nat, Fin (S k)
| FS : forall k:nat, Fin k -> Fin (S k).

(На Идрисе https://github.com/idris-lang/Idris-dev/blob/maste... )

Я изменил этот тип и получил такой
Inductive Fin : nat -> Type :=
| FZ : Fin 0
| FS : forall k:nat, Fin k -> Fin (S k).

С помощью такого типа можно задать или пустое множество или множество из конечного числа элементов.

PS: Создал группу про Coq, выкладываю переводы глав официального справочного руководства, пишу что интересного заметил. Буду рад обсудить различные вопросы.