Email Gateway (Aug 18 2022 at 12:12): Email Gateway (Aug 18 2022 at 12:12):From: John Matthews <matthews@galois.com>
Hi,
I would like to automatically prove the following lemma:
lemma
"[|\<not> 100 < nat (x); 0 \<le> x|]
==> nat x + 11 = nat ((x + 11) mod 4294967296)"
I thought this fell within the fragment that arith can handle, but it
can't seem to prove it. I know how to prove this manually, but is
there something else I can use to prove it in a single command?
Thanks,
-john
Email Gateway (Aug 18 2022 at 12:13):From: Tobias Nipkow <nipkow@in.tum.de>
It appears there is a bug. Which is not so easy do diagnose :-(
Tobias
John Matthews schrieb:
Email Gateway (Aug 18 2022 at 12:13):From: Amine Chaieb <chaieb@in.tum.de>
Hi John,
There is a problem converting this goal into a goal over int. The new
goal after conversion still contains nat and int, which which the core
presburger tactic can not cope. We need a more clever conversion, which
takes numerals into account, which occur in a statement containing both
nat and int with explicit conversions (nat and int).
This could be more involved than the actual approach, an I think we can
not come around a specialized procedure -- i.e. a conversion or a set of
simprocs + rules.
Amine.
PS: We could think about adding some intro rules to presburger if such
statements occur often. Candidates are mod_pos_pos_trivial and mod_less
and others, to prove that some modulo operations are basically the same
as the usual operations assuming that the input is within the size of
the modulus.
Tobias Nipkow wrote:
Email Gateway (Aug 18 2022 at 12:13):From: John Matthews <matthews@galois.com>
Ok, thanks for looking into this, Amine.
-john
Last updated: May 03 2024 at 04:19 UTC