Email Gateway (May 09 2022 at 15:40): Email Gateway (May 09 2022 at 15:40):From: Lawrence Paulson <lp15@cam.ac.uk>
We have an entry by Jonas Bayer, Marco David, Abhik Pal and Benedikt Stock on the theory of representing natural numbers as digits:
We formalize how a natural number can be expanded into its digits in some base and prove properties about functions that operate on digit expansions. This includes the formalization of concepts such as digit shifts and carries. For a base that is a power of 2 we formalize the binary AND, binary orthogonality and binary masking of two natural numbers.
What’s really interesting is the last line of the abstract:
This library on digit expansions builds the basis for the formalization of the DPRM theorem.
In other words, it’s the first instalment of the huge development promised here: https://drops.dagstuhl.de/opus/volltexte/2019/11088/pdf/LIPIcs-ITP-2019-33.pdf
Looking forward to the rest! It is now online at https://www.isa-afp.org/entries/Digit_Expansions.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC