[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Thu, 30 Mar 2023 13:08:43 -0400*References*: <a754d530-0927-4337-bff3-3e51e7ea5b55n@googlegroups.com> <FF11075D-DF25-4700-957D-C01C8597F581@gmail.com>

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

<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 writingWITNESS e \in Natwhich 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.StephanOn 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 usingtlapm --toolbox m nwhere m and n denote the interval of lines in the module that you'd like the prover to check.StephanOn 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.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a754d530-0927-4337-bff3-3e51e7ea5b55n%40googlegroups.com.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/ztIjM7zb_iU/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/FF11075D-DF25-4700-957D-C01C8597F581%40gmail.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.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUUp2G07nL3hTGe05Rh4r_qAHb%2BDo4CkWLiYGygGSUiiyQ%40mail.gmail.com.

**References**:**Re: [tlaplus] Optimizing proof check time***From:*Andrew Helwer

**Re: [tlaplus] Optimizing proof check time***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Graph of actions that enable other actions** - Next by Date:
**Re: [tlaplus] Graph of actions that enable other actions** - Previous by thread:
**Re: [tlaplus] Optimizing proof check time** - Next by thread:
**[tlaplus] Help understanding why this proof validates** - Index(es):