# Re: [tlaplus] Optimizing proof check time

Unfortunately switching the proof from

<2>c. \E n \in Nat : 2*n = x + 2
<3> SUFFICES
ASSUME (c + 1) \in Nat
PROVE 2*(c + 1) = x + 2
BY Isa
to

<2>c. \E n \in Nat : 2*n = x + 2
<3> (c + 1) \in Nat BY <2>a
<3> WITNESS (c + 1) \in Nat

doesn't reduce proof time; actually it increases it because I can't indicate that a WITNESS proof step should use Isabelle!

Andrew

On Thu, Mar 30, 2023 at 12:25 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
If the solvers don’t figure out the witness term for existential goals, you can help by writing

WITNESS e \in Nat

which transforms the goal \E x \in Nat : P(n) to proving P(e). Note that WITNESS doesn’t take a proof. If it isn’t completely obvious, add a preliminary step that shows e \in Nat.

Stephan

On 30 Mar 2023, at 18:04, Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

﻿
The --line flag has proven helpful. I might whip up a quick rust program that uses the tree-sitter grammar to find all lines with terminal proofs, runs tlapm FileName.tla --line N, measures the wall clock time for each, then prints out a sorted list of the longest-running proofs.

I'm having trouble proving a goal of type \E n \in Nat : P(n). It times out every other solver before Isabelle finally catches it. So I can reduce the time by specifying BY Isa, but I would be interested in knowing whether there's a way to break it down further to speed up checking:

Andrew

On Tuesday, March 28, 2023 at 2:47:55 AM UTC-4 Stephan Merz wrote:
If you send me (off-list) your proofs, I can have a look, and that may help us optimize the encoding for the back-end provers. My hunch is that it's not just arithmetic but rather a combination, such as function application and arithmetic. Breaking down complex proofs into smaller steps will in general help speed up proof checking, as may introducing local definitions for abstracting complex subformulas. A trivial way to reduce wall-clock time is to explicitly indicate the relevant back-end if SMT (which is called first) doesn't succeed so that you don't have to wait for it to time out. But my advice would be not to exaggerate: this is a rabbit hole that's probably not worth exploring.

Not sure I understand your last question, but perhaps you systematically invoke the prover on the entire module (from the command line). The Toolbox GUI really helps for launching the prover on individual obligations, but you can also run it from the command line using

tlapm --toolbox m n

where m and n denote the interval of lines in the module that you'd like the prover to check.

Stephan

On 27 Mar 2023, at 19:24, Andrew Helwer <andrew...@xxxxxxxxx> wrote:

I've written some arithmetic proofs where the prover does eventually validate the proof, albeit after a fairly long wait time. In general, can one reduce proof check time by breaking down a long-running proof into smaller substeps? Is there a way to check which steps are taking a long time so you know where to focus efforts?

Thanks!

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXEh034sKeX4Tdm21UWZ069Q89hAC9Fb2L9cMFf9oSOjw%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.