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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Mon, 21 Nov 2022 17:55:42 -0800 (PST)*References*: <57a329dc-6578-4235-ad56-a579e35c2234n@googlegroups.com> <1986E5A8-0341-431E-AF85-8443FFDAD787@gmail.com> <5ae6ca5e-e749-4373-afce-13ceea4655a1n@googlegroups.com> <76B44782-88F5-492F-AAD9-34CA3F1DCC96@gmail.com>

Thanks, Stephan! Very interesting. Semantics are different from syntax, of course. Always nice to peek into the other side.

Andrew

On Monday, November 21, 2022 at 11:00:41 AM UTC-5 Stephan Merz wrote:

Hi Andrew,you are right that the SUFFICES keyword is optional in the grammar. However, its presence changes the meaning of the step. Consider the following example of a step claiming that some predicate P is provable.<1>x. P<2>1. SUFFICES QBY ... \* proof establishing ASSUME Q PROVE P<2>. QEDBY ... \* proof establishing QStep <2>1 reduces the proof of P to that of Q, i.e. its proof requires inferring P provided Q is provable. The current goal is now no longer P, but Q, and the QED step must prove that Q holds.On the other hand, consider the following:<1>x. P

<2>1. Q

BY ... \* proof establishing Q

<2>. QED

BY ... \* proof establishing P (possibly using Q)

Here, step <2>1 just asserts Q as a fact, and the BY clause must allow it to be proved. The current goal is still P, and therefore the QED step must establish P. It may use the fact Q by invoking <2>1 in the BY clause for the QED step. So, while both proofs are syntactically legal, their logical meaning is different.At the end of the day, the same arguments must be provided in both proofs, but in a different order, and one or the other may feel more natural in a given context. In proof assistant jargon, the first approach is called "backward chaining", and the second one is called "forward chaining". The latter is the default in TLAPS.Also, this discussion is actually unrelated to the original question about WITNESS: that keyword is intended for instantiating existential quantification, and it doesn't make sense to write SUFFICES WITNESS e.Regards,StephanOn 21 Nov 2022, at 15:41, Andrew Helwer <andrew...@xxxxxxxxx> wrote:To expand on Stephan's reply, the SUFFICES keyword is actually optional in SUFFICES steps. So just writing an _expression_ without any keyword prependediswriting a SUFFICES step.AndrewOn Sunday, November 20, 2022 at 3:16:56 AM UTC-5 Stephan Merz wrote:Hi Jaco,the directive "WITNESS e" quite clearly does not require proof, and by analogy (and in order to simplify the grammar) it was decided that "WITNESS e \in S" would not take a proof either but that the fact "e \in S" should follow obviously from the context. What you can do is write something like the following where the first step inserts the required fact in the context.<1>. e \in SBY ...<1>. WITNESS e \in SPersonally, I tend to use WITNESS rarely but usually write something like<1>x. e \in SBY ...<1>y. P(e)BY ...<1>z. \E x \in S : P(x)BY <1>x, <1>yRegards,StephanOn 19 Nov 2022, at 14:15, Jaco van de Pol <jaco...@xxxxxxxxx> wrote:Hi,My "WITNESS x \in y" generates a proof obligation, so it would be nice towrite WITNESS x\in y BY <proof>, but as far as I understand this is notpossible. Is there a reason? Is there a general work around?Thanks for your thoughts,

Jaco van de Pol--

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/57a329dc-6578-4235-ad56-a579e35c2234n%40googlegroups.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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5ae6ca5e-e749-4373-afce-13ceea4655a1n%40googlegroups.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/88131963-4670-49b6-8792-018d33a726e7n%40googlegroups.com.

**References**:**[tlaplus] WITNESS BY***From:*Jaco van de Pol

**Re: [tlaplus] WITNESS BY***From:*Stephan Merz

**Re: [tlaplus] WITNESS BY***From:*Andrew Helwer

**Re: [tlaplus] WITNESS BY***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] WITNESS BY** - Next by Date:
**[tlaplus] User defined symmetry in TLA+ Toolbox** - Previous by thread:
**Re: [tlaplus] WITNESS BY** - Next by thread:
**[tlaplus] User defined symmetry in TLA+ Toolbox** - Index(es):