MinMax Refinement Proof in TLAPS

[Balaji Arun]

TLAPS noob here.

I am reading the "Auxiliary Variables in TLA+" paper and have been trying to prove the theorem that MinMax1 implements MinMax2 using TLAPS. Below is my partial attempt at the proof. I understood from Stephen Merz's response to another post that I need to separately prove setMax and setMin due to the CHOOSE construct, which I did. But, I am having a hard time proving step <3>1. I appreciate any comments on my approach.

------------------------------- MODULE MinMax1 ------------------------------

EXTENDS Integers, TLAPS, FiniteSetTheorems

setMax(S) == CHOOSE t \in S : \A s \in S : t >= s

setMin(S) == CHOOSE t \in S : \A s \in S : t =< s

CONSTANTS Lo, Hi, Both, None

ASSUME Assumption == {Lo, Hi, Both, None} \cap Int = { }

VARIABLES x, turn, y

vars == <<x, turn, y>>

Init ==  /\ x = None

         /\ turn = "input"

         /\ y = {}

InputNum ==  /\ turn = "input"

             /\ turn' = "output"

            /\ x' \in Int

            /\ y' = y

Respond == /\ turn = "output"

           /\ turn' = "input"

          /\ y' = y \cup {x}

          /\ x' = IF x = setMax(y') THEN IF x = setMin(y') THEN Both ELSE Hi  

                                    ELSE IF x = setMin(y') THEN Lo   ELSE None

Next == InputNum \/ Respond

Spec == Init /\ [][Next]_vars

-----------------------------------------------------------------------------

Infinity      == CHOOSE n : n \notin Int

MinusInfinity == CHOOSE n : n \notin (Int \cup {Infinity})

M == INSTANCE MinMax2

        WITH min <- IF y = {} THEN Infinity      ELSE setMin(y),

            max <- IF y = {} THEN MinusInfinity ELSE setMax(y)

TypeOK == /\ x \in Int \cup {Lo, Hi, Both, None}

         /\ turn \in {"input", "output"}

         /\ y \in SUBSET Int

Inv == /\ TypeOK

      /\ \/ /\ turn = "output"

            /\ x \in Int

         \/ /\ turn = "input"

            /\ x \in {Lo, Hi, Both, None}

                     

LEMMA MaxIntegers ==

  ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S)

 PROVE  /\ setMax(S) \in S

        /\ \A yy \in S : yy <= setMax(S)

<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E xx \in T : \A yy \in T : yy <= xx

<1>1. P({})

 OBVIOUS

<1>2. ASSUME NEW T, NEW xx, P(T), xx \notin T

     PROVE  P(T \cup {xx})

 <2>. HAVE T \cup {xx} \in SUBSET Int

 <2>1. CASE \A yy \in T : yy <= xx

   BY <2>1, Isa

 <2>2. CASE \E yy \in T : ~(yy <= xx)

   <3>. T # {}

     BY <2>2

   <3>1. PICK yy \in T : \A zz \in T : zz <= yy

     BY <1>2

   <3>2. xx <= yy

     BY <2>2, <3>1

   <3>3. QED  BY <3>1, <3>2

 <2>. QED  BY <2>1, <2>2

<1>. HIDE DEF P

<1>3. P(S)  BY <1>1, <1>2, FS_Induction, IsaM("blast")

<1>. QED  BY <1>3, Zenon DEF setMax, P

LEMMA MinIntegers ==

 ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S)

 PROVE  /\ setMin(S) \in S

        /\ \A yy \in S : yy >= setMin(S)

<1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E xx \in T : \A yy \in T : yy >= xx

<1>1. P({})

 OBVIOUS

<1>2. ASSUME NEW T, NEW xx, P(T), xx \notin T

     PROVE  P(T \cup {xx})

 <2>. HAVE T \cup {xx} \in SUBSET Int

 <2>1. CASE \A yy \in T : yy >= xx

   BY <2>1, Isa

 <2>2. CASE \E yy \in T : ~(yy >= xx)

   <3>. T # {}

     BY <2>2

   <3>1. PICK yy \in T : \A zz \in T : zz >= yy

     BY <1>2

   <3>2. xx >= yy

     BY <2>2, <3>1

   <3>3. QED  BY <3>1, <3>2

 <2>. QED  BY <2>1, <2>2

<1>. HIDE DEF P

<1>3. P(S)  BY <1>1, <1>2, FS_Induction, IsaM("blast")

<1>. QED  BY <1>3, Zenon DEF setMin, P

LEMMA IInv == Spec => []Inv

<1> USE Assumption DEF Inv

<1>1. Init => Inv

 BY DEF Init, TypeOK

<1>2. Inv /\ [Next]_vars => Inv'

 BY DEF Next, vars, TypeOK, InputNum, Respond, setMax, setMin

<1>3. QED

  BY  <1>1, <1>2, PTL

 DEF Spec

THEOREM Implements == Spec => M!Spec

<1> USE Assumption, M!Assumption

<1>1. Init => M!Init

 BY DEF Init, M!Init, MinusInfinity, Infinity, M!MinusInfinity, M!Infinity

<1>2. Inv /\ [Next]_vars => [M!Next]_M!vars

 <2> SUFFICES ASSUME Inv,

                     [Next]_vars

              PROVE  [M!Next]_M!vars

   OBVIOUS

 <2>1. CASE InputNum

   BY <2>1

   DEF InputNum, M!Next, M!vars, M!InputNum

 <2>2. CASE Respond

   <3>1. CASE /\ turn = "output"

              /\ turn' = "input"

              /\ y' = y \cup {x}

     <4>1. CASE /\ y = {}

                /\ x' = Both

       BY <4>1, <3>1, <2>2

       DEF Respond,

           Inv, TypeOK,

           Next, vars, InputNum, Respond,

           setMax, setMin,

           Infinity, MinusInfinity,

           M!Next, M!vars, M!InputNum, M!Respond,

           M!Infinity, M!MinusInfinity,

           M!IsLeq, M!IsGeq

     <4>2. CASE /\ y = {x}

                /\ x' = Both

       BY <4>2, <3>1, <2>2

       DEF Respond,

           Inv, TypeOK,

           Next, vars, InputNum, Respond,

           setMax, setMin,

           Infinity, MinusInfinity,

           M!Next, M!vars, M!InputNum, M!Respond,

           M!Infinity, M!MinusInfinity,

           M!IsLeq, M!IsGeq

     <4>3. CASE /\ ~(\E yy \in y : yy > x)

                /\ x' = Hi

     <4>4. CASE /\ ~(\E yy \in y : yy < x)

                /\ x' = Lo

     <4>5. CASE /\ \E yy \in y : yy > x

                /\ \E yy \in y : yy > x

                /\ x' = None

     <4>6. QED

       BY  <4>1, <4>2, <4>3, <4>4, <4>5, <3>1, <2>2, MaxIntegers, MinIntegers

       DEF Respond,

           Inv, TypeOK,

           Next, vars, InputNum, Respond,

           setMax, setMin,

           Infinity, MinusInfinity,

           M!Next, M!vars, M!InputNum, M!Respond,

           M!Infinity, M!MinusInfinity,

           M!IsLeq, M!IsGeq

   <3>2. QED

      BY <3>1, <2>2

      DEF Respond

 <2>3. CASE UNCHANGED vars

   BY <2>3 DEF vars, M!vars

 <2>4. QED

   BY <2>1, <2>2, <2>3 DEF Next

<1>3. QED

  BY <1>1, <1>2, PTL, IInv

 DEF Spec, M!Spec

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

[Stephan Merz]

Hello,

I don't understand the structure of your proof. Step <3>1 (in the proof of theorem "Implements") is a CASE, which we can reformulate abstractly as

<3>1. ASSUME X PROVE P

(where X is the case assumption and P is the assertion of the enclosing step). Now, you prove this step using several more CASE steps

<4>1. CASE A

<4>2. CASE B

<4>3. CASE C

<4>4. CASE D

<4>5. CASE E

<4>6. QED

Each of <4>1-<4>5 proves P, assuming A, B etc. (The proofs of these steps may also refer to X since this is the enclosing CASE assumption.) The QED step has to ensure that the case distinction is complete, that is, that

A \/ B \/ C \/ D \/ E => X

is valid (in the context of any assumptions from the enclosing proof steps). It is absolutely not clear to me how this would be the case – in particular, A ... E mention the variables y, x, and x' whereas X contains x, y, y' and turn'.

Also, I don't understand why you structure the proof in this way. The case assumption X in fact follows from the enclosing CASE assumption "Respond", so you could simply write

<3>1. X  BY <2>2 DEF Respond

In order to discharge the overall proof obligation, you certainly want to establish M!Respond and therefore show the five conjuncts in the definition of this action, given the definition of Respond (in the implementation) and the refinement mapping. This will probably require case distinctions following the definition of the refinement mapping (y = {} or not) and those in the definitions of IsLeq / IsGeq but I don't see why the assumptions A, ..., E would help here.

Regards,

Stephan

--
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/b24fe285-fbfe-4117-8560-7836646f51b2%40googlegroups.com.

[Balaji Arun]

Hello Stephen,

Thanks for the reply. I understood your point about <3>1 and have rewritten the steps as follows. The QED steps are satisfied when I run the prover. Now, I am struck with <4>2. Am I correct in assuming that my cases are correct since the QED step <5>4 checks out? If so, how do I know why the set of provided facts for <5>1 is not enough (since the proof fails). Is there a way for me to debug my proof? The reason I ask is sometimes I see that the proof tactics play a role in the success of the proof within a timeout. So, I dont really know when I should increase the timeout, try a different proof technique, or work on my proof steps.

THEOREM Implements == Spec => M!Spec

<1> USE Assumption, M!Assumption

<1>1. Init => M!Init

 BY DEF Init, M!Init, MinusInfinity, Infinity, M!MinusInfinity, M!Infinity

<1>2. Inv /\ [Next]_vars => [M!Next]_M!vars

 <2> SUFFICES ASSUME Inv,

                     [Next]_vars

              PROVE  [M!Next]_M!vars

   OBVIOUS

 <2>1. CASE InputNum

   BY <2>1

   DEF InputNum, M!Next, M!vars, M!InputNum

 <2>2. CASE Respond

   <3>1. CASE y = {}

     BY  <3>1, <2>2

     DEF Inv, TypeOK,

         Next, vars, InputNum, Respond,

         setMax, setMin,

         Infinity, MinusInfinity,

         M!Next, M!vars, M!InputNum, M!Respond,

         M!Infinity, M!MinusInfinity,

         M!IsLeq, M!IsGeq

   <3>2. CASE y # {}

     <4>1. CASE y = {x}

       BY <4>1, <3>2, <2>2

       DEF Inv, TypeOK,

           Next, vars, InputNum, Respond,

           setMax, setMin,

           Infinity, MinusInfinity,

           M!Next, M!vars, M!InputNum, M!Respond,

           M!Infinity, M!MinusInfinity,

           M!IsLeq, M!IsGeq

     <4>2. CASE y # {x}

       <5>1. CASE M!IsLeq(x, setMin(y))

          BY <5>1, <4>2, <3>2, <2>2, MinIntegers

         DEF Inv, TypeOK,

           Next, vars, InputNum, Respond,

           setMax, setMin,

           Infinity, MinusInfinity,

           M!Next, M!vars, M!InputNum, M!Respond,

           M!Infinity, M!MinusInfinity,

           M!IsLeq, M!IsGeq

       <5>2. CASE M!IsGeq(x, setMax(y))

       <5>3. CASE /\ ~M!IsLeq(x, setMin(y))

                  /\ ~M!IsGeq(x, setMax(y))

       <5>4. QED

         BY <5>1, <5>2, <5>3, <4>2, <3>2, <2>2

     <4>3. QED

       BY <4>1, <4>2, <3>2, <2>2

   <3>3. QED

     BY <3>1, <3>2, <2>2

     DEF Respond,

         Inv, TypeOK,

         Next, vars, InputNum, Respond,

         setMax, setMin,

         Infinity, MinusInfinity,

         M!Next, M!vars, M!InputNum, M!Respond,

         M!Infinity, M!MinusInfinity,

         M!IsLeq, M!IsGeq

 <2>3. CASE UNCHANGED vars

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Stephan Merz]

Hello,

Thanks for the reply. I understood your point about <3>1 and have rewritten the steps as follows. The QED steps are satisfied when I run the prover. Now, I am struck with <4>2. Am I correct in assuming that my cases are correct since the QED step <5>4 checks out?

yes, success of that step shows you that your decomposition into cases is adequate for proving the enclosing goal.

If so, how do I know why the set of provided facts for <5>1 is not enough (since the proof fails). Is there a way for me to debug my proof? The reason I ask is sometimes I see that the proof tactics play a role in the success of the proof within a timeout. So, I dont really know when I should increase the timeout, try a different proof technique, or work on my proof steps.

Understanding why a proof fails is hard. It could be that the assertion is wrong or it could be that the automatic backends are not strong enough to understand why the assertion holds. In order to better understand what is going on, you will have to look at the proof obligation that the PM displays, and the smaller the obligation is, the easier it will be for you to understand it. It is therefore not helpful to just expand all definitions and use all available facts – also, that risks making the provers confused. It is better to introduce lemmas and outline the proof as a sequence of small steps (you may later collapse them into a larger step once you've understood how the proof really works).

Doing so in the concrete example reveals that quite a bit of scaffolding is necessary, such as showing that infinity / minus infinity is different from integers or reasoning about how the minimum of a set evolves when an element is added etc. I also strengthened the invariant to include the fact that the set y is always finite, since this is needed for the lemmas about setMin / setMax.

I have not completed the proof, but I hope that the outline in the attached module will help you better understand how to successfully write proofs. It may be the case that some facts proved in sub-cases of <3>10 / <3>11 will again be needed in the proof of <3>12. In that case you may want to refactor the proof to introduce them as level-3 steps and use them wherever needed. (That's why I left some "space" before <3>10.)

Regards,

Stephan

P.S.: Instead of copying and pasting parts of proofs, please attach TLA+ modules that can be directly loaded into the Toolbox.

[Balaji Arun]

Hello Stephan,

Thanks for the reply. 

I was having a hard time using the definitions of min and max from MinMax2 in MinMax1. It seems that defining min and max in the spec itself rather than passing to the INSTANCE declaration does the trick. I am still working on the proof, but I have learnt quite a lot since. Thank you.