diff --git a/specifications/ewd998/EWD998_proof.tla b/specifications/ewd998/EWD998_proof.tla index 420efcfe..9515d554 100644 --- a/specifications/ewd998/EWD998_proof.tla +++ b/specifications/ewd998/EWD998_proof.tla @@ -2,7 +2,7 @@ (***************************************************************************) (* Proofs checked by TLAPS about the EWD998 specification. *) (***************************************************************************) -EXTENDS EWD998, FiniteSetTheorems, TLAPS +EXTENDS EWD998, FiniteSetTheorems, FunctionTheorems, FiniteSetsExtTheorems, TLAPS USE NAssumption @@ -43,76 +43,13 @@ THEOREM TypeCorrect == Init /\ [][Next]_vars => []TypeOK <1>. QED BY <1>1, <1>2, PTL (***************************************************************************) -(* Lemmas about FoldFunction that should go to a library. *) -(***************************************************************************) -IsAssociativeOn(op(_,_), S) == - \A x,y,z \in S : op(x, op(y,z)) = op(op(x,y), z) - -IsCommutativeOn(op(_,_), S) == - \A x,y \in S : op(x,y) = op(y,x) - -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. *) +(* The provers have trouble applying the generic lemmas to the specific *) +(* instances required for the spec, so the ones needed here are restated *) +(* for the operators that appear in the inductive invariant. *) (***************************************************************************) LEMMA NodeIsFinite == IsFiniteSet(Node) BY FS_Interval DEF Node -LEMMA PlusACI == - /\ IsAssociativeOn(+, Nat) - /\ IsCommutativeOn(+, Nat) - /\ IsIdentityOn(+, 0, Nat) - /\ IsAssociativeOn(+, Int) - /\ IsCommutativeOn(+, Int) - /\ IsIdentityOn(+, 0, Int) -BY DEF IsAssociativeOn, IsCommutativeOn, IsIdentityOn - LEMMA SumEmpty == ASSUME NEW fun PROVE Sum(fun, {}) = 0 @@ -122,7 +59,19 @@ 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 \ {e}) + BY NodeIsFinite, FS_Subset +<1>2. e \notin inds \ {e} + OBVIOUS +<1>3. inds = (inds \ {e}) \union {e} + OBVIOUS +<1>4. \A s \in (inds \ {e}) \union {e} : fun[s] \in Int + OBVIOUS +<1>5. MapThenSumSet(LAMBDA s : fun[s], (inds \ {e}) \union {e}) + = fun[e] + MapThenSumSet(LAMBDA s : fun[s], inds \ {e}) + BY <1>1, <1>2, <1>4, MapThenSumSetAddElement +<1>. QED + BY <1>3, <1>5 DEF Sum, MapThenSumSet, FoldFunctionOnSet LEMMA SumSingleton == ASSUME NEW fun \in [Node -> Int], NEW x \in Node @@ -133,25 +82,53 @@ 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 x \in inds1 \union inds2 : fun[x] \in Int + OBVIOUS +<1>. QED + BY <1>1, <1>2, MapThenSumSetDisjointUnion + DEF Sum, MapThenSumSet, FoldFunctionOnSet 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 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 i \in inds : fun[i] \in Int + OBVIOUS +<1>3. \A t,u \in Int : t + u \in Int + OBVIOUS +<1>4. 0 \in Int + OBVIOUS +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, FoldFunctionOnSetType 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 i \in inds : fun[i] \in Nat + OBVIOUS +<1>3. \A t,u \in Nat : t + u \in Nat + OBVIOUS +<1>4. 0 \in Nat + OBVIOUS +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, FoldFunctionOnSetType, IsaM("blast") DEF Sum LEMMA SumZero == ASSUME NEW fun \in [Node -> Int], NEW inds \in SUBSET Node, diff --git a/specifications/ewd998/Functions.tla b/specifications/ewd998/Functions.tla deleted file mode 100644 index 4b0652b0..00000000 --- a/specifications/ewd998/Functions.tla +++ /dev/null @@ -1,176 +0,0 @@ ------------------------------- MODULE Functions ----------------------------- -(***************************************************************************) -(* `^{\large\bf \vspace{12pt} *) -(* Notions about functions including injection, surjection, and bijection.*) -(* Originally contributed by Tom Rodeheffer, MSR. *) -(* \vspace{12pt}}^' *) -(***************************************************************************) - -LOCAL INSTANCE Folds - -(***************************************************************************) -(* Restriction of a function to a set (should be a subset of the domain). *) -(***************************************************************************) -Restrict(f,S) == [ x \in S |-> f[x] ] - -(***************************************************************************) -(* Restriction of a function to the subset of its domain satisfying a *) -(* test predicate. *) -(* *) -(* Example: *) -(* (LET f == (0 :> "a" @@ 1 :> "b" @@ 2 :> "c") *) -(* IN RestrictDomain(f, LAMBDA x : x \in {0,2})) *) -(* = (0 :> "a" @@ 2 :> "c") *) -(***************************************************************************) -RestrictDomain(f, Test(_)) == Restrict(f, {x \in DOMAIN f : Test(x)}) - -(***************************************************************************) -(* Restriction of a function to the subset of its domain for which the *) -(* function values satisfy a test predicate. *) -(* *) -(* Example: *) -(* (LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* IN RestrictValues(f, LAMBDA y : y \in {0,2})) *) -(* = ("a" :> 0 @@ "b" :> 2) *) -(* *) -(* This is similar to the operator SelectSeq from the standard Sequences *) -(* module and related to standard "filter" functions in functional *) -(* programming. However, SelectSeq produces sequences, whereas *) -(* RestrictValues will in general not. For example, *) -(* *) -(* RestrictValues([0,1,2], LAMBDA y : y \in {0,2}) *) -(* = (1 :> 0 @@ 3 :> 2) *) -(***************************************************************************) -RestrictValues(f, Test(_)) == - LET S == {x \in DOMAIN f : Test(f[x])} - IN Restrict(f, S) - -(***************************************************************************) -(* Check if a function narrow is a restriction of a function wide, i.e. *) -(* Is the domain of narrow a subset of that of wide, and does the *) -(* projection of wide on the domain of narrow have the same image as *) -(* narrow does. *) -(* *) -(* Examples: *) -(* IsRestriction([one |-> 1], [one |-> 1, two |-> 2]) *) -(* IsRestriction([one |-> 1], [one |-> 1]) *) -(* ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3]) *) -(* ~IsRestriction([one |-> 1], [2 |-> two]) *) -(* ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2]) *) -(***************************************************************************) -IsRestriction(narrow, wide) == - /\ DOMAIN narrow \subseteq DOMAIN wide - /\ \A x \in DOMAIN narrow \intersect DOMAIN wide: narrow[x] = wide[x] - -(***************************************************************************) -(* Range of a function. *) -(* Note: The image of a set under function f can be defined as *) -(* Range(Restrict(f,S)). *) -(***************************************************************************) -Range(f) == { f[x] : x \in DOMAIN f } - -(***************************************************************************) -(* Assuming DOMAIN f \subseteq DOMAIN g, apply the binary operation T to *) -(* the corresponding elements of the two functions f and g. *) -(* *) -(* Example: *) -(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* g == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 3) *) -(* IN Pointwise(f,g,+) = ("a" :> 1 @@ "b" :> 2 @@ "c" :> 5 ) *) -(***************************************************************************) -Pointwise(f, g, T(_,_)) == [ e \in DOMAIN f |-> T(f[e], g[e]) ] - -(***************************************************************************) -(* The inverse of a function. *) -(* Example: *) -(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* IN Inverse(f, DOMAIN f, Range(f)) = *) -(* (0 :> "a" @@ 1 :> "b" @@ 2 :> "c") *) -(* Example: *) -(* LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) *) -(* IN Inverse(f, DOMAIN f, {1,3}) = *) -(* 1 :> "b" @@ 3 :> "a") *) -(***************************************************************************) -Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t] - -(***************************************************************************) -(* The inverse of a function. *) -(***************************************************************************) -AntiFunction(f) == Inverse(f, DOMAIN f, Range(f)) - -(***************************************************************************) -(* A function is injective iff it maps each element in its domain to a *) -(* distinct element. *) -(* *) -(* This definition is overridden by TLC in the Java class Functions.java *) -(* The operator is overridden by the Java method with the same name. *) -(***************************************************************************) -IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b - -(***************************************************************************) -(* Set of injections between two sets. *) -(***************************************************************************) -Injection(S,T) == { M \in [S -> T] : IsInjective(M) } - - -(***************************************************************************) -(* A map is a surjection iff for each element in the range there is some *) -(* element in the domain that maps to it. *) -(***************************************************************************) -Surjection(S,T) == { M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t } - - -(***************************************************************************) -(* A map is a bijection iff it is both an injection and a surjection. *) -(***************************************************************************) -Bijection(S,T) == Injection(S,T) \cap Surjection(S,T) - - -(***************************************************************************) -(* An injection, surjection, or bijection exists if the corresponding set *) -(* is nonempty. *) -(***************************************************************************) -ExistsInjection(S,T) == Injection(S,T) # {} -ExistsSurjection(S,T) == Surjection(S,T) # {} -ExistsBijection(S,T) == Bijection(S,T) # {} - --------------------------------------------------------------------------------- - -FoldFunction(op(_,_), base, fun) == - (***************************************************************************) - (* Applies the binary function op on all elements of fun in arbitrary *) - (* order starting with op(f[k], base). The resulting function is: *) - (* op(f[i],op(f[j], ..., op(f[k],base) ...)) *) - (* *) - (* op must be associative and commutative, because we can not assume a *) - (* particular ordering of i, j, and k *) - (* *) - (* Example: *) - (* FoldFunction(LAMBDA x,y: {x} \cup y, {}, <<1,2,1>>) = {1,2} *) - (***************************************************************************) - MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, DOMAIN fun) - - -FoldFunctionOnSet(op(_,_), base, fun, indices) == - (***************************************************************************) - (* Applies the binary function op on the given indices of fun in arbitrary *) - (* order starting with op(f[k], base). The resulting function is: *) - (* op(f[i],op(f[j], ..., op(f[k],base) ...)) *) - (* *) - (* op must be associative and commutative, because we can not assume a *) - (* particular ordering of i, j, and k *) - (* *) - (* indices must be a subset of DOMAIN(fun) *) - (* *) - (* Example: *) - (* FoldFunctionOnSet(LAMBDA x,y: {x} \cup y, {}, <<1,2>>, {}) = {} *) - (***************************************************************************) - MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices) - -============================================================================= -\* Modification History -\* Last modified Tue Nov 01 08:46:11 CET 2022 by merz -\* Last modified Mon Apr 05 03:25:53 CEST 2021 by marty -\* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav -\* Last modified Fri May 03 12:55:35 PDT 2013 by tomr -\* Created Thu Apr 11 10:30:48 PDT 2013 by tomr diff --git a/specifications/ewd998/manifest.json b/specifications/ewd998/manifest.json index dafe41cc..9d8c35b8 100644 --- a/specifications/ewd998/manifest.json +++ b/specifications/ewd998/manifest.json @@ -162,7 +162,7 @@ "features": [], "models": [], "proof": { - "maxRuntimeMinutes": 2 + "maxRuntimeMinutes": 4 } }, { @@ -170,11 +170,6 @@ "features": [], "models": [] }, - { - "path": "specifications/ewd998/Functions.tla", - "features": [], - "models": [] - }, { "path": "specifications/ewd998/SmokeEWD998.tla", "features": [],