Re: [isabelle] Solving big quantifier-free linear real arithmetic goals

[Manuel Eberl]

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


On 29/09/16 21:50, Sascha Boehme wrote:
> 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
>
>
> Am Samstag, 09. April 2016 22:34 CEST, Manuel Eberl <ebe...@in.tum.de> schrieb:
>
>> 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,
>>
>> Manuel
>>
>
>
>
>
>
>
>