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

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Tue, 21 Jan 2020 16:45:14 +0200

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.

**Follow-Ups**:**Re: [tlaplus] Reusing TypeOK theorem in TLAPS***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Questionnaire about the tech scenario TLA+ is applied** - Next by Date:
**[tlaplus] v2-tlapm installation failure** - Previous by thread:
**[tlaplus] Questionnaire about the tech scenario TLA+ is applied** - Next by thread:
**Re: [tlaplus] Reusing TypeOK theorem in TLAPS** - Index(es):