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