Use semantic subset formula inside inductive defns

3 files changed, 45 insertions, 24 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index f1f29c4..f80e164 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -1992,6 +1992,13 @@ inductiveConditionFormulaAt _ replacement = \case
     CheckedInductiveRecursiveCondition{checkedInductiveRecursiveTerm, checkedInductiveRecursiveCarrierTemplate} ->
         isElementOf checkedInductiveRecursiveTerm (instantiate1 replacement checkedInductiveRecursiveCarrierTemplate)
 
+semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula
+semanticSubsetFormula reserved left right =
+    makeForall [witnessVar]
+        (isElementOf (TermVar witnessVar) left `Implies` isElementOf (TermVar witnessVar) right)
+    where
+        witnessVar = freshGeneratedVar (reserved <> freeVars left <> freeVars right) "x"
+
 inductiveSoundnessGoals :: CheckedInductive -> [Formula]
 inductiveSoundnessGoals checked =
     inductiveMonotonicityGoals checked <> inductiveDomainGoals checked
@@ -1999,9 +2006,9 @@ inductiveSoundnessGoals checked =
 inductiveMonotonicityGoals :: CheckedInductive -> [Formula]
 inductiveMonotonicityGoals checked =
     [ forallIfNeeded [leftVar, rightVar]
-        ( IsSubsetOf Nowhere (TermVar leftVar) (TermVar rightVar)
+        ( semanticSubsetFormula usedVars (TermVar leftVar) (TermVar rightVar)
             `Implies`
-            IsSubsetOf Nowhere
+            semanticSubsetFormula usedVars
                 (instantiate1 (TermVar leftVar) checkedInductiveRecursiveCarrierTemplate)
                 (instantiate1 (TermVar rightVar) checkedInductiveRecursiveCarrierTemplate)
         )
@@ -2067,7 +2074,8 @@ inductiveIntroFormula checked intro =
 
 inductiveDomSubsetFormula :: CheckedInductive -> Formula
 inductiveDomSubsetFormula checked =
-    forallIfNeeded (checkedInductiveParams checked) (IsSubsetOf Nowhere (inductiveCarrierTerm checked) (checkedInductiveDomain checked))
+    forallIfNeeded (checkedInductiveParams checked)
+        (semanticSubsetFormula (inductiveUsedVars checked) (inductiveCarrierTerm checked) (checkedInductiveDomain checked))
 
 inductiveCasesFormula :: CheckedInductive -> Formula
 inductiveCasesFormula checked =
@@ -2092,7 +2100,11 @@ inductiveInductFormula checked =
     where
         subsetVar = freshGeneratedVar (inductiveUsedVars checked) "S"
         closures = inductiveInductionClosure checked subsetVar <$> NonEmpty.toList (checkedInductiveIntros checked)
-        conclusion = IsSubsetOf Nowhere (inductiveCarrierTerm checked) (TermVar subsetVar)
+        conclusion =
+            semanticSubsetFormula
+                (Set.insert subsetVar (inductiveUsedVars checked))
+                (inductiveCarrierTerm checked)
+                (TermVar subsetVar)
 
 inductiveInductionClosure :: CheckedInductive -> VarSymbol -> CheckedInductiveIntro -> Formula
 inductiveInductionClosure checked subsetVar intro =
diff --git a/source/Render/Html.hs b/source/Render/Html.hs
index 90bef42..a45f422 100644
--- a/source/Render/Html.hs
+++ b/source/Render/Html.hs
@@ -2112,6 +2112,15 @@ elementOfFormula :: Expr -> Expr -> Formula
 elementOfFormula left right =
     FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere ElementSymbol []) (right :| []))
 
+semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula
+semanticSubsetFormula reserved left right =
+    forallIfNeeded [witnessVar]
+        (impliesFormula
+            (elementOfFormula (ExprVar witnessVar) left)
+            (elementOfFormula (ExprVar witnessVar) right))
+    where
+        witnessVar = freshDatatypeVar (reserved <> Set.fromList (exprVars left <> exprVars right)) "x"
+
 equalsFormula :: Expr -> Expr -> Formula
 equalsFormula left right =
     FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere EqSymbol []) (right :| []))
@@ -2331,7 +2340,7 @@ inductiveIntroFormula info clause =
 inductiveDomSubsetFormula :: InductiveRenderInfo -> Formula
 inductiveDomSubsetFormula info =
     forallIfNeeded (inductiveRenderParams info)
-        (FormulaChain (ChainBase (inductiveRenderCarrierExpr info :| []) Positive (Relation Nowhere SubseteqSymbol []) (inductiveRenderDomainExpr info :| [])))
+        (semanticSubsetFormula (inductiveUsedVars info) (inductiveRenderCarrierExpr info) (inductiveRenderDomainExpr info))
 
 inductiveCasesFormula :: InductiveRenderInfo -> Formula
 inductiveCasesFormula info =
@@ -2354,7 +2363,10 @@ inductiveInductFormula info =
         subsetVar = freshDatatypeVar (inductiveUsedVars info) "S"
         closures = inductiveInductionClosure subsetVar <$> NonEmpty.toList (inductiveRenderClauses info)
         conclusion =
-            FormulaChain (ChainBase (inductiveRenderCarrierExpr info :| []) Positive (Relation Nowhere SubseteqSymbol []) (ExprVar subsetVar :| []))
+            semanticSubsetFormula
+                (Set.insert subsetVar (inductiveUsedVars info))
+                (inductiveRenderCarrierExpr info)
+                (ExprVar subsetVar)
 
 inductiveInductionClosure :: VarSymbol -> InductiveRenderClause -> Formula
 inductiveInductionClosure subsetVar clause =
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"]