Re: [tlaplus] MinMax Refinement Proof in TLAPS

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

On Wednesday, April 8, 2020 at 10:12:36 AM UTC-4, Stephan Merz wrote:

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

On 6 Apr 2020, at 21:41, Balaji Arun <ba2...@xxxxxx> wrote:

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 =============================================================================

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b24fe285-fbfe-4117-8560-7836646f51b2%40googlegroups.com.