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 <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Proof about sorting
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 mySort_def = Define `
(mySort [] = []) /\
(mySort (h::t) = (insert h (mySort t)))`;
EVAL ``mySort [2;4;1;5;3;2]``
> val it = |- mySort [2; 4; 1; 5; 3; 2] = [1; 2; 2; 3; 4; 5] : thm
Now I want to prove the property0: for any pop: list, if it is sorted by
mySort, the first element in pop will less than or equal to other elements in
pop.
I try to represent property0 in HOL4, but I meet a question, that is ``mySort
pop`` isn't a bool term, so I use two ways to solve it:
1, !pop. (pop = mySort pop) ==> EVERY(\x. (HD pop) <= x) pop
2, !pop. EVERY (\x. HD (mySort pop) <= x) (mySort pop)
However, I can't prove both of them. When I used the Induct tactic to `pop` or
`mySort pop`, the goal will be more and more complex, and the property0 can't
reflect in the proving process, it seems unsolvable. Does the representation of
1 and 2 is wrong, or the definition of mySort is wrong too？How can I prove the
property0?
By the way, I prove 3 property about mySort and insert during I prove 1 and 2.
val INSNOTNULL_POP = prove(``!h pop.insert h pop <> []``,
RW_TAC std_ss [] >>
Cases_on `pop` >-
RW_TAC list_ss [insert_def] >>
RW_TAC list_ss [insert_def]);
val SORTNOTNULL_POP = prove(``!pop. pop <> [] ==> mySort pop <> [] /\ (mySort
pop= insert (HD pop) (mySort (TL pop)))``,
RW_TAC list_ss [] >| [
Cases_on `pop` >-
RW_TAC list_ss [mySort_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP],
Induct_on `pop` >-
RW_TAC list_ss [] >>
RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def]
]);
val SORTNULL_POP = prove(``!pop. (pop = []) <=>(mySort pop = [])``,
GEN_TAC >>
EQ_TAC >-
RW_TAC list_ss [mySort_def] >>
Induct_on `pop` >-
RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def] >>
Cases_on `pop` >-
RW_TAC list_ss [mySort_def,insert_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP]);
Regards,
Liu
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
