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

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: Jul 15 2022 at 23:21 UTC