More list simps

[ordinarymath]

Add more simps about lists
This adds LENGTH_TAKE_EQ_MIN
and makes DROP_TAKE_EQ_NIL simps.
Rational for making LENGTH_TAKE_EQ_MIN simp is that
before that rewriting
DROP n (TAKE n ls) = []
would rewrite with DROP_EQ_NIL
!ls n. DROP n ls = [] <=> LENGTH ls <= n
to
LENGTH (TAKE n ls) <= n
With this simp rule it will rewrite to
MIN n (LENGTH ls) <= n

[binghe]

List auto simplifications should be updated carefully because many user code depends on the current (imperfect) status.

I don't like the following theorems becoming automatic, because 1) the RHS term didn't get smaller; 2) number subtractions and MIN are hard to handle and many times unexpected; 3) There are other ways to rewrite TAKE, DROP and LENGTH (TAKE ..), and user should be able to choose theorem after rw [] and simp [].

TAKE n (x::xs) = x::(TAKE (n-1) xs)
DROP n (x::xs) = DROP (n-1) xs
LENGTH (TAKE n xs) = MIN n (LENGTH xs)

[ordinarymath]

TAKE n (x::xs) = x::(TAKE (n-1) xs)
DROP n (x::xs) = DROP (n-1) xs

I'm confused. These two theorems were already simp.

[ordinarymath]

I just updated the syntax from using export_rewrites.

[ordinarymath]

LENGTH (TAKE n xs) = MIN n (LENGTH xs)

For this theorem I have realized that HOL4 is terrible with MIN and MAX. I plan to write a general conv simp procedure on lattices while this PR remains as a draft.

[binghe]

I just updated the syntax from using export_rewrites.

Alright, it seems that TAKE_cons is the main device to rewrite TAKE on literal lists:

> SRULE [] (ASSUME ``TAKE 3 [1;2;3;4;5] = l``);
[31541]:   rewriting TAKE 3 [1; 2; 3; 4; 5] with [rewrite:TAKE_cons.1]|- 0 < n ==> TAKE n (x::xs) = x::TAKE (n - 1) xs
[34890]:   rewriting TAKE (3 - 1) [2; 3; 4; 5] with [rewrite:TAKE_cons.1]|- 0 < n ==> TAKE n (x::xs) = x::TAKE (n - 1) xs
[38728]:   rewriting TAKE (3 - 1 - 1) [3; 4; 5] with [rewrite:TAKE_cons.1]|- 0 < n ==> TAKE n (x::xs) = x::TAKE (n - 1) xs
[42678]:   rewriting 0 < 1 with [rewrite:LT1_EQ0.1]|- x < 1 <=> x = 0
[45744]:   rewriting TAKE (3 - 1 - 1 - 1) [4; 5] with [rewrite:TAKE_cons.1]|- 0 < n ==> TAKE n (x::xs) = x::TAKE (n - 1) xs
[49628]:   rewriting 1 - 1 with [rewrite:SUB_EQUAL_0.1]|- c - c = 0
[52720]:   rewriting 0 < 0 with [rewrite:NOT_LESS_0.1]|- n < 0 <=> F
[55597]:   couldn't solve: 0 < 3 - 1 - 1 - 1
[57513]:   rewriting 1 - 1 with [rewrite:SUB_EQUAL_0.1]|- c - c = 0
[60813]:   rewriting TAKE 0 [4; 5] with [rewrite:TAKE_0.1]|- TAKE 0 l = []
val it =  [.] |- l = [1; 2; 3]: thm

I was thinking that TAKE n (x::xs) should only be rewritten when n is a literal numeral, otherwise the result with n - 1 explicitly occur on the new term would be hard to handle. I still think this is an issue, but if it's already there then don't change it as otherwise existing user code may break.

[mn200]

I like the look of the one that does LENGTH (TAKE ..) = MIN ... but @ordinarymath can figure out the breakages.

[binghe]

There's no more issues on CI images. The remaining broken theories (currently only listTheory) are due to additional automatic simplifications. But, let's say, if any proof beyond listTheory and rich_listTheory are still broken, especially those under examples/, then it means the changes here would break more unknown user code, and should not be merged (at least all new [simp] tags should be removed.)

[ordinarymath]

I'm planning such that the new breakages are fixed by a better simplification rule/ decision procedure for MAX and MIN. Or lattices in general #1434 .