Merge pull request #2975 from lemmy/mku-ExprOptimizerSubset

ExprOptimizer: Rewrite `S \in SUBSET T` when it occurs in subexpressions

.unreleased/features/rewrite.md

@@ -0,0 +1 @@
+Handle expressions such as  S \in SUBSET T  in ExprOptimizer by rewriting the expression into  \A r \in S: r \in T

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala

@@ -93,7 +93,7 @@ class ExprOptimizer(nameGen: UniqueNameGenerator, tracker: TransformationTracker
         val b = BoolT1
         val domEq = tla.eql(tla.dom(rec).as(strSetT), tla.enumSet(fields: _*).as(strSetT)).as(b)
         val fieldsEq = fields.zip(values.zip(sets)).map { case (key, (value, set)) =>
-          tla.in(tla.appFun(rec, key).as(value.typeTag.asTlaType1()), set).as(b)
+          apply(tla.in(tla.appFun(rec, key).as(value.typeTag.asTlaType1()), set).as(b))
         }
         apply(tla.and(domEq +: fieldsEq: _*).as(b))
       }
@@ -121,10 +121,15 @@ class ExprOptimizer(nameGen: UniqueNameGenerator, tracker: TransformationTracker
         val domEq = tla.eql(tla.dom(r).as(SetT1(domType)), tla.enumSet(fields: _*).as(strSetT)).as(b)
 
         val fieldsEq = fields.zip(values.zip(sets)).map { case (key, (value, set)) =>
-          tla.in(tla.appFun(r, key).as(value.typeTag.asTlaType1()), set).as(b)
+          apply(tla.in(tla.appFun(r, key).as(value.typeTag.asTlaType1()), set).as(b))
         }
         apply(tla.forall(r, setRec, tla.and(domEq +: fieldsEq: _*).as(b)).as(b))
       }
+
+    // S ∈ SUBSET T ~~> ∀ s ∈ S: s ∈ T
+    case OperEx(TlaSetOper.in, lSet, OperEx(TlaSetOper.powerset, rSet)) =>
+      val lMem = tla.name(nameGen.newName()).as(getElemType(lSet))
+      apply(tla.forall(lMem, lSet, tla.in(lMem, apply(rSet)).as(BoolT1)).as(BoolT1))
   }
 
   /**

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala

@@ -184,6 +184,19 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach {
     assert(expected == output)
   }
 
+  test("""S \in SUBSET T ~~> \A s \in S: s \in T""") {
+    val T = name("T").as(intSetT)
+    val S = name("S").as(intSetT)
+    val powSetT = powSet(T).as(intSetT)
+    val input = in(S, powSetT).as(boolT)
+    val output = optimizer.apply(input)
+
+    val s = name("t_1").as(intT)
+    val expected = forall(s, S, in(s, T).as(boolT)).as(boolT)
+
+    assert(expected == output)
+  }
+
   // optimizations for set cardinalities
 
   test("""Cardinality(S) = 0 becomes S = {}""") {