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

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Wed, 22 Jan 2020 15:03:52 +0200*References*: <CAFteovJFJPvHyQObPEMHAgeLqydEbAdbVzqGvXBqbrgYcDAOFA@mail.gmail.com> <15408610-7AF0-4638-9A96-24B1549D7534@gmail.com>

Thanks! Karolis On Wed, Jan 22, 2020 at 2:43 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote: > > Hello, > > in short, in order to use a temporal-level theorem inside the proof of another one, your proof should be written as follows: > > THEOREM ThmA == Spec => []A > > THEOREM ThmB == Spec => []B > <1>1. Init (* /\ A *) => B > <1>2. B /\ [Next]_vars (* /\ A /\ A' *) => B' > <1>. QED BY <1>1, <1>2, ThmA, PTL DEF Spec > > The commented parts indicate where you may make use of the invariant proved in ThmA. > > As a rule of thumb, do not decompose temporal-level implications into ASSUME ... PROVE steps, but make sure that all hypotheses used for proving a fact that will be passed to the PTL proof method are constant level or [] formulas. The reason is that PTL will try to apply the necessitation rule F |- []F to promote any fact to a boxed formula, but it can do so only if there are no state- or action-level hypotheses in the context where that fact was established. For example, the steps <1>1 and <1>2 of your proof of SpecIInvB are established in the context of the assumption Spec, which is not a [] formula (due to the initial condition), and that's indicated by the "non-[]" warnings that you see in the proof obligation. As a result, the preservation of the invariant (step <1>2) cannot be "boxed" as it would need to be in order to apply temporal induction. > > Regards, > Stephan > > > > On 21 Jan 2020, at 15:45, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote: > > > > 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. > > -- > 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/15408610-7AF0-4638-9A96-24B1549D7534%40gmail.com. -- 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/CAFteovLR5zUwh-BTEf2Nw%3DAJOMUgVu7_Ti0PP1z%3DhVNGxJb3hQ%40mail.gmail.com.

**References**:**[tlaplus] Reusing TypeOK theorem in TLAPS***From:*Karolis Petrauskas

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

- Prev by Date:
**Re: [tlaplus] Reusing TypeOK theorem in TLAPS** - Next by Date:
**[tlaplus] ClassCastException: LetInNode cannot be cast to class OpApplNode** - Previous by thread:
**Re: [tlaplus] Reusing TypeOK theorem in TLAPS** - Next by thread:
**[tlaplus] v2-tlapm installation failure** - Index(es):