Towards a TLAPS stdlib#127
Conversation
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>
There was a problem hiding this comment.
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
IsSortedpredicate toSequencesExtplus supporting theorems (empty/singleton/append/concat/subseq) inSequencesExtTheorems. - Added a collection of
Containslemmas (including generalized heterogeneous variants) inSequencesExtTheorems, with proofs in the corresponding_proofsmodule. - Added a “superset of a majority is a majority” theorem to
FiniteSetsExtTheorems, with a proof in the corresponding_proofsmodule.
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
left a comment
muenchnerkindl
left a comment
There was a problem hiding this comment.
Excellent initiative! I have a few comments, mainly suggestions for simpler proofs.
|
|
||
| (*************************************************************************) | ||
| (* Any superset (within U) of a majority of U is itself a majority. *) | ||
| (*************************************************************************) |
There was a problem hiding this comment.
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)
There was a problem hiding this comment.
Your def is similar to what appears e.g. in https://github.com/microsoft/CCF/blob/main/tla/consensus/ccfraft.tla#L427-L429
| (* 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) |
There was a problem hiding this comment.
Do we prefer Range or ToSet?
|
|
||
| THEOREM ContainsSingleton == | ||
| ASSUME NEW S, NEW x \in S | ||
| PROVE /\ << x >> \in Seq(S) |
There was a problem hiding this comment.
The first conjunct looks unnecessary to me, and it is only vaguely related to the statement of the theorem.
| (* element type as the prefix, so these variants apply when the two sides *) | ||
| (* of a concatenation carry heterogeneous messages. *) | ||
| (***************************************************************************) | ||
| THEOREM ContainsAppendGen == |
There was a problem hiding this comment.
This is just a reformulation of ContainsAppend. I don't understand what is meant by "generalized membership".
There was a problem hiding this comment.
"element type", "heterogeneous messages" sounds like nonsense.
There was a problem hiding this comment.
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.
|
|
||
| THEOREM SortedSingleton == | ||
| ASSUME NEW S, NEW x \in S, NEW op(_,_) | ||
| PROVE IsSorted(<< x >>, op) |
There was a problem hiding this comment.
BY DEF IsSorted works.
| NEW e \in S, s # << >> => op(s[Len(s)], e) | ||
| PROVE IsSorted(Append(s, e), op) |
There was a problem hiding this comment.
BY DEF IsSorted works.
| 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) |
There was a problem hiding this comment.
BY DEF IsSorted works.
| ASSUME NEW S, NEW op(_,_), | ||
| \A x \in S : ~ op(x, x), | ||
| NEW s \in Seq(S), IsSorted(s, op) | ||
| PROVE IsInjective(s) |
There was a problem hiding this comment.
BY DEF IsSorted, IsInjective works.
| 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) |
There was a problem hiding this comment.
BY DEF IsSorted works.
|
@muenchnerkindl Do you want to take this PR over? |
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
|
@lemmy could you have a look and check? |
…roofs module Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
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.