[isabelle-dev] smt in the repository

[Manuel Eberl]

In my experience, many of the supplied facts are usually trivialities
that only obscure what is really going on.

To illustrate my point, consider the following random example I just
picked from the AFP:

  hence "4 - 4 * A / (A - D) = -4 * D / (A - D)"
    using ‹A ≠ D›
    by (smt ab_semigroup_mult_class.mult_ac(1) diff_divide_eq_iff
eq_iff_diff_eq_0 mult_minus1 mult_minus1_right mult_numeral_1_right
right_diff_distrib_numeral times_divide_eq_right)

None of these facts are very interesting. My personal idea of a readable
Isabelle proof is that it should, as far as possible, not refer to
trivial facts like "-1 * z = -z". We have automation to take care of that.

Indeed, that whole smt proof can be replaced with "by (simp add:
field_simps)"

Of course, I recognise that there are cases where smt is much more
useful than here. It's just my impression that the
sledgehammer-generated smt proofs usually contain too much "noise" like
this for my taste. Not that sledgehammer is to blame here; this is a
problem inherent in how smt works.


There are rare cases where I was not easily able to replace a metis/smt
proof with an equally short "normal" proof. In these, I was really at a
loss about how Z3 proved the fact (so in that sense, the proof was
unreadable). I was always able to find an Isar proof eventually, though.
I for one think that's better, but I wouldn't impose this view on
anybody else.

Manuel


On 26/05/2020 18:08, Lawrence Paulson wrote:
> For a solver that is designed to cope with thousands of clauses, I would be surprised if it suffered such a regression that it could fail for the trivial problems we present to it. I’m not aware of an occasion when any of the 2400+ occurrences have ever failed.
> 
> I would also question the claim that they are unusually unreadable. The attached list of theorems tends to omit a lot of routine reasoning and therefore lists the critical three or four facts required for the proof.
> 
> Larry
> 
>> On 26 May 2020, at 16:58, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>
>> Z3 ist not under our control. If it changes, those proofs may no longer work. Hence I am very sceptical of having them in the distribution.
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>