Confine set induction to outer proofs

5 files changed, 92 insertions, 13 deletions

diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs
index 358ba70..afdc45b 100644
--- a/source/Checking/Exact/Proof.hs
+++ b/source/Checking/Exact/Proof.hs
@@ -55,6 +55,7 @@ data ExactProofError
     | ExactProofSetInductionVariableRequired !Location
     | ExactProofSetInductionVariableNotActive
         !Location !Raw.VarSymbol
+    | ExactProofSetInductionNotOutermost !Location
     | ExactProofSetInductionGoalMismatch !Location
     | ExactProofSetExtensionalityGoalMismatch !Location
     | ExactProofSetExtensionalityDirectionsUnavailable !Location
@@ -81,6 +82,7 @@ exactProofErrorLocation = \case
     ExactProofSetInductionVariableRequired location -> location
     ExactProofSetInductionVariableNotActive location _variable ->
         location
+    ExactProofSetInductionNotOutermost location -> location
     ExactProofSetInductionGoalMismatch location -> location
     ExactProofSetExtensionalityGoalMismatch location -> location
     ExactProofSetExtensionalityDirectionsUnavailable location -> location
@@ -110,6 +112,8 @@ renderExactProofError = \case
     ExactProofSetInductionVariableNotActive location variable ->
         at location <> "the set-induction variable " <> shown variable
             <> " is not an active exact binder"
+    ExactProofSetInductionNotOutermost location ->
+        at location <> "set induction must currently be outermost"
     ExactProofSetInductionGoalMismatch location ->
         at location <> "the set-induction variable does not belong to this goal"
     ExactProofSetExtensionalityGoalMismatch location ->
@@ -284,7 +288,7 @@ prepareExactProof block explicitProof =
                                 location
                                 context
                                 locals
-                                antecedents
+                                (Just antecedents)
                                 bodyGoal
                                 sourceProof
                 let withAssumptions =
@@ -441,7 +445,8 @@ prepareProof
     :: Location
     -> Exact.ExactBinderContext
     -> [PreparedLocal]
-    -> [ScopedCheckedCore ObjectId]
+    -- Only the initial proof carries set-induction antecedents.
+    -> Maybe [ScopedCheckedCore ObjectId]
     -> ScopedCheckedCore ObjectId
     -> Raw.Proof
     -> Prepare failure PreparedProof
@@ -467,7 +472,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 fallback
                 context'
                 locals
-                []
+                Nothing
                 goal'
                 continuation
     Raw.Assume location statement continuation -> do
@@ -489,7 +494,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 fallback
                 context
                 (locals <> [local])
-                []
+                Nothing
                 conclusion
                 continuation
     Raw.TakeVar location variables bound statement justification continuation -> do
@@ -520,12 +525,15 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 fallback
                 context'
                 (locals <> [local])
-                []
+                Nothing
                 goal'
                 continuation
     Raw.BySetInduction location variable continuation ->
-        case continuation of
-            Raw.Qed maybeLocation justification -> do
+        case (inductionAntecedents, continuation) of
+            (Nothing, _proof) ->
+                throwProof
+                    (ExactProofSetInductionNotOutermost location)
+            (Just antecedents, Raw.Qed maybeLocation justification) -> do
                 sourceVariable <-
                     case variable of
                         Just (Raw.TermExpr (Raw.ExprVar candidate)) ->
@@ -544,7 +552,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                         (Exact.exactBinderContextIndex
                             sourceVariable context)
                 let property =
-                        foldr implyChecked goal inductionAntecedents
+                        foldr implyChecked goal antecedents
                 hypothesis <-
                     maybe
                         (throwProof
@@ -560,7 +568,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                         (locals <> [local])
                         goal
                         justification
-            _ ->
+            (Just _antecedents, _proof) ->
                 throwProof (ExactProofUnsupportedStep location)
     Raw.Have location since statement justification continuation -> do
         when (isJust since)
@@ -577,7 +585,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 fallback
                 context
                 (locals <> [local])
-                []
+                Nothing
                 goal
                 continuation
     Raw.Subclaim location statement subproof continuation -> do
@@ -589,7 +597,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 location
                 context
                 locals
-                []
+                Nothing
                 claim
                 subproof
         local <- allocateLocal ExactDerivedClaim context claim
@@ -598,7 +606,7 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 fallback
                 context
                 (locals <> [local])
-                []
+                Nothing
                 goal
                 continuation
     proof ->
diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs
index e6c596c..0ef5698 100644
--- a/source/Felix/Cache/Codec.hs
+++ b/source/Felix/Cache/Codec.hs
@@ -75,7 +75,7 @@ newtype CacheEpoch = CacheEpoch Word32
 
 currentCacheEpoch :: CacheEpoch
 currentCacheEpoch =
-    CacheEpoch 12
+    CacheEpoch 13
 
 cacheEpochValue :: CacheEpoch -> Word32
 cacheEpochValue (CacheEpoch value) =
diff --git a/source/Felix/Migration.hs b/source/Felix/Migration.hs
index bf25790..0633cba 100644
--- a/source/Felix/Migration.hs
+++ b/source/Felix/Migration.hs
@@ -180,6 +180,7 @@ typedMigrationModules =
         , migrationProjectModule "test/phase5/exact-failure.tex"
         , migrationProjectModule "test/phase5/exact-proofs.tex"
         , migrationProjectModule "test/phase5/exact-proof-failure.tex"
+        , migrationProjectModule "test/phase5/exact-induction-nested.tex"
         , migrationProjectModule "test/phase5/exact-runtime-failure.tex"
         , migrationProjectModule "test/phase5/exact-source-axiom.tex"
         , migrationProjectModule "test/phase5/exact-source-axiom-assumptions.tex"
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