verified fulcrum in agda

Fulcrum.agda

module Fulcrum where

open import Data.Integer as ℤ
open import Data.List hiding (sum)
open import Data.List.Any; open Membership-≡
open import Data.Nat as ℕ using (ℕ; _∸_)
open import Data.Product
open import Data.Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty

sum : List ℤ → ℤ
sum = foldr _+_ (+ 0)

abs : ℤ → ℤ
abs x = + ∣ x ∣

-- ≤ is a decidable total ordering on ℤ.
open DecTotalOrder decTotalOrder using (total) renaming (refl to ≤-refl; trans to _∙_)

invert : ∀{x y} → ¬(x ≤ y) → y ≤ x -- if it ain't one way, it's t'other
invert {x}{y} ¬x≤y with total x y
... | inj₁ x≤y = ⊥-elim (¬x≤y x≤y)
... | inj₂ y≤x = y≤x

-- A verified minimum-finder. Finds the element of a non-empty list which yields
-- the minimum output under an ℤ-valued "weight" function.
module _ {a : Set} (weight : a → ℤ) where
  Min : a → List a → Set
  -- "x is the minimum element of l"
  Min x l = x ∈ l × ∀ {y} → y ∈ l → weight x ≤ weight y

  -- Given a nonempty list, find its minimum.
  findMin : (x : a) → (xs : List a) → Σ[ min ∈ a ] Min min (x ∷ xs)
  findMin x [] = x , here refl , λ { (here refl) → ≤-refl ; (there ()) }
  findMin x (x₁ ∷ xs) with findMin x₁ xs
  ... | min , posn , tiny with weight x ≤? weight min
  ... | yes p = x , here refl , λ { (here refl) → ≤-refl ; (there posn) → p ∙ tiny posn }
  ... | no ¬p = min , there posn , λ { (here refl) → invert ¬p ; (there posn) → tiny posn }

-- I'm not sure this `fv` lines up with the one in Hillel's Dafny program. I
-- think my use of indices may be off by one. This hilights a problem with
-- verification: what if the spec is wrong?
fv : List ℤ → ℕ → ℤ
fv elems i = abs (sum (take i elems) - sum (drop i elems))

-- Finds the valid indices into a list. Another place spec-incorrectness could
-- creep in. Perhaps I should "verify" this function by relating it to the type
-- of elements of a list, (_ ∈ l). Then my spec would have a spec!
indices : ∀{a : Set} → List a → List ℕ
indices [] = []
indices (x ∷ xs) = length xs ∷ indices xs

Fulcrum : ℕ → List ℤ → Set
-- "i is the index of the fulcrum of elems"
Fulcrum i elems = Min (fv elems) i (indices elems)

-- A slow verified implementation of Fulcrum just uses findMin directly:
findFulcrumSlow : (x : ℤ) (xs : List ℤ) → Σ[ i ∈ ℕ ] Fulcrum i (x ∷ xs)
findFulcrumSlow x xs = findMin (fv (x ∷ xs)) (length xs) (indices xs) 

-- A faster verified implementation uses running totals each way.
-- TODO.