[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] MinMax Refinement Proof in TLAPS



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