Email Gateway (Aug 22 2022 at 13:07): Email Gateway (Aug 22 2022 at 13:07):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I am currently working on some Social Choice Theory. The proof basically
works by deriving a number of equalities and inequalities over real
numbers and then showing that they are inconsistent.
I have already derived these conditions and now need to show that they
are actually inconsistent. This is goal1 in the attachment. Here, pmf is
from HOL-Probability and sds, R1, R2, a, b, c, d etc. are
constants/fixed locale variables whose properties are irrelevant for
this goal. To emphasise this: I can restate the goal by generalising it
a bit, introducing real variables for all the expressions (see goal2).
If one simplifies this a bit and eliminates redundant variables, one
obtains goal3.
I tried the following things:
– smt (i.e. Z3) is able to solve goal1 within .3 seconds; proof
reconstruction takes another 12 seconds.
– smt solves goal2 within .5 seconds; proof reconstruction seems to take
longer than my patience will permit though.
– smt solves goal3 within .3 seconds; proof reconstruction takes 67 seconds.
– Both goals should be solvable by linarith in theory. I tried it and
gave up after an hour or so.
This raises the following questions:
– Why is this trivial for Z3 but impossible for linarith?
– Is there any hope of tweaking linarith to get this proof through?
– Why does proof reconstruction take so much longer on goal2 and goal3,
even though they are arguably ‘simpler’?
I know that proofs using smt are not allowed in the AFP, so the prospect
that I can only prove this with smt is a bit troubling.
Incidentally, another question: Is there any easy way to turn something
like goal1 into something like goal2, i.e. generalise all real
non-literals in a term to real variables? I wrote my own very ad-hoc
tactic for this, but it seems like quite a common use case.
Cheers,
Email Gateway (Aug 22 2022 at 14:10):From: Sascha Boehme <boehmes@in.tum.de>
Hi Manuel,
You might be interested to hear that the next Isabelle release will provide a new method named argo that is capable of solving such goals without invoking an external tool. With argo, your goals can be proved within five seconds on off-the-shelf hardware.
Cheers,
Sascha
Email Gateway (Aug 22 2022 at 14:10):From: Manuel Eberl <eberlm@in.tum.de>
Hallo Sascha,
very nice indeed! I shall take a look at it.
I've since converted the SMT-based proof into a fully-structured Isar
proof (which was my goal anyway, I just wasn't sure whether it was
feasible – it was)
Still, I'm sure this will be very useful if I ever run into similar
issues in the future.
Cheers,
Manuel
Last updated: Apr 25 2024 at 16:19 UTC