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