Email Gateway (Aug 18 2022 at 17:54): Email Gateway (Aug 18 2022 at 17:54):From: Sascha Boehme <boehmes@in.tum.de>
Hi Matthias,
It seems that declaring rules as "z3_rule" hasn't been a feature
extensively tested so far. It worked only overly restricted. The
next Isabelle release will be fixed in that respect.
Cheers,
Sascha
Matthias Schmalz wrote:
Email Gateway (Aug 18 2022 at 18:09):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
Hello,
when trying to proof the following (with z3):
lemma "x * y ≤ (0 :: int) ⟹ x ≤ 0 ∨ y ≤ 0"
by smt
I get a proof reconstruction failure:
Z3 found a proof, but proof reconstruction failed at the following subgoal:
assumptions:
x * y ≤ 0
¬ y ≤ 0
¬ x ≤ 0
proposition: False
Adding a rule to the lemma group "z3_rule" might solve this problem.
I tried to add an appropriate lemma to the group z3_rule, but without
success. Does anyone have an idea of how to make proof reconstruction
succeed in this case?
-Matthias
Email Gateway (Aug 18 2022 at 18:09):From: Sascha Boehme <boehmes@in.tum.de>
Hello,
This is the incompleteness of proof reconstruction for Z3 in Isabelle.
Although Z3 can find proofs for some nonlinear arithmetic problems, we
currently do not support proof reconstruction for such proofs and
consequently fail on them.
The error message indicates some means to "complete" proof
reconstruction in certain cases by proving intermediate steps in
advance. I wonder, however, which rule you proved here, since the Z3
proof reconstruction step that failed looks nearly identical to your
original goal.
If you're willing to accept alternatives, here is one. You can prove
the lemma by Metis:
lemma "x * y ≤ (0 :: int) ⟹ x ≤ 0 ∨ y ≤ 0"
by (metis mult_le_0_iff)
Cheers,
Sascha
Matthias Schmalz wrote:
Email Gateway (Aug 18 2022 at 18:09):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
Hi Sascha,
thanks for explaining.
This is a minimal example for illustrating the problem, and I do not
really want to prove it with Z3. Yet, this kind of reconstruction
failure arises with more complicated examples, where Z3 would be useful.
So is there an easy way (e.g., by declaring a z3_rule) of making proof
reconstruction succeed in my example?
-Matthias
Last updated: Nov 21 2024 at 12:39 UTC