git.iko.soy/Idris-dev
on master help sign in
Replace some Heap proofs with impossible.
5d71e52Stephen Drodge
libs/base/Data/Heap.idr+5−20
compare with master
unifiedsplit
@@ -5,6 +5,7 @@
5
5
6module Data.Heap
6module Data.Heap
7
7
8+%default total
8%access public
9%access public
9
10
10abstract data MaxiphobicHeap : Type -> Type where
11abstract data MaxiphobicHeap : Type -> Type where
@@ -82,12 +83,12 @@ insert e = merge $ singleton e
82--------------------------------------------------------------------------------
83--------------------------------------------------------------------------------
83
84
84findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a
85findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a
85−findMinimum Empty p = ?findMinimumEmptyAbsurd
86+findMinimum Empty refl impossible
86−findMinimum (Node s l e r) p = e
87+findMinimum (Node s l e r) p = e
87
88
88deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a
89deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a
89−deleteMinimum Empty p = ?deleteMinimumEmptyAbsurd
90+deleteMinimum Empty refl impossible
90−deleteMinimum (Node s l e r) p = merge l r
91+deleteMinimum (Node s l e r) p = merge l r
91
92
92--------------------------------------------------------------------------------
93--------------------------------------------------------------------------------
93-- Conversions to and from lists (and a derived heap sorting algorithm)
94-- Conversions to and from lists (and a derived heap sorting algorithm)
@@ -173,22 +174,6 @@ isEmptySizeZeroNodeAbsurd = proof {
173 exact p;
174 exact p;
174}
175}
175
176
176−findMinimumEmptyAbsurd = proof {
177− intros;
178− refine FalseElim;
179− refine absurdBoolDischarge;
180− rewrite p;
181− trivial;
182−}
183−
184−deleteMinimumEmptyAbsurd = proof {
185− intros;
186− refine FalseElim;
187− refine absurdBoolDischarge;
188− rewrite p;
189− trivial;
190−}
191−
192--------------------------------------------------------------------------------
177--------------------------------------------------------------------------------
193-- Debug
178-- Debug
194--------------------------------------------------------------------------------
179--------------------------------------------------------------------------------