The Coq mailing list

[Basile Clement <basile AT clement.pm>]

Hello Frédéric,

`itauto` is the "obvious" solution I didn't dare hoping for :)

Thanks,
- Basile

On Tue, 2021-04-20 at 21:36 +0200, Frédéric Besson wrote:
> Hello Basile,
> 
> lia does:
> 1) naive conjunctive normal form + a tiny bit of arithmetic
> 2) genuine arithmetic reasoning
> 
> Given the shape of the goal, 1) is probably exploding.
> After subst, the goal seems to simplify a lot.
> The tiny bit of arithmetic is then probably sufficient to make the
> CNF
> shrink ... exponentially - you're lucky!
> 
> So, this is unfortunate but not completely unexpected.
>  
> This gives me the opportunity to  unashamedly  advertise a better way
> to proceed. I have recently implemented a tactic `itauto tac`[*]
> which 
> uses a SAT solver and runs `tac` on the leaves of a propositional
> proof
> search. For your goal, `itauto lia` succeeds instantly.
> 
> Best,
> --
> Frédéric
> 
> [*] https://gitlab.inria.fr/fbesson/itauto
> 
> 
> On Tue, 2021-04-20 at 18:36 +0200, Basile Clement wrote:
> > Dear Coq-Club,
> > 
> > It seems like `lia` fails on some goals containing equalities, but
> > succeeds after a simple application of the `subst` tactic.  See
> > attached .v file for such an example.
> > 
> > I was surprised by this, because I assumed that exploiting
> > substitutions (i.e. equalities where one side is a variable) would
> > be
> > generally beneficial due to reducing the number of variables to
> > handle.
> > 
> > Is this expected from the `lia` tactic?
> > 
> > Regards,
> > - Basile
> 
>