Fulcrum.agda

module Fulcrum where

open import Data.Maybe using (Maybe ; nothing ; just)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Vec
open import Relation.Nullary
open import Data.Product hiding (map)
open import Data.Fin hiding (_+_ ; _-_ ; _≤_ ; _<_)
open import Data.Sum using (_⊎_ ; [_,_]′ ; inj₁ ; inj₂)
open import Data.Integer hiding (suc ; _+_ ; _≤_ ; _<_)
open import Relation.Binary.PropositionalEquality
open import Data.Empty

-- Take the sum of a vector of integers.
sumint : ∀ {n} -> Vec ℤ n -> ℤ
sumint = foldr _ Data.Integer._+_ (+ 0)

-- Decidable and total preorders.
record DecTotPre {A : Set} (_R_ : A -> A -> Set) : Set where
  field
    dec : ∀ x y -> Dec (x R y)
    rf  : ∀ {x} -> x R x
    tr  : ∀ {x y z} -> x R y -> y R z -> x R z
    tot : ∀{x y} -> x R y ⊎ y R x
open DecTotPre

tot' : {A : Set} {_R_ : A -> A -> Set} -> DecTotPre _R_ -> ∀{x y} -> ¬ (x R y) -> y R x
tot' r {x} {y} p = [ (λ w → ⊥-elim (p w)) , (λ z → z) ]′ (tot r {x} {y})

-- Given a non-empty vector of elements of A, and a decidable total preorder _≤_ on A,
-- find the index i such that the i-th element is the minimum among all elements,
-- according to _≤_.
--
-- The returned index is guaranteed to be within bounds.
minimum : ∀{n} {A : Set}
       -> (_≤_ : A -> A -> Set) -> DecTotPre _≤_
       -> (xs : Vec A (suc n))
       -> Σ (Fin (suc n)) λ i → ∀ j -> lookup i xs ≤ lookup j xs
minimum {zero} _≤_ r (x ∷ []) = zero , λ { zero → rf r ; (suc ()) }
minimum {suc n} _≤_ r (x ∷ xs) with minimum _≤_ r xs
minimum _≤_ r (x ∷ xs) | i , p with dec r x (lookup i xs)
minimum _≤_ r (x ∷ xs) | i , p | yes q = zero , λ { zero → rf r ; (suc j) → tr r q (p j) }
minimum _≤_ r (x ∷ xs) | i , p | no ¬p = suc i , λ { zero → tot' r ¬p ; (suc j) → p j }

-- Given a natural number n, return the vector 0..n-1.
indices : (n : ℕ) -> Vec (Fin n) n
indices zero = []
indices (suc n) = zero ∷ map (raise 1) (indices n)

-- The element at the i-th position of a vector of indices is the index i itself.
lkp : ∀{n} -> (i : Fin n) -> lookup i (indices n) ≡ i
lkp zero = refl
lkp {suc n} (suc i) = trans (aux i (indices n) {raise 1}) (cong suc (lkp i))
  where
    aux : {A B : Set} -> ∀{n} (i : Fin n) (xs : Vec A n) {f : A -> B}
         -> lookup i (map f xs) ≡ f (lookup i xs)
    aux zero (x ∷ xs) = refl
    aux (suc i) (x ∷ xs) = aux i xs

-- A natural number i in the set of naturals below n is provably so.
fin-bound : ∀{n} -> (i : Fin n) -> toℕ i < n
fin-bound zero = s≤s z≤n
fin-bound (suc x) = s≤s (fin-bound x)

-- If i ≤ n, then there exists some remainder m, such that n ≡ i + m.
factor : ∀{i n} -> i ≤ n -> Σ ℕ λ m -> n ≡ i + m
factor z≤n = _ , refl
factor (s≤s p) = _ , cong suc (proj₂ (factor p))

-- Take the first i elements of a vector of at least i elements.
take' : {A : Set} -> ∀{i n} -> i ≤ n -> Vec A n -> Vec A i
take' {A} {i} p v = take i (subst (Vec A) (proj₂ (factor p)) v)

-- Drop the first i elements from a vector of at least i elements.
drop' : {A : Set} -> ∀{i n} -> i ≤ n -> Vec A n -> Σ ℕ (Vec A)
drop' {A} {i} p v = _ , (drop i (subst (Vec A) (proj₂ (factor p)) v))

-- Given a vector xs and an index within bounds,
-- compute | sum(xs[..i]) - sum(xs[i..]) |.
compute-sum : ∀{n} -> Vec ℤ n -> (i : Fin n) -> ℕ
compute-sum xs i = ∣ sumint (take' i-times xs) - sumint (proj₂ (drop' i-times xs)) ∣
  where suc-i-times = <⇒≤pred (fin-bound (suc i)) ; i-times = <⇒≤ (fin-bound i)

-- Two valid indices i, j for a vector xs are related iff the corresponding
-- computed sum is related by _≤_.
R : ∀{n} -> Vec ℤ n -> Fin n -> Fin n -> Set
R xs i j = compute-sum xs i ≤ compute-sum xs j

-- The relation on indices R defined above is a decidable, total preorder.
myRel : ∀{n} -> (xs : Vec ℤ n) -> DecTotPre (R xs)
myRel {n} xs =
  record { dec = λ x y → Data.Nat._≤?_ _ _
         ; rf = ≤-reflexive refl ; tr = ≤-trans ; tot = ≤-total _ _ }

-- Given a vector of integers, either it is empty, or we can find an index i
-- that is guaranteed to be within bounds, and such that for any index j,
-- | sum(xs[..i]) - sum(xs[i..]) | ≤ | sum(xs[..j]) - sum(xs[j..]) |.
fulcrum : ∀{n} -> (xs : Vec ℤ n)
     -> n ≡ 0  -- either it is empty

     -- or we can find an index i that is within bounds, and such that
     -- for any index j, | sum(xs[..i]) - sum(xs[i..]) | ≤ | sum(xs[..j]) - sum(xs[j..]) |.
      ⊎ Σ (Fin n) (λ i → ∀ j -> compute-sum xs i ≤ compute-sum xs j)

fulcrum {zero} xs = inj₁ refl
fulcrum {suc n} xs =
  inj₂ (proj₁ aux , λ j → subst₂ (R xs) (lkp (proj₁ aux)) (lkp j) (proj₂ aux j))
  where aux = minimum (R xs) (myRel xs) (indices (suc n))

fulcrum' : ∀{n} -> (xs : Vec ℤ n) -> Maybe ℕ
fulcrum' xs = [ (λ _ -> nothing) , (λ x → just (toℕ (proj₁ x))) ]′ (fulcrum xs)

test1 : fulcrum' (+ 5 ∷ + 5 ∷ + 10 ∷ []) ≡ just 2
test1 = refl

test2 : fulcrum' (+ 1 ∷ + 2 ∷ + 3 ∷ + 4 ∷ + 5 ∷ + 0 - (+ 7) ∷ []) ≡ just 2
test2 = refl