Re: [isabelle] linarith_split_limit_exceeded (current value is 9)



I just wanted to add that just you see that message doesn't mean this is
actually the reason why your theorem wasn't proven. In my experience,
increasing that limit when you get that message very rarely leads to a
successful proof.

Manuel


On 29/05/2020 13:27, Lawrence Paulson wrote:
> Hi Angeliki, you have a number of options for modifying this limit:
> 
> At the top level of a theory file:
> 
> 	declare [[linarith_split_limit = 15]]
> 
> At the top level of a proof:
> 
> 	note [[linarith_split_limit = 15]]
> 
> Before an individual proof step:
> 
>  	using [[linarith_split_limit = 15]]
> 
> What I don’t know was how high you can take this limit before things fall apart.
> 
> Larry
> 
>> On 28 May 2020, at 12:15, Dr A. Koutsoukou-Argyraki <ak2110 at cam.ac.uk> wrote:
>>
>> Hello,
>>
>> In my formalisation I'm using various very simple algebraic calculations
>> as I do everything step by step
>> ( adding up factors, expanding/ getting rid of - outside parentheses, showing equality of algebraic expressions etc etc.. )that I
>> would expect would be solved by linarith or simp or auto.
>>
>> Very often, when I call Sledgehammer or try0 I keep getting
>> "Proof found"
>> and then repeatedly the message :
>> "
>> linarith_split_limit_exceeded (current value is 9)"
>>
>> I can see this issue has been discussed before but I'm not sure how I could get rid of this problem.
>> Is there some setting/ macro/plugin I could change perhaps?
>>
>> Many thanks in advance,
>> Angeliki
>>
> 
> 




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