{-# OPTIONS --cubical-compatible #-}
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Connectives.Disjunction

module Padova2025.VerifiedAlgorithms.InsertionSort.Implementation
  (A : Set) (_≤_ : A → A → Set) (cmp? : (x y : A) → x ≤ y ⊎ y ≤ x) where

Implementation#

Explanation

Contract: “insert x ys” is ascendingly ordered, if “ys” is ascendingly ordered.

Exercise 1insert

insert : A → List A → List A
insert = {!!}

The reference solution uses: [] _∷_ left right

Your solution

Reference solution

insert : A → List A → List A
insert x []       = x ∷ []
insert x (y ∷ ys) with cmp? x y
... | left  x≤y = x ∷ (y ∷ ys)
... | right y≤x = y ∷ insert x ys

Exercise 2sort

sort : List A → List A
sort = {!!}

The reference solution uses: [] _∷_ insert

Your solution

Reference solution

sort : List A → List A
sort []       = []
sort (x ∷ xs) = insert x (sort xs)