[isabelle] linarith error · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] linarith error

Email Gateway (Aug 22 2022 at 18:58):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi list,

while investigating why the proof reconstruction (smt) of some veriT proof failed, I found that the tactic linarith fails on the following example:

lemma ‹¬ (p_241 :: int) < 1 + (p_244 * p_244 + 2 * p_244) ⟹
p_241 < p_253 * p_253 ⟹
(1 + p_244) * (1 + p_244) = 1 + p_244 + p_244 * (1 + p_244) ⟹
(1 + p_244) * p_244 = p_244 + p_244 * p_244 ⟹
p_244 * (1 + p_244) = (1 + p_244) * p_244 ⟹
p_253 * p_253 = (1 + p_244) * (1 + p_244) ⟹ False
›
apply linarith

It fails with the following error message:
exception Fail raised (line 416 of "~~/src/Provers/Arith/fast_lin_arith.ML"): Linear arithmetic: failed to add thms
(the same exception is raised in the repository version).

I am aware that the goal can be solved by presburger but I would prefer to understand why it fails and whether I can do anything during proof reconstruction to avoid the problem. Does anyone know why linarith fails on this example?

Cheers,
Mathias

Email Gateway (Aug 22 2022 at 18:59):

From: Sascha Böhme <boehmes@in.tum.de>
Hi Mathias,

linarith is some intricate proof method. You can gain some insight by using the option [[linarith_trace]]. In your particular case, it seems that linarith’s internal application of the simplifier is too ambitious and simplifies an equation to True. A subsequent step that tries to conclude a+c=b+d from the equations a=b and c=d fails when given True as one of the two equations. One can certainly transform any True into, for instance, the equation 0=0, but I suspect that this might not be as as easy as it seems.

A simpler solution is to transform your problem by applying the law of distributivity:

I’m unsure if that helps in your particular case.

Regards,
Sascha

Email Gateway (Aug 22 2022 at 18:59):

From: Sascha Böhme <boehmes@in.tum.de>
Hi Dominique,

linarith is an intricate proof method. You can gain some insight by using the option [[linarith_trace]]. In your case, the simplifier that is applied internally in linarith is too ambitious and reduces an equation to True. Then, a subsequent step that tries to produce a+c=b+d from the two equations a=b and c=d fails when given True as one the equations. One can certainly transform every True into, for instance, the equation 0=0, but I suspect that this would not be as easy as it seems.

There is fortunately some way to circumvent these intricacies. You can preprocess the lemma by applying the law of distributivity. This results in a goal that is „more“ like a linear problem. Then linarith succeeds.

I’m unsure if that helps in your particular case.

Regards,
Sascha

Email Gateway (Aug 22 2022 at 19:00):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Sacha,

On 28. Jan 2019, at 21:58, Sascha Böhme <boehmes@in.tum.de> wrote:

Hi Dominique,

linarith is an intricate proof method. You can gain some insight by using the option [[linarith_trace]]. In your case, the simplifier that is applied internally in linarith is too ambitious and reduces an equation to True. Then, a subsequent step that tries to produce a+c=b+d from the two equations a=b and c=d fails when given True as one the equations.

Thanks for the analysis.

One can certainly transform every True into, for instance, the equation 0=0, but I suspect that this would not be as easy as it seems.

There is fortunately some way to circumvent these intricacies. You can preprocess the lemma by applying the law of distributivity. This results in a goal that is „more“ like a linear problem. Then linarith succeeds.

lemma ‹¬ (p_241 :: int) < 1 + (p_244 * p_244 + 2 * p_244) ⟹
p_241 < p_253 * p_253 ⟹
(1 + p_244) * (1 + p_244) = 1 + p_244 + p_244 * (1 + p_244) ⟹
(1 + p_244) * p_244 = p_244 + p_244 * p_244 ⟹
p_244 * (1 + p_244) = (1 + p_244) * p_244 ⟹
p_253 * p_253 = (1 + p_244) * (1 + p_244) ⟹ False
›
by (unfold int_distrib) linarith

I’m unsure if that helps in your particular case.

Well, I can preprocess the goal before calling Z3_Replay_Methods.arith_th_lemma (https://isabelle.in.tum.de/repos/isabelle/file/2755c387f1e6/src/HOL/Tools/SMT/z3_replay_methods.ML#l88 <https://isabelle.in.tum.de/repos/isabelle/file/2755c387f1e6/src/HOL/Tools/SMT/z3_replay_methods.ML#l88>).

Given that I was reconstructing veriT proofs, do you think that this kind of preprocessing also makes sense to replay arithmetic steps Z3 proof?

Thanks,
Mathias

Regards,
Sascha

Von: Mathias Fleury <mailto:mathias.fleury12@gmail.com>
Gesendet: Donnerstag, 24. Januar 2019 10:23
An: Isabelle User <mailto:isabelle-users@cl.cam.ac.uk>
Betreff: [isabelle] linarith error

Hi list,

while investigating why the proof reconstruction (smt) of some veriT proof failed, I found that the tactic linarith fails on the following example:

lemma ‹¬ (p_241 :: int) < 1 + (p_244 * p_244 + 2 * p_244) ⟹
p_241 < p_253 * p_253 ⟹
(1 + p_244) * (1 + p_244) = 1 + p_244 + p_244 * (1 + p_244) ⟹
(1 + p_244) * p_244 = p_244 + p_244 * p_244 ⟹
p_244 * (1 + p_244) = (1 + p_244) * p_244 ⟹
p_253 * p_253 = (1 + p_244) * (1 + p_244) ⟹ False
›
apply linarith

It fails with the following error message:
exception Fail raised (line 416 of "~~/src/Provers/Arith/fast_lin_arith.ML"): Linear arithmetic: failed to add thms
(the same exception is raised in the repository version).

I am aware that the goal can be solved by presburger but I would prefer to understand why it fails and whether I can do anything during proof reconstruction to avoid the problem. Does anyone know why linarith fails on this example?

Cheers,
Mathias

Email Gateway (Aug 22 2022 at 19:00):

From: Sascha Böhme <boehmes@in.tum.de>
Hi Mathias,

Your suggestion might be beneficial, but I'm not aware of any concrete Z3 example in which this preprocessing would help. Just go ahead and try if nothing breaks. I’ve seen that some definition unfolding is already applied in the Z3 replay code. Maybe you can just add the distributivity rules there?

Regards,
Sascha

Von: Mathias Fleury
Gesendet: Montag, 28. Januar 2019 22:17
An: Sascha Böhme
Cc: Isabelle User
Betreff: Re: [isabelle] linarith error

Hi Sacha,

On 28. Jan 2019, at 21:58, Sascha Böhme <boehmes@in.tum.de> wrote:

Hi Dominique,

linarith is an intricate proof method. You can gain some insight by using the option [[linarith_trace]]. In your case, the simplifier that is applied internally in linarith is too ambitious and reduces an equation to True. Then, a subsequent step that tries to produce a+c=b+d from the two equations a=b and c=d fails when given True as one the equations.

Thanks for the analysis.

One can certainly transform every True into, for instance, the equation 0=0, but I suspect that this would not be as easy as it seems.

There is fortunately some way to circumvent these intricacies. You can preprocess the lemma by applying the law of distributivity. This results in a goal that is „more“ like a linear problem. Then linarith succeeds.

lemma ‹¬ (p_241 :: int) < 1 + (p_244 * p_244 + 2 * p_244) ⟹
p_241 < p_253 * p_253 ⟹
(1 + p_244) * (1 + p_244) = 1 + p_244 + p_244 * (1 + p_244) ⟹
(1 + p_244) * p_244 = p_244 + p_244 * p_244 ⟹
p_244 * (1 + p_244) = (1 + p_244) * p_244 ⟹
p_253 * p_253 = (1 + p_244) * (1 + p_244) ⟹ False
›
by (unfold int_distrib) linarith

I’m unsure if that helps in your particular case.

Given that I was reconstructing veriT proofs, do you think that this kind of preprocessing also makes sense to replay arithmetic steps Z3 proof?

Thanks,
Mathias

Regards,
Sascha

Von: Mathias Fleury <mailto:mathias.fleury12@gmail.com>
Gesendet: Donnerstag, 24. Januar 2019 10:23
An: Isabelle User <mailto:isabelle-users@cl.cam.ac.uk>
Betreff: [isabelle] linarith error

Hi list,

while investigating why the proof reconstruction (smt) of some veriT proof failed, I found that the tactic linarith fails on the following example:

lemma ‹¬ (p_241 :: int) < 1 + (p_244 * p_244 + 2 * p_244) ⟹
p_241 < p_253 * p_253 ⟹
(1 + p_244) * (1 + p_244) = 1 + p_244 + p_244 * (1 + p_244) ⟹
(1 + p_244) * p_244 = p_244 + p_244 * p_244 ⟹
p_244 * (1 + p_244) = (1 + p_244) * p_244 ⟹
p_253 * p_253 = (1 + p_244) * (1 + p_244) ⟹ False
›
apply linarith

It fails with the following error message:
exception Fail raised (line 416 of "~~/src/Provers/Arith/fast_lin_arith.ML"): Linear arithmetic: failed to add thms
(the same exception is raised in the repository version).

I am aware that the goal can be solved by presburger but I would prefer to understand why it fails and whether I can do anything during proof reconstruction to avoid the problem. Does anyone know why linarith fails on this example?

Cheers,
Mathias

Last updated: Nov 21 2024 at 12:39 UTC