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

[Nicholas Fiorentini]

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

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

[Stephan Merz]

Hello,

it's not your fault that this proof doesn't go through. The obligation falls into the theory of non-linear integer arithmetic, which is undecidable and for which SMT solvers implement heuristics. Unfortunately, these are quite brittle, in particular when quantifiers are involved as in this case (namely the definition of Divides). At the time when that chapter of the Hyperbook was written, the version of CVC3 that was then the default solver used by TLAPS must have been able to prove that obligation. I now tried CVC3, CVC4 and Z3, and none of them found the proof automatically, so we must break down the proof one level further and indicate the witness terms for the existential quantifier – see below.

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?

I don't think that there is a single best approach. The two definitions differ in that, for example, the Hyperbook versions have Divides(-2,4) or Divides(0,0), in contrast to the versions on the Web page. But for the Euclid algorithm, we are only interested in positive natural numbers (and the GCD theorems are only stated for those), so these differences should not matter.

Regards,

Stephan

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. ASSUME NEW i \in Int, NEW q \in Int, m = i*q, NEW r \in Int, n = i*r
        PROVE  \E z \in Int : n-m = i*z
     <2>1. r-q \in Int /\ n-m = i*(r-q)
       BY <1>1
     <2>. QED  BY <2>1
  <1>2. ASSUME NEW i \in Int, NEW q \in Int, m = i*q, NEW r \in Int, n-m = i*r
        PROVE  \E z \in Int : n = i*z
     <2>1. r+q \in Int /\ n = i*(r+q)
       BY <1>2
     <2>. QED  BY <2>1
  <1> QED
    BY <1>1, <1>2 DEF GCD, SetMax , DivisorsOf, Divides

---

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 qual...@legalmail.it

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.

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7e0fc5aa-f0c0-4f74-807b-bf0d5a114261%40googlegroups.com.

[Nicholas Fiorentini]

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

[Stephan Merz]

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

--
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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0cdf0ab6-f6a5-49dd-8292-ca15db5a01d8%40googlegroups.com.

[Emil Koutanov]

The approach I took was to reference a slightly modified version of Lemma Div, that is casually mentioned in Lamport's hyperbook. It was amended to the following, and I have taken the liberty of proving it:

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.