Email Gateway (Aug 22 2022 at 19:02): Email Gateway (Aug 22 2022 at 19:02):From: Mathias Fleury <mathias.fleury12@gmail.com>
Dear Tobias,
On 4. Feb 2019, at 10:45, Tobias Nipkow <nipkow@in.tum.de> wrote:
Dear Mathias,
It took me some time to remember the key point: linarith uses Fourier-Motzkin elimnation which is complere for rationals and reals but incomplete for integers. For the latter we have Presburger, but it is too slow for the example.
The idea of eliminating common factors first is interesting. I have no idea if this is always beneficial.
I asked our local expert of linear arithmetics, Martin Bromberger:
tl;dr: Eliminating common factors helps much more than it hurts, especially for linear integer arithmetic; but there are cases, although rare, where it might be harmful.
Detailed explanation:
Fourier-Motzkin transformation over the reals/rationals: is just a projection. And the projection does not change if we eliminate common factors because this elimination is equivalence preserving. (There is one exception... Your projection may change because your Fourier-Motzkin implementation might change the variable elimination order. Yay heuristics...) What changes, however, is the run time needed to compute the projection. Whether you are faster or worse depends on the overhead of eliminating common factors vs. the speed-up you gain by having smaller coefficients. Personally, I think you would gain a speed-up.
Fourier-Motzkin transformation over the integers: eliminating common factors alone should not change whether a problem is solvable or unsolvable. Because the projection stays the same :-) Unless, (i) you combine it with rounding ("2 * x:int + 4 * y:int <= 1" simplifies to "x:int + 2 * y:int <= 0 = \floor(1/2)") or (ii) if you simplify strict inequalities over integer variables ("a:int < 1" simplifies to "a:int <= 0", but "2 * a:int < 2" simplifies to "2 * a:int <= 1"). I assume (ii) is what happened in your example (because (i) is a form of eliminating common factors) and thanks to eliminating common factors you removed some rational/real solutions and made the problem solvable. And because this is possible (i) and (ii) are also normally done for arithmetic inequalities. (Still, you might very rarely get worse results because your Fourier-Motzkin implementation changes the variable elimination order due to heuristic shenanigans…)
PS: Eliminating common factors and (i) and (ii) are not just preprocessing steps but inprocessing steps. You should apply them after every intermediate step of Fourier-Motzkin transformation…
Since the existing code is quite delicate, I also don't want to mess with it.
I was more thinking of a preprocessing step, than a change to linarith itself. Which I expect to be a much bigger task.
Is there a simproc for eliminating common factors? I suspect not in full generality, because the simplifier leaves "10 * (i::int) ≤ 25 * j" alone. There is one by Larry for the simple case "m * t <= n * u" where m and n have a common factor. I have no idea how much work it would be to generalize it.
Thanks for the pointer.
Best regards,
Mathias
Best regards
TobiasOn 01/02/2019 18:38, Mathias Fleury wrote:
Hi list,
after trying to reconstruct more veriT proofs, I found out the following lemma cannot be discharged by linarith:
lemma "¬ 0 ≤ int (size l') ∨
¬ 10 * int (size lr) < 4 + 14 * int (size rr) ∨
10 * int (size lr) ≤ 15 + 25 * int (size l') ∨
¬ 10 * int (size lr) + 10 * int (size rr) ≤ 30 + 25 * int (size l') "
apply linarith (* fails *)
oops
However, if I simplify the coefficients by dividing by 5, then linearity is able to prove the goal:
lemma "¬ 0 ≤ int (size l') ∨
¬ 5 * int (size lr) < 2 + 7 * int (size rr) ∨
2 * int (size lr) ≤ 3 + 5 * int (size l') ∨
¬ 2 * int (size lr) + 2 * int (size rr) ≤ 6 + 5 * int (size l') "
apply linarith
done
Is there any simproc able to do this simplification automatically? If there is one, is there any reason why linarith does not use it by default?
Thanks,
Mathias
Email Gateway (Aug 22 2022 at 19:03):From: Tobias Nipkow <nipkow@in.tum.de>
Mathias,
Actually, a simproc to cancel all common factors is easy: Givem t1 <= t2, where
t1 and t2 are sums, compute the common factor m of t1 and t2 and the remainders
t1' and t2'. Prove by rewriting with distributivity that (t1 <= t2) = (m*t1' <=
mt2'). Prove by simproc that (mt1' <= m*t2') = (t1' <= t2') - see
Tools/numeral_simprocs.ML.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 19:05):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
On 4. Feb 2019, at 17:20, Tobias Nipkow <nipkow@in.tum.de> wrote:
Mathias,
Actually, a simproc to cancel all common factors is easy: Givem t1 <= t2, where t1 and t2 are sums, compute the common factor m of t1 and t2 and the remainders t1' and t2'. Prove by rewriting with distributivity that (t1 <= t2) = (mt1' <= mt2'). Prove by simproc that (mt1' <= mt2') = (t1' <= t2') - see Tools/numeral_simprocs.ML.
I implemented that. I followed what was already in Tools/numeral_simprocs.ML. Then I activated the
procedure as simproc on nat and 'a :: linordered_ring_strict (which includes int and reals) and run it on the (non-slow part of) AFP.
When trying it out on the AFP, some proofs broke because of the reordering meaning. So if we want to activate such simproc, we would have to adapt some proofs:
by (clarsimp simp add: cos_one_2pi) (metis mult_minus_right of_int_of_nat)
~>
by (clarsimp simp add: cos_one_2pi) (metis mult_minus_left of_int_of_nat)
Nevertheless, it turns out things are a bit more complicated than I expected. They are already two different simprocs that can cancel terms, but do different things:
* eq_cancel_numeral_factor: it cancels term, but on the way, it reorders terms.
(2::int) * a * b = 2 * b' * a' ~> a * b = a' * b'
* eq_cancel_factor: it cancels a terms, but without reordering terms:
(2::int) * a * b = 2 * b' * a' ~> 2 = 0 ∨ a * b = b' * a'
[2 = 0 can be simplified to false later, yielding a * b = b' * a']
I have a few questions:
* Does anyone know why some cancelation simprocs sort terms?
* Are simprocs supposed to be confluent, i.e., reach the same conclusion independently of the order they are applied?
Best,
Mathias
Tobias
On 04/02/2019 15:29, Mathias Fleury wrote:
Dear Tobias,
On 4. Feb 2019, at 10:45, Tobias Nipkow <nipkow@in.tum.de <mailto:nipkow@in.tum.de>> wrote:
Dear Mathias,
It took me some time to remember the key point: linarith uses Fourier-Motzkin elimnation which is complere for rationals and reals but incomplete for integers. For the latter we have Presburger, but it is too slow for the example.
The idea of eliminating common factors first is interesting. I have no idea if this is always beneficial.
I asked our local expert of linear arithmetics, Martin Bromberger:
tl;dr: Eliminating common factors helps much more than it hurts,
especially for linear integer arithmetic; but there are cases, although
rare, where it might be harmful.Detailed explanation:
Fourier-Motzkin transformation over the reals/rationals: is just a
projection. And the projection does not change if we eliminate common
factors because this elimination is equivalence preserving. (There is one
exception... Your projection may change because your Fourier-Motzkin
implementation might change the variable elimination order. Yay
heuristics...) What changes, however, is the run time needed to compute
the projection. Whether you are faster or worse depends on the overhead of
eliminating common factors vs. the speed-up you gain by having smaller
coefficients. Personally, I think you would gain a speed-up.Fourier-Motzkin transformation over the integers: eliminating common
factors alone should not change whether a problem is solvable or
unsolvable. Because the projection stays the same :-) Unless, (i) you
combine it with rounding ("2 * x:int + 4 * y:int <= 1" simplifies to
"x:int + 2 * y:int <= 0 = \floor(1/2)") or (ii) if you simplify strict
inequalities over integer variables ("a:int < 1" simplifies to "a:int <=
0", but "2 * a:int < 2" simplifies to "2 * a:int <= 1"). I assume (ii) is
what happened in your example (because (i) is a form of eliminating common
factors) and thanks to eliminating common factors you removed some
rational/real solutions and made the problem solvable. And because this is
possible (i) and (ii) are also normally done for arithmetic inequalities.
(Still, you might very rarely get worse results because your
Fourier-Motzkin implementation changes the variable elimination order due
to heuristic shenanigans…)PS: Eliminating common factors and (i) and (ii) are not just preprocessing
steps but inprocessing steps. You should apply them after every
intermediate step of Fourier-Motzkin transformation…Since the existing code is quite delicate, I also don't want to mess with it.
I was more thinking of a preprocessing step, than a change to linarith itself. Which I expect to be a much bigger task.
Is there a simproc for eliminating common factors? I suspect not in full generality, because the simplifier leaves "10 * (i::int) ≤ 25 * j" alone. There is one by Larry for the simple case "m * t <= n * u" where m and n have a common factor. I have no idea how much work it would be to generalize it.
Thanks for the pointer.
Best regards,
Mathias
Best regards
Tobias
On 01/02/2019 18:38, Mathias Fleury wrote:
Hi list,
after trying to reconstruct more veriT proofs, I found out the following lemma cannot be discharged by linarith:
lemma "¬ 0 ≤ int (size l') ∨
¬ 10 * int (size lr) < 4 + 14 * int (size rr) ∨
10 * int (size lr) ≤ 15 + 25 * int (size l') ∨
¬ 10 * int (size lr) + 10 * int (size rr) ≤ 30 + 25 * int (size l') "
apply linarith (* fails *)
oops
However, if I simplify the coefficients by dividing by 5, then linearity is able to prove the goal:
lemma "¬ 0 ≤ int (size l') ∨
¬ 5 * int (size lr) < 2 + 7 * int (size rr) ∨
2 * int (size lr) ≤ 3 + 5 * int (size l') ∨
¬ 2 * int (size lr) + 2 * int (size rr) ≤ 6 + 5 * int (size l') "
apply linarith
done
Is there any simproc able to do this simplification automatically? If there is one, is there any reason why linarith does not use it by default?
Thanks,
Mathias
Email Gateway (Aug 22 2022 at 19:06):From: Tobias Nipkow <nipkow@in.tum.de>
I don't believe we have a master plan for arithmetic simprocs. Or only for some
of them. It is all grown historically, with sometimes odd interactions.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 19:06):From: Manuel Eberl <eberlm@in.tum.de>
I've been mentioning this issue occasionally over the last few years.
Considering how well computer algebra systems can handle equations and
inequalities, there /must/ be room for improvement in Isabelle/HOL.
Unfortunately, I've had little luck finding out what exactly it is that
these systems do, and in any case it is probably a lot of work. To make
matters worse, it might well break a lot of existing proofs if we switch
it on by default, and no one will use it if we don't.
Manuel
Email Gateway (Aug 22 2022 at 19:06):From: Manuel Eberl <eberlm@in.tum.de>
I just realised that I should have read more than the first sentence of
your email; I interpreted "Master plan for arithmetic simprocs" as "plan
for the future development of arithmetic simprocs". Now I see that's not
what you meant.
Still, if anyone has some opinions on what I wrote or feels inclined to
implement this, do come forward.
Manuel
Email Gateway (Aug 22 2022 at 19:06):From: Lawrence Paulson <lp15@cam.ac.uk>
I would love to see the following paper implemented:
https://tel.archives-ouvertes.fr/IMAG/hal-01505598v1
It discovers equalities and is therefore useful even when it can’t prove the goal outright. I guess it would be a medium-sized project.
Larry
Email Gateway (Aug 22 2022 at 19:06):From: Manuel Eberl <eberlm@in.tum.de>
I've seen that paper but I'm not sure how useful it would be in an
Isabelle context, at least in an Isar proof. There, the typical workflow
is that you have a fixed goal to prove and you chain in all the facts
that are needed to prove it and then you call a method that can either
solve it or it fails.
The only workflow I could possibly imagine is in apply-style
exploration: You run "apply linarith2" on your goal and if it can't
solve it, it prints a list of learned inequalities, and then you
manually go through that to see if there are any interesting ones among
them and then copypaste them back into your Isar proof before that.
Since this use of the method is purely diagnostic, there would be no
need to formalise the "learning new equalities" part at all.
I'm not saying that it wouldn't be interesting to formalise this method
just for the sake of formalising it; it's certainly interesting from a
theoretical viewpoint in any case. I'm just not sure that it would be
/that/ useful as an Isabelle tool.
By the way, since we're talking about simprocs, I'm currently offering a
student project at TUM to implement some extremely specialised simprocs
to tackle things like "ln(12) = 2*ln(2) + ln(3)", "of_nat n + 1 / 2 ∉ ℤ
= False", and "totient 1234 = 616" etc. Let's see if someone bites.
Manuel
Email Gateway (Aug 22 2022 at 19:06):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi list,
after trying to reconstruct more veriT proofs, I found out the following lemma cannot be discharged by linarith:
lemma "¬ 0 ≤ int (size l') ∨
¬ 10 * int (size lr) < 4 + 14 * int (size rr) ∨
10 * int (size lr) ≤ 15 + 25 * int (size l') ∨
¬ 10 * int (size lr) + 10 * int (size rr) ≤ 30 + 25 * int (size l') "
apply linarith (* fails *)
oops
However, if I simplify the coefficients by dividing by 5, then linearity is able to prove the goal:
lemma "¬ 0 ≤ int (size l') ∨
¬ 5 * int (size lr) < 2 + 7 * int (size rr) ∨
2 * int (size lr) ≤ 3 + 5 * int (size l') ∨
¬ 2 * int (size lr) + 2 * int (size rr) ≤ 6 + 5 * int (size l') "
apply linarith
done
Is there any simproc able to do this simplification automatically? If there is one, is there any reason why linarith does not use it by default?
Thanks,
Mathias
Email Gateway (Aug 22 2022 at 19:07):From: Tobias Nipkow <nipkow@in.tum.de>
There should be no need to divide by 5, linarith should not need it. Alas, ...
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 19:09):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
I had a look at the trace. The problems seems to be "¬ 10 * t2 ≤ 15 + 25 * t1".
If not simplified, it is transformed to "16 <= 10 * t2 + ~25 * t1" (in the tracing: "16 <= 10, 0, ~25")
After simplification, it becomes "¬ 2 * t2 ≤ 3 + 5 * t1", which is transformed to "4 <= 2 * t2 + ~5 * t1" (in the tracing: "4 <= 2, 0, ~5")
The latter yields an equivalent (but slightly stronger at a first glance) equality: "20 <= 10 * t2 + ~25 * t1". This equality is equivalent to "16 <= 10 * t2 + ~25 * t1", but linarith does not notice.
If I replace "10 * t2 ≤ 15 + 25 * t1" by "10 * t2 ≤ 19 + 25 * t1", then the refutation works (and this two expressions are equivalent).
On 1. Feb 2019, at 19:49, Tobias Nipkow <nipkow@in.tum.de> wrote:
There should be no need to divide by 5, linarith should not need it. Alas, …
Or is linarith suppose to preprocess the (in)equalities?
Mathias
The same example without the constants:
consts t1 :: int
consts t2 :: int
consts t3 :: int
definition "eq1 ≡ ¬ 0 ≤ t1 ∨ ¬ 10 * t2 < 4 + 14 * t3 ∨
10 * t2 ≤ 15 + 25 * t1 ∨ ¬ 10 * t2 + 10 * t3 ≤ 30 + 25 * t1"
definition "eq3 ≡ ¬ 0 ≤ t1 ∨ ¬ 10 * t2 < 4 + 14 * t3 ∨
2 * t2 ≤ 3 + 5 * t1 ∨ ¬ 2 * t2 + 2 * t3 ≤ 6 + 5 * t1"
lemma "eq1 "
unfolding eq1_def
supply [[linarith_trace]]
apply linarith
oops
(*
Trying to refute subgoal 1
¬ 0 ≤ t1 ∨
¬ 10 * t2 < 4 + 14 * t3 ∨
10 * t2 ≤ 15 + 25 * t1 ∨ ¬ 10 * t2 + 10 * t3 ≤ 30 + 25 * t1
prove:
Preprocessing yields 1 subgoal(s) total.
Splitting of inequalities yields 1 subgoal(s) total.
Refutation failed.
Trying to refute subgoal 1
0 ≤ t1 ⟹
10 * t2 < 4 + 14 * t3 ⟹
¬ 10 * t2 ≤ 15 + 25 * t1 ⟹
10 * t2 + 10 * t3 ≤ 30 + 25 * t1 ⟹ False
prove:
Preprocessing yields 1 subgoal(s) total.
Splitting of inequalities yields 1 subgoal(s) total.
0 <= 0, 0, 1
~3 <= ~10, 14, 0
16 <= 10, 0, ~25
~30 <= ~10, ~10, 25
0 <= 0, 0, 1
16 <= 10, 0, ~25
~225 <= ~120, 0, 175
0 <= 0, 0, 1
~33 <= 0, 0, ~125
~33 <= 0, 0, 0
Refutation failed.
*)
lemma "eq3 "
unfolding eq3_def
supply [[linarith_trace]]
apply linarith
done
(*
Trying to refute subgoal 1
¬ 0 ≤ t1 ∨
¬ 10 * t2 < 4 + 14 * t3 ∨
2 * t2 ≤ 3 + 5 * t1 ∨ ¬ 2 * t2 + 2 * t3 ≤ 6 + 5 * t1
prove:
Preprocessing yields 1 subgoal(s) total.
Splitting of inequalities yields 1 subgoal(s) total.
Refutation failed.
Trying to refute subgoal 1
0 ≤ t1 ⟹
10 * t2 < 4 + 14 * t3 ⟹
¬ 2 * t2 ≤ 3 + 5 * t1 ⟹ 2 * t2 + 2 * t3 ≤ 6 + 5 * t1 ⟹ False
prove:
Preprocessing yields 1 subgoal(s) total.
Splitting of inequalities yields 1 subgoal(s) total.
0 <= 0, 0, 1
~3 <= ~10, 14, 0
4 <= 2, 0, ~5
~6 <= ~2, ~2, 5
0 <= 0, 0, 1
4 <= 2, 0, ~5
~45 <= ~24, 0, 35
0 <= 0, 0, 1
3 <= 0, 0, ~25
3 <= 0, 0, 0
Contradiction! (1)
*)
On 1. Feb 2019, at 19:49, Tobias Nipkow <nipkow@in.tum.de> wrote:
There should be no need to divide by 5, linarith should not need it. Alas, ...
Tobias
On 01/02/2019 18:38, Mathias Fleury wrote:
Hi list,
after trying to reconstruct more veriT proofs, I found out the following lemma cannot be discharged by linarith:
lemma "¬ 0 ≤ int (size l') ∨
¬ 10 * int (size lr) < 4 + 14 * int (size rr) ∨
10 * int (size lr) ≤ 15 + 25 * int (size l') ∨
¬ 10 * int (size lr) + 10 * int (size rr) ≤ 30 + 25 * int (size l') "
apply linarith (* fails *)
oops
However, if I simplify the coefficients by dividing by 5, then linearity is able to prove the goal:
lemma "¬ 0 ≤ int (size l') ∨
¬ 5 * int (size lr) < 2 + 7 * int (size rr) ∨
2 * int (size lr) ≤ 3 + 5 * int (size l') ∨
¬ 2 * int (size lr) + 2 * int (size rr) ≤ 6 + 5 * int (size l') "
apply linarith
done
Is there any simproc able to do this simplification automatically? If there is one, is there any reason why linarith does not use it by default?
Thanks,
Mathias
Email Gateway (Aug 22 2022 at 19:11):From: Makarius <makarius@sketis.net>
In principle a proof tool can propose to add more Isar text as
"sendback" source snippets, e.g. see recent versions of the "induct"
family of methods. The main problem is probably technical, to place
further facts in the right spot before the goal statement: that would
require new sendback properties such that the Prover IDE knows what is
intended (Isabelle/Scala understands more Isar structure and syntax than
Isabelle/ML).
Makarius
Email Gateway (Aug 22 2022 at 19:12):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Mathias,
It took me some time to remember the key point: linarith uses Fourier-Motzkin
elimnation which is complere for rationals and reals but incomplete for
integers. For the latter we have Presburger, but it is too slow for the example.
The idea of eliminating common factors first is interesting. I have no idea if
this is always beneficial. Since the existing code is quite delicate, I also
don't want to mess with it.
Is there a simproc for eliminating common factors? I suspect not in full
generality, because the simplifier leaves "10 * (i::int) ≤ 25 * j" alone. There
is one by Larry for the simple case "m * t <= n * u" where m and n have a common
factor. I have no idea how much work it would be to generalize it.
Best regards
Tobias
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC