[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Proofs of integer properties



Hi Chris,


1) GCD3 theorem information in the text seems to suggest the following should work:
==========================
THEOREM GCD3 == \A m, n \in Number : (n > m) => (GCD(m, n) = GCD(m, n-m)) 
  <1> SUFFICES ASSUME NEW m \in Number, NEW n \in Number,
                      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 LemmaDiv DEF Divides
  <1> QED
    BY DEF GCD, SetMax, DivisorsOf, Divides
==========================
But <1>1 doesn't prove. I probably misunderstood.

I'm not quite sure which part of the hyperbook you looked at. The informal proof in the main track has four steps and uses lemma Div. The formal proof in the proof track (chapter 11.2) doesn't mention that lemma: in fact, the SMT backend is smart enough to perform that reasoning. Reconstructing the lemma from what is written in the hyperbook, I obtain

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

and this is indeed proved. It's very similar to what you wrote except that (a) I don't invoke LemmaDiv, (b) all steps are unnumbered, and (c) I use Nat and Int whereas you have Number and Int. Let's look at each difference:

(a) Adding LemmaDiv (whatever it may be) might confuse the backend but it seems unlikely that this is the problem.

(b) It's obvious that you need to add <1>1 as a fact to the proof of the QED step, but that doesn't affect the proof of your step <1>1.

(c) This must be the real difference: you should expand the definition of Number, otherwise the prover cannot apply the definition of Divides, which (according to the hyperbook) is stated for Int.

Anyway, I attach my full module to this message so that we are on the same page.

2) The proofs section breaking down Inv /\ [Next]_vars => Inv', I needed to add 'BY UNCHANGED vars' to steps <2>2 and <2>3. It didn't seem to pick it up from ASSUMES, and I didn't see anything in the text about it.

I don't quite see where you are pointing since the hyperbook doesn't seem to show all the details of that proof but I presume that the assumption UNCHANGED vars appears the step enclosing the one you are trying to prove. You have to invoke that step in the facts that appear in the BY clause, as in:

<4>42. ASSUME Inv, UNCHANGED vars PROVE Inv'
  BY <4>42 DEF Inv, vars

The basic principle is that all necessary facts and definitions have to be named explicitly in proofs, except for those mentioned in a USE [DEF] clause or for facts in unnumbered steps that cannot be named. The apparently circular reference <4>42 in the step above refers to the assumption of the current step. References to <4>42 outside of its own proof refer to the entire ASSUME PROVE clause.

By the way, the module attached to this message contains a simpler proof of the theorem: the decompositions introduced in the hyperbook are given for pedagogical purposes.


3) I couldn't get a TLC model to run with the Euclid PlusCal module. It just won't start, no error messages or anything. I had a model running for GCD module just fine.

I cannot reproduce this problem. More specifically, I can run TLC on the module attached to this message. Concretely, I instantiated M and N by 42 and 24 and told TLC to verify the invariants Inv and PartialCorrectness. As expected, TLC complains that it cannot enumerate Int, so I have to override the definition of Int (in Advanced Options -> Definition Override), for example by the interval -100 .. 100.

4) I saw an assertion when I accidentally put a proof step <1>4 in USE DEF <1>4 instead of USE <1>4 DEF ..  I assumed it was not surprising this caused weirdness. 

Yes, this should eventually be caught by the proof manager instead of raising an assertion ...

In general I am really impressed with the quality of the environment and the documentation. I have wanted to look into using formal methods for a while but the literature is almost incomprehensible. You really need to just dive in and play with it, but then the trick is finding tools etc. etc. For learning purposes it really helps to just be able to jump in, build a specification, test it against a model and then prove it.

Thanks. Feedback is important to improve the tool and the doc.

One comment about the hyperbook in particular, the text description building up proofs is good to follow along and force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

It might be helpful to have the actual TLA+ modules accompany the hyperbook, rather than just the PDF versions (even the ASCII in PDF form).

Regards,
Stephan

Attachment: Euclid.tla
Description: Binary data

Attachment: GCD.tla
Description: Binary data