# [tlaplus] MinMax Refinement Proof in TLAPS

• From: Balaji Arun <ba2669@xxxxxx>
• Date: Mon, 6 Apr 2020 12:41:19 -0700 (PDT)

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 == <<x, turn, y>>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.