Towards a TLAPS stdlib by lemmy · Pull Request #127 · tlaplus/CommunityModules

lemmy · 2026-07-09T00:19:00Z

This PR is the result of Opus 4.8 analyzing a large corpus of existing TLAPS proofs to identify recurring, broadly applicable proof obligations. Those common proof patterns have been extracted into reusable lemmas and added to the CommunityModules for wider reuse.

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>

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>

Copilot

Pull request overview

This PR extends the CommunityModules “stdlib” of reusable TLAPS lemmas by adding commonly needed theorems about sequence membership (Contains), sortedness (IsSorted), and a finite-set “majority” monotonicity property, along with accompanying TLAPS proofs.

Changes:

Added a new IsSorted predicate to SequencesExt plus supporting theorems (empty/singleton/append/concat/subseq) in SequencesExtTheorems.
Added a collection of Contains lemmas (including generalized heterogeneous variants) in SequencesExtTheorems, with proofs in the corresponding _proofs module.
Added a “superset of a majority is a majority” theorem to FiniteSetsExtTheorems, with a proof in the corresponding _proofs module.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
modules/SequencesExtTheorems.tla	Adds new `Contains` and `IsSorted` theorem statements for reuse in other proofs.
modules/SequencesExtTheorems_proofs.tla	Provides TLAPS proofs for the new `Contains` and `IsSorted` theorems (currently contains proof issues called out in comments).
modules/SequencesExt.tla	Introduces the new `IsSorted` definition used by the added theorems.
modules/FiniteSetsExtTheorems.tla	Adds a majority-related theorem statement (`SupersetOfMajorityIsMajority`).
modules/FiniteSetsExtTheorems_proofs.tla	Adds the proof for `SupersetOfMajorityIsMajority` (currently missing key reasoning steps, called out in comments).

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

muenchnerkindl

Excellent initiative! I have a few comments, mainly suggestions for simpler proofs.

muenchnerkindl · 2026-07-09T07:52:16Z

+
+(*************************************************************************)
+(* Any superset (within U) of a majority of U is itself a majority.      *)
+(*************************************************************************)


Why not, but in my experience a more abstract definition of a quorum system as sets (of processes) such that any two quorums intersect and closed under superset is easier to use. Something like

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 }

One could then show that majorities constitute a quorum system, i.e.

THEOREM MajorityIsQS == ASSUME NEW S, S # {}, IsFiniteSet(S) PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) } \in QuorumSystem(S)

Your def is similar to what appears e.g. in https://github.com/microsoft/CCF/blob/main/tla/consensus/ccfraft.tla#L427-L429

muenchnerkindl · 2026-07-09T07:55:43Z

+(* Membership in a sequence coincides with membership in its image set.    *)
+THEOREM ContainsToSet ==
+  ASSUME NEW S, NEW s \in Seq(S), NEW e
+  PROVE  Contains(s, e) <=> e \in ToSet(s)


Do we prefer Range or ToSet?

muenchnerkindl · 2026-07-09T07:57:24Z

+
+THEOREM ContainsSingleton ==
+  ASSUME NEW S, NEW x \in S
+  PROVE  /\ << x >> \in Seq(S)


The first conjunct looks unnecessary to me, and it is only vaguely related to the statement of the theorem.

muenchnerkindl · 2026-07-09T07:58:20Z

+(* element type as the prefix, so these variants apply when the two sides   *)
+(* of a concatenation carry heterogeneous messages.                         *)
+(***************************************************************************)
+THEOREM ContainsAppendGen ==


This is just a reformulation of ContainsAppend. I don't understand what is meant by "generalized membership".

"element type", "heterogeneous messages" sounds like nonsense.

The theorems about "generalized" membership (including this one) were removed, and indeed these theorems became completely redundant after I removed some "type" assumptions from theorem statements. I just pushed a new version of SequencesExtTheorems.tla since I had forgotten to copy the relaxed theorem statements over from the _proofs module.

muenchnerkindl · 2026-07-09T09:42:58Z

+
+THEOREM SortedSingleton ==
+  ASSUME NEW S, NEW x \in S, NEW op(_,_)
+  PROVE  IsSorted(<< x >>, op)


BY DEF IsSorted works.

muenchnerkindl · 2026-07-09T09:43:43Z

+         NEW e \in S, s # << >> => op(s[Len(s)], e)
+  PROVE  IsSorted(Append(s, e), op)


BY DEF IsSorted works.

muenchnerkindl · 2026-07-09T09:44:22Z

+         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 DEF IsSorted works.

muenchnerkindl · 2026-07-09T09:45:16Z

+  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 works.

muenchnerkindl · 2026-07-09T09:45:58Z

+  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 works.

lemmy · 2026-07-10T00:02:53Z

@muenchnerkindl Do you want to take this PR over?

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl · 2026-07-10T18:46:52Z

@lemmy could you have a look and check?

…roofs module Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

lemmy · 2026-07-13T18:57:10Z

@lemmy could you have a look and check?

LGTM

uguryavuz · 2026-07-14T16:08:11Z

Out of curiosity, is this corpus of TLAPS proofs available?

muenchnerkindl · 2026-07-14T16:28:06Z

Just merged into the proof modules in the CommunityModules. But the title is a little pompous, it's mainly two operators for checking if an element appears in a sequence and about sorted sequences, with a few accompanying theorems.

lemmy · 2026-07-15T14:23:39Z

Out of curiosity, is this corpus of TLAPS proofs available?

You could be interested in https://github.com/specula-org/tlaps-bench

* several theorems about graphs Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * rename operators in tests for graphs Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * rename proofs module so that it will be picked up by CI Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * fix two proof steps that appear to be shaky in the CI check Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * Add tests for Graphs SimplePath, AreConnectedIn and IsStronglyConnected Check the operators exhaustively against their pure TLA+ definitions and the ConnectionsIn oracle over all graphs on up to three nodes, plus edge cases (self-loops, arguments outside the node set, composite/non-normalized node values). [Tests] Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * Add Graphs module overrides for SimplePath, AreConnectedIn and IsStronglyConnected Register three Java overrides in TLCOverrides. SimplePath enumerates simple paths via DFS instead of materializing SeqOf(node, Cardinality(node)); AreConnectedIn and IsStronglyConnected use BFS (the latter forward and on the transpose) rather than the quadratic all-pairs pure-TLA+ definitions. The overrides cut GraphsTests (exhaustive checks over all graphs on up to four nodes `\cup Graphs({1, 2, 3})`) from ~15 to ~5 minutes. TLC's code is not reused: its only Value-based graph algorithm, TransitiveClosure.Warshall, is non-reflexive, drops isolated nodes and is O(V^3), so it fits none of these operators. [TLC] Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * 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> * several theorems about graphs Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * rename operators in tests for graphs Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * rename proofs module so that it will be picked up by CI Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * fix two proof steps that appear to be shaky in the CI check Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * minor changes Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * make SCCs maximal Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * Add AbstractGraphs class to share implementation between directed and undirected graph modules Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * final cleanup Signed-off-by: Stephan Merz <stephan.merz@loria.fr> --------- Signed-off-by: Stephan Merz <stephan.merz@loria.fr> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Co-authored-by: Markus Alexander Kuppe <github.com@lemmster.de> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

lemmy and others added 2 commits July 8, 2026 16:49

lemmy requested a review from Copilot July 9, 2026 00:19

Copilot started reviewing on behalf of lemmy July 9, 2026 00:19 View session

Copilot AI reviewed Jul 9, 2026

View reviewed changes

Comment thread modules/SequencesExtTheorems_proofs.tla Outdated

Comment thread modules/SequencesExtTheorems_proofs.tla Outdated

Comment thread modules/SequencesExtTheorems_proofs.tla Outdated

Comment thread modules/FiniteSetsExtTheorems_proofs.tla

muenchnerkindl reviewed Jul 9, 2026

View reviewed changes

muenchnerkindl added 2 commits July 10, 2026 17:03

theorems about sequences, finite sets, and quorum systems

15d49d4

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

fixing two apparently brittle proofs

c5b1627

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl marked this pull request as ready for review July 10, 2026 18:46

align theorem statements in SequencesExtTheorems with those in the _p…

c27bdc9

…roofs module Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl merged commit 7b0e76c into master Jul 14, 2026
6 checks passed

lemmy deleted the mku-stdlib branch July 15, 2026 14:22

		NEW e \in S, s # << >> => op(s[Len(s)], e)
		PROVE IsSorted(Append(s, e), op)

Uh oh!

Conversation

lemmy commented Jul 9, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

muenchnerkindl left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lemmy commented Jul 10, 2026

Uh oh!

muenchnerkindl commented Jul 10, 2026

Uh oh!

lemmy commented Jul 13, 2026

Uh oh!

Uh oh!

uguryavuz commented Jul 14, 2026

Uh oh!

muenchnerkindl commented Jul 14, 2026

Uh oh!

lemmy commented Jul 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

4 participants