Make SimpleEventually proof a bit less simple.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

examples/SimpleEventually.tla

@@ -3,33 +3,58 @@
 EXTENDS TLAPS
 
 
-VARIABLE x
-
-
-Init == x = FALSE
-Next == x = FALSE /\ x' = TRUE
-System == Init /\ [][Next]_x /\ WF_x(Next)
-
-
-THEOREM System => <>(x = TRUE)
-<1>1. SUFFICES (System /\ []~(x = TRUE)) => FALSE
-    BY <1>1, PTL
-<1> DEFINE TypeOK == x \in BOOLEAN
-<1> HIDE DEF TypeOK
-<1>2. (Init /\ [][Next]_x) => []TypeOK
-    <2>1. Init => TypeOK
-        BY DEF Init, TypeOK
-    <2>2. ASSUME TypeOK /\ [Next]_x
-          PROVE TypeOK'
-        BY <2>2 DEF TypeOK, Next
-    <2> QED
-        BY <2>1, <2>2, PTL
-<1>3. ASSUME TypeOK /\ ~(x = TRUE)
-      PROVE ENABLED <<Next>>_x
-    BY <1>3, ExpandENABLED DEF Next
-<1>4. ASSUME <<Next>>_x
+VARIABLE x, y
+vars == <<x, y>>
+
+TypeOK ==
+    /\ x \in BOOLEAN
+    /\ y \in BOOLEAN
+
+Init ==
+    /\ x = FALSE
+    /\ y = FALSE
+
+A ==
+    /\ x = FALSE
+    /\ x' = TRUE
+    /\ UNCHANGED y
+
+B ==
+    /\ y = FALSE
+    /\ y' = TRUE
+    /\ UNCHANGED x
+
+Next ==
+    A \/ B
+
+System ==
+    Init /\ [][Next]_vars /\ WF_vars(A)
+
+-------------------------------------------------------------------------------
+
+LEMMA TypeCorrect == System => []TypeOK
+<1>1. Init => TypeOK BY DEF Init, TypeOK
+<1>2. TypeOK /\ [Next]_vars => TypeOK' BY DEF TypeOK, Next, vars, A, B
+<1>. QED BY <1>1, <1>2, PTL DEF System, TypeOK, Init, Next, A, B
+
+-------------------------------------------------------------------------------
+
+Prop ==
+    <>(x = TRUE)
+
+\* The PM needs this hint for the liveness proof to be accepted.
+LEMMA Equiv == ~(x = TRUE) <=> (x = FALSE) OBVIOUS
+USE Equiv
+
+THEOREM System => Prop
+<1>1. SUFFICES (System /\ [](x = FALSE)) => FALSE 
+    BY <1>1, PTL DEF Prop
+<1>3. ASSUME TypeOK /\ (x = FALSE)
+      PROVE ENABLED <<A>>_vars
+    BY <1>3, ExpandENABLED DEF Next, vars, A, B
+<1>4. ASSUME <<A>>_vars
       PROVE (x = TRUE)'
-    BY <1>4 DEF Next
+    BY <1>4 DEF Next, vars, A, B
 <1> QED
-    BY <1>2, <1>3, <1>4, PTL DEF System, Init
+    BY TypeCorrect, <1>3, <1>4, PTL DEF System, Init, Prop
 ================================================================================