📥 Download raw
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Connectives.Disjunction

module Padova2025.VerifiedAlgorithms.InsertionSort.CorrectByConstruction
  (A : Set) (_≤_ : A → A → Set) (-∞ : A) (min! : {x : A} → -∞ ≤ x) (cmp? : (x y : A) → x ≤ y ⊎ y ≤ x) where

Correct by construction

Ordered output lists

Let us introduce the type OList l of ascendingly ordered lists where all elements are ≥ l. In other words, OList l is the type of ordered lists bounded from below by l.

data OList (l : A) : Set where
  nil  : OList l
  cons : (x : A) → l ≤ x → OList x → OList l

insert : {l : A} → (x : A) → l ≤ x → OList l → OList l
insert = {!!}

sort : List A → OList -∞
sort = {!!}

An alternative definition of ordered lists is as follows.

open import Padova2025.ProvingBasics.Termination.Gas using (𝟙; tt)

data OList₁ : Set
_≤head_ : A → OList₁ → Set

data OList₁ where
  nil  : OList₁
  cons : (x : A) (xs : OList₁) → x ≤head xs → OList₁

x ≤head nil         = 𝟙
x ≤head cons y ys _ = x ≤ y

However, working with this alternative definition is a bit more cumbersome than with OList.

Expand.

Ordered and permuted output lists

As in the module on post-hoc verification, let us now also ensure in a correct-by-construction way that the output list produced by insertion sort is a permutation of the input list.

The following type declaration is as in the module on post-hoc verification.

data _◂_↝_ : A → List A → List A → Set where
  here  : {x : A} {xs : List A} → x ◂ xs ↝ (x ∷ xs)
  there : {x y : A} {ys xys : List A} → x ◂ ys ↝ xys → x ◂ (y ∷ ys) ↝ (y ∷ xys)

The type OPList l xs is the type of ordered lists whose elements are bounded from below by l and which are permutations of xs.

data OPList (l : A) : List A → Set where
  nil  : OPList l []
  cons : {ys xys : List A} → (x : A) → OPList x ys → l ≤ x → (x ◂ ys ↝ xys) → OPList l xys

As the outputs are now sufficiently constrained by the types, Agda’s automatic proof search C-c C-a will be able to correctly fill in several key terms in the following two definitions.

insert' : {l : A} {ys : List A} → (x : A) → OPList l ys → l ≤ x → OPList l (x ∷ ys)
insert' = {!!}

sort' : (xs : List A) → OPList -∞ xs
sort' = {!!}

Comment on the requirement of -∞.