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

*From*: shinsa82 <shinsa82@xxxxxxxxx>*Date*: Thu, 25 Jul 2019 09:55:33 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Re: When to use TLA+.** - Next by Date:
**[tlaplus] Fingerprint Collision** - Previous by thread:
**Re: [tlaplus] Proving INV1** - Next by thread:
**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+** - Index(es):