Email Gateway (Aug 19 2022 at 11:27): Email Gateway (Aug 19 2022 at 11:27):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I'm getting annoyed by the tediousness required to discharge seemingly
trivial problems on words and thought I would try the "smt" method on them.
(BTW: Is proof reconstruction available for Bitvectors?)
I found a strange behaviour (in 2012, 2013 and ffc3f1659a25): Consider
the two goals stated below. They are equivalent, the only difference is
between free and bound variables. Yet "smt" can only solve the second
goal and suggests a possibly spurious counter-example for the first one.
theory Scratch imports "~~/src/HOL/Word/Word" begin
lemma "⋀degree k. (degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
using [[smt_oracle=true]]
apply smt (* Fails, talks about possibly spurious counter-example *)
oops
lemma "(degree :: 32 word) ≤ 3 ⟹ k ≤ degree ⟹ k + 1 ≠ 0"
using [[smt_oracle=true]]
apply smt (* Succeeds *)
done
Is this some known limitation or a bug in the preprocessing?
Best regards,
Lars
Email Gateway (Aug 19 2022 at 11:28):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Hey Lars.
I'm not sure if proof reconstruction is now available for bitvectors.
Sascha and I looked at the problem a few years ago, and the conclusion
was it was doable but the performance was a tad disappointing.
The tactic we implemented to help discharge the theory-lemmas appearing
in bitvector proofs is available, and should be in your context under
the name word_bitwise. It does the bitwise expansion of your problem and
some minor simplification. Together with real simplification it solves
both of these problems, although a bit slowly.
Thomas.
Email Gateway (Aug 19 2022 at 11:28):From: Thomas Sewell <thomas.sewell@nicta.com.au>
To clarify, you need to import the src/HOL/Word/WordBitwise which should probably be included by default.
Thomas.
Thomas Sewell <Thomas.Sewell@nicta.com.au> wrote:
Last updated: Apr 19 2024 at 12:27 UTC