|
Необходимо построить тип данных на некотором функциональном языке.
Это тип данных должен содержать параметр - количество его элементов.
Эти элементы соответственно должны быть различными.
Они должны быть линейно упорядочены, должен быть наименьшей и наибольший элемент.
На таком типе данных будут строиться функции для перехода к следующему и предыдущему элементу, доступу к наименьшему и наибольшему элементу.
В общем так сказать список цифр или алфавит.
На 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.
Но тут как минимум отсутствует упорядоченность, а вручную запаришься её описывать.
Прошу помочь, долго уже бьюсь над этой проблемой.
|
02.03.2016, 18:32 
