# Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)

Thank you very much Stephan for the detailed explanation and the solution. I used your solution to keep the main theorem GCD3 simple, so the step is now out as a separate lemma (see below).

Regarding the whole thing of not being able to prove the theorem as before: is this sort of regression problematic in the contest of theorem proving? I'm imagining what could happen if in a few years a work (or a published paper) is no longer "provable" due to regressions in the software. I've seen this has already partially discussed in this forum regarding regressions introduced by a new release of TLAPS.

The GCD3 theorem with the separate lemma.

THEOREM CommonDivisorsWithDifference == \A m, n \in Nat \ {0} : \A i \in Int :
(n > m) => (Divides(i, m) /\ Divides(i, n) <=> Divides(i, m) /\ Divides(i, n - m))
<1> SUFFICES ASSUME NEW m \in Nat \ {0},
NEW n \in Nat \ {0},
NEW i \in Int,
n > m
PROVE Divides(i, m) /\ Divides(i, n) <=> Divides(i, m) /\ Divides(i, n - m)
OBVIOUS
\* proving =>
<1>a ASSUME NEW z \in Int,
m = i*z,
NEW r \in Int,
n = i*r
PROVE Divides(i, n - m)
<2> r-z \in Int /\ n-m = i*(r-z)
BY <1>a
<2> QED BY DEF Divides
\* proving <=
<1>b ASSUME NEW z \in Int,
n - m = i*z,
NEW r \in Int,
m = i*r
PROVE Divides(i, n)
<2> z + r \in Int /\ n = i*(z+r)
BY <1>b
<2> QED BY DEF Divides
\* QED
<1> QED BY <1>a, <1>b DEF Divides

THEOREM GCD3 == \A m, n \in Nat \ {0}:
(n > m) => (GCD(m, n) = GCD(m, n - m))
<1> SUFFICES ASSUME NEW m \in Nat \ {0},
NEW n \in Nat \ {0},
n > m
PROVE  GCD(m, n) = GCD(m, n-m)
OBVIOUS
<1> CommonDivisorsWithDifference
BY CommonDivisorsWithDifference DEF Divides
<1> QED
BY DEF GCD, SetMax , DivisorsOf

--
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.