Confine set induction to outer proofs

2 files changed, 70 insertions, 0 deletions

diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs
index 2d99f6d..7cf14b0 100644
--- a/source/Test/Unit/Core.hs
+++ b/source/Test/Unit/Core.hs
@@ -44,6 +44,9 @@ unitTests =
             "checks scoped canonical weakening and substitution"
             checksScopedCanonicalOperations
         , testCase
+            "builds set-induction hypotheses from the complete property"
+            buildsSetInductionHypotheses
+        , testCase
             "thaws checked closed terms without changing them"
             thawsCheckedClosedTerms
         , testPropertyNamed
@@ -252,6 +255,45 @@ checksScopedCanonicalOperations = do
             <$> closeScopedCore root
         )
 
+buildsSetInductionHypotheses :: Assertion
+buildsSetInductionHypotheses = do
+    claimProperty <-
+        either
+            (assertFailure . show)
+            pure
+            (checkScopedCanonicalCore
+                testGlobalType
+                [TySet]
+                (CImp
+                    (CEq TySet
+                        (CBound 0)
+                        (CIntrinsic Empty))
+                    (CEq TySet
+                        (CBound 0)
+                        (CBound 0))))
+    hypothesis <-
+        maybe
+            (assertFailure "set-induction hypothesis was not constructed")
+            pure
+            (scopedSetInductionHypothesis 0 claimProperty)
+    assertEqual
+        "antecedent and goal are both generalized over the member"
+        (CForall TySet
+            (CImp
+                (CApp
+                    (CApp
+                        (CIntrinsic Member)
+                        (CBound 0))
+                    (CBound 1))
+                (CImp
+                    (CEq TySet
+                        (CBound 0)
+                        (CIntrinsic Empty))
+                    (CEq TySet
+                        (CBound 0)
+                        (CBound 0)))))
+        (scopedCoreTerm hypothesis)
+
 thawsCheckedClosedTerms :: Assertion
 thawsCheckedClosedTerms = do
     let source =
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index c73029c..b8a7854 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -116,6 +116,8 @@ unitTests =
             doesNotTreatMarkerOnlyNounAsSet
         , testCase "rejects proof-local generalization"
             rejectsProofLocalGeneralization
+        , testCase "rejects nested exact set induction"
+            rejectsNestedExactSetInduction
         , testCase "compiles exact omitted proofs"
             compilesExactOmittedProofs
         , testCase "propagates and reuses exact escape authority"
@@ -3732,6 +3734,32 @@ retainsExactPrefixBeforeFailure = do
         _result ->
             assertFailure "unexpected runtime proof failure"
 
+rejectsNestedExactSetInduction :: Assertion
+rejectsNestedExactSetInduction = do
+    result <-
+        withAcceptedFixtureVampire "felix-nested-set-induction" \prover ->
+            runNoLoggingT
+                (Api.verifyMeasured
+                    prover
+                    "test/phase5/exact-induction-nested.tex")
+    case result of
+        Left
+            (Api.VerificationTypedModuleError
+                _source
+                (Module.TypedActionFailed
+                    (Module.TypedExactProofFailed
+                        (ExactProof.ExactProofSetInductionNotOutermost
+                            location)))
+                prefix) -> do
+            assertEqual "nested induction line" 7 (locLine location)
+            assertBool "failed proof publishes no theorem"
+                (null (Declaration.pendingModulePrefixBatches prefix))
+        Left err ->
+            assertFailure
+                ("unexpected nested-induction failure: " <> show err)
+        Right{} ->
+            assertFailure "nested exact set induction was admitted"
+
 routesProductionVerification :: Assertion
 routesProductionVerification =
     Temp.withSystemTempDirectory "felix-production-route" \directory -> do