Use semantic subset formula inside inductive defns

1 files changed, 15 insertions, 18 deletions

diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs
index a5ee61a..cea5873 100644
--- a/source/Test/Unit/Checking.hs
+++ b/source/Test/Unit/Checking.hs
@@ -103,7 +103,9 @@ unitTests = testGroup "Checking"
         expectChecks inductiveInductReferenceBlocks
     , testCase "inductive generates monotonicity obligations for recursive carriers" do
         text <- encodedTasksText goodMonotoneInductiveBlocks
-        assertContains "monotonicity task for wrapped carrier" "subseteq(wrap(Xxa),wrap(Xxb))" text
+        assertContains "monotonicity antecedent expands subset" "elem(Xx1,Xxa)=>elem(Xx1,Xxb)" text
+        assertContains "monotonicity conclusion expands subset" "elem(Xx1,wrap(Xxa))=>elem(Xx1,wrap(Xxb))" text
+        assertNotContains "monotonicity task avoids subseteq" "subseteq(" text
     , testCase "inductive rejects recursive premises outside carrier positions" do
         expectCheckingError "carrier of a membership premise" [badRecursiveTermInductiveBlock]
     , testCase "inductive rejects malformed recursive premises" do
@@ -463,8 +465,7 @@ goodInductiveBlock =
 
 goodInductiveBlocks :: [Block]
 goodInductiveBlocks =
-    [ subseteqDefinitionBlock
-    , goodInductiveBlock
+    [ goodInductiveBlock
     ]
 
 goodMonotoneInductiveBlock :: Block
@@ -482,8 +483,7 @@ goodMonotoneInductiveBlock =
 
 goodMonotoneInductiveBlocks :: [Block]
 goodMonotoneInductiveBlocks =
-    [ subseteqDefinitionBlock
-    , wrapSignatureBlock
+    [ wrapSignatureBlock
     , goodMonotoneInductiveBlock
     ]
 
@@ -504,7 +504,9 @@ inductiveIntroAndDomainReferenceBlocks =
     , BlockProof Nowhere Nowhere
         (Qed (Just Nowhere) (JustificationRef ("fin_intro_1" :| [])))
     , BlockLemma Nowhere "inductive_dom_subset_ref"
-        (Lemma [] (makeForall ["A"] (IsSubsetOf Nowhere (finTerm (var "A")) (powTerm (var "A")))))
+        (Lemma [] $
+            makeForall ["A"] $
+                semanticSubsetFormula (Set.fromList ["A"]) (finTerm (var "A")) (powTerm (var "A")))
     , BlockProof Nowhere Nowhere
         (Qed (Just Nowhere) (JustificationRef ("fin_dom_subset" :| [])))
     ]
@@ -647,8 +649,7 @@ datatypeConstructorThenOperatorBlocks =
 
 frozenSymbolDefinitionBlocks :: [Block]
 frozenSymbolDefinitionBlocks =
-    [ subseteqDefinitionBlock
-    , laterSignatureBlock
+    [ laterSignatureBlock
     , freezingInductiveBlock
     , BlockDefn Nowhere "later_operator_definition" (DefnOp laterSym ["A"] emptySet)
     ]
@@ -668,8 +669,7 @@ freezingInductiveBlock =
 
 canonicalizedDomainFreezeBlocks :: [Block]
 canonicalizedDomainFreezeBlocks =
-    [ subseteqDefinitionBlock
-    , laterSignatureBlock
+    [ laterSignatureBlock
     , BlockAbbr Nowhere "domain_alias_abbr"
         (Abbreviation
             (SymbolMixfix domainAliasSym)
@@ -686,8 +686,7 @@ canonicalizedDomainFreezeBlocks =
 
 transitiveFrozenDefinitionBlocks :: [Block]
 transitiveFrozenDefinitionBlocks =
-    [ subseteqDefinitionBlock
-    , laterSignatureBlock
+    [ laterSignatureBlock
     , BlockDefn Nowhere "middle_later_alias_definition" (DefnOp middleLaterAliasSym ["A"] (laterTerm (var "A")))
     , BlockDefn Nowhere "indirect_later_alias_definition" (DefnOp indirectLaterAliasSym ["A"] (middleLaterAliasTerm (var "A")))
     , BlockInductive Nowhere "transitive_freeze_inductive" Inductive
@@ -779,7 +778,10 @@ finInductFormula =
                     (consTerm (var "a") (var "B") `isElementOf` var "S"))
             ]
             `Implies`
-            IsSubsetOf Nowhere (finTerm (var "A")) (var "S"))
+            semanticSubsetFormula
+                (Set.fromList ["A", "S"])
+                (finTerm (var "A"))
+                (var "S"))
 
 goodDatatypeClauses :: NonEmpty DatatypeClause
 goodDatatypeClauses =
@@ -874,11 +876,6 @@ propformSignatureFormula =
     makeForall ["z"]
         ((var "z" `eq` propformTerm) `Implies` (var "z" `eq` var "z"))
 
-subseteqDefinitionBlock :: Block
-subseteqDefinitionBlock =
-    BlockDefn Nowhere "subseteq_definition"
-        (DefnPredicate [] (PredicateRelation SubseteqSymbol) ("A" :| ["B"]) (var "A" `eq` var "B"))
-
 wrapSignatureBlock :: Block
 wrapSignatureBlock =
     mixfixSignatureBlock "wrap_signature" wrapSym ["A"]