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 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] : thmNow 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
------------------------------------------------------------------------------ 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
