git.iko.soy/Idris-dev
on master help sign in
Test commit after hosing my local copy of the repository through fiddling with git and reverts. Starting on a correctness proof of the heap implementation. Type checking now much faster.
34459abDominic Mulligan
lib/prelude/heap.idr+26
compare with master
unifiedsplit
@@ -30,6 +30,15 @@ total size : MaxiphobicHeap a -> Nat
30size Empty = O
30size Empty = O
31size (Node s l e r) = s
31size (Node s l e r) = s
32
32
33+isValidHeap : Ord a => MaxiphobicHeap a -> Bool
34+isValidHeap Empty = True
35+isValidHeap (Node s l e r) =
36+ dominates e l && dominates e r && s == S (size l + size r)
37+ where
38+ dominates : Ord a => a -> MaxiphobicHeap a -> Bool
39+ dominates e Empty = True
40+ dominates e (Node s l e' r) = e' <= e
41+
33--------------------------------------------------------------------------------
42--------------------------------------------------------------------------------
34-- Basic heaps
43-- Basic heaps
35--------------------------------------------------------------------------------
44--------------------------------------------------------------------------------
@@ -141,6 +150,23 @@ total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h =
141isEmptySizeZero Empty p = refl
150isEmptySizeZero Empty p = refl
142isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
151isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
143
152
153+total emptyHeapValid : Ord a => isValidHeap empty = True
154+emptyHeapValid = refl
155+
156+total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
157+singletonHeapValid e = refl
158+
159+{-
160+total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->
161+ (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->
162+ (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True
163+mergePreservesValidHeaps Empty Empty lp rp = refl
164+mergePreservesValidHeaps Empty (Node rs rl re rr) lp rp = rp
165+mergePreservesValidHeaps (Node ls ll le lr) Empty lp rp = lp
166+mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
167+ ?mergePreservesValidHeapsBody
168+-}
169+
144--------------------------------------------------------------------------------
170--------------------------------------------------------------------------------
145-- Proofs
171-- Proofs
146--------------------------------------------------------------------------------
172--------------------------------------------------------------------------------