module ListProof

import Prelude.List
import Prelude.Nat
import Prelude.Bool

%access public export

ifelse : (b : Bool) -> (t : a) -> (e : a) -> a
ifelse False t e = e
ifelse True t e = t

placeSorted : (n : Nat) -> (l : List Nat) -> List Nat
placeSorted n [] = [n]
placeSorted n (x :: xs) =
  ifelse (n <= x)  (n :: x :: xs) (x :: (placeSorted n xs))

bubbleSortNat : (l : List Nat) -> List Nat
bubbleSortNat [] = []
bubbleSortNat (x :: xs) =
  let nl = bubbleSortNat xs in
      placeSorted x nl

testSort : bubbleSortNat [3, 2, 4, 1] = [1, 2, 3, 4]
testSort = Refl

msorted : (l : List Nat) -> Bool
msorted [] = True
msorted (x :: []) = True
msorted (x :: (y :: xs)) = ifelse (x <= y) (msorted (y :: xs)) False

testSorted : msorted [3, 2, 4, 1] = False
testSorted = Refl

lemMsorted : (x : Nat) -> (xs : List Nat) -> msorted (x :: xs) = True -> msorted xs = True
lemMsorted x [] prf = Refl
lemMsorted x (y :: ys) prf with (x <= y) proof p
  lemMsorted x (y :: ys) prf | True = prf
  lemMsorted x (y :: ys) prf | False = absurd prf


placeSortedProof : (x : Nat) -> (xs : List Nat) -> msorted xs = True -> msorted (placeSorted x xs) = True
placeSortedProof x [] prf = Refl
placeSortedProof x (y :: xs) prf with (x <= y) proof p
  placeSortedProof x (y :: xs) prf | True = rewrite sym p in prf
  placeSortedProof x (y :: xs) prf | False = ?placeSortedProof_rhs