Useful HOL functions not in the Lem library

Issue #50 new
Scott Owens
created an issue

In CakeML, I use the following functions which are in HOL, but not in the Lem library (according to grep). Some of these might be of sufficiently general interest to include:

Num (converts integer to natural)

num_to_dec_string (converts number to string in base 10)

neg (negates an integer)

ALL_DISTINCT (true iff a list contains no duplicates)

RTC (reflexive transitive closure)

COUNT_LIST (given a natural n, returns a list [1..n])

ZIP (zips a list. Lem has List.zip curried which maps to its own list_combine in HOL. HOL's ZIP is tupled, and annoying as that is, I want to map Lem List.zip to HOL ZIP)

Comments (4)

  1. Thomas Tuerk

    I originally had mappings for ZIP in the library. The problem is, that it is an underspecified function in HOL. if the two lists don't have the same length, the semantics is undefined. The same problem exists for OCaml. So, we can't reliably map to the same semantics in all backends for this underspecified function. We can inlcude an unsafe function mapping to "ZIP" in list_extra, though.

  2. Thomas Tuerk

    I added "zip_same_length" now. For the other functions:

    neg is called "~" (ascii: "numNegate") and is overloaded for several number types

    RTC is called "reflexiveTransitiveClosure", the mapping to RTC is not done however, because RTC is defined on the predicate representation of relations, not the set one. As discussed in the meeting last week, we map only to sets for the time beeing. A mapping where we can decide, which HOL library and which representation of maps to target, will follow.

    The others we can consider adding in the future. However, for the time beeing I personally prefer to keep the library clean and small. One can easily define these additional functions in some private / project dependend library though and add - if often used - later.

  3. Log in to comment