[tlaplus] Reusing TypeOK theorem in TLAPS

[Karolis Petrauskas <k.petrauskas@xxxxxxxxx>]

Hello,

I'm trying to reuse the "Spec => []TypeOK" theorem in other theorems
regarding inductive invariants, and have stuck.
Bellow is a small example to reproduce my problem.

------------------------------ MODULE TestPTL ------------------------------
EXTENDS Naturals, TLAPS
VARIABLES x
Init == x = 0
Next == x' = x + 1
Spec == Init /\ [][Next]_x
--------------------------------
TypeOK == x \in Nat
THEOREM SpecTypeOK == Spec => []TypeOK
  <1>1. Init => TypeOK BY DEF Init, TypeOK
  <1>2. TypeOK /\ [Next]_x => TypeOK' BY DEF TypeOK, Next
  <1>q. QED BY <1>1, <1>2, PTL DEF Spec
--------------------------------
IInv == x >= 0
THEOREM SpecIInvA == TypeOK /\ Spec => []IInv
  <1> SUFFICES ASSUME TypeOK PROVE Spec => []IInv OBVIOUS
  <1>1. Init => IInv BY DEF Init, IInv
  <1>2. IInv /\ [Next]_x => IInv' BY DEF IInv, Next, TypeOK
  <1>q. QED BY <1>1, <1>2, PTL DEF Spec

THEOREM SpecIInvB == Spec => []IInv
  <1>a. SUFFICES ASSUME Spec PROVE Spec => []IInv OBVIOUS
  <1>b. TypeOK BY <1>a, SpecTypeOK, PTL
  <1>1. Init => IInv BY DEF Init, IInv
  <1>2. IInv /\ [Next]_x => IInv' BY <1>b DEF IInv, Next, TypeOK
  <1>q. QED BY <1>1, <1>2, PTL DEF Spec
=============================================================================

Theorems SpecTypeOK and SpecIInvA are proved successfully, and that's OK.
In SpecIInvA I want to avoid having TypeOK as an assumption, therefore the
theorem SpecIInvB is formulated identically, just omitting the TypeOK
before the implication.
TypeOK is needed in <1>2, therefore I proved it in <1>b using SpecTypeOK.
The problem here is that in this case the last step (<1>q) is not
proved anymore, and I don't understand why.
It looks the same, as in SpecIInvA.
The state at this step is:

ASSUME NEW VARIABLE x,
       Init => IInv (* non-[] *),
       IInv /\ [Next]_x => IInv' (* non-[] *)
PROVE  Init /\ [][Next]_x => []IInv

Thanks in advance,
Karolis Petrauskas

-- 
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/CAFteovJFJPvHyQObPEMHAgeLqydEbAdbVzqGvXBqbrgYcDAOFA%40mail.gmail.com.