From 5d2e5ff900345896d8f36186cbb89e9fdc656801 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Tue, 17 Mar 2026 14:02:00 +0100 Subject: [PATCH 1/2] basic theory of sets with cardinality --- .../de/uka/ilkd/key/proof/rules/ldt.key | 1 + .../de/uka/ilkd/key/proof/rules/set.key | 27 +++ .../de/uka/ilkd/key/proof/rules/setRules.key | 168 ++++++++++++++++++ .../ilkd/key/proof/rules/standardRules.key | 1 + key.ui/examples/set/setExample.key | 5 + 5 files changed, 202 insertions(+) create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key create mode 100644 key.ui/examples/set/setExample.key diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key index d54f2527f00..260500988ad 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ldt.key @@ -24,6 +24,7 @@ permission, reach, seq, + set, map, freeADT, wellfound, diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key new file mode 100644 index 00000000000..f17a6d69d1d --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key @@ -0,0 +1,27 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ + +\sorts { + /*! @defaultValue(sEmpty) */ + Set; +} + +\functions { + \unique Set sEmpty; + + // other constructors + Set sSingleton(any); + Set sUnion(Set, Set); + Set sIntersect(Set, Set); + Set sSetMinus(Set, Set); + Set sInfiniteUnion{true}(Set); + + int sCard(Set); +} + +\predicates { + sElementOf(any, Set); + sSubset(Set, Set); + sDisjoint(Set, Set); +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key new file mode 100644 index 00000000000..0fadb42a867 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key @@ -0,0 +1,168 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ + +\schemaVariables { + \term any a, b; + \term Set s, t, EQ; +} + +\rules { + + // -------------------------------------------------------------------------- + // axioms for sElementOf + // -------------------------------------------------------------------------- + + sElementOfEmpty { + \find(sElementOf(a, sEmpty)) + \replacewith(false) + \heuristics(concrete) + }; + + sElementOfSingleton { + \find(sElementOf(a, sSingleton(b))) + \replacewith(a = b) + \heuristics(simplify) + }; + + sElementOfUnion { + \find(sElementOf(a, sUnion(s, t))) + \replacewith(sElementOf(a, s) | sElementOf(a, t)) + \heuristics(simplify_enlarging) + }; + + sElementOfIntersect { + \find(sElementOf(a, sIntersect(s, t))) + \replacewith(sElementOf(a, s) & sElementOf(a, t)) + \heuristics(simplify_enlarging) + }; + + sElementOfSetMinus { + \find(sElementOf(a, sSetMinus(s, t))) + \replacewith(sElementOf(a, s) & !sElementOf(a, t)) + \heuristics(simplify_enlarging) + }; + + sElementOfInfiniteUnion { + // TODO: alpha or any (was like this already in locSetsRules)? + \schemaVar \variables alpha av; + \find(sElementOf(a, sInfiniteUnion{av;}(s))) + \varcond(\notFreeIn(av, a)) + \replacewith(\exists av; sElementOf(a, s)) + \heuristics(simplify) + }; + + // -------------------------------------------------------------------------- + // EQ versions of axioms (these are lemmata) + // -------------------------------------------------------------------------- + sElementOfUnionEQ { + \assumes(sUnion(s, t) = EQ ==>) + \find(sElementOf(a, EQ)) + \sameUpdateLevel + \replacewith(sElementOf(a, s) | sElementOf(a, t)) + \heuristics(simplify_enlarging) + }; + + sElementOfIntersectEQ { + \assumes(sIntersect(s, t) = EQ ==>) + \find(sElementOf(a, EQ)) + \sameUpdateLevel + \replacewith(sElementOf(a, s) & sElementOf(a, t)) + \heuristics(simplify_enlarging) + }; + + sElementOfSetMinusEQ { + \assumes(sSetMinus(s, t) = EQ ==>) + \find(sElementOf(a, EQ)) + \sameUpdateLevel + \replacewith(sElementOf(a, s) & !sElementOf(a, t)) + \heuristics(simplify_enlarging) + }; + + sElementOfInfiniteUnionEQ { + \schemaVar \variables alpha av; + \assumes(sInfiniteUnion{av;}(s) = EQ ==>) + \find(sElementOf(a, EQ)) + \sameUpdateLevel + \varcond(\notFreeIn(av, a)) + \replacewith(\exists av; sElementOf(a, s)) + \heuristics(simplify) + }; + + // -------------------------------------------------------------------------- + // axioms for cardinality + // -------------------------------------------------------------------------- + sCardNonNegative { + \find(sCard(s)) + \sameUpdateLevel + \add(sCard(s) >= 0 ==>) + \heuristics(inReachableStateImplication) + }; + + sCardEmpty { + \find(sCard(sEmpty)) + \replacewith(0) + \heuristics(concrete) + }; + + sCardSingleton { + \find(sCard(sSingleton(b))) + \replacewith(1) + \heuristics(simplify) + }; + + + // -------------------------------------------------------------------------- + // axioms for set predicates (reduce to sElementOf) + // -------------------------------------------------------------------------- + + equalityTosElementOf { + \schemaVar \variables any av; + \find(s = t) + \varcond(\notFreeIn(av, s, t)) + \replacewith(\forall av; (sElementOf(av, s) <-> sElementOf(av, t))) + \heuristics(semantics_blasting) + }; + + sEmptyEqualsSingleton { + \find(sEmpty = sSingleton(a)) + \replacewith(false) + \heuristics(concrete) + }; + + sSingletonEqualsEmpty { + \find(sSingleton(a) = sEmpty) + \replacewith(false) + \heuristics(concrete) + }; + + unionWithSingletonEqualsUnionWithSingleton { + \find(sUnion(s, sSingleton(a)) = sUnion(t, sSingleton(a))) + + \replacewith(sSetMinus(s, sSingleton(a)) = sSetMinus(t, sSingleton(a))) + // TODO: why is this a simplification? (DB) + \heuristics(simplify) + }; + + unionWithSingletonEqualsUnionWithSingleton_2 { + \find(sUnion(sSingleton(a), s) = sUnion(sSingleton(a), t)) + \replacewith(sSetMinus(s, sSingleton(a)) = sSetMinus(t, sSingleton(a))) + \heuristics(simplify) + }; + + subsetTosElementOf { + \schemaVar \variables any av; + \find(sSubset(s, t)) + \varcond(\notFreeIn(av, s, t)) + \replacewith(\forall av; (sElementOf(av, s) -> sElementOf(av, t))) + \heuristics(semantics_blasting) + }; + + disjointToElementOf { + \schemaVar \variables any av; + \find(sDisjoint(s, t)) + \varcond(\notFreeIn(av, s, t)) + \replacewith(\forall av; (!sElementOf(av, s) | !sElementOf(av, t))) + \heuristics(semantics_blasting) + }; +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key index 96c6fc2136b..56e17e800e5 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/standardRules.key @@ -47,6 +47,7 @@ \include seqCoreRules, seqRules; \include seqPerm; \include seqPerm2; +\include setRules; // rules for Java (order does not matter, since not provable anyway) \include javaRules; diff --git a/key.ui/examples/set/setExample.key b/key.ui/examples/set/setExample.key new file mode 100644 index 00000000000..2a12b42c3a9 --- /dev/null +++ b/key.ui/examples/set/setExample.key @@ -0,0 +1,5 @@ + +\problem { +\forall Set s1; (\forall Set s2; + (sIntersect(s1, s2) = sEmpty <-> \forall any a; (sElementOf(a, s1) -> !sElementOf(a, s2)))) +} From 25e7e58504e5fb8b6b8a7a33b0bed6d9d4570404 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 18 Mar 2026 19:33:46 +0100 Subject: [PATCH 2/2] made sets polymorphic, added very small example to RAP --- .../de/uka/ilkd/key/proof/rules/set.key | 24 +-- .../de/uka/ilkd/key/proof/rules/setRules.key | 140 +++++++++--------- .../proof/runallproofs/ProofCollections.java | 1 + key.ui/examples/set/setExample.key | 5 - .../standard_key/polymorphic/setExample.key | 9 ++ 5 files changed, 93 insertions(+), 86 deletions(-) delete mode 100644 key.ui/examples/set/setExample.key create mode 100644 key.ui/examples/standard_key/polymorphic/setExample.key diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key index f17a6d69d1d..37566a7163e 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/set.key @@ -3,25 +3,25 @@ * SPDX-License-Identifier: GPL-2.0-only */ \sorts { - /*! @defaultValue(sEmpty) */ - Set; + \generic T; + Set<[T]>; } \functions { - \unique Set sEmpty; + \unique Set<[T]> sEmpty<[T]>; // other constructors - Set sSingleton(any); - Set sUnion(Set, Set); - Set sIntersect(Set, Set); - Set sSetMinus(Set, Set); - Set sInfiniteUnion{true}(Set); + Set<[T]> sSingleton<[T]>(T); + Set<[T]> sUnion<[T]>(Set<[T]>, Set<[T]>); + Set<[T]> sIntersect<[T]>(Set<[T]>, Set<[T]>); + Set<[T]> sSetMinus<[T]>(Set<[T]>, Set<[T]>); + Set<[T]> sInfiniteUnion<[T]>{true}(Set<[T]>); - int sCard(Set); + int sCard<[T]>(Set<[T]>); } \predicates { - sElementOf(any, Set); - sSubset(Set, Set); - sDisjoint(Set, Set); + sElementOf<[T]>(T, Set<[T]>); + sSubset<[T]>(Set<[T]>, Set<[T]>); + sDisjoint<[T]>(Set<[T]>, Set<[T]>); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key index 0fadb42a867..a47ad7addcb 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/setRules.key @@ -3,8 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ \schemaVariables { - \term any a, b; - \term Set s, t, EQ; + \term T a, b; + \term Set<[T]> s, t, EQ; } \rules { @@ -13,79 +13,80 @@ // axioms for sElementOf // -------------------------------------------------------------------------- - sElementOfEmpty { - \find(sElementOf(a, sEmpty)) + sElementOfSEmpty { + \find(sElementOf<[T]>(a, sEmpty<[T]>)) \replacewith(false) \heuristics(concrete) }; - sElementOfSingleton { - \find(sElementOf(a, sSingleton(b))) + sElementOfSSingleton { + \find(sElementOf<[T]>(a, sSingleton<[T]>(b))) \replacewith(a = b) \heuristics(simplify) }; - sElementOfUnion { - \find(sElementOf(a, sUnion(s, t))) - \replacewith(sElementOf(a, s) | sElementOf(a, t)) + sElementOfSUnion { + \find(sElementOf<[T]>(a, sUnion<[T]>(s, t))) + \replacewith(sElementOf<[T]>(a, s) | sElementOf<[T]>(a, t)) \heuristics(simplify_enlarging) }; - sElementOfIntersect { - \find(sElementOf(a, sIntersect(s, t))) - \replacewith(sElementOf(a, s) & sElementOf(a, t)) + sElementOfSIntersect { + \find(sElementOf<[T]>(a, sIntersect<[T]>(s, t))) + \replacewith(sElementOf<[T]>(a, s) & sElementOf<[T]>(a, t)) \heuristics(simplify_enlarging) }; - sElementOfSetMinus { - \find(sElementOf(a, sSetMinus(s, t))) - \replacewith(sElementOf(a, s) & !sElementOf(a, t)) + sElementOfSSetMinus { + \find(sElementOf<[T]>(a, sSetMinus<[T]>(s, t))) + \replacewith(sElementOf<[T]>(a, s) & !sElementOf<[T]>(a, t)) \heuristics(simplify_enlarging) }; - sElementOfInfiniteUnion { + sElementOfSInfiniteUnion { // TODO: alpha or any (was like this already in locSetsRules)? \schemaVar \variables alpha av; - \find(sElementOf(a, sInfiniteUnion{av;}(s))) + \find(sElementOf<[T]>(a, sInfiniteUnion<[T]>{av;}(s))) \varcond(\notFreeIn(av, a)) - \replacewith(\exists av; sElementOf(a, s)) + \replacewith(\exists av; sElementOf<[T]>(a, s)) \heuristics(simplify) }; // -------------------------------------------------------------------------- // EQ versions of axioms (these are lemmata) // -------------------------------------------------------------------------- - sElementOfUnionEQ { - \assumes(sUnion(s, t) = EQ ==>) - \find(sElementOf(a, EQ)) + sElementOfSUnionEQ { + \assumes(sUnion<[T]>(s, t) = EQ ==>) + \find(sElementOf<[T]>(a, EQ)) \sameUpdateLevel - \replacewith(sElementOf(a, s) | sElementOf(a, t)) + \replacewith(sElementOf<[T]>(a, s) | sElementOf<[T]>(a, t)) \heuristics(simplify_enlarging) }; - sElementOfIntersectEQ { - \assumes(sIntersect(s, t) = EQ ==>) - \find(sElementOf(a, EQ)) + sElementOfSIntersectEQ { + \assumes(sIntersect<[T]>(s, t) = EQ ==>) + \find(sElementOf<[T]>(a, EQ)) \sameUpdateLevel - \replacewith(sElementOf(a, s) & sElementOf(a, t)) + \replacewith(sElementOf<[T]>(a, s) & sElementOf<[T]>(a, t)) \heuristics(simplify_enlarging) }; sElementOfSetMinusEQ { - \assumes(sSetMinus(s, t) = EQ ==>) - \find(sElementOf(a, EQ)) + \assumes(sSetMinus<[T]>(s, t) = EQ ==>) + \find(sElementOf<[T]>(a, EQ)) \sameUpdateLevel - \replacewith(sElementOf(a, s) & !sElementOf(a, t)) + \replacewith(sElementOf<[T]>(a, s) & !sElementOf<[T]>(a, t)) \heuristics(simplify_enlarging) }; - sElementOfInfiniteUnionEQ { + sElementOfSInfiniteUnionEQ { + // TODO: alpha or any (was like this already in locSetsRules)? \schemaVar \variables alpha av; - \assumes(sInfiniteUnion{av;}(s) = EQ ==>) - \find(sElementOf(a, EQ)) + \assumes(sInfiniteUnion<[T]>{av;}(s) = EQ ==>) + \find(sElementOf<[T]>(a, EQ)) \sameUpdateLevel \varcond(\notFreeIn(av, a)) - \replacewith(\exists av; sElementOf(a, s)) + \replacewith(\exists av; sElementOf<[T]>(a, s)) \heuristics(simplify) }; @@ -93,76 +94,77 @@ // axioms for cardinality // -------------------------------------------------------------------------- sCardNonNegative { - \find(sCard(s)) + \find(sCard<[T]>(s)) \sameUpdateLevel - \add(sCard(s) >= 0 ==>) + \add(sCard<[T]>(s) >= 0 ==>) \heuristics(inReachableStateImplication) }; - sCardEmpty { - \find(sCard(sEmpty)) + sCardSEmpty { + \find(sCard<[T]>(sEmpty<[T]>)) \replacewith(0) \heuristics(concrete) }; - sCardSingleton { - \find(sCard(sSingleton(b))) + sCardSSingleton { + \find(sCard<[T]>(sSingleton<[T]>(b))) \replacewith(1) \heuristics(simplify) }; - // -------------------------------------------------------------------------- // axioms for set predicates (reduce to sElementOf) // -------------------------------------------------------------------------- - equalityTosElementOf { - \schemaVar \variables any av; - \find(s = t) - \varcond(\notFreeIn(av, s, t)) - \replacewith(\forall av; (sElementOf(av, s) <-> sElementOf(av, t))) - \heuristics(semantics_blasting) - }; - - sEmptyEqualsSingleton { - \find(sEmpty = sSingleton(a)) + sEmptyEqualsSSingleton { + \find(sEmpty<[T]> = sSingleton<[T]>(a)) \replacewith(false) \heuristics(concrete) }; - sSingletonEqualsEmpty { - \find(sSingleton(a) = sEmpty) + sSingletonEqualsSEmpty { + \find(sSingleton<[T]>(a) = sEmpty<[T]>) \replacewith(false) \heuristics(concrete) }; - unionWithSingletonEqualsUnionWithSingleton { - \find(sUnion(s, sSingleton(a)) = sUnion(t, sSingleton(a))) + sUnionWithSSingletonEqualsSUnionWithSSingleton { + \find(sUnion<[T]>(s, sSingleton<[T]>(a)) = sUnion<[T]>(t, sSingleton<[T]>(a))) - \replacewith(sSetMinus(s, sSingleton(a)) = sSetMinus(t, sSingleton(a))) - // TODO: why is this a simplification? (DB) + \replacewith(sSetMinus<[T]>(s, sSingleton<[T]>(a)) = sSetMinus<[T]>(t, sSingleton<[T]>(a))) \heuristics(simplify) }; - unionWithSingletonEqualsUnionWithSingleton_2 { - \find(sUnion(sSingleton(a), s) = sUnion(sSingleton(a), t)) - \replacewith(sSetMinus(s, sSingleton(a)) = sSetMinus(t, sSingleton(a))) + sUnionWithSSingletonEqualsSUnionWithSSingleton_2 { + \find(sUnion<[T]>(sSingleton<[T]>(a), s) = sUnion<[T]>(sSingleton<[T]>(a), t)) + \replacewith(sSetMinus<[T]>(s, sSingleton<[T]>(a)) = sSetMinus<[T]>(t, sSingleton<[T]>(a))) \heuristics(simplify) }; - subsetTosElementOf { - \schemaVar \variables any av; - \find(sSubset(s, t)) + equalityToSElementOf { + \schemaVar \variables T av; + \find(s = t) \varcond(\notFreeIn(av, s, t)) - \replacewith(\forall av; (sElementOf(av, s) -> sElementOf(av, t))) - \heuristics(semantics_blasting) + \replacewith(\forall av; (sElementOf<[T]>(av, s) <-> sElementOf<[T]>(av, t))) + //\heuristics(semantics_blasting) + \heuristics(simplify_enlarging) + }; + + sSubsetToSElementOf { + \schemaVar \variables T av; + \find(sSubset<[T]>(s, t)) + \varcond(\notFreeIn(av, s, t)) + \replacewith(\forall av; (sElementOf<[T]>(av, s) -> sElementOf<[T]>(av, t))) + //\heuristics(semantics_blasting) + \heuristics(simplify_enlarging) }; - disjointToElementOf { - \schemaVar \variables any av; - \find(sDisjoint(s, t)) + sDisjointToSElementOf { + \schemaVar \variables T av; + \find(sDisjoint<[T]>(s, t)) \varcond(\notFreeIn(av, s, t)) - \replacewith(\forall av; (!sElementOf(av, s) | !sElementOf(av, t))) - \heuristics(semantics_blasting) + \replacewith(\forall av; (!sElementOf<[T]>(av, s) | !sElementOf<[T]>(av, t))) +// \heuristics(semantics_blasting) + \heuristics(simplify_enlarging) }; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index 4c8b12135ac..14ff02f126b 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -1003,6 +1003,7 @@ public static ProofCollection automaticJavaDL() throws IOException { g = c.group("PolymorphicSorts"); g.loadable("standard_key/polymorphic/pseq.key"); + g.provable("standard_key/polymorphic/setExample.key"); // use for debugging purposes. // c.keep("VSTTE10"); diff --git a/key.ui/examples/set/setExample.key b/key.ui/examples/set/setExample.key deleted file mode 100644 index 2a12b42c3a9..00000000000 --- a/key.ui/examples/set/setExample.key +++ /dev/null @@ -1,5 +0,0 @@ - -\problem { -\forall Set s1; (\forall Set s2; - (sIntersect(s1, s2) = sEmpty <-> \forall any a; (sElementOf(a, s1) -> !sElementOf(a, s2)))) -} diff --git a/key.ui/examples/standard_key/polymorphic/setExample.key b/key.ui/examples/standard_key/polymorphic/setExample.key new file mode 100644 index 00000000000..760608820f1 --- /dev/null +++ b/key.ui/examples/standard_key/polymorphic/setExample.key @@ -0,0 +1,9 @@ +\sorts { + T; +} + +\problem { + \forall Set<[T]> s1; (\forall Set<[T]> s2; + (sIntersect<[T]>(s1, s2) = sEmpty<[T]> <-> + (\forall T a; (sElementOf<[T]>(a, s1) -> !sElementOf<[T]>(a, s2))))) +}