Add more theorems and constants

[xrchz]

At a high level, this PR includes:

• bool_to_bit
• theorems about chunks including a tail-recursive version
• theorems about dropWhile
• theorems about word_to_bin_list/word_from_bin_list -- operating on words as a list of bits
• some theorems about BITWISE etc. mostly in service of the above

These theorems were produced as part of an upcoming improvement to cv evaluation of Keccak_256

[binghe]

Hi,

You should first fix CI tests of other builds and handle OT builds at last. From the latest CI test results I think your removal of previous assumption 32 is not right:

32 |- !f g M N. M = N /\ (!x. x = N ==> f x = g x) ==> LET f M = LET g N

Besides, even the goal doesn't show up as part of the generated goals, in principle we should NOT delete any proof from prove_base_assumsScript.sml. Instead, we should still keep this proof under a different name (LET_CONG in this case), at the end of this file, just like other existing proofs without a th* name.

My understanding is that, these extra proofs are those needed by core theories beyond boss. Missing any of these proofs will cause leaking assumptions later, e.g. when hol-real is built and installed.

[xrchz]

You should first fix CI tests of other builds and handle OT builds at last. From the latest CI test results I think your removal of previous assumption 32 is not right:

I've reverted that change. How would you recommend to proceed now?

[xrchz]

Maybe we're done? all the CI checks pass

[mn200]

Looks good. Please think about suggestions.

[binghe]

You should first fix CI tests of other builds and handle OT builds at last. From the latest CI test results I think your removal of previous assumption 32 is not right:

I've reverted that change. How would you recommend to proceed now?

The fix is good. But it seems that the newly added th61 is nothing but the existing BOOL_EQ_DISTINCT appeared later:

(* |- (T <=/=> F) /\ (F <=/=> T) *)
val BOOL_EQ_DISTINCT = store_thm("BOOL_EQ_DISTINCT", concl boolTheory.BOOL_EQ_DISTINCT,
  PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]);

I suggest removing the above redundant theorem (maybe you can consider using its shorter proof for th61) and put val BOOL_EQ_DISTINCT = th61; after th61 for backward compatibility. Both actions are optional, because redundant theorems create at most warnings when installing OT articles, and the name BOOL_EQ_DISTINCT is actually not used later in this same file.

P. S. previous this bridging theorem didn't show up in the generated goals because it's not used in any proof of core theories before boss, but it will be used later. Now because your new theorems directly use it, so it's moved into the generated goals. I don't have a good solution to prevent future OT builds broken for this kind of issues.

[xrchz]

I suggest removing the above redundant theorem (maybe you can consider using its shorter proof for th61) and put val BOOL_EQ_DISTINCT = th61; after th61 for backward compatibility.

Thanks for the feedback! I followed this suggestion.