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

THEOREM Div == \A m \in Nat \ {0}, n \in Nat \ {0}, d \in Int :

Divides(d, m) /\ Divides(d, n) <=> Divides(d, m) /\ Divides(d, n-m)

<1> SUFFICES ASSUME NEW m \in Nat \ {0}, NEW n \in Nat \ {0}, NEW d \in Int

PROVE /\ Divides(d, m) /\ Divides(d, n) => Divides(d, n-m)

/\ Divides(d, m) /\ Divides(d, n-m) => Divides(d, n)

OBVIOUS

<1>1. Divides(d, m) /\ Divides(d, n) => Divides(d, n-m)

<2>1. SUFFICES ASSUME NEW g \in Int, m = d*g,

NEW q \in Int, n = d*q

PROVE \E y \in Int : n-m = d*y

BY DEF Divides

<2>2. n-m = d*(q-g)

BY <2>1

<2>3. QED

BY <2>2

<1>2. Divides(d, m) /\ Divides(d, n-m) => Divides(d, n)

<2>1. SUFFICES ASSUME NEW g \in Int, m = d*g,

NEW q \in Int, n-m = d*q

PROVE \E y \in Int : n = d*y

BY DEF Divides

<2>2. n = d*(q+g)

BY <2>1

<2>3. QED

BY <2>2

<1>3. QED

BY <1>1, <1>2

With Div in place, GCD3 can simply be written as:

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>1. \A i \in Int : Divides(i, m) /\ Divides(i, n) <=> Divides(i, m) /\ Divides(i, n-m)

BY Div

<1>2. QED

BY <1>1 DEF GCD, SetMax, DivisorsOf

While I don't profess that it's the most elegant approach, it is sufficiently fine-grained, minimising the size of each 'leap' and the number of theorems employed by each step. This makes it more resilient towards subtle regressions in Isabelle which have tripped me up in the past.

On Sunday, April 19, 2020 at 10:43:57 PM UTC+10 Stephan Merz wrote:

Hello again Nicholas,

I don't think any proof assistant promises backward compatibility because that would severely restrict change. In this particular case, the issue moreover appears to have been caused by changes in automatic back-end provers that are not under our control. The mechanism that Isabelle/HOL has adopted with the Archive of Formal Proofs [1] is to collect major proof developments and run regression tests with every new release of the prover. When proofs fail, the Isabelle implementors assess whether they consider the change to be overall positive or if it breaks too many developments. In case the change is retained, maintainers of the collection (and/or the original author) fix the failing proofs so that they are kept up to date with new Isabelle releases.

For TLAPS, we do not yet have a critical mass of proofs but some day we may wish to implement a similar policy.

Regards,
Stephan

[1] https://www.isa-afp.org

On 19 Apr 2020, at 14:33, 'Nicholas Fiorentini' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0cdf0ab6-f6a5-49dd-8292-ca15db5a01d8%40googlegroups.com.