@@ -30,6 +30,15 @@ total size : MaxiphobicHeap a -> Nat
3030size Empty = O
3131size (Node s l e r) = s
3232
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+
3342--------------------------------------------------------------------------------
3443-- Basic heaps
3544--------------------------------------------------------------------------------
@@ -141,6 +150,23 @@ total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h =
141150isEmptySizeZero Empty p = refl
142151isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
143152
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+
144170--------------------------------------------------------------------------------
145171-- Proofs
146172--------------------------------------------------------------------------------