Re: Proofs of integer properties

On Saturday, November 8, 2014 8:44:23 AM UTC-8, Stephan Merz wrote:

Hi Chris,

1) GCD3 theorem information in the text seems to suggest the following should work:
==========================

<snip>

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

I was looking at both. I may have confused myself.

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.

Thank you! I was wondering why I couldn't get Number to work, and of course I am not expanding its definition. I had already rewritten it to use Nat \ {0} but of course missed the QED BY <1>1.

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.

Yes thank you, this is the problem. I didn't realise you need to refer to the step's assumptions in the BY line. Most of my issues so far seem to be syntax errors and misunderstanding the scoping of rule inclusion.

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.

I give up. Your modules model check just fine. My euclid module, which is almost identical to yours, simply refuses to. I guess there must be something screwy in my environment. I tried literally copying the contents of your files into mine, running a model check and it still won't run.

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).

Agreed.

Regards,
Stephan