Re: [isabelle] Issue with smt and linear arithmetic



Thank you for the analysis, Sascha. Your suggestion for solving the problem would indeed be welcome. The core of the problem is that we don't have a completeness result about what our arithmetic simplification procedures do. They do what they do.

In this particular case the problem comes from the fact that although linear arithmetic dutifully multiplies the inequations by 2 to get rid of the /2, the effect is not what is intended: 2*(x+y)/2 is not simplified to x+y, instead the 2 is pulled inside. This is in contrast to 2*x/2, which is simplified to x. The problem here is that although there is a simproc that simplifies 2*(x+y)/2 to x+y, it cannot do its job because distributivity kicks in first. [In case you wonder if linear arithmetic needs distributivity, it does: you cannot even build HOL if you remove distributivity from the linear arithmetic setup.]

Tobias

On 14/08/2016 12:28, Sascha BÃhme wrote:
Hi Lukas,

linarith works as follows: Based on a decomposition of the original problem into a set of linear inequalities, it tries to find a refutation for them. The trace for the refutation is used to replay the steps, which should yield the Theorem False in the end. Proof replay essentially applies the simplifier with a carefully selected simpset. Whenever the final theorem differs from False, the warning you noticed is shown.

In your particular case, the obvious simplification for â(2x +2y) / 2â is not performed, because some rule or simproc is missing in linarithâs simpset. Extending the simpset appropriately would be a solution. Iâll see what I can do, such that your issue is resolved in the next release of Isabelle.

Cheers,
Sascha


Von: Lukas Bulwahn


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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