Skip to content

Commit 7b0e76c

Browse files
lemmyclaudemuenchnerkindl
authored
Towards a TLAPS stdlib (#127)
* Theorems about Contains and majority supersets Add and prove membership theorems for SequencesExt!Contains (empty/Append/Cons/Concat/Tail/singleton plus heterogeneous-type Append/Concat variants) and SupersetOfMajorityIsMajority for FiniteSetsExt. All obligations checked with TLAPS. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * IsSorted operator and sortedness theorems Add SequencesExt!IsSorted(s, op(_,_)), which holds iff s is sorted with respect to an arbitrary binary relation op, with a formal doc comment and examples. Add and prove the accompanying theorems SortedEmpty, SortedSingleton, SortedAppend, SortedConcat, SortedInjective and SortedSubSeq, whose order hypotheses on op (transitivity, irreflexivity) are stated locally so they apply to any relation. All obligations checked with TLAPS. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * theorems about sequences, finite sets, and quorum systems Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * fixing two apparently brittle proofs Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * align theorem statements in SequencesExtTheorems with those in the _proofs module Signed-off-by: Stephan Merz <stephan.merz@loria.fr> --------- Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Signed-off-by: Stephan Merz <stephan.merz@loria.fr> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Co-authored-by: Stephan Merz <stephan.merz@loria.fr>
1 parent dac9808 commit 7b0e76c

8 files changed

Lines changed: 326 additions & 0 deletions

‎modules/FiniteSetsExtTheorems.tla‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -357,5 +357,23 @@ THEOREM MinNat ==
357357
PROVE /\ Min(S) \in S
358358
/\ \A y \in S : Min(S) <= y
359359

360+
---------------------------------------------------------------------------
361+
362+
(*************************************************************************)
363+
(* Theorems about majorities. A "majority" of a finite set U is any *)
364+
(* subset whose cardinality is more than half that of U. This *)
365+
(* generalizes the notion of a quorum used in distributed-consensus *)
366+
(* specifications, where U is the set of servers. *)
367+
(*************************************************************************)
368+
369+
(*************************************************************************)
370+
(* Any superset (within U) of a majority of U is itself a majority. *)
371+
(*************************************************************************)
372+
THEOREM SupersetOfMajorityIsMajority ==
373+
ASSUME NEW U, IsFiniteSet(U),
374+
NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2,
375+
2 * Cardinality(Q1) > Cardinality(U)
376+
PROVE 2 * Cardinality(Q2) > Cardinality(U)
377+
360378

361379
===========================================================================

‎modules/FiniteSetsExtTheorems_proofs.tla‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -621,4 +621,20 @@ THEOREM MinNat ==
621621
/\ \A y \in S : Min(S) <= y
622622
BY MinIntBounded, \A y \in S : 0 <= y
623623

624+
---------------------------------------------------------------------------
625+
626+
(*************************************************************************)
627+
(* Any superset (within U) of a majority of U is itself a majority. *)
628+
(*************************************************************************)
629+
THEOREM SupersetOfMajorityIsMajority ==
630+
ASSUME NEW U, IsFiniteSet(U),
631+
NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2,
632+
2 * Cardinality(Q1) > Cardinality(U)
633+
PROVE 2 * Cardinality(Q2) > Cardinality(U)
634+
<1>1. IsFiniteSet(Q2) /\ Cardinality(Q2) <= Cardinality(U) BY FS_Subset
635+
<1>2. IsFiniteSet(Q1) /\ Cardinality(Q1) <= Cardinality(Q2) BY <1>1, FS_Subset
636+
<1>3. Cardinality(Q1) \in Nat /\ Cardinality(Q2) \in Nat /\ Cardinality(U) \in Nat
637+
BY FS_CardinalityType, <1>1, <1>2
638+
<1>. QED BY <1>2, <1>3
639+
624640
================================================================================

‎modules/Quorum.tla‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
--------------------------------- MODULE Quorum -----------------------------
2+
3+
(***************************************************************************)
4+
(* A quorum system for a set S is a non-empty collection of quorums, i.e. *)
5+
(* subsets of S such that any two quorums intersect. It is typically also *)
6+
(* assumed that a superset of a quorum is itself a quorum. *)
7+
(* *)
8+
(* For example, given a finite and non-empty set S of servers, the sets of *)
9+
(* strict majorities among servers form a quorum system. *)
10+
(***************************************************************************)
11+
12+
QuorumSystem(S) ==
13+
{ QS \in SUBSET (SUBSET S) :
14+
/\ QS # {}
15+
/\ \A Q1, Q2 \in QS : Q1 \cap Q2 # {}
16+
/\ \A Q1, Q2 \in SUBSET S : Q1 \in QS /\ Q1 \subseteq Q2 => Q2 \in QS
17+
}
18+
19+
=============================================================================

‎modules/QuorumTheorems.tla‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
----------------------------- MODULE QuorumTheorems -------------------------
2+
EXTENDS Quorum, Integers, FiniteSets
3+
4+
(***************************************************************************)
5+
(* Direct consequences of the definition of a quorum system. *)
6+
(***************************************************************************)
7+
8+
THEOREM QuorumsIntersect ==
9+
ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS
10+
PROVE \E s \in S : s \in Q1 \cap Q2
11+
12+
THEOREM QuorumSuperset ==
13+
ASSUME NEW S, NEW QS \in QuorumSystem(S),
14+
NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2
15+
PROVE Q2 \in QS
16+
17+
(***************************************************************************)
18+
(* Strict majorities of a non-empty set S form a quorum system. *)
19+
(***************************************************************************)
20+
21+
THEOREM MajoritiesQuorumSystem ==
22+
ASSUME NEW S, IsFiniteSet(S), S # {}
23+
PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) }
24+
\in QuorumSystem(S)
25+
26+
=============================================================================

‎modules/QuorumTheorems_proofs.tla‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
------------------------- MODULE QuorumTheorems_proofs ----------------------
2+
EXTENDS Quorum, Integers, FiniteSetTheorems, FiniteSetsExtTheorems
3+
4+
(***************************************************************************)
5+
(* Direct consequences of the definition of a quorum system. *)
6+
(***************************************************************************)
7+
8+
THEOREM QuorumsIntersect ==
9+
ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS
10+
PROVE \E s \in S : s \in Q1 \cap Q2
11+
BY DEF QuorumSystem
12+
13+
THEOREM QuorumSuperset ==
14+
ASSUME NEW S, NEW QS \in QuorumSystem(S),
15+
NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2
16+
PROVE Q2 \in QS
17+
BY DEF QuorumSystem
18+
19+
(***************************************************************************)
20+
(* Strict majorities of a non-empty set S form a quorum system. *)
21+
(***************************************************************************)
22+
23+
THEOREM MajoritiesQuorumSystem ==
24+
ASSUME NEW S, IsFiniteSet(S), S # {}
25+
PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) }
26+
\in QuorumSystem(S)
27+
BY FS_CardinalityType, FS_EmptySet, FS_Subset, FS_Union DEF QuorumSystem
28+
29+
=============================================================================

‎modules/SequencesExt.tla‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,31 @@ BoundedSeq(S, n) ==
106106
Contains(s, e) ==
107107
\E i \in 1..Len(s) : s[i] = e
108108

109+
(**************************************************************************)
110+
(* TRUE iff the sequence s is sorted with respect to the binary *)
111+
(* relation op, i.e. op(s[i], s[j]) holds for every pair of positions *)
112+
(* i, j in the domain of s with i < j. *)
113+
(* *)
114+
(* No assumptions are made about op; its meaning is fixed by the *)
115+
(* caller. When op is a strict order (irreflexive and transitive), *)
116+
(* s is strictly increasing and therefore duplicate-free; when op is *)
117+
(* a reflexive relation such as <=, equal elements may be adjacent. *)
118+
(* Instantiating op with the converse relation sorts s in the *)
119+
(* opposite direction. The empty sequence and every singleton are *)
120+
(* vacuously sorted under any op. *)
121+
(* *)
122+
(* Examples: *)
123+
(* IsSorted(<<>>, <) = TRUE *)
124+
(* IsSorted(<<5>>, <) = TRUE *)
125+
(* IsSorted(<<1, 2, 3>>, <) = TRUE *)
126+
(* IsSorted(<<1, 2, 2>>, <) = FALSE (not strictly increasing) *)
127+
(* IsSorted(<<1, 2, 2>>, <=) = TRUE *)
128+
(* IsSorted(<<3, 2, 1>>, <) = FALSE *)
129+
(* IsSorted(<<3, 2, 1>>, >) = TRUE *)
130+
(**************************************************************************)
131+
IsSorted(s, op(_, _)) ==
132+
\A i, j \in 1..Len(s) : i < j => op(s[i], s[j])
133+
109134
(**************************************************************************)
110135
(* Reverse the given sequence s: Let l be Len(s) (length of s). *)
111136
(* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>> *)

‎modules/SequencesExtTheorems.tla‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,97 @@ THEOREM SequencesInductionCons ==
4747
\A s \in Seq(S), e \in S : P(s) => P(Cons(e,s))
4848
PROVE \A seq \in Seq(S) : P(seq)
4949

50+
(***************************************************************************)
51+
(* Theorems about Contains. *)
52+
(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *)
53+
(***************************************************************************)
54+
55+
(* Membership in a sequence coincides with membership in its image set. *)
56+
THEOREM ContainsRange ==
57+
ASSUME NEW S, NEW s \in Seq(S), NEW e
58+
PROVE Contains(s, e) <=> e \in Range(s)
59+
60+
THEOREM ContainsEmpty ==
61+
ASSUME NEW e
62+
PROVE ~ Contains(<< >>, e)
63+
64+
THEOREM ContainsAppend ==
65+
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
66+
PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x)
67+
68+
THEOREM ContainsSingleton ==
69+
ASSUME NEW S, NEW x
70+
PROVE \A e : Contains(<< x >>, e) <=> e = x
71+
72+
THEOREM ContainsConcat ==
73+
ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e
74+
PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e))
75+
76+
THEOREM ContainsCons ==
77+
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
78+
PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e))
79+
80+
THEOREM ContainsTail ==
81+
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e
82+
PROVE Contains(Tail(s), e) => Contains(s, e)
83+
84+
(* An element other than the head of a non-empty sequence that occurs in *)
85+
(* the sequence also occurs in its tail. *)
86+
THEOREM ContainsTailExceptHead ==
87+
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e,
88+
Contains(s, e), e # Head(s)
89+
PROVE Contains(Tail(s), e)
90+
91+
(***************************************************************************)
92+
(* Theorems about IsSorted (see SequencesExt). *)
93+
(* *)
94+
(* The relevant order properties of op (transitivity, irreflexivity) *)
95+
(* are stated locally as hypotheses of each theorem, so that the *)
96+
(* theorems apply to an arbitrary binary relation op rather than only *)
97+
(* to relations globally known to be orders. *)
98+
(***************************************************************************)
99+
100+
THEOREM SortedEmpty ==
101+
ASSUME NEW op(_,_)
102+
PROVE IsSorted(<< >>, op)
103+
104+
THEOREM SortedSingleton ==
105+
ASSUME NEW S, NEW x \in S, NEW op(_,_)
106+
PROVE IsSorted(<< x >>, op)
107+
108+
(* Appending an element that dominates the last one keeps the sequence *)
109+
(* sorted, provided the ordering relation is transitive. *)
110+
THEOREM SortedAppend ==
111+
ASSUME NEW S, NEW op(_,_),
112+
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),
113+
NEW s \in Seq(S), IsSorted(s, op),
114+
NEW e \in S, s # << >> => op(s[Len(s)], e)
115+
PROVE IsSorted(Append(s, e), op)
116+
117+
(* Concatenating two sorted sequences whose boundary elements are ordered *)
118+
(* yields a sorted sequence (for a transitive ordering relation). *)
119+
THEOREM SortedConcat ==
120+
ASSUME NEW S, NEW op(_,_),
121+
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),
122+
NEW s \in Seq(S), NEW t \in Seq(S),
123+
IsSorted(s, op), IsSorted(t, op),
124+
(Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1])
125+
PROVE IsSorted(s \o t, op)
126+
127+
(* A sequence sorted by an irreflexive relation has no repeated elements. *)
128+
THEOREM SortedInjective ==
129+
ASSUME NEW S, NEW op(_,_),
130+
\A x \in S : ~ op(x, x),
131+
NEW s \in Seq(S), IsSorted(s, op)
132+
PROVE IsInjective(s)
133+
134+
(* Any contiguous subsequence of a sorted sequence is sorted. *)
135+
THEOREM SortedSubSeq ==
136+
ASSUME NEW S, NEW op(_,_),
137+
NEW s \in Seq(S), IsSorted(s, op),
138+
NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s)
139+
PROVE IsSorted(SubSeq(s, m, n), op)
140+
50141
(***************************************************************************)
51142
(* Theorems about InsertAt and RemoveAt. *)
52143
(* InsertAt(seq,i,elt) == *)

‎modules/SequencesExtTheorems_proofs.tla‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,108 @@ THEOREM SequencesInductionCons ==
7979
<2>. QED BY <2>1
8080
<1>. QED BY <1>2, <1>3, NatInduction, Isa
8181

82+
(***************************************************************************)
83+
(* Theorems about Contains. *)
84+
(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *)
85+
(***************************************************************************)
86+
87+
THEOREM ContainsRange ==
88+
ASSUME NEW S, NEW s \in Seq(S), NEW e
89+
PROVE Contains(s, e) <=> e \in Range(s)
90+
BY DEF Contains, Range
91+
92+
THEOREM ContainsEmpty ==
93+
ASSUME NEW e
94+
PROVE ~ Contains(<< >>, e)
95+
BY DEF Contains
96+
97+
THEOREM ContainsAppend ==
98+
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
99+
PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x)
100+
BY DEF Contains
101+
102+
THEOREM ContainsSingleton ==
103+
ASSUME NEW x
104+
PROVE \A e : Contains(<< x >>, e) <=> e = x
105+
BY Isa DEF Contains
106+
107+
THEOREM ContainsConcat ==
108+
ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e
109+
PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e))
110+
<1>1. ASSUME Contains(s \o t, e), ~ Contains(t, e) PROVE Contains(s, e)
111+
BY <1>1 DEF Contains
112+
<1>2. ASSUME Contains(s, e) PROVE Contains(s \o t, e)
113+
<2>. PICK i \in 1 .. Len(s) : s[i] = e
114+
BY <1>2 DEF Contains
115+
<2>. QED BY i \in 1 .. Len(s \o t) DEF Contains
116+
<1>3. ASSUME Contains(t, e) PROVE Contains(s \o t, e)
117+
<2>. PICK i \in 1 .. Len(t) : t[i] = e
118+
BY <1>3 DEF Contains
119+
<2>. QED BY Len(s)+i \in 1 .. Len(s \o t) DEF Contains
120+
<1>. QED BY <1>1, <1>2, <1>3
121+
122+
THEOREM ContainsCons ==
123+
ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e
124+
PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e))
125+
BY ContainsConcat, ContainsSingleton, <<x>> \in Seq({x}) DEF Cons
126+
127+
THEOREM ContainsTail ==
128+
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e
129+
PROVE Contains(Tail(s), e) => Contains(s, e)
130+
BY DEF Contains
131+
132+
THEOREM ContainsTailExceptHead ==
133+
ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e,
134+
Contains(s, e), e # Head(s)
135+
PROVE Contains(Tail(s), e)
136+
BY DEF Contains
137+
138+
(***************************************************************************)
139+
(* Theorems about IsSorted. *)
140+
(* IsSorted(s, op) == \A i,j \in 1..Len(s) : i<j => op(s[i],s[j]) *)
141+
(***************************************************************************)
142+
143+
THEOREM SortedEmpty ==
144+
ASSUME NEW op(_,_)
145+
PROVE IsSorted(<< >>, op)
146+
BY DEF IsSorted
147+
148+
THEOREM SortedSingleton ==
149+
ASSUME NEW S, NEW x \in S, NEW op(_,_)
150+
PROVE IsSorted(<< x >>, op)
151+
BY DEF IsSorted
152+
153+
THEOREM SortedAppend ==
154+
ASSUME NEW S, NEW op(_,_),
155+
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),
156+
NEW s \in Seq(S), IsSorted(s, op),
157+
NEW e \in S, s # << >> => op(s[Len(s)], e)
158+
PROVE IsSorted(Append(s, e), op)
159+
BY DEF IsSorted
160+
161+
THEOREM SortedConcat ==
162+
ASSUME NEW S, NEW op(_,_),
163+
\A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z),
164+
NEW s \in Seq(S), NEW t \in Seq(S),
165+
IsSorted(s, op), IsSorted(t, op),
166+
(Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1])
167+
PROVE IsSorted(s \o t, op)
168+
BY SMTT(20) DEF IsSorted
169+
170+
THEOREM SortedInjective ==
171+
ASSUME NEW S, NEW op(_,_),
172+
\A x \in S : ~ op(x, x),
173+
NEW s \in Seq(S), IsSorted(s, op)
174+
PROVE IsInjective(s)
175+
BY DEF IsSorted, IsInjective
176+
177+
THEOREM SortedSubSeq ==
178+
ASSUME NEW S, NEW op(_,_),
179+
NEW s \in Seq(S), IsSorted(s, op),
180+
NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s)
181+
PROVE IsSorted(SubSeq(s, m, n), op)
182+
BY DEF IsSorted
183+
82184
(***************************************************************************)
83185
(* Theorems about InsertAt and RemoveAt. *)
84186
(* InsertAt(seq,i,elt) == *)

0 commit comments

Comments
 (0)