That's to say, I need to create my own sorted predicate? I realised it in the
past few days, however, I have no idea about this, I always wanted to implement
it by myself. But now, I find I just need to use SORTED,as follows:
val mysorted_def = Define `
mysorted xs = SORTED (\x y. x <= y) xs`
Thank you very much! I will try my proofs again.
Regards,
Liu
-----Original Messages-----
From:michael.norr...@data61.csiro.au
Sent Time:2017-12-04 13:35:21 (Monday)
To: 2015200...@mail.buct.edu.cn
Cc: hol-info@lists.sourceforge.net
Subject: Re: [Hol-info] Proof about sorting
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.
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 14:38
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
Cc: hol4_QA <hol-info@lists.sourceforge.net>
Subject: Re: Re: [Hol-info] Proof about sorting
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
