Email Gateway (Aug 22 2022 at 09:03): Email Gateway (Aug 22 2022 at 09:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts for linear arithmetic in Isabelle,
I wondered why the simplifier can prove statements such as the following for nat, int,
rat, and real, but fails for enat.
lemma "3 < x ==> 2 < x"
I found that the linarith solver does it for nat, int, rat, and real. Unfortunately, there
seems to be no setup for enat (or ereal). I therefore briefly tried to configure linarith
for enat by mimicking what has been done for nat. Since I do not know the workings of the
linarith prover and could not find any documentation on it, my attempt failed. I only got
warnings such as "Linear arithmetic should have refuted the assumptions. Please inform
Tobias Nipkow." or errors like "Linear arithmetic: failed to add thms".
Is it in principle possible to configure linarith for enat? Is there any documentation
what rewrite rules, cancellation simprocs and the like it needs?
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 09:04):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Andreas,
Unfortunately the linear arithmetic decision procedure does not work for
extended numbers, we had investigated that as well. The decision procedure works
for all types in a class that requires certain cancellation laws, probably x+y
<= x+z ==> y <= z. This fails in the presence of infinities.
This is a sore problem and the only way around it seems to be to eliminate the
infinities first, i.e. reduce it to the basic type. But that has to be done by
plain old deduction as it would be very tricky to integrate such a step into the
existing decision procedure.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:04):From: Larry Paulson <lp15@cam.ac.uk>
Perhaps the nonstandard integers are the solution here. Nonstandard theories satisfy all the first-order properties of the corresponding standard theories. I’m not sure what state they are in, however. Was linear arithmetic ever set up for them?
Larry
Email Gateway (Aug 22 2022 at 09:05):From: Tobias Nipkow <nipkow@in.tum.de>
I strongly suspect linear arithmetic was never set up for any nonstandard type.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:06):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Larry and Tobias,
The idea with non-standard integers sound interesting, so I investigated a bit further.
Linear arithmetic works for all types in linordered_dom thanks to the generic setup in
Int.thy. Since the hyperreals are an instance thereof, linarith works for them.
Unfortunately, the hypernaturals are not, so linarith does not work for them. However, I
think that one could make it work. I tried to adapt the setup for ordinary naturals to
hypernaturals. It did not work out of the box because hypnat is not a type constructor,
but a synonym for "nat star" and the Lin_Arith.add_discrete_type only accepts type
constructors. Therefore, I copied the hypnat type to a type constructor hypernat with
typedef and did the adaptation there. I now have a setup that works for my tiny examples
on hypernat such as "3 < x ==> 2 < (x :: hypernat)". But as I am no expert for linarith, I
don't know whether it is complete.
The next question is how this could be used to implement a solver or simproc on enat. I
defined a function hnat_of_neat :: enat => hypernat that respects orders and commutes with
numerals. Thus, one can transform the goal "3 < x ==> 2 < (x :: enat)" to "3 <
hnat_of_enat x ⟹ 2 < hnat_of_enat x". Unfortunately, linarith fails to prove this goal,
although it succeeds on the more general "3 < y ==> 2 < y", and I do not know why.
Do you think that this is a viable way to go?
Do I really need a copy hypernat of nat star just for the sake of having a type
constructor?
Does linarith provide some support for going from enat to hypernat? I noticed that there
is the function Lin_Arith.add_inj_const, but I do not know what this is good for.
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:06):From: Larry Paulson <lp15@cam.ac.uk>
Personally I would prefer an approach that used the hyper-naturals instead of type enat. They have better algebraic properties, though you don’t get a unique infinite number.
Larry Paulson
Email Gateway (Aug 22 2022 at 09:06):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Switching to the hyper-naturals is not really an option for me because my work builds on
other parts that use enat, too. Unfortunately, the idea I have sketched does not scale to
larger examples, because the conversions between enat and hypernat do not distribute over
subtraction. One would have to implement case splits in the translation, which looks like
a bigger project and requires more thought first.
Thanks for your input,
Andreas
Last updated: Apr 24 2024 at 20:16 UTC