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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 5 Dec 2019 08:44:27 +0100*References*: <5d12aa41-9036-4ba4-856a-bf5070853122@googlegroups.com> <CAJSuO-_Wo9UhL3_Di9NpLO+SDLj-tuSNbLoSPObjwP_-JMKpyQ@mail.gmail.com> <CACOXEhA-Z-DrYi-rjdd6o0D+gGLe9YBZ4-TPUf+F=y175-10uQ@mail.gmail.com>

Following up on Saksham's reply: integer division is written \div in TLA+ and is supported by the prover. Proving theorems about an _expression_ CHOOSE x \in S : P(x) is more complicated because it usually requires showing that there is some element of S that satisfies P. Since you mention min and max, below is a proof by induction over finite sets that shows that any finite and non-empty set of integers has a maximum element. (Your module needs to extend the modules FiniteSetTheorems, which contains FS_Induction and other useful theorems about finite sets and TLAPS.) Assuming that you are more interested in proving theorems about an algorithm than about elementary lemmas about data, you may want to leave such lemmas unproved. Stephan
-- Max(S) == CHOOSE x \in S : \A y \in S : y <= x LEMMA MaxIntegers == ASSUME NEW S \in SUBSET Int, S # {}, IsFiniteSet(S) PROVE /\ Max(S) \in S /\ \A y \in S : y <= Max(S) <1>. DEFINE P(T) == T \in SUBSET Int /\ T # {} => \E x \in T : \A y \in T : y <= x <1>1. P({}) OBVIOUS <1>2. ASSUME NEW T, NEW x, P(T), x \notin T PROVE P(T \cup {x}) <2>. HAVE T \cup {x} \in SUBSET Int <2>1. CASE \A y \in T : y <= x BY <2>1, Isa <2>2. CASE \E y \in T : ~(y <= x) <3>. T # {} BY <2>2 <3>1. PICK y \in T : \A z \in T : z <= y BY <1>2 <3>2. x <= y BY <2>2, <3>1 <3>3. QED BY <3>1, <3>2 <2>. QED BY <2>1, <2>2 <1>. HIDE DEF P <1>3. P(S) BY <1>1, <1>2, FS_Induction, IsaM("blast") <1>. QED BY <1>3, Zenon DEF Max, P
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/351DDFCD-04E4-4D96-921C-B712F09A5288%40gmail.com. |

**References**:**[tlaplus] Using a Division Operator with TLAPS***From:*hjh2bs

**Re: [tlaplus] Using a Division Operator with TLAPS***From:*Saksham Chand

**Re: [tlaplus] Using a Division Operator with TLAPS***From:*Hans He

- Prev by Date:
**Re: [tlaplus] Using a Division Operator with TLAPS** - Next by Date:
**[tlaplus] Re: How to understand the concept "step simulation"** - Previous by thread:
**Re: [tlaplus] Using a Division Operator with TLAPS** - Next by thread:
**[tlaplus] New blog series: TLA+ for startups** - Index(es):