[isabelle-dev] SMT in Isabelle2013 (was: Re: AFP: Session AVL-Trees broken)

[Jasmin Blanchette]

Hi Makarius,

Am 03.01.2013 um 15:26 schrieb Makarius:

> If Sasche still wants to make some more refinements, e.g. to address
> 
>  Z3 proof parser (line 34): unknown function symbol: "S2!val!0"
>  http://isabelle.in.tum.de/repos/isabelle/annotate/b1f4291eb916/src/HOL/SMT_Examples/SMT_Tests.thy#l122
> 
> there are still approx. 2 weeks left to do it.

Sascha just wrote to me: "If I'm not mistaken, this is a problem that surfaced about 1.5 years ago for the first time. The Z3 developers made a change to the proof format that is not very easy to fix for us. It would require type inference after parsing the (proof) terms. Essentially, a big part of Z3 proof reconstruction need to be touched, revised and mostly rewritten."

It might be that the bug [*] is more likely to arise with Z3 3.2 than with 3.1 or whichever version was used to generate the certificate before. In any case, Isabelle2012 has included Z3 3.2, so users have been exposed to this issue for almost a year now.

Hence, Sascha and I will look at the issue, and at any Z3 4.x-specific issues, after the release.

On the other hand, he has a change to the monomorphizer in the pipeline since October and might be able to introduce some enhancements in the coming days (to make it more complete -- i.e. generate monomorphic instances that previously were strangely forgotten). We'll proceed by steps there, first upgrading the "smt" method, then Sledgehammer. The change should be fairly straightforward; should there be any issues, we can postpone it to after the release. I've included the email that triggered this line of work at the bottom of this email, for the record.

Jasmin

[*] Actually, "bug" is a big word. The "smt" method's reconstruction is heuristic in parts and known to be incomplete. (Indeed, even "metis" is incomplete with respect to Joe Hurd's Metis, even though the prover has only six simple well-documented proof rules.) Incompleteness can strike any time.


Anfang der weitergeleiteten E-Mail:

> Von: Jasmin Blanchette <jasmin.blanchette at gmail.com>
> Datum: 29. Oktober 2012 13:11:49 MEZ
> An: Sascha Boehme <boehmes at in.tum.de>
> Betreff: Help with monomorphization
> 
> Hi Sascha,
> 
> I found some cases where the monomorphization algorithm seems to be behaving rather suboptimally.
> 
> 
> FIRST EXAMPLE
> 
> Here's the first example; all you need is "Main":
> 
>   consts P :: "'a => bool"
>   consts Q :: "'a => bool"
> 
>   lemma foo: "P (0::'a::zero) | Q (0::'b::zero)"
>   sorry
> 
>   lemma "P (0::'c::zero) | Q (0::'d::zero)"
>   using [[monomorph_keep_partial_instances = false]]
>   using [[smt_trace]]
>   apply (smt foo)
> 
> This will fail. (It will also fail if "monomorph_keep_partial_instances" is set to true, but the output is less clear then.) Here's the beginning of the SMT trace:
> 
>   SMT: Assertions:
>     P (0∷'d) ∨ Q (0∷'c)  [!]
>     P (0∷'d) ∨ Q (0∷'d)  [!]
>     P (0∷'c) ∨ Q (0∷'c)  [!]
>     ¬ (P (0∷'c) ∨ Q (0∷'d))
> 
> Strangely enough, all combinations of 'c's and 'd's are tried, except the right one!
> 
> 
> SECOND EXAMPLE
> 
>   consts P :: "'a => bool"
> 
>   lemma foo: "P (0::'a::zero) | P (0::'b::zero)"
>   sorry
> 
>   lemma "P (0::'c::zero) | P (0::'d::zero)"
>   using [[monomorph_keep_partial_instances = false]]
>   using [[smt_trace]]
>   apply (smt foo)
> 
> This example fails even more brutally than the previous one:
> 
>   SMT: Assertions:
>     ¬ (P (0∷'c) ∨ P (0∷'d))
> 
> 
> THIRD EXAMPLE
> 
>   lemma "map f (map g xs) = map (%x. f (g x)) xs"
>   using [[monomorph_keep_partial_instances = false]]
>   using [[smt_trace]]
>   apply (smt map_map o_def)
> 
> This will fail (also with partial instances). Here, it's easy to see that the provided facts are enough ("using map_map unfolding o_def ."); but the monomorphizer is really failing to do its job:
> 
>   SMT: Assertions:
>     map f (map g xs) ≠ map (λx. f (g x)) xs
> 
> 
> I don't understand the code well enough to fix it. Although the first and second example are constructed, the third one is real -- I ran into this issue myself -- and I've met similar problems with other composition theorems. I hope you can help me here...
> 
> Cheers,
> 
> Jasmin
>