I’m pretty confident that your property is a consequence of being SORTED; see
SORTED_EQ in sortingTheory for example.
You would then need to establish that your function does indeed create lists
that are SORTED.
Your property0 is also too specific, you shouldn’t require pop = mySort pop.
Hi Michael,
I have been seen these documents before, but there is no theorem same to which
I wanted. Also, I try to use QSORT to prove the property1 which same as
property0, as follows:
!xs. EVERY (\y. HD (QSORT (\x. $<= x) xs) <= y) xs
Induct >-
RW_TAC list_ss [] >>
RW_TAC list_ss
You might like to try the following
(1) a predicate sorted, to mean each list member is <= the next one
(2) a lemma that inserting an element into a sorted list gives a sorted list
Jeremy
On 04/12/17 12:58, Liu Gengyang wrote:
Hi,
Recently I am meeting a problem, it has been confusing me a
There are proofs that quick-sort and merge-sort are correct in the distribution
already. Perhaps looking at these examples in src/sort will give you some
clues.
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 13:02
To: hol4_QA
Hi,
Recently I am meeting a problem, it has been confusing me a few days, seeking
for help.
I defined a sorting predicate mySort:
val insert_def = Define `
(insert x [] = [x]) /\
(insert x (h::t) = if x <= h
then (x::h::t)
else (h::(insert x t)))`;
val
