The Euclid algorithm and TLAPS 1.4.5
37 views
Skip to first unread message
sido...@gmail.com
May 6, 2020, 4:05:34 PM5/6/20
to tlaplus
Hi,
I have just upgraded TLAPS from v1.4.3 to v1.4.5. I use TLA+ Toolbox v1.7.0 on Ubuntu.
And unfortunately TLAPS is not able to prove the following part of the Euclid algorithm:
THEOREM GCDProperty3 == ASSUME
NEW p \in Number,
NEW q \in Number,
q > p
PROVE GCD(p, q) = GCD(p, q - p)
<1> USE DEF Divisors, |
<1>1 \A d \in Number: d | p /\ d | q => d | (q - p)
BY DEF Number
<1>2 \A d \in Number: d | p /\ d | (q - p) => d | q
BY DEF Number
<1> QED
BY <1>1, <1>2 DEF GCD
NEW p \in Number,
NEW q \in Number,
q > p
PROVE GCD(p, q) = GCD(p, q - p)
<1> USE DEF Divisors, |
<1>1 \A d \in Number: d | p /\ d | q => d | (q - p)
BY DEF Number
<1>2 \A d \in Number: d | p /\ d | (q - p) => d | q
BY DEF Number
<1> QED
BY <1>1, <1>2 DEF GCD
More precisely, it cannot prove <1>1 and <1>2. I can see timeout after 30 seconds or something.
Downgrading to v1.4.3 solves the issue.
Has anybody encountered a similar issue? Or maybe somebody managed to prove the Euclid algorithm with TLAPS v1.4.5?
Best Regards,
Pawel
sido...@gmail.com
May 6, 2020, 4:10:43 PM5/6/20
to tlaplus
Okay, it looks like somebody else had the same issue: "TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)"
Reply all
Reply to author
Forward
0 new messages