Re: [tlaplus] Reusing TypeOK theorem in TLAPS

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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.