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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/61020587-764f-43bf-859f-24001b37baa4%40googlegroups.com.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.
By the way, is there any way to declare a formula including variables by "NEW <something> Invariant"?
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d3afd887-ba2f-4b58-b001-b5484a6f5da1%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d3afd887-ba2f-4b58-b001-b5484a6f5da1%40googlegroups.com.