Skip to content

Instantly share code, notes, and snippets.

@barakmich
Created January 4, 2018 22:59
Show Gist options
  • Save barakmich/0acc709290c46d74a8585cd83a7fa270 to your computer and use it in GitHub Desktop.
Save barakmich/0acc709290c46d74a8585cd83a7fa270 to your computer and use it in GitHub Desktop.
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
@clayrat
Copy link

clayrat commented Jan 5, 2018

You need to mirror the structure of msorted:

placeSortedProof : (x : Nat) -> (xs : List Nat) -> msorted xs = True -> msorted (placeSorted x xs) = True
placeSortedProof x [] prf = Refl
placeSortedProof x [y] prf with (x <= y) proof p 
  placeSortedProof x [y] prf | True = rewrite sym p in Refl
  placeSortedProof x [y] prf | False = ?wat
placeSortedProof x (y :: y' :: ys) prf with (x <= y) proof p
  placeSortedProof x (y :: y' :: ys) prf | True = rewrite sym p in prf
  placeSortedProof x (y :: y' :: ys) prf | False with (x <= y') proof p'
    placeSortedProof x (y :: y' :: ys) prf | False | True = rewrite sym p' in ?wat2
    placeSortedProof x (y :: y' :: ys) prf | False | False = let tt = placeSortedProof x ys ?prf in ?wat3

To fill wat and wat2 you also need functions to rotate inequalities ala x<=y = False -> y<x = True.
For wat3 you'll also need a lemma that y < x = True -> msorted (placeSorted x xs) = True -> msorted (y :: placeSorted x xs) = True
(Also you might as well switch to So)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment