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

Hello,

After having tried the tutorial from the official TLAPS site, I moved to the chapter 11 of the TLA+ Hyperbook.

I was able to prove GCD1 and GCD2, but now I'm stuck on GCD3. I'm at the very last part of the proof: using BY DEF Divides to check the main step of the proof, thus concluding the whole proof. The problem is that TLAPS is unable to use prove this. Here the obligation:

ASSUME NEW CONSTANT m \in Nat \ {0},
NEW CONSTANT n \in Nat \ {0},
n > m
PROVE \A i \in Int :
(\E q \in Int : m = i * q) /\ (\E q \in Int : n = i * q)
<=> (\E q \in Int : m = i * q) /\ (\E q \in Int : n - m = i * q)

Reading the book seems that this should not happen. What I'm doing wrong?

I also tried changing the few Int with Nat. Btw, why this module defines Divides and DivisorOf over all Int instead of a subset like in https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html? What is the best approach in this case?

Thanks for your help,

Nicholas

Here my tla file. In bold the line with the problem.

--------------------------- MODULE GCDProperties ---------------------------

EXTENDS Integers, FiniteSets, TLAPS, NaturalsInduction

Divides(p, n) == \E q \in Int : n = p * q

DivisorsOf(n) == {p \in Int : Divides(p, n)}

SetMax(S) == CHOOSE i \in S : \A j \in S : i >= j

GCD(m, n) == SetMax(DivisorsOf(m) \cap DivisorsOf(n))

THEOREM GCD1 == \A m \in Nat \ {0} : GCD(m, m) = m

<1> SUFFICES ASSUME NEW m \in Nat \ {0}

PROVE GCD(m, m) = m

OBVIOUS

<1>1 Divides(m, m)

BY DEF Divides

<1>2 \A i \in Nat : Divides(i, m) => (i =< m)

BY DEF Divides

<1> QED

BY <1>1, <1>2 DEF GCD, SetMax, DivisorsOf

THEOREM GCD2 == \A m, n \in Nat \ {0} : GCD(m, n) = GCD(n, m)

BY DEF GCD

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

BY DEF Divides

<1> QED

BY DEF GCD, SetMax, DivisorsOf

=============================================================================

Sito Web: www.qualitade.com
Trovaci su:

Via Mantova 137, 26100 Cremona

+39 0372 1931375

P.IVA: 01643800194 | Capitale Sociale: 10.000 euro

Informativa Privacy

Questa email ha per destinatari dei contatti presenti negli archivi di Qualitade S.r.l.. Tutte le informazioni vengono trattate e tutelate nel rispetto della normativa vigente sulla protezione dei dati personali (Reg. EU 2016/679). Per richiedere informazioni e/o variazioni e/o la cancellazione dei vostri dati presenti nei nostri archivi potete inviare una email a qualitade@xxxxxxxxxxxx

Avviso di Riservatezza

Il contenuto di questa e-mail e degli eventuali allegati, è strettamente confidenziale e destinato alla/e persona/e a cui è indirizzato. Se avete ricevuto per errore questa e-mail, vi preghiamo di segnalarcelo immediatamente e di cancellarla dal vostro computer. E' fatto divieto di copiare e divulgare il contenuto di questa e-mail. Ogni utilizzo abusivo delle informazioni qui contenute da parte di persone terze o comunque non indicate nella presente e-mail, potrà essere perseguito ai sensi di legge.