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



Hi,

I sometimes run into this problem too, and I would wish I could disable
the splitter altogether, instead of increasing its limit.
Unfortunately, this seems not to be possible (?).

--
  Peter


On Fri, 2020-05-29 at 13:32 +0200, Manuel Eberl wrote:
> 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.