💟 🍕 👩‍👧 Agdaで検証済みのQuickSort 💍 👩🏽‍🤝‍👨🏿 👩‍🔬

親愛なるhabrayuzerさん、こんにちは！

型付きラムダ計算、つまり依存型に関するいくつかの本を読んだ後、興味深いパターンを見ました：どこでも、最初の例はソートされたリスト型の定義です。すべては問題ありませんが、この定義を超えるものはありませんでした。そこで、このギャップを見つけて、リストを取得して別のリストと2つの証明を返す関数を実装しました。 1つは結果が入力の順列であることを証明し、もう1つは結果がソートされたリストであることを証明します。

正式な説明

このパートでは、後で使用する主なタイプといくつかの補助機能を示します。また、Agdaの興味深い構文上の魅力もここに示されます。 Agdaにあまり詳しくない人のために、会議SPbHUG / FProg 2012-07 で Jan Malakhovskyのビデオ/スライドを見ることをお勧めします。または、Agda Webサイト（大きくはありません）またはこのチュートリアルからマニュアルをめくる。

リスト定義

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)

ここにリストがあります。標準ライブラリから取得した定義。ご覧のとおり、リストアイテムは、任意のタイプの値、さらにはタイプやタイプのタイプなどの値にすることができます。これは、高次ポリモーフィズムの使用により可能です。レベルを担当するパラメーターが導入されます。つまり、通常の型はSet 0型、 Set 0はSet 1型などです。
また、この定義では、Agdaで演算子がどのように宣言されているか、つまり引数がある場所にアンダースコアを使用して宣言できます。このメソッドを使用すると、単一の要素[_]からリストを返す関数など、さまざまな非常に興味深い形式を定義できることに注意してください。

すべての演算子（アンダースコア付きのコンビネータ）に対して、優先度と結合性を指定できることに注意してください。また、Agdaでは、スペースとブラケット（丸括弧および中括弧）のないUnicodeシーケンスは用語です。
また、括弧と中括弧にも注意を払う必要があります。型を示す中括弧は、この引数が暗黙的であり、コンパイラーによって出力されることを示します。

「ソート済みリスト」と入力します

 data Sorted {A} (_≤_ : A → A → Set) : List A → Set where nil : Sorted _≤_ [] one : {x : A} → Sorted _≤_ [ x ] two : {x : A} → ∀ {yl} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l)

これは、ソートされたリストの述語の定義です。設計者は公理と見なされるべきです。 nilの公理と空のリストと1つの要素からのリストがソートされるという公理があります。また、 並べ替えられた型は、順序を担当する述語_≤_に依存していることがわかります 。これは、比較関数のようなものですが、依存型です（引数は通常の型の値であり、結果は値が証明である型です）。公理2は、 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 ll perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂)

タイプ（述語）「順列」。引数は2つのリストです。導入された公理は次のとおりです。refl-リストはそれ自体の順列です。 perm-あるリストlが別のリストlの順列であることの証明がある場合（この証明は型permutation l（l₁++x₂∷x₁∷l₂）の値です ）、任意の2つのリストを並べ替える場合要素を配置すると、新しいリストは最初のリストの順列であることがわかります。

「量」と入力します

 data _⊎_ {ab} (A : Set a) (B : Set b) : Set (a ⊔ b) where inj₁ : (x : A) → A ⊎ B inj₂ : (y : B) → A ⊎ B

さて、ここではすべてが単純です-それは依存型ではなく-Haskellのいずれかの類似物です。

製品の種類

 record Σ {ab} (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 _×_ : ∀ {ab} (A : Set a) (B : Set b) → Set (a ⊔ b) A × B = Σ[ _ ∶ A ] B

これはタプルの類似物です。この型はコンストラクタを1つしか持つことができないため、 レコードが使用されます。この定義は依存型を使用します。最初の要素は特定の値であり、2番目はこの要素に対する何らかの述語の実行の証明です。しかし、もちろん、そのように使用する必要はありません。通常のタプルのように（ _×_を介して）実行できます-要素間の依存関係は無視されます。 構文を使用すると、単純な可能性が少ない場合に新しい構文構成を定義できます。

ソート機能

 sort : {A : Set} {_≤_ : A → A → Set} → (∀ xy → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l')

最後に、ソート関数のタイプを説明します：この関数は、順序を決定する（暗黙の）述語、および入力値に対して、1番目が2番目より大きい、または2番目が1番目より大きいという証明を返す関数を受け入れます。読者は、ソートされたリスト結果の証明を作成するためにこの関数が使用されると推測したと思います。また、もちろん、入力パラメーターの1つはソートされるリストです。
ソート関数は、リストと2つの証明（ソートと順列）を返します。

ソート機能の実装

もちろん、ここではこの関数の実装はありません。コードを表示してすみませんが、自分で説明してすみません。したがって、ソート関数を作成するときに必要ないくつかの補助関数の証明（実装）を提供します。

動作するソースはここにあります。

使用されるAgda-2.3.1および標準ライブラリ-0.6

 {-# 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} → ∀ {yl} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l) data Permutation {A} : List A → List A → Set where refl : ∀ {l} → Permutation ll perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂) ≡-elim : ∀ {l} {A : Set l} {xy : A} → x ≡ y → (P : A → Set l) → P x → P y ≡-elim refl _ p = p ≡-sym : ∀ {l} {A : Set l} {xy : A} → x ≡ y → y ≡ x ≡-sym refl = refl ≡-trans : ∀ {l} {A : Set l} {xyz : 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 : (xy : ℕ) → (x ≤ y) ⊎ (y ≤ x) decNat zero y = inj₁ z≤n decNat (suc x) (suc y) with decNat xy ... | inj₁ p = inj₁ (s≤sp) ... | inj₂ p = inj₂ (s≤sp) 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₁ hx (t ++ l₃) refl p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃) p₁ = perm-del-ins-r (l₁ ++ [ h ]) xt 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 : ∀ ht → h ∈ h ∷ t cons : ∀ h {xl} → 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 ll' → 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 ll' → ConstrainedList (λ x → x ≤ h) l → ∀ {g'} → Sorted _≤_ g' → ∀ {g} → Permutation gg' → 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 ht) pgg') sg' quickSort : {A : Set} {_≤_ : A → A → Set} → (∀ xy → (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 : ∀ ilg → 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 [] lg 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 tx) 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 [] hl' g' loop (h' ∷ t) lg 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 tl (h' ∷ g) cl (h≤h' ∷ cg) (perm-trans p p') where p₁ : l ++ g ++ h' ∷ t ≡ (l ++ g) ++ h' ∷ t p₁ = ≡-sym $ ++-assoc lg (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' ] gt 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 lgh' 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 : ∀ {ab} {A : Set a} {B : Set b} {xy} → x ≡ y → (f : A → B) → fx ≡ fy ≡-cong refl _ = refl ≡-elim : ∀ {l} {A : Set l} {xy : A} → x ≡ y → (P : A → Set l) → P x → P y ≡-elim refl _ p = p ≡-sym : ∀ {l} {A : Set l} {xy : A} → x ≡ y → y ≡ x ≡-sym refl = refl ≡-trans : ∀ {l} {A : Set l} {xyz : A} → x ≡ y → y ≡ z → x ≡ z ≡-trans refl refl = refl

ここでわかるように、すべてが単純です。公理は1つだけであり、2つのオブジェクトが同一である場合に等しいということです。また、等価性の証明を処理するための補助関数も定義します。ここではすべてが明確だと思います。 ≡-elimの例でのみ説明します： x≡y型の引数の唯一の値はreflであり、暗黙のパラメーターが1つあり、which -elim refl _ p行では同時にxとyに等しいため、値p typeおよび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の場合のように、 $はアプリケーション演算子にすぎません。定義から、この関数（または補題と言えます）が3つの任意のリストの連結操作の結合性を証明することは明らかです。コンパイル中に、既存の定義を使用して用語が部分的に削減されることに注意してください。この機能では、次のことが行われます。
期間

 ≡-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₁ hx (t ++ l₃) refl p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃) p₁ = perm-del-ins-r (l₁ ++ [ h ]) xt 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₃

これらの機能はより興味深いものです。ここで、型を定理または補題とみなし、対応する型の用語を証拠と見なす場合、特定のステートメントの証拠（および対応する型の用語）がいくつあってもよいことは明らかです。たとえば、上記の機能は簡単に証明できるように思えます。また、私が引用したソート済みリストのタイプが一種のシングルトンであることも興味深いです。各タイプには1つの代表があります。順列に関しては、1つのタイプに対して、無限の数の異なる用語が存在する可能性があります（たとえば、リストが変更されないように、同じ要素を2回再配置できます）。

自然数で注文する

 data ℕ : Set where zero : ℕ suc : ℕ → ℕ data _≤_ : ℕ → ℕ → Set where z≤n : ∀ {n} → zero ≤ n s≤s : ∀ {mn} (m≤n : m ≤ n) → suc m ≤ suc n decNat : (xy : ℕ) → (x ≤ y) ⊎ (y ≤ x) decNat zero y = inj₁ z≤n decNat (suc x) (suc y) with decNat xy ... | inj₁ p = inj₁ (s≤sp) ... | inj₂ p = inj₂ (s≤sp) decNat (suc x) zero = inj₂ z≤n

そして最後に、自然数の順序を決定するための解決手順。（変数の名前の付け方に注意してください-スペースのない用語を持つものすべて。）述語_≤_が使用されます。 2つの公理が導入され、1つは任意の数がゼロ以上であることを示し、もう1つは、1つの数がもう1つより大きい場合、1つが追加された場合に比率が保持されることを示します。
ここでもwith構文が使用されていますが、その使用法は非常に明確だと思います。

それだけです:)

このようなプログラムを書くことは非常に興味深いと自分から言います。

Agdaで検証済みのQuickSort