[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 == 

    ASSUME

        NEW Invariant,

        ASSUME Init PROVE Invariant,

        ASSUME Invariant, Act1 PROVE Invariant',

        ASSUME Invariant, Act2 PROVE Invariant',

    PROVE

        Spec => []Invariant

PROOF

    <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.