Re: [isabelle] z3 proof reconstruction failure


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)


Matthias Schmalz wrote:
> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.