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 [listTheory.EVERY_DEF,QSORT_DEF] >| [
FULL_SIMP_TAC list_ss [PARTITION_DEF] >>
Cases_on `xs` >| [
FULL_SIMP_TAC list_ss [PART_DEF,listTheory.EVERY_DEF] >>
`l1 = []` by RW_TAC std_ss [] >>
`l2 = []` by RW_TAC std_ss [] >>
FULL_SIMP_TAC list_ss [QSORT_DEF],
……
(*Here,I think I need to prove any elements in l1 are smaller than h firstly,
then to prove HD [x++y++z] = HD [x], so I can prove this subgoal.
Unfortunately, I am failed*)
In addition, I think the definition about sorting(i.e. mergesortN_curried_def,
QSORT_curried_DEF, QSORT3_curried_DEF etc.) in mergesortTheory and
sortingTheory is different from mine. Even if I proved property1, I still can't
prove property0.
Regards,
Liu
-----Original Messages-----
From:michael.norr...@data61.csiro.au
Sent Time:2017-12-04 11:03:39 (Monday)
To: 2015200...@mail.buct.edu.cn, hol-info@lists.sourceforge.net
Cc:
Subject: Re: [Hol-info] Proof about sorting
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
