Email Gateway (Apr 22 2025 at 17:37): Email Gateway (Apr 22 2025 at 17:37):From: Florian Haftmann <florian.haftmann@cit.tum.de>
As far I can see, the best solution is to disregard
word_eq_numeral_iff_iszero [simp] and calculate equality on word values
in the same manner as <= and < is calculated by default in HOL-
Library.Word.
I started to re-arrange this but stumbled over an elementary issue: IMHO
non-trivial computations on word numerals should only be carried out if
the length is fixed – otherwise there will be artifacts of the
conversion to int in the resulting term. Practically, this could be
achieved using a precondition ‹LENGTH('a) = numeral n› on the
corresponding rewrites. @list Any opinions?
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Apr 22 2025 at 23:18):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
On 23 Apr 2025, at 03:37, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:
As far I can see, the best solution is to disregard word_eq_numeral_iff_iszero [simp] and calculate equality on word values in the same manner as <= and < is calculated by default in HOL- Library.Word.
I started to re-arrange this but stumbled over an elementary issue: IMHO non-trivial computations on word numerals should only be carried out if the length is fixed – otherwise there will be artifacts of the conversion to int in the resulting term. Practically, this could be achieved using a precondition ‹LENGTH('a) = numeral n› on the corresponding rewrites. @list Any opinions?
I agree that restricting non-trivial numeric computation to instances makes sense (depending on what non-trivial turns out to be), but I’m not a fan of conditional rewrites like that. They will always apply and be rejected often. Even if it might not obviously impact performance immediately, it is an ingredient for performance problems later on and at the least it will make all simp traces involving words very annoying to read.
If we’re in a simproc, could we match more explicitly on the type in the term?
A bit less general: it might be enough to instantiate the corresponding rules to numeral type arguments. That would mean arithmetic only works on numeral word lengths, not other types people have built. We could alleviate that by providing a lemma set where the length type has a known consistent name so that it is easy to produce those instances with [where .. ] for people who are using non-numeral types for lengths (we do a few times for abstraction, but rarely).
Cheers,
Gerwin
Last updated: May 30 2025 at 04:27 UTC