ewd998/EWD998_proof: reuse CommunityModules FunctionTheorems

Drop the local Functions.tla (it was the older copy without
SumFunctionOnSet) so EXTENDS Functions resolves to the CommunityModules
version, which lets EWD998_proof EXTEND the proven FunctionTheorems
module. Remove the locally-restated, unproven FoldFunctionOnSet*
lemmas (FoldFunctionIsFoldFunctionOnSet, ...Empty, ...Iterate, ...Union,
...Equal, ...Type) -- they were effectively axioms and are now obtained
from FunctionTheorems.

Keep IsAssociativeOn / IsCommutativeOn / IsIdentityOn and PlusACI as
named-operator wrappers, and add a small PlusOnIntAC lemma that bundles
ACI + closure + base in the shape the CM theorems' premises expect
(mirrors the IntegersAC helper inside FunctionTheorems_proofs.tla).
Rewrite each Sum* lemma as a short structured proof citing the CM
theorem; this also closes SumIterate, SumUnion and SumEqual, whose
previous proofs were commented out as failing or missing.

tlapm verifies all 835 obligations in EWD998_proof.tla.

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

specifications/ewd998/EWD998_proof.tla

@@ -2,7 +2,7 @@
 (***************************************************************************)
 (* Proofs checked by TLAPS about the EWD998 specification.                 *)
 (***************************************************************************)
-EXTENDS EWD998, FiniteSetTheorems, TLAPS
+EXTENDS EWD998, FunctionTheorems, FiniteSetTheorems, TLAPS
 
 USE NAssumption
 
@@ -43,7 +43,10 @@ THEOREM TypeCorrect == Init /\ [][Next]_vars => []TypeOK
 <1>. QED  BY <1>1, <1>2, PTL
 
 (***************************************************************************)
-(* Lemmas about FoldFunction that should go to a library.                  *)
+(* Names for the algebraic properties of a binary operator over a domain.  *)
+(* The CommunityModules theorems below (FoldFunctionOnSetAC,               *)
+(* FoldFunctionOnSetDisjointUnion, etc.) state these premises inline; the  *)
+(* named-operator wrappers let us cite them more readably via PlusACI.     *)
 (***************************************************************************)
 IsAssociativeOn(op(_,_), S) ==
   \A x,y,z \in S : op(x, op(y,z)) = op(op(x,y), z)
@@ -54,52 +57,11 @@ IsCommutativeOn(op(_,_), S) ==
 IsIdentityOn(op(_,_), e, S) ==
   \A x \in S : op(e,x) = x
 
-LEMMA FoldFunctionIsFoldFunctionOnSet ==
-  ASSUME NEW op(_,_), NEW base, NEW fun
-  PROVE  FoldFunction(op, base, fun) = FoldFunctionOnSet(op, base, fun, DOMAIN fun)
-
-LEMMA FoldFunctionOnSetEmpty ==
-  ASSUME NEW op(_,_), NEW base, NEW fun
-  PROVE  FoldFunctionOnSet(op, base, fun, {}) = base 
-
-LEMMA FoldFunctionOnSetIterate ==
-  ASSUME NEW op(_,_), 
-         NEW S, IsFiniteSet(S), NEW T, 
-         NEW base \in T, NEW fun \in [S -> T], 
-         NEW inds \in SUBSET S, NEW e \in inds,
-         IsAssociativeOn(op, T), IsCommutativeOn(op, T), IsIdentityOn(op, base, T)
-  PROVE  FoldFunctionOnSet(op, base, fun, inds)
-       = op(fun[e], FoldFunctionOnSet(op, base, fun, inds \ {e}))
-
-LEMMA FoldFunctionOnSetUnion ==
-  ASSUME NEW op(_,_),
-         NEW S, IsFiniteSet(S), NEW T,
-         NEW base \in T, NEW fun \in [S -> T],
-         NEW inds1 \in SUBSET S, NEW inds2 \in SUBSET S, inds1 \cap inds2 = {},
-         IsAssociativeOn(op, T), IsCommutativeOn(op, T), IsIdentityOn(op, base, T)
-  PROVE  FoldFunctionOnSet(op, base, fun, inds1 \cup inds2)
-         = op(FoldFunctionOnSet(op, base, fun, inds1), FoldFunctionOnSet(op, base, fun, inds2))
-
-LEMMA FoldFunctionOnSetEqual ==
-  ASSUME NEW op(_,_),
-         NEW S, IsFiniteSet(S), NEW T, NEW base \in T,
-         NEW f \in [S -> T], NEW g \in [S -> T],
-         NEW inds \in SUBSET S,
-         \A x \in inds : f[x] = g[x]
-  PROVE  FoldFunctionOnSet(op, base, f, inds) = FoldFunctionOnSet(op, base, g, inds)
-
-LEMMA FoldFunctionOnSetType == 
-  ASSUME NEW op(_,_),
-         NEW S, NEW T, IsFiniteSet(S), 
-         NEW base \in T, NEW fun \in [S -> T],
-         NEW inds \in SUBSET S,
-         \A x,y \in T : op(x,y) \in T
-  PROVE  FoldFunctionOnSet(op, base, fun, inds) \in T
-
 (***************************************************************************)
-(* The provers have trouble applying these generic lemmas to the specific  *)
-(* instances required for the spec so we restate them for the operators    *)
-(* that appear in the definition of the inductive invariant.               *)
+(* Specializations of FunctionTheorems' generic FoldFunctionOnSet*         *)
+(* theorems to the (+, 0) monoid on Int/Nat that underlies the spec's     *)
+(* Sum operator. Restating them as Sum* lemmas avoids dragging the AC     *)
+(* premises through every call site of the inductive invariant proof.     *)
 (***************************************************************************)
 LEMMA NodeIsFinite == IsFiniteSet(Node)
 BY FS_Interval DEF Node
@@ -113,6 +75,24 @@ LEMMA PlusACI ==
   /\ IsIdentityOn(+, 0, Int)
 BY DEF IsAssociativeOn, IsCommutativeOn, IsIdentityOn
 
+(***************************************************************************)
+(* Closure + ACI + neutral element of (+, 0) on Nat and Int, in the form   *)
+(* expected by the FoldFunctionOnSet* theorem premises. (FunctionTheorems  *)
+(* uses an analogous local lemma in its own proofs.)                       *)
+(***************************************************************************)
+LEMMA PlusOnIntAC ==
+  /\ 0 \in Int
+  /\ \A x,y \in Int : x+y \in Int
+  /\ \A x,y \in Int : x+y = y+x
+  /\ \A x,y,z \in Int : x + (y+z) = (x+y) + z
+  /\ \A x \in Int : 0 + x = x
+BY PlusACI DEF IsAssociativeOn, IsCommutativeOn, IsIdentityOn
+
+LEMMA PlusOnNatClosure ==
+  /\ 0 \in Nat
+  /\ \A x,y \in Nat : x+y \in Nat
+OBVIOUS
+
 LEMMA SumEmpty ==
   ASSUME NEW fun
   PROVE  Sum(fun, {}) = 0 
@@ -122,7 +102,11 @@ LEMMA SumIterate ==
   ASSUME NEW fun \in [Node -> Int], 
          NEW inds \in SUBSET Node, NEW e \in inds
   PROVE  Sum(fun, inds) = fun[e] + Sum(fun, inds \ {e})
-\* BY FoldFunctionOnSetIterate, NodeIsFinite, PlusACI DEF Sum (* fails *)
+<1>1. IsFiniteSet(inds)
+  BY NodeIsFinite, FS_Subset
+<1>2. \A j \in inds : fun[j] \in Int
+  OBVIOUS
+<1>. QED  BY <1>1, <1>2, FoldFunctionOnSetAC, PlusOnIntAC, IsaM("iprover") DEF Sum
 
 LEMMA SumSingleton ==
   ASSUME NEW fun \in [Node -> Int], NEW x \in Node
@@ -133,25 +117,40 @@ LEMMA SumUnion ==
   ASSUME NEW fun \in [Node -> Int],
          NEW inds1 \in SUBSET Node, NEW inds2 \in SUBSET Node, inds1 \cap inds2 = {}
   PROVE  Sum(fun, inds1 \cup inds2) = Sum(fun, inds1) + Sum(fun, inds2)
+<1>1. IsFiniteSet(inds1) /\ IsFiniteSet(inds2)
+  BY NodeIsFinite, FS_Subset
+<1>2. \A j \in inds1 \cup inds2 : fun[j] \in Int
+  OBVIOUS
+<1>. QED  BY <1>1, <1>2, FoldFunctionOnSetDisjointUnion, PlusOnIntAC, IsaM("iprover") DEF Sum
 
 LEMMA SumEqual ==
   ASSUME NEW f \in [Node -> Int], NEW g \in [Node -> Int],
          NEW inds \in SUBSET Node,
          \A x \in inds : f[x] = g[x]
   PROVE  Sum(f, inds) = Sum(g, inds)
-\* BY FoldFunctionOnSetEqual, NodeIsFinite DEF Sum (* fails *)
+<1>1. IsFiniteSet(inds)
+  BY NodeIsFinite, FS_Subset
+<1>. QED  BY <1>1, FoldFunctionOnSetEqual, Zenon DEF Sum
 
 LEMMA SumIsInt == 
   ASSUME NEW fun \in [Node -> Int],
          NEW inds \in SUBSET Node
   PROVE  Sum(fun, inds) \in Int
-BY FoldFunctionOnSetType, NodeIsFinite, Isa DEF Sum
+<1>1. IsFiniteSet(inds)
+  BY NodeIsFinite, FS_Subset
+<1>2. \A j \in inds : fun[j] \in Int
+  OBVIOUS
+<1>. QED  BY <1>1, <1>2, FoldFunctionOnSetType, PlusOnIntAC, IsaM("iprover") DEF Sum
 
 LEMMA SumIsNat == 
   ASSUME NEW fun \in [Node -> Nat],
          NEW inds \in SUBSET Node
   PROVE  Sum(fun, inds) \in Nat
-BY FoldFunctionOnSetType, NodeIsFinite, \A x,y \in Nat: x+y \in Nat, IsaM("blast") DEF Sum
+<1>1. IsFiniteSet(inds)
+  BY NodeIsFinite, FS_Subset
+<1>2. \A j \in inds : fun[j] \in Nat
+  OBVIOUS
+<1>. QED  BY <1>1, <1>2, FoldFunctionOnSetType, PlusOnNatClosure, IsaM("iprover") DEF Sum
 
 LEMMA SumZero ==
   ASSUME NEW fun \in [Node -> Int], NEW inds \in SUBSET Node,

specifications/ewd998/Functions.tla

@@ -170,11 +170,6 @@
       "features": [],
       "models": []
     },
-    {
-      "path": "specifications/ewd998/Functions.tla",
-      "features": [],
-      "models": []
-    },
     {
       "path": "specifications/ewd998/SmokeEWD998.tla",
       "features": [],