Email Gateway (Oct 13 2020 at 18:34): Email Gateway (Oct 13 2020 at 18:34):From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,
I was trying to infer the following:
theory Scratch
imports Complex_Main
begin
notepad begin
fix a n :: nat
assume "a dvd n" "a < n powr (1/3)" "1 < n"
then have "a < n" by (smt divide_le_eq_1_pos of_nat_1_eq_iff of_nat_less_iff powr_less_cancel powr_one_gt_zero_iff)
end
This smt call has been suggested by Sledgehammer, but with the words
"proof reconstruction failed". Here is the exact error it generates:
exception THM 1 raised (line 2237 of "thm.ML"):
RSN: no unifiers
1 < n
¬ real n + - 1 * real 1 ≤ 0 ⟹ 1 < n
Is this a bug? It certainly seems like one...
Regards,
Jakub Kądziołka
Email Gateway (Oct 31 2020 at 08:50):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Jakub,
I had a look at that and it is a bug in the proof produced by Z3.
One proof step (modus ponens) is:
1 < n real n + - 1 * real 1 ≤ 0 <--> 1 < n
================================================ mp
real n + - 1 * real 1 ≤ 0
The problem is that the rule mp is specified to have the form:
P P<-->Q
============== mp
Q
However, in this proof step produced by Z3, the terms P and Q of the
equivalence are swapped. So, this is an issue in the proof.
The bad news is: it makes no sense to report the issue, because our Z3
version is too old -- and the proof format has changed compared to the
version that is currently used, so it is not only about updating the
binary shipped with Isabelle.
The second bad news: using veriT (the new alternative backend for smt)
works but it takes 7s, so no chance here either...
Thanks for reporting,
Mathias
Last updated: Jan 04 2025 at 20:18 UTC