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

Reply via email to