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. QEDEach 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, thatA \/ B \/ C \/ D \/ E => Xis 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 RespondIn 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,StephanOn 6 Apr 2020, at 21:41, Balaji Arun 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, FiniteSetTheoremssetMax(S) == CHOOSE t \in S : \A s \in S : t >= ssetMin(S) == CHOOSE t \in S : \A s \in S : t =< sCONSTANTS Lo, Hi, Both, NoneASSUME Assumption == {Lo, Hi, Both, None} \cap Int = { }VARIABLES x, turn, yvars == <>Init ==  /\ x = None         /\ turn = "input"          /\ y = {}InputNum ==  /\ turn = "input"             /\ turn' = "output"             /\ x' \in Int             /\ y' = yRespond == /\ 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 NoneNext == InputNum \/ RespondSpec == Init /\ [][Next]_vars-----------------------------------------------------------------------------Infinity      == CHOOSE n : n \notin IntMinusInfinity == 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 IntInv == /\ 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, PLEMMA 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, PLEMMA 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 SpecTHEOREM 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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b24fe285-fbfe-4117-8560-7836646f51b2%40googlegroups.com. -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/63676597-8A03-44C4-A3A0-DD7801FBD695%40gmail.com.