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

[tlaplus] Meta-theorem (induction lemma) in TLA+

I want to prove a meta-theorem (or induction lemma, tactic) for a specification and reuse it in other proofs, like Coq.

I wonder if its possible or not.

Consider the following spec:


vars == <state variables>

Act1 == ...

Act2 == ...

Next == Act1 \/ Act2

Spec == Init /\ [][Next]_vars


Then we expect the following lemma hold for any non-temporal formula "Invariant", and we want to use it to prove, say, its type invariance.

(I know its too simple. Actually I want to consider more complicated cases)

I was able to prove the lemma, but I could not "apply" the lemma to the type invariant theorem.

Is there anything wrong?


LEMMA SpecInduction == 


        NEW Invariant,

        ASSUME Init PROVE Invariant,

        ASSUME Invariant, Act1 PROVE Invariant',

        ASSUME Invariant, Act2 PROVE Invariant',


        Spec => []Invariant


    <1>1. Init => Invariant OBVIOUS

    <1>2. Invariant /\ Next => Invariant' OBVIOUS

    <1>3. Invariant /\ UNCHANGED vars => Invariant' OBVIOUS

    <1> QED BY PTL, <1>1, <1>2, <1>3 DEF Spec


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/61020587-764f-43bf-859f-24001b37baa4%40googlegroups.com.