Доброго времени суток, уважаемый читатель!
Прочитав несколько книг по типизированном лямбда исчисление, а именно по зависимым типам, увидел интересную закономерность: везде первым примером приводится определение типа «отсортированный список». Все бы хорошо, но дальше этого определения ничего не было. Вот я и придумал восполнить этот пробел и реализовать функцию, принимающую список, и возвращающую другой список и два доказательства. Одно доказывает, что результат — это перестановка входа, а другое доказывает, что результат — отсортированный список.
Формальное описание
В этой части я приведу основные типы, которые будут далее использоваться, и некоторые вспомогательные функции. Также тут будут показаны некоторые интересные синтаксические прелести Agda. Для тех, кто не сильно знаком с Agda, рекомендую посмотреть видео/слайды Яна Малаховского на встрече SPbHUG/FProg 2012-07 — это по-моему единственное введение в Agda на русском (ну я больше не встречал). Или же пролистать мануал с сайта Agda (он не большой) или этот туториал.
Определения списка
data List {a} (A : Set a) : Set a where
[] : List A
_∷_ : (x : A) (xs : List A) → List A
[_] : ∀ {a} {A : Set a} → A → List A
[ x ] = x ∷ []
_++_ : ∀ {a} {A : Set a} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
Тут у нас определен список. Определение взято из стандартной библиотеки. Как видно элементами списка могут быть значения любых типов, даже типы и типы типов и так далее. Это возможно из-за использования high-order полиморфизма: вводится параметр a, который отвечает за уровень, то есть обычные типы имеют тип Set 0, Set 0 имеет тип Set 1 и т.д.
Также в этом определении видно как в Agda объявляются операторы, а именно через нижние подчеркивания, на месте которых будут аргументы. Следует заметить, что этот способ разрешает определять самые разные и очень интересные формы, как например функция, возвращающая список с одного элемента [_].
Нужно заметить, что для всех операторов (комбинаторов с нижними подчеркиваниями) можно указывать приоритет и ассоциативность. Также в Agda любая Юникод-последовательность без пробелов и скобок (круглых и фигурных) есть терм.
Также следует обратить внимание на круглые и фигурные скобки: фигурные скобки в указании типа говорят, что этот аргумент неявный и будет выводиться компилятором.
Тип «отсортированный список»
data Sorted {A} (_≤_ : A → A → Set) : List A → Set where
nil : Sorted _≤_ []
one : {x : A} → Sorted _≤_ [ x ]
two : {x : A} → ∀ {y l} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l)
Это определение предиката «отсортированный список». Конструкторы стоит рассматривать как аксиомы. Имеем аксиомы nil и one которые говорят, что пустой список и список с одного элемента отсортированные. Также видим, что тип Sorted зависит от предиката _≤_, который отвечает за порядок — что-то вроде функции сравнения, но зависимо-типовая (аргументы — значения обычного типа, а результатом является некоторый тип, значением которого есть доказательство). Аксиома two говорит следующее: если мы имеем доказательство того, что x ≤ y (x ≤ y — это тип, а значение типа x ≤ y — это доказательство того, что x ≤ y. См. Изоморфизм Карри-Ховарда), и доказательство того, что некоторый список с головой y — отсортированный (этим доказательством есть значение типа Sorted _≤_ (y ∷ l)), то и список x ∷ y ∷ l тоже будет отсортированный.
Тип «перестановка»
data Permutation {A} : List A → List A → Set where
refl : ∀ {l} → Permutation l l
perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂)
Тип (предикат) «перестановка». Аргументы — два списка. Вводимые аксиомы: refl — список является перестановкой самого себя; perm — если имеем доказательство, что некоторый список l есть перестановкой другого списка l₁ ++ x₂ ∷ x₁ ∷ l₂ (доказательством этого будет значение типа Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂)), то если переставить в другом списке два произвольных элемента местами, получим, что новый список является перестановкой первого.
Тип «сумма»
data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
inj₁ : (x : A) → A ⊎ B
inj₂ : (y : B) → A ⊎ B
Ну тут все просто — это не зависимый тип — аналог Either в Haskell.
Произведение типов
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
syntax Σ A (λ x → B) = Σ[ x ∶ A ] B
_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ _ ∶ A ] B
Это — аналог кортежа. Используется record, поскольку у данного типа может быть только один конструктор. Это определение использует зависимый тип: первый элемент — это некоторое значение, а второй — доказательство исполнения некоторого предиката на этом элементе. Но, конечно, так его использовать не обязательно, можно просто как обычный кортеж (через _×_) — тогда зависимость между элементами игнорируется. syntax разрешает задавать новые синтаксические конструкции, если простых возможностей мало.
Функция сортировки
sort : {A : Set} {_≤_ : A → A → Set} → (∀ x y → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l')
Наконец опишем тип функции сортировки: эта функция принимает (неявно) предикат, определяющий порядок, также функцию, которая для входных значений возвращает доказательство, что первое больше второго или что второе больше первого. Думаю читатель догадался, что эта функция будет использоваться для построения доказательства отсортированности списка-результата. Также, конечно, одним из входных параметров является список, который будет сортироваться.
Функция sort возвращает список и два доказательства (отсортированности и перестановки).
Реализация функции сортировки
Конечно же никакой реализации этой функции тут не будет — не то, что бы мне жалко было показывать код, мне жалко себя объяснять его. По-этому я приведу доказательства (реализации) некоторых вспомогательных функций, которые мне понадобились во время написания функции сортировки.
{-# OPTIONS --no-termination-check #-}
module QuickSort where
open import IO.Primitive using () renaming (putStrLn to putCoStrLn)
open import Data.String using (toCostring; String) renaming (_++_ to _+s+_)
open import Data.List
open import Data.Nat
open import Data.Nat.Show
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Function
data Sorted {A} (_≤_ : A → A → Set) : List A → Set where
nil : Sorted _≤_ []
one : {x : A} → Sorted _≤_ [ x ]
two : {x : A} → ∀ {y l} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l)
data Permutation {A} : List A → List A → Set where
refl : ∀ {l} → Permutation l l
perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂)
≡-elim : ∀ {l} {A : Set l} {x y : A} → x ≡ y → (P : A → Set l) → P x → P y
≡-elim refl _ p = p
≡-sym : ∀ {l} {A : Set l} {x y : A} → x ≡ y → y ≡ x
≡-sym refl = refl
≡-trans : ∀ {l} {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡-trans refl refl = refl
++-assoc : ∀ {l} {A : Set l} (l₁ l₂ l₃ : List A) → (l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃)
++-assoc [] l₂ l₃ = refl
++-assoc (h ∷ t) l₂ l₃ = ≡-elim (≡-sym $ ++-assoc t l₂ l₃) (λ x → h ∷ x ≡ h ∷ t ++ (l₂ ++ l₃)) refl
decNat : (x y : ℕ) → (x ≤ y) ⊎ (y ≤ x)
decNat zero y = inj₁ z≤n
decNat (suc x) (suc y) with decNat x y
... | inj₁ p = inj₁ (s≤s p)
... | inj₂ p = inj₂ (s≤s p)
decNat (suc x) zero = inj₂ z≤n
perm-trans : ∀ {A} {l₁ l₂ l₃ : List A} → Permutation l₁ l₂ → Permutation l₂ l₃ → Permutation l₁ l₃
perm-trans p refl = p
perm-trans p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm l₁ x₁ x₂ l₂ $ perm-trans p₁ p₂
perm-sym : ∀ {A} {l₁ l₂ : List A} → Permutation l₁ l₂ → Permutation l₂ l₁
perm-sym refl = refl
perm-sym (perm l₁ x₁ x₂ l₂ p) = perm-trans (perm l₁ x₂ x₁ l₂ refl) (perm-sym p)
perm-del-ins-r : ∀ {A} (l₁ : List A) (x : A) (l₂ l₃ : List A) → Permutation (l₁ ++ x ∷ l₂ ++ l₃) (l₁ ++ l₂ ++ x ∷ l₃)
perm-del-ins-r l₁ x [] l₃ = refl
perm-del-ins-r l₁ x (h ∷ t) l₃ = perm-trans p₀ p₅
where p₀ : Permutation (l₁ ++ x ∷ h ∷ t ++ l₃) (l₁ ++ h ∷ x ∷ t ++ l₃)
p₀ = perm l₁ h x (t ++ l₃) refl
p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃)
p₁ = perm-del-ins-r (l₁ ++ [ h ]) x t l₃
p₂ : (l₁ ++ [ h ]) ++ t ++ x ∷ l₃ ≡ l₁ ++ h ∷ t ++ x ∷ l₃
p₂ = ++-assoc l₁ [ h ] (t ++ x ∷ l₃)
p₃ : (l₁ ++ [ h ]) ++ x ∷ t ++ l₃ ≡ l₁ ++ h ∷ x ∷ t ++ l₃
p₃ = ++-assoc l₁ [ h ] (x ∷ t ++ l₃)
p₄ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
p₄ = ≡-elim p₂ (λ y → Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) y) p₁
p₅ : Permutation (l₁ ++ h ∷ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
p₅ = ≡-elim p₃ (λ y → Permutation y (l₁ ++ h ∷ t ++ x ∷ l₃)) p₄
perm-del-ins-l : ∀ {A} (l₁ l₂ : List A) (x : A) (l₃ : List A) → Permutation (l₁ ++ l₂ ++ x ∷ l₃) (l₁ ++ x ∷ l₂ ++ l₃)
perm-del-ins-l l₁ l₂ x l₃ = perm-sym $ perm-del-ins-r l₁ x l₂ l₃
perm-++ : ∀ {A} {x₁ y₁ x₂ y₂ : List A} → Permutation x₁ y₁ → Permutation x₂ y₂ → Permutation (x₁ ++ x₂) (y₁ ++ y₂)
perm-++ refl refl = refl
perm-++ (perm {x₁} l₁ e₁ e₂ l₂ p) (refl {z₂}) = perm-trans p₅ p₇
where p₁ : Permutation (x₁ ++ z₂) ((l₁ ++ e₂ ∷ e₁ ∷ l₂) ++ z₂)
p₁ = perm-++ p refl
p₂ : (l₁ ++ e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂
p₂ = ++-assoc l₁ (e₂ ∷ e₁ ∷ l₂) z₂
p₃ : l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂
p₃ = ≡-elim (++-assoc [ e₂ ] (e₁ ∷ l₂) z₂) (λ x → l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ x) refl
p₄ : l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂
p₄ = ≡-elim (++-assoc [ e₁ ] l₂ z₂) (λ x → l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ x) refl
g₂ : (l₁ ++ e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂
g₂ = ++-assoc l₁ (e₁ ∷ e₂ ∷ l₂) z₂
g₃ : l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂
g₃ = ≡-elim (++-assoc [ e₁ ] (e₂ ∷ l₂) z₂) (λ x → l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ x) refl
g₄ : l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ e₂ ∷ l₂ ++ z₂
g₄ = ≡-elim (++-assoc [ e₂ ] l₂ z₂) (λ x → l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ x) refl
p₅ : Permutation (x₁ ++ z₂) (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂)
p₅ = ≡-elim (≡-trans p₂ $ ≡-trans p₃ p₄) (Permutation (x₁ ++ z₂)) p₁
p₆ : Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂) (l₁ ++ e₁ ∷ e₂ ∷ l₂ ++ z₂)
p₆ = perm l₁ e₁ e₂ (l₂ ++ z₂) refl
p₇ : Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂) ((l₁ ++ e₁ ∷ e₂ ∷ l₂) ++ z₂)
p₇ = ≡-elim (≡-sym $ ≡-trans g₂ $ ≡-trans g₃ g₄) (Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂)) p₆
perm-++ {_} {x₁} {y₁} .{_} .{_} p₁ (perm {x₂} l₁ e₁ e₂ l₂ p₂) = ≡-elim p₇ (Permutation (x₁ ++ x₂)) p₆
where p' : Permutation (x₁ ++ x₂) (y₁ ++ l₁ ++ e₂ ∷ e₁ ∷ l₂)
p' = perm-++ p₁ p₂
p₃ : y₁ ++ l₁ ++ e₂ ∷ e₁ ∷ l₂ ≡ (y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂
p₃ = ≡-sym $ ++-assoc y₁ l₁ (e₂ ∷ e₁ ∷ l₂)
p₄ : Permutation (x₁ ++ x₂) ((y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂)
p₄ = ≡-elim p₃ (Permutation (x₁ ++ x₂)) p'
p₅ : Permutation ((y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂) ((y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂)
p₅ = perm (y₁ ++ l₁) e₁ e₂ l₂ refl
p₆ : Permutation (x₁ ++ x₂) ((y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂)
p₆ = perm-trans p₄ p₅
p₇ : (y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂ ≡ y₁ ++ l₁ ++ e₁ ∷ e₂ ∷ l₂
p₇ = ++-assoc y₁ l₁ (e₁ ∷ e₂ ∷ l₂)
++-[] : ∀ {l} {A : Set l} (l : List A) → l ++ [] ≡ l
++-[] [] = refl
++-[] (h ∷ t) = ≡-trans p₀ p₁
where p₀ : (h ∷ t) ++ [] ≡ h ∷ t ++ []
p₀ = ++-assoc [ h ] t []
p₁ : h ∷ t ++ [] ≡ h ∷ t
p₁ = ≡-elim (++-[] t) (λ x → h ∷ t ++ [] ≡ h ∷ x) refl
data ConstrainedList {A} (P : A → Set) : List A → Set where
[] : ConstrainedList P []
_∷_ : {x : A} {xs : List A} (p : P x) → ConstrainedList P xs → ConstrainedList P (x ∷ xs)
infix 2 _∈_
data _∈_ {A} : A → List A → Set where
exact : ∀ h t → h ∈ h ∷ t
cons : ∀ h {x l} → x ∈ l → x ∈ h ∷ l
create-∈ : ∀ {A} (l₁ : List A) (x : A) (l₂ : List A) → x ∈ (l₁ ++ x ∷ l₂)
create-∈ [] x l₂ = exact x l₂
create-∈ (h₁ ∷ t₁) x l₂ = cons h₁ $ create-∈ t₁ x l₂
perm-∈ : ∀ {A l l'} {x : A} → x ∈ l → Permutation l' l → x ∈ l'
perm-∈ p refl = p
perm-∈ {A} .{l₁ ++ x₁ ∷ x₂ ∷ l₂} {l'} {x} p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm-∈ (loop l₁ x₁ x₂ l₂ p₁) p₂
where loop : ∀ l₁ x₁ x₂ l₂ → x ∈ l₁ ++ x₁ ∷ x₂ ∷ l₂ → x ∈ l₁ ++ x₂ ∷ x₁ ∷ l₂
loop [] .x x₂ l₂ (exact .x .(x₂ ∷ l₂)) = cons x₂ $ exact x l₂
loop [] .x₁ .x .l₂ (cons x₁ (exact .x l₂)) = exact x (x₁ ∷ l₂)
loop [] .x₁ .x₂ l₂ (cons x₁ (cons x₂ p)) = cons x₂ $ cons x₁ p
loop (.x ∷ t₁) x₁ x₂ l₂ (exact .x .(t₁ ++ x₁ ∷ x₂ ∷ l₂)) = exact x (t₁ ++ x₂ ∷ x₁ ∷ l₂)
loop (.h₁ ∷ t₁) x₁ x₂ l₂ (cons h₁ p) = cons h₁ $ loop t₁ x₁ x₂ l₂ p
constr-∈ : ∀ {A l} {x : A} → ∀ {P} → ConstrainedList P l → x ∈ l → P x
constr-∈ [] ()
constr-∈ (p ∷ _) (exact _ _) = p
constr-∈ (_ ∷ cl) (cons _ p) = constr-∈ cl p
sortedHelper₂ : ∀ {A _≤_} {h : A} → ∀ {l'} → Sorted _≤_ l' → ∀ {l} → Permutation l l' → ConstrainedList (λ x → x ≤ h) l → ∀ {g'} → Sorted _≤_ (h ∷ g') → Sorted _≤_ (l' ++ h ∷ g')
sortedHelper₂ {_} {_≤_} {h} {l'} sl' pll' cl {g'} sg' = loop [] l' refl sl'
where loop : ∀ l₁ l₂ → l₁ ++ l₂ ≡ l' → Sorted _≤_ l₂ → Sorted _≤_ (l₂ ++ h ∷ g')
loop _ .[] _ nil = sg'
loop l₁ .(x ∷ []) p (one {x}) = two (constr-∈ cl $ perm-∈ x∈l' pll') sg'
where x∈l' : x ∈ l'
x∈l' = ≡-elim p (λ l → x ∈ l) (create-∈ l₁ x [])
loop l₁ .(x ∷ y ∷ l) p≡ (two {x} {y} {l} x≤y ps) = two x≤y $ loop (l₁ ++ [ x ]) (y ∷ l) p' ps
where p' : (l₁ ++ [ x ]) ++ y ∷ l ≡ l'
p' = ≡-trans (++-assoc l₁ [ x ] (y ∷ l)) p≡
sortedHelper₁ : ∀ {A _≤_} {h : A} → ∀ {l'} → Sorted _≤_ l' → ∀ {l} → Permutation l l' → ConstrainedList (λ x → x ≤ h) l → ∀ {g'} → Sorted _≤_ g' → ∀ {g} → Permutation g g' → ConstrainedList (λ x → h ≤ x) g → Sorted _≤_ (l' ++ h ∷ g')
sortedHelper₁ sl' pll' cl nil _ _ = sortedHelper₂ sl' pll' cl one
sortedHelper₁ sl' pll' cl {h ∷ t} sg' pgg' cg = sortedHelper₂ sl' pll' cl $ two (constr-∈ cg $ perm-∈ (exact h t) pgg') sg'
quickSort : {A : Set} {_≤_ : A → A → Set} → (∀ x y → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l')
quickSort _ [] = [] , nil , refl
quickSort {A} {_≤_} _≤?_ (h ∷ t) = loop t [] [] [] [] refl
where loop : ∀ i l g → ConstrainedList (λ x → x ≤ h) l → ConstrainedList (λ x → h ≤ x) g → Permutation t ((l ++ g) ++ i) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation (h ∷ t) l')
loop [] l g cl cg p = l' ++ h ∷ g' , sortedHelper₁ sl' pll' cl sg' pgg' cg , perm-trans p₃ p₄
where lSort = quickSort _≤?_ l
gSort = quickSort _≤?_ g
l' = proj₁ lSort
g' = proj₁ gSort
sl' = proj₁ $ proj₂ lSort
sg' = proj₁ $ proj₂ gSort
pll' = proj₂ $ proj₂ lSort
pgg' = proj₂ $ proj₂ gSort
p₁ : Permutation (l ++ g) (l' ++ g')
p₁ = perm-++ pll' pgg'
p₂ : Permutation t (l' ++ g')
p₂ = perm-trans (≡-elim (++-[] (l ++ g)) (λ x → Permutation t x) p) p₁
p₃ : Permutation (h ∷ t) (h ∷ l' ++ g')
p₃ = perm-++ (refl {_} {[ h ]}) p₂
p₄ : Permutation (h ∷ l' ++ g') (l' ++ h ∷ g')
p₄ = perm-del-ins-r [] h l' g'
loop (h' ∷ t) l g cl cg p with h' ≤? h
... | inj₁ h'≤h = loop t (h' ∷ l) g (h'≤h ∷ cl) cg (perm-trans p p')
where p' : Permutation ((l ++ g) ++ h' ∷ t) (h' ∷ (l ++ g) ++ t)
p' = perm-del-ins-l [] (l ++ g) h' t
... | inj₂ h≤h' = loop t l (h' ∷ g) cl (h≤h' ∷ cg) (perm-trans p p')
where p₁ : l ++ g ++ h' ∷ t ≡ (l ++ g) ++ h' ∷ t
p₁ = ≡-sym $ ++-assoc l g (h' ∷ t)
p₂ : l ++ (h' ∷ g) ++ t ≡ (l ++ h' ∷ g) ++ t
p₂ = ≡-sym $ ++-assoc l (h' ∷ g) t
p₃ : (h' ∷ g) ++ t ≡ h' ∷ g ++ t
p₃ = ++-assoc [ h' ] g t
p₄ : l ++ h' ∷ g ++ t ≡ l ++ (h' ∷ g) ++ t
p₄ = ≡-sym $ ≡-elim p₃ (λ x → l ++ x ≡ l ++ h' ∷ g ++ t) refl
p₅ : Permutation (l ++ g ++ h' ∷ t) (l ++ h' ∷ g ++ t)
p₅ = perm-del-ins-l l g h' t
p₆ : Permutation ((l ++ g) ++ h' ∷ t) (l ++ h' ∷ g ++ t)
p₆ = ≡-elim p₁ (λ x → Permutation x (l ++ h' ∷ g ++ t)) p₅
p' : Permutation ((l ++ g) ++ h' ∷ t) ((l ++ h' ∷ g) ++ t)
p' = ≡-elim (≡-trans p₄ p₂) (λ x → Permutation ((l ++ g) ++ h' ∷ t) x) p₆
showl : List ℕ → String
showl [] = "[]"
showl (h ∷ t) = show h +s+ "∷" +s+ showl t
l₁ : List ℕ
l₁ = 19 ∷ 6 ∷ 13 ∷ 2 ∷ 8 ∷ 15 ∷ 1 ∷ 10 ∷ 11 ∷ 2 ∷ 17 ∷ 4 ∷ [ 3 ]
l₂ = quickSort decNat l₁
main = putCoStrLn ∘ toCostring $ showl $ proj₁ l₂
Пропозициональная эквивалентность
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
≡-cong : ∀ {a b} {A : Set a} {B : Set b} {x y} → x ≡ y → (f : A → B) → f x ≡ f y
≡-cong refl _ = refl
≡-elim : ∀ {l} {A : Set l} {x y : A} → x ≡ y → (P : A → Set l) → P x → P y
≡-elim refl _ p = p
≡-sym : ∀ {l} {A : Set l} {x y : A} → x ≡ y → y ≡ x
≡-sym refl = refl
≡-trans : ∀ {l} {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡-trans refl refl = refl
Как видим тут все просто: только одна аксиома, которая говорит, что два объекта равны, если они одно и то же. Также здесь определены вспомогательные функции для работой с доказательствами эквивалентности. Я думаю, тут более-мение все понятно. Поясню лишь на примере ≡-elim: единственным значением аргумента типа x ≡ y можеть быть refl, у которого есть один неявный параметр, который в строке ≡-elim refl _ p равный одновременно и x и y, по-этому и значение p имеет одновременно тип и P x и P y, а если значение p имеет тип P y, то в этой ситуации это и будет результат функции ≡-elim.
Ассоциативность операции конкатенации
++-assoc : ∀ {l} {A : Set l} (l₁ l₂ l₃ : List A) → (l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃)
++-assoc [] l₂ l₃ = refl
++-assoc (h ∷ t) l₂ l₃ = ≡-cong (++-assoc t l₂ l₃) (λ x → h ∷ x)
Тут $ — ни что иное как оператор аппликации, как в Haskell. Из определения понятно, что эта функция (или можна сказать лемма) доказывает для трех произвольных списков ассоциативность операции конкатенации. Хочу заметить, что во время компиляции термы частично редуцируются с использованием существующих определений. В данной функции происходит следующее:
терм
≡-cong (++-assoc t l₂ l₃) (λ x → h ∷ x)имеет тип
h ∷ (t ++ l₂) ++ l₃ ≡ h ∷ t ++ (l₂ ++ l₃)а нам нужен тип
(l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃)или
((h ∷ t) ++ l₂) ++ l₃ ≡ (h ∷ t) ++ (l₂ ++ l₃)это с учетом, что
l₁ = h ∷ t
далее компилятор, используя определение конкатенации редуцирует данные термы к некоторому общему виду.
Попробуйте с терма, используя определение конкатенации,
((h ∷ t) ++ l₂) ++ l₃ ≡ (h ∷ t) ++ (l₂ ++ l₃)получить терм
h ∷ (t ++ l₂) ++ l₃ ≡ h ∷ t ++ (l₂ ++ l₃)Также нужно учитывать, что операция конкатенации правоассоциативна — но это для понимания не принципиально.
Транзитивность и симметричность перестановки
perm-trans : ∀ {A} {l₁ l₂ l₃ : List A} → Permutation l₁ l₂ → Permutation l₂ l₃ → Permutation l₁ l₃
perm-trans p refl = p
perm-trans p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm l₁ x₁ x₂ l₂ $ perm-trans p₁ p₂
perm-sym : ∀ {A} {l₁ l₂ : List A} → Permutation l₁ l₂ → Permutation l₂ l₁
perm-sym refl = refl
perm-sym (perm l₁ x₁ x₂ l₂ p) = perm-trans (perm l₁ x₂ x₁ l₂ refl) (perm-sym p)
«Длинная» перестановка влево и вправо
perm-del-ins-r : ∀ {A} (l₁ : List A) (x : A) (l₂ l₃ : List A) → Permutation (l₁ ++ x ∷ l₂ ++ l₃) (l₁ ++ l₂ ++ x ∷ l₃)
perm-del-ins-r l₁ x [] l₃ = refl
perm-del-ins-r l₁ x (h ∷ t) l₃ = perm-trans p₀ p₅
where p₀ : Permutation (l₁ ++ x ∷ h ∷ t ++ l₃) (l₁ ++ h ∷ x ∷ t ++ l₃)
p₀ = perm l₁ h x (t ++ l₃) refl
p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃)
p₁ = perm-del-ins-r (l₁ ++ [ h ]) x t l₃
p₂ : (l₁ ++ [ h ]) ++ t ++ x ∷ l₃ ≡ l₁ ++ h ∷ t ++ x ∷ l₃
p₂ = ++-assoc l₁ [ h ] (t ++ x ∷ l₃)
p₃ : (l₁ ++ [ h ]) ++ x ∷ t ++ l₃ ≡ l₁ ++ h ∷ x ∷ t ++ l₃
p₃ = ++-assoc l₁ [ h ] (x ∷ t ++ l₃)
p₄ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
p₄ = ≡-elim p₂ (λ y → Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) y) p₁
p₅ : Permutation (l₁ ++ h ∷ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
p₅ = ≡-elim p₃ (λ y → Permutation y (l₁ ++ h ∷ t ++ x ∷ l₃)) p₄
perm-del-ins-l : ∀ {A} (l₁ l₂ : List A) (x : A) (l₃ : List A) → Permutation (l₁ ++ l₂ ++ x ∷ l₃) (l₁ ++ x ∷ l₂ ++ l₃)
perm-del-ins-l l₁ l₂ x l₃ = perm-sym $ perm-del-ins-r l₁ x l₂ l₃
Эти функции более интересные. Тут я лишь хочу отметить, что если рассматривать типы как теоремы или леммы, а термы соответствующего типа как доказательства, то очевидно, что доказательств определенного утверждения (как и термов соответствующего типа) может быть любое количество. Вот например мне кажется, что функцию выше можно доказать проще. Также интересно, что приведенный мной тип «отсортированный список» является своего рода синглтон: каждый тип имеет по одному представителю. А что касается перестановки, то для одного типа может быть бесконечное количество различных термов (можно например два раза переставить одни и те же элементы так, что списки не изменятся).
Порядок на натуральных числах
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
decNat : (x y : ℕ) → (x ≤ y) ⊎ (y ≤ x)
decNat zero y = inj₁ z≤n
decNat (suc x) (suc y) with decNat x y
... | inj₁ p = inj₁ (s≤s p)
... | inj₂ p = inj₂ (s≤s p)
decNat (suc x) zero = inj₂ z≤n
Ну и наконец разрешающая процедура для определения порядка на натуральных числах. (Обратите внимание как именуются переменные — все, что без пробелов есть терм.) Используется предикат _≤_. Вводятся две аксиомы, одна из которых говорит, что любое число больше или равно нуля, а другая, что если одно число больше равно другого, то соотношение сохранится, если к ним прибавить по единице.
Также тут используется конструкция with — но я думаю ее использование предельно ясно.
Вот и все:)
От себя скажу, что писать такие программы ну очень интересно.
Автор: dima_mendeleev
