From 6bb7abfda94f5ded1fb4e3776de6716b3b2d0d1c Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 3 Nov 2026 16:52:49 -0800 Subject: [PATCH] Preserve the SANY binding of SUBSET against \ and \union. SANY assigns SUBSET precedence 10-13, so SUBSET Nat \ {0} parses as (SUBSET Nat) \ {0} and SUBSET S \union {x} parses as (SUBSET S) \union {x}. The Summary of TLA+ gives SUBSET precedence 8-8, the same as \, \cup, and \cap, and an overlapping range is a syntax error. Pull request 1508 applies that table in SANY, after which these expressions no longer parse. The parentheses record the binding SANY has been using. Related to tlaplus/tlaplus#1508 https://github.com/tlaplus/tlaplus/pull/1508 See tlaplus/rfcs#28 https://github.com/tlaplus/rfcs/issues/28 [Refactor] Co-authored-by: Grok 4.7 Signed-off-by: Markus Alexander Kuppe --- modules/FiniteSetsExtTheorems.tla | 2 +- modules/FiniteSetsExtTheorems_proofs.tla | 4 ++-- modules/FoldsTheorems.tla | 2 +- modules/FoldsTheorems_proofs.tla | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/modules/FiniteSetsExtTheorems.tla b/modules/FiniteSetsExtTheorems.tla index 6f22eb6..533e678 100644 --- a/modules/FiniteSetsExtTheorems.tla +++ b/modules/FiniteSetsExtTheorems.tla @@ -188,7 +188,7 @@ THEOREM ProductSetZero == (* bounded by the product of the full set. *) (*************************************************************************) THEOREM ProductSetNatSubset == - ASSUME NEW S \in SUBSET Nat \ {0}, IsFiniteSet(S), + ASSUME NEW S \in SUBSET (Nat \ {0}), IsFiniteSet(S), NEW T \in SUBSET S PROVE ProductSet(T) <= ProductSet(S) diff --git a/modules/FiniteSetsExtTheorems_proofs.tla b/modules/FiniteSetsExtTheorems_proofs.tla index 29a3b28..2daa477 100644 --- a/modules/FiniteSetsExtTheorems_proofs.tla +++ b/modules/FiniteSetsExtTheorems_proofs.tla @@ -295,7 +295,7 @@ THEOREM ProductSetZero == <2>. QED BY DEF P THEOREM ProductSetNatSubset == - ASSUME NEW S \in SUBSET Nat \ {0}, IsFiniteSet(S), + ASSUME NEW S \in SUBSET (Nat \ {0}), IsFiniteSet(S), NEW T \in SUBSET S PROVE ProductSet(T) <= ProductSet(S) <1>. DEFINE U == S \ T @@ -362,7 +362,7 @@ THEOREM MapThenSumSetAddElement == ASSUME NEW S, IsFiniteSet(S), NEW x, x \notin S, NEW op(_), \A s \in S \union {x} : op(s) \in Int PROVE MapThenSumSet(op, S \union {x}) = op(x) + MapThenSumSet(op, S) -<1>. \A T \in SUBSET S \union {x} : T # {} => (CHOOSE t \in T : TRUE) \in T +<1>. \A T \in SUBSET (S \union {x}) : T # {} => (CHOOSE t \in T : TRUE) \in T OBVIOUS <1>. /\ 0 \in Int /\ \A i,j \in Int : i+j \in Int diff --git a/modules/FoldsTheorems.tla b/modules/FoldsTheorems.tla index a51f79c..c332071 100644 --- a/modules/FoldsTheorems.tla +++ b/modules/FoldsTheorems.tla @@ -102,7 +102,7 @@ THEOREM MapThenFoldSetACAddElement == \A t,u \in Typ : op(t,u) = op(u,t), \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), NEW S, IsFiniteSet(S), NEW x, x \notin S, - NEW choose(_), \A T \in SUBSET S \union {x} : T # {} => choose(T) \in T, + NEW choose(_), \A T \in SUBSET (S \union {x}) : T # {} => choose(T) \in T, \A s \in S \union {x} : f(s) \in Typ PROVE MapThenFoldSet(op, base, f, choose, S \union {x}) = op(f(x), MapThenFoldSet(op, base, f, choose, S)) diff --git a/modules/FoldsTheorems_proofs.tla b/modules/FoldsTheorems_proofs.tla index 68cca64..fba7852 100644 --- a/modules/FoldsTheorems_proofs.tla +++ b/modules/FoldsTheorems_proofs.tla @@ -271,7 +271,7 @@ THEOREM MapThenFoldSetACAddElement == \A t,u \in Typ : op(t,u) = op(u,t), \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v), NEW S, IsFiniteSet(S), NEW x, x \notin S, - NEW choose(_), \A T \in SUBSET S \union {x} : T # {} => choose(T) \in T, + NEW choose(_), \A T \in SUBSET (S \union {x}) : T # {} => choose(T) \in T, \A s \in S \union {x} : f(s) \in Typ PROVE MapThenFoldSet(op, base, f, choose, S \union {x}) = op(f(x), MapThenFoldSet(op, base, f, choose, S))