How to refer to steps in TLAPS proofs? (new to TLA+)

19 views
Skip to first unread message

Saswata Paul

unread,
Jul 5, 2019, 2:48:46 AM7/5/19
to tlaplus
In page 6 of the paper "How to write a proof" (http://lamport.azurewebsites.net/pubs/lamport-how-to-write.pdf), It has been stated that "Part 3 of the statement of step <5>2 is numbered <5>.2.3. 

By that syntax, in the proof of irrationality given in Figure 5. (page 7), <1>1.1 should refer to gcd(m,n)=1. However, later in the proof of m^2=2(n^2), it says PROOF: <1>1.1 implies (m/n)^2 = 2. How can gcd(m,n)=1 imply (m/n)^2 = 2 ? 

I think I am missing something subtle about the numbering of steps here (or my sleepless mind is making a silly mistake elsewhere). Any help is appreciated.

PS: the content of page 7 is given below:

1.PNG

 

Stephan Merz

unread,
Jul 5, 2019, 3:04:03 AM7/5/19
to tla...@googlegroups.com
The justification should certainly read 

"Step <1>1.2 and assumption <0>:2 imply that (m/n)^2 = 2"

Please note that this document precedes the design of TLAPS and that the proof has not been checked mechanically.

Regards,
Stephan

<1.PNG>

 

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d8d12743-bb95-4bec-b8f8-2986de55e930%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
<1.PNG>

Saswata Paul

unread,
Jul 5, 2019, 3:14:55 AM7/5/19
to tla...@googlegroups.com
This makes much more sense now. Thank you!


On Friday, July 5, 2019, Stephan Merz <stepha...@gmail.com> wrote:
The justification should certainly read 

"Step <1>1.2 and assumption <0>:2 imply that (m/n)^2 = 2"

Please note that this document precedes the design of TLAPS and that the proof has not been checked mechanically.

Regards,
Stephan

On 5 Jul 2019, at 08:48, Saswata Paul <paulsa...@gmail.com> wrote:

In page 6 of the paper "How to write a proof" (http://lamport.azurewebsites.net/pubs/lamport-how-to-write.pdf), It has been stated that "Part 3 of the statement of step <5>2 is numbered <5>.2.3. 

By that syntax, in the proof of irrationality given in Figure 5. (page 7), <1>1.1 should refer to gcd(m,n)=1. However, later in the proof of m^2=2(n^2), it says PROOF: <1>1.1 implies (m/n)^2 = 2. How can gcd(m,n)=1 imply (m/n)^2 = 2 ? 

I think I am missing something subtle about the numbering of steps here (or my sleepless mind is making a silly mistake elsewhere). Any help is appreciated.

PS: the content of page 7 is given below:

<1.PNG>

 

--
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@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d8d12743-bb95-4bec-b8f8-2986de55e930%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
<1.PNG>

--
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/P2DcOueePrU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1804728D-8AC6-4F94-BE2D-3DB160416EA9%40gmail.com.
Reply all
Reply to author
Forward
0 new messages