diff --git a/modules/FiniteSetsExtTheorems.tla b/modules/FiniteSetsExtTheorems.tla index 7c07b29..6f22eb6 100644 --- a/modules/FiniteSetsExtTheorems.tla +++ b/modules/FiniteSetsExtTheorems.tla @@ -357,5 +357,23 @@ THEOREM MinNat == PROVE /\ Min(S) \in S /\ \A y \in S : Min(S) <= y +--------------------------------------------------------------------------- + +(*************************************************************************) +(* Theorems about majorities. A "majority" of a finite set U is any *) +(* subset whose cardinality is more than half that of U. This *) +(* generalizes the notion of a quorum used in distributed-consensus *) +(* specifications, where U is the set of servers. *) +(*************************************************************************) + +(*************************************************************************) +(* Any superset (within U) of a majority of U is itself a majority. *) +(*************************************************************************) +THEOREM SupersetOfMajorityIsMajority == + ASSUME NEW U, IsFiniteSet(U), + NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2, + 2 * Cardinality(Q1) > Cardinality(U) + PROVE 2 * Cardinality(Q2) > Cardinality(U) + =========================================================================== diff --git a/modules/FiniteSetsExtTheorems_proofs.tla b/modules/FiniteSetsExtTheorems_proofs.tla index 511d9c5..29a3b28 100644 --- a/modules/FiniteSetsExtTheorems_proofs.tla +++ b/modules/FiniteSetsExtTheorems_proofs.tla @@ -621,4 +621,20 @@ THEOREM MinNat == /\ \A y \in S : Min(S) <= y BY MinIntBounded, \A y \in S : 0 <= y +--------------------------------------------------------------------------- + +(*************************************************************************) +(* Any superset (within U) of a majority of U is itself a majority. *) +(*************************************************************************) +THEOREM SupersetOfMajorityIsMajority == + ASSUME NEW U, IsFiniteSet(U), + NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2, + 2 * Cardinality(Q1) > Cardinality(U) + PROVE 2 * Cardinality(Q2) > Cardinality(U) +<1>1. IsFiniteSet(Q2) /\ Cardinality(Q2) <= Cardinality(U) BY FS_Subset +<1>2. IsFiniteSet(Q1) /\ Cardinality(Q1) <= Cardinality(Q2) BY <1>1, FS_Subset +<1>3. Cardinality(Q1) \in Nat /\ Cardinality(Q2) \in Nat /\ Cardinality(U) \in Nat + BY FS_CardinalityType, <1>1, <1>2 +<1>. QED BY <1>2, <1>3 + ================================================================================ diff --git a/modules/Quorum.tla b/modules/Quorum.tla new file mode 100644 index 0000000..584f369 --- /dev/null +++ b/modules/Quorum.tla @@ -0,0 +1,19 @@ +--------------------------------- MODULE Quorum ----------------------------- + +(***************************************************************************) +(* A quorum system for a set S is a non-empty collection of quorums, i.e. *) +(* subsets of S such that any two quorums intersect. It is typically also *) +(* assumed that a superset of a quorum is itself a quorum. *) +(* *) +(* For example, given a finite and non-empty set S of servers, the sets of *) +(* strict majorities among servers form a quorum system. *) +(***************************************************************************) + +QuorumSystem(S) == + { QS \in SUBSET (SUBSET S) : + /\ QS # {} + /\ \A Q1, Q2 \in QS : Q1 \cap Q2 # {} + /\ \A Q1, Q2 \in SUBSET S : Q1 \in QS /\ Q1 \subseteq Q2 => Q2 \in QS + } + +============================================================================= diff --git a/modules/QuorumTheorems.tla b/modules/QuorumTheorems.tla new file mode 100644 index 0000000..b36acb1 --- /dev/null +++ b/modules/QuorumTheorems.tla @@ -0,0 +1,26 @@ +----------------------------- MODULE QuorumTheorems ------------------------- +EXTENDS Quorum, Integers, FiniteSets + +(***************************************************************************) +(* Direct consequences of the definition of a quorum system. *) +(***************************************************************************) + +THEOREM QuorumsIntersect == + ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS + PROVE \E s \in S : s \in Q1 \cap Q2 + +THEOREM QuorumSuperset == + ASSUME NEW S, NEW QS \in QuorumSystem(S), + NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2 + PROVE Q2 \in QS + +(***************************************************************************) +(* Strict majorities of a non-empty set S form a quorum system. *) +(***************************************************************************) + +THEOREM MajoritiesQuorumSystem == + ASSUME NEW S, IsFiniteSet(S), S # {} + PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) } + \in QuorumSystem(S) + +============================================================================= diff --git a/modules/QuorumTheorems_proofs.tla b/modules/QuorumTheorems_proofs.tla new file mode 100644 index 0000000..d2d27e4 --- /dev/null +++ b/modules/QuorumTheorems_proofs.tla @@ -0,0 +1,29 @@ +------------------------- MODULE QuorumTheorems_proofs ---------------------- +EXTENDS Quorum, Integers, FiniteSetTheorems, FiniteSetsExtTheorems + +(***************************************************************************) +(* Direct consequences of the definition of a quorum system. *) +(***************************************************************************) + +THEOREM QuorumsIntersect == + ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS + PROVE \E s \in S : s \in Q1 \cap Q2 +BY DEF QuorumSystem + +THEOREM QuorumSuperset == + ASSUME NEW S, NEW QS \in QuorumSystem(S), + NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2 + PROVE Q2 \in QS +BY DEF QuorumSystem + +(***************************************************************************) +(* Strict majorities of a non-empty set S form a quorum system. *) +(***************************************************************************) + +THEOREM MajoritiesQuorumSystem == + ASSUME NEW S, IsFiniteSet(S), S # {} + PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) } + \in QuorumSystem(S) +BY FS_CardinalityType, FS_EmptySet, FS_Subset, FS_Union DEF QuorumSystem + +============================================================================= diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index bb4a14d..28679e7 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -106,6 +106,31 @@ BoundedSeq(S, n) == Contains(s, e) == \E i \in 1..Len(s) : s[i] = e +(**************************************************************************) +(* TRUE iff the sequence s is sorted with respect to the binary *) +(* relation op, i.e. op(s[i], s[j]) holds for every pair of positions *) +(* i, j in the domain of s with i < j. *) +(* *) +(* No assumptions are made about op; its meaning is fixed by the *) +(* caller. When op is a strict order (irreflexive and transitive), *) +(* s is strictly increasing and therefore duplicate-free; when op is *) +(* a reflexive relation such as <=, equal elements may be adjacent. *) +(* Instantiating op with the converse relation sorts s in the *) +(* opposite direction. The empty sequence and every singleton are *) +(* vacuously sorted under any op. *) +(* *) +(* Examples: *) +(* IsSorted(<<>>, <) = TRUE *) +(* IsSorted(<<5>>, <) = TRUE *) +(* IsSorted(<<1, 2, 3>>, <) = TRUE *) +(* IsSorted(<<1, 2, 2>>, <) = FALSE (not strictly increasing) *) +(* IsSorted(<<1, 2, 2>>, <=) = TRUE *) +(* IsSorted(<<3, 2, 1>>, <) = FALSE *) +(* IsSorted(<<3, 2, 1>>, >) = TRUE *) +(**************************************************************************) +IsSorted(s, op(_, _)) == + \A i, j \in 1..Len(s) : i < j => op(s[i], s[j]) + (**************************************************************************) (* Reverse the given sequence s: Let l be Len(s) (length of s). *) (* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>> *) diff --git a/modules/SequencesExtTheorems.tla b/modules/SequencesExtTheorems.tla index a04ddbd..9462873 100644 --- a/modules/SequencesExtTheorems.tla +++ b/modules/SequencesExtTheorems.tla @@ -47,6 +47,97 @@ THEOREM SequencesInductionCons == \A s \in Seq(S), e \in S : P(s) => P(Cons(e,s)) PROVE \A seq \in Seq(S) : P(seq) +(***************************************************************************) +(* Theorems about Contains. *) +(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *) +(***************************************************************************) + +(* Membership in a sequence coincides with membership in its image set. *) +THEOREM ContainsRange == + ASSUME NEW S, NEW s \in Seq(S), NEW e + PROVE Contains(s, e) <=> e \in Range(s) + +THEOREM ContainsEmpty == + ASSUME NEW e + PROVE ~ Contains(<< >>, e) + +THEOREM ContainsAppend == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x) + +THEOREM ContainsSingleton == + ASSUME NEW S, NEW x + PROVE \A e : Contains(<< x >>, e) <=> e = x + +THEOREM ContainsConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e + PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e)) + +THEOREM ContainsCons == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e)) + +THEOREM ContainsTail == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e + PROVE Contains(Tail(s), e) => Contains(s, e) + +(* An element other than the head of a non-empty sequence that occurs in *) +(* the sequence also occurs in its tail. *) +THEOREM ContainsTailExceptHead == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e, + Contains(s, e), e # Head(s) + PROVE Contains(Tail(s), e) + +(***************************************************************************) +(* Theorems about IsSorted (see SequencesExt). *) +(* *) +(* The relevant order properties of op (transitivity, irreflexivity) *) +(* are stated locally as hypotheses of each theorem, so that the *) +(* theorems apply to an arbitrary binary relation op rather than only *) +(* to relations globally known to be orders. *) +(***************************************************************************) + +THEOREM SortedEmpty == + ASSUME NEW op(_,_) + PROVE IsSorted(<< >>, op) + +THEOREM SortedSingleton == + ASSUME NEW S, NEW x \in S, NEW op(_,_) + PROVE IsSorted(<< x >>, op) + +(* Appending an element that dominates the last one keeps the sequence *) +(* sorted, provided the ordering relation is transitive. *) +THEOREM SortedAppend == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), IsSorted(s, op), + NEW e \in S, s # << >> => op(s[Len(s)], e) + PROVE IsSorted(Append(s, e), op) + +(* Concatenating two sorted sequences whose boundary elements are ordered *) +(* yields a sorted sequence (for a transitive ordering relation). *) +THEOREM SortedConcat == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), NEW t \in Seq(S), + IsSorted(s, op), IsSorted(t, op), + (Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1]) + PROVE IsSorted(s \o t, op) + +(* A sequence sorted by an irreflexive relation has no repeated elements. *) +THEOREM SortedInjective == + ASSUME NEW S, NEW op(_,_), + \A x \in S : ~ op(x, x), + NEW s \in Seq(S), IsSorted(s, op) + PROVE IsInjective(s) + +(* Any contiguous subsequence of a sorted sequence is sorted. *) +THEOREM SortedSubSeq == + ASSUME NEW S, NEW op(_,_), + NEW s \in Seq(S), IsSorted(s, op), + NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s) + PROVE IsSorted(SubSeq(s, m, n), op) + (***************************************************************************) (* Theorems about InsertAt and RemoveAt. *) (* InsertAt(seq,i,elt) == *) diff --git a/modules/SequencesExtTheorems_proofs.tla b/modules/SequencesExtTheorems_proofs.tla index 3c4700c..5db8707 100644 --- a/modules/SequencesExtTheorems_proofs.tla +++ b/modules/SequencesExtTheorems_proofs.tla @@ -79,6 +79,108 @@ THEOREM SequencesInductionCons == <2>. QED BY <2>1 <1>. QED BY <1>2, <1>3, NatInduction, Isa +(***************************************************************************) +(* Theorems about Contains. *) +(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *) +(***************************************************************************) + +THEOREM ContainsRange == + ASSUME NEW S, NEW s \in Seq(S), NEW e + PROVE Contains(s, e) <=> e \in Range(s) +BY DEF Contains, Range + +THEOREM ContainsEmpty == + ASSUME NEW e + PROVE ~ Contains(<< >>, e) +BY DEF Contains + +THEOREM ContainsAppend == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x) +BY DEF Contains + +THEOREM ContainsSingleton == + ASSUME NEW x + PROVE \A e : Contains(<< x >>, e) <=> e = x +BY Isa DEF Contains + +THEOREM ContainsConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e + PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e)) +<1>1. ASSUME Contains(s \o t, e), ~ Contains(t, e) PROVE Contains(s, e) + BY <1>1 DEF Contains +<1>2. ASSUME Contains(s, e) PROVE Contains(s \o t, e) + <2>. PICK i \in 1 .. Len(s) : s[i] = e + BY <1>2 DEF Contains + <2>. QED BY i \in 1 .. Len(s \o t) DEF Contains +<1>3. ASSUME Contains(t, e) PROVE Contains(s \o t, e) + <2>. PICK i \in 1 .. Len(t) : t[i] = e + BY <1>3 DEF Contains + <2>. QED BY Len(s)+i \in 1 .. Len(s \o t) DEF Contains +<1>. QED BY <1>1, <1>2, <1>3 + +THEOREM ContainsCons == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e)) +BY ContainsConcat, ContainsSingleton, <> \in Seq({x}) DEF Cons + +THEOREM ContainsTail == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e + PROVE Contains(Tail(s), e) => Contains(s, e) +BY DEF Contains + +THEOREM ContainsTailExceptHead == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e, + Contains(s, e), e # Head(s) + PROVE Contains(Tail(s), e) +BY DEF Contains + +(***************************************************************************) +(* Theorems about IsSorted. *) +(* IsSorted(s, op) == \A i,j \in 1..Len(s) : i op(s[i],s[j]) *) +(***************************************************************************) + +THEOREM SortedEmpty == + ASSUME NEW op(_,_) + PROVE IsSorted(<< >>, op) +BY DEF IsSorted + +THEOREM SortedSingleton == + ASSUME NEW S, NEW x \in S, NEW op(_,_) + PROVE IsSorted(<< x >>, op) +BY DEF IsSorted + +THEOREM SortedAppend == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), IsSorted(s, op), + NEW e \in S, s # << >> => op(s[Len(s)], e) + PROVE IsSorted(Append(s, e), op) +BY DEF IsSorted + +THEOREM SortedConcat == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), NEW t \in Seq(S), + IsSorted(s, op), IsSorted(t, op), + (Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1]) + PROVE IsSorted(s \o t, op) +BY SMTT(20) DEF IsSorted + +THEOREM SortedInjective == + ASSUME NEW S, NEW op(_,_), + \A x \in S : ~ op(x, x), + NEW s \in Seq(S), IsSorted(s, op) + PROVE IsInjective(s) +BY DEF IsSorted, IsInjective + +THEOREM SortedSubSeq == + ASSUME NEW S, NEW op(_,_), + NEW s \in Seq(S), IsSorted(s, op), + NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s) + PROVE IsSorted(SubSeq(s, m, n), op) +BY DEF IsSorted + (***************************************************************************) (* Theorems about InsertAt and RemoveAt. *) (* InsertAt(seq,i,elt) == *)