В первой части статьи про язык Arend мы рассматривали простейшие индуктивные типы, рекурсивные функции, классы и множества.
2. Сортировка списков в Arend
2.1 Упорядоченные списки в Arend
Определим тип упорядоченных списков как пару, состоящую из списка и доказательства его упорядоченности. Как мы уже говорили, в Arend зависимые пары определяются при помощи ключевого слова Sigma. Определение типа Sorted дадим через сопоставление с образцом, вдохновившись определением из уже упомянутой статьи про упорядоченные списки.
func SortedList (O : LinearOrder.Dec) => Sigma (l : List O) (Sorted l)
data Sorted {A : LinearOrder.Dec} (xs : List A) : Prop elim xs
| nil => nilSorted
| :-: x nil => singletonSorted
| :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))
Обратите внимание: Arend сумел автоматически вывести, что тип Sorted содержится во вселенной Prop. Это произошло потому, что все три образца в определении Sorted являются взаимно исключающими, а конструктор consSorted имеет два параметра, оба из которых принадлежат Prop.
Докажем какое-нибудь очевидное свойство предиката Sorted, скажем, что хвост упорядоченного списка сам является упорядоченным списком (это свойство пригодится нам в дальнейшем).
Читать полностью »
