Migrate to `Felix` namespaceHEADhotg

1 files changed, 1443 insertions, 0 deletions

diff --git a/source/Felix/Checking/Kernel/Proof.hs b/source/Felix/Checking/Kernel/Proof.hs
new file mode 100644
index 0000000..d4ccedc
--- /dev/null
+++ b/source/Felix/Checking/Kernel/Proof.hs
@@ -0,0 +1,1443 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Small proof-producing natural-deduction combinators. Every resulting tree
+-- is still replayed independently before it can authorize a fact.
+module Felix.Checking.Kernel.Proof
+    ( ProofContext
+    , rootProofContext
+    , proofContextTypes
+    , scopedTerm
+    , BuiltProof
+    , builtProofStatement
+    , builtProofDerivation
+    , importedProof
+    , foundationProof
+    , hypothesisProof
+    , implicationEliminationProof
+    , implicationIntroductionProof
+    , forallEliminationProof
+    , forallIntroductionProof
+    , falsumEliminationProof
+    , equalityReflexivityProof
+    , equalityReverseProof
+    , equalityCongruenceApplicationProof
+    , equalityModusPonensProof
+    , conversionProof
+    , doubleNegationEliminationProof
+    , conjunctionTerm
+    , conjunctionIntroductionProof
+    , conjunctionLeftProof
+    , conjunctionRightProof
+    , disjunctionTerm
+    , disjunctionLeftProof
+    , disjunctionRightProof
+    , disjunctionEliminationProof
+    , validateCaseAnalysisComposition
+    , validateDoubleNegationComposition
+    , validateFalsumEliminationComposition
+    , validateSetInductionComposition
+    , existentialTerm
+    , existentialIntroductionProof
+    , existentialEliminationProof
+    , setLfpBoundProof
+    , setLfpFixedProof
+    , setLfpInductProof
+    , KernelProofBuildError(..)
+    ) where
+
+import Base
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+import Felix.Checking.Kernel.Derivation
+import Felix.Checking.Kernel.Semantics qualified as Semantics
+import Felix.Checking.Kernel.SetLfp qualified as SetLfp
+
+import Control.Monad (unless)
+import Data.Bifunctor (first)
+import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Text qualified as Text
+import Numeric.Natural (Natural)
+
+
+data ProofContext global = ProofContext
+    !CheckedFoundation
+    !(global -> Maybe CoreType)
+    ![CoreType]
+    ![ScopedCheckedCore global]
+
+rootProofContext
+    :: CheckedFoundation
+    -> (global -> Maybe CoreType)
+    -> ProofContext global
+rootProofContext foundation globalType =
+    ProofContext foundation globalType [] []
+
+proofContextTypes
+    :: ProofContext global
+    -> [CoreType]
+proofContextTypes
+        (ProofContext
+            _foundation
+            _globalType
+            context
+            _hypotheses) =
+    context
+
+data BuiltProof global = BuiltProof
+    !(ScopedCheckedCore global)
+    !(KernelDerivation global)
+
+builtProofStatement
+    :: BuiltProof global
+    -> ScopedCheckedCore global
+builtProofStatement
+        (BuiltProof statement _derivation) =
+    statement
+
+builtProofDerivation
+    :: BuiltProof global
+    -> KernelDerivation global
+builtProofDerivation
+        (BuiltProof _statement derivation) =
+    derivation
+
+data KernelProofBuildError
+    = ProofTermIllTyped !CoreCheckError
+    | ProofSemanticsFailed
+        !Semantics.KernelSemanticsError
+    | ProofFoundationArgumentMismatch
+        !FoundationAxiomTag
+    | ProofHypothesisNotFound
+    | ProofExpectedEquality
+    | ProofExpectedUnaryBinder
+    | ProofSetLfpRuleFailed !Text
+    | ProofConversionPlanFailed !Text
+    | ProofStructuralCompositionMismatch !Text
+    deriving stock (Show, Eq)
+
+scopedTerm
+    :: ProofContext global
+    -> CanonicalTerm global
+    -> Either
+        KernelProofBuildError
+        (ScopedCheckedCore global)
+scopedTerm
+        (ProofContext
+            _foundation
+            globalType
+            context
+            _hypotheses) =
+    first ProofTermIllTyped
+        . checkScopedCanonicalCore
+            globalType
+            context
+
+importedProof
+    :: ProofContext global
+    -> ImportIx
+    -> FrozenCheckedCore global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+importedProof context index statement =
+    pure
+        (BuiltProof
+            (embedClosedCore
+                (proofContextTypes context)
+                statement)
+            (importedFactDerivation index))
+
+foundationProof
+    :: ProofContext global
+    -> FoundationAxiomTag
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+foundationProof
+        context@(ProofContext
+            foundation
+            _globalType
+            _types
+            _hypotheses)
+        tag =
+    pure
+        (BuiltProof
+            (embedClosedCore
+                (proofContextTypes context)
+                (mapFrozenGlobals
+                    absurd
+                    (foundationAxiomFrozen
+                        foundation
+                        tag)))
+            (foundationFactDerivation tag))
+
+hypothesisProof
+    :: Eq global
+    => ProofContext global
+    -> ScopedCheckedCore global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+hypothesisProof
+        (ProofContext
+            _foundation
+            _globalType
+            _context
+            hypotheses)
+        statement =
+    case List.findIndex (== statement) hypotheses of
+        Nothing ->
+            Left ProofHypothesisNotFound
+        Just index ->
+            pure
+                (BuiltProof
+                    statement
+                    (localHypothesisDerivation
+                        (hypothesisIx
+                            (fromIntegral index))))
+
+implicationEliminationProof
+    :: Eq global
+    => ProofContext global
+    -> BuiltProof global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+implicationEliminationProof
+        (ProofContext
+            _foundation
+            globalType
+            _context
+            _hypotheses)
+        implication
+        premise = do
+    conclusion <-
+        first ProofSemanticsFailed
+            (Semantics.implicationElimination
+                globalType
+                (builtProofStatement implication)
+                (builtProofStatement premise))
+    pure
+        (BuiltProof
+            conclusion
+            (implicationEliminationDerivation
+                (builtProofDerivation implication)
+                (builtProofDerivation premise)))
+
+implicationIntroductionProof
+    :: ProofContext global
+    -> ScopedCheckedCore global
+    -> ( ProofContext global
+         -> BuiltProof global
+         -> Either
+            KernelProofBuildError
+            (BuiltProof global)
+       )
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+implicationIntroductionProof
+        (ProofContext
+            foundation
+            globalType
+            types
+            hypotheses)
+        premise
+        buildBody = do
+    let extended =
+            ProofContext
+                foundation
+                globalType
+                types
+                (premise : hypotheses)
+        premiseProof =
+            BuiltProof
+                premise
+                (localHypothesisDerivation
+                    (hypothesisIx 0))
+    body <-
+        buildBody extended premiseProof
+    conclusion <-
+        first ProofSemanticsFailed
+            (Semantics.implicationIntroduction
+                globalType
+                premise
+                (builtProofStatement body))
+    pure
+        (BuiltProof
+            conclusion
+            (implicationIntroductionDerivation
+                premise
+                (builtProofDerivation body)))
+
+forallEliminationProof
+    :: ProofContext global
+    -> BuiltProof global
+    -> ScopedCheckedCore global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+forallEliminationProof
+        (ProofContext
+            _foundation
+            globalType
+            _types
+            _hypotheses)
+        quantified
+        argument = do
+    conclusion <-
+        first ProofSemanticsFailed
+            (Semantics.forallElimination
+                globalType
+                (builtProofStatement quantified)
+                argument)
+    pure
+        (BuiltProof
+            conclusion
+            (forallEliminationDerivation
+                (builtProofDerivation quantified)
+                argument))
+
+forallIntroductionProof
+    :: ProofContext global
+    -> CoreType
+    -> ( ProofContext global
+         -> ScopedCheckedCore global
+         -> Either
+            KernelProofBuildError
+            (BuiltProof global)
+       )
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+forallIntroductionProof
+        (ProofContext
+            foundation
+            globalType
+            types
+            hypotheses)
+        binderType
+        buildBody = do
+    weakenedHypotheses <-
+        traverse
+            (first ProofTermIllTyped
+                . weakenScopedCore
+                    globalType
+                    binderType)
+            hypotheses
+    let extended =
+            ProofContext
+                foundation
+                globalType
+                (binderType : types)
+                weakenedHypotheses
+    variable <-
+        scopedTerm extended (CBound 0)
+    body <-
+        buildBody extended variable
+    conclusion <-
+        first ProofSemanticsFailed
+            (Semantics.forallIntroduction
+                globalType
+                binderType
+                (builtProofStatement body))
+    pure
+        (BuiltProof
+            conclusion
+            (forallIntroductionDerivation
+                binderType
+                (builtProofDerivation body)))
+
+falsumEliminationProof
+    :: ProofContext global
+    -> BuiltProof global
+    -> ScopedCheckedCore global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+falsumEliminationProof
+        (ProofContext
+            _foundation
+            globalType
+            _types
+            _hypotheses)
+        falsum
+        target = do
+    conclusion <-
+        first ProofSemanticsFailed
+            (Semantics.falsumElimination
+                globalType
+                (builtProofStatement falsum)
+                target)
+    pure
+        (BuiltProof
+            conclusion
+            (falsumEliminationDerivation
+                (builtProofDerivation falsum)
+                target))
+
+equalityReflexivityProof
+    :: ProofContext global
+    -> ScopedCheckedCore global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+equalityReflexivityProof
+        (ProofContext
+            _foundation
+            globalType
+            _types
+            _hypotheses)
+        operand = do
+    equality <-
+        first ProofSemanticsFailed
+            (Semantics.equalityReflexivity
+                globalType
+                operand)
+    pure
+        (BuiltProof
+            equality
+            (scopedEqualityReflexivityDerivation
+                operand))
+
+equalityCongruenceApplicationProof
+    :: ProofContext global
+    -> BuiltProof global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+equalityCongruenceApplicationProof
+        (ProofContext
+            _foundation
+            globalType
+            _types
+            _hypotheses)
+        functionEquality
+        argumentEquality = do
+    equality <-
+        first ProofSemanticsFailed
+            (Semantics.equalityCongruenceApplication
+                globalType
+                (builtProofStatement functionEquality)
+                (builtProofStatement argumentEquality))
+    pure
+        (BuiltProof
+            equality
+            (equalityCongruenceApplicationDerivation
+                (builtProofDerivation
+                    functionEquality)
+                (builtProofDerivation
+                    argumentEquality)))
+
+equalityModusPonensProof
+    :: Eq global
+    => ProofContext global
+    -> BuiltProof global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+equalityModusPonensProof
+        (ProofContext
+            _foundation
+            globalType
+            _types
+            _hypotheses)
+        equality
+        premise = do
+    conclusion <-
+        first ProofSemanticsFailed
+            (Semantics.equalityModusPonens
+                globalType
+                (builtProofStatement equality)
+                (builtProofStatement premise))
+    pure
+        (BuiltProof
+            conclusion
+            (equalityModusPonensDerivation
+                (builtProofDerivation equality)
+                (builtProofDerivation premise)))
+
+conversionProof
+    :: Eq global
+    => ProofContext global
+    -> BuiltProof global
+    -> ScopedCheckedCore global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+conversionProof
+        (ProofContext
+            _foundation
+            globalType
+            _types
+            _hypotheses)
+        source
+        target = do
+    plan <-
+        first (ProofConversionPlanFailed . Text.pack . show)
+            (conversionPlan 100000)
+    result <-
+        first ProofSemanticsFailed
+            (Semantics.convertJudgment
+                globalType
+                (conversionPlanBudget plan)
+                (builtProofStatement source)
+                target)
+    pure
+        (BuiltProof
+            result
+            (convertJudgmentDerivation
+                (builtProofDerivation source)
+                target
+                plan))
+
+equalityReverseProof
+    :: Eq global
+    => ProofContext global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+equalityReverseProof context equality = do
+    (operandType, left, right) <-
+        equalityParts
+            (builtProofStatement equality)
+    leftOperand <-
+        scopedTerm context left
+    weakenedLeft <-
+        first ProofTermIllTyped
+            (weakenScopedCore
+                (contextGlobalType context)
+                operandType
+                leftOperand)
+    function <-
+        scopedTerm context
+            (CLam operandType
+                (CEq
+                    operandType
+                    (CBound 0)
+                    (scopedCoreTerm
+                        weakenedLeft)))
+    functionReflexivity <-
+        equalityReflexivityProof
+            context
+            function
+    appliedEquality <-
+        equalityCongruenceApplicationProof
+            context
+            functionReflexivity
+            equality
+    leftReflexivity <-
+        equalityReflexivityProof
+            context
+            leftOperand
+    appliedLeft <-
+        scopedTerm context
+            (CApp
+                (scopedCoreTerm function)
+                left)
+    appliedLeftReflexivity <-
+        conversionProof
+            context
+            leftReflexivity
+            appliedLeft
+    reversedApplication <-
+        equalityModusPonensProof
+            context
+            appliedEquality
+            appliedLeftReflexivity
+    expected <-
+        scopedTerm context
+            (CEq operandType right left)
+    conversionProof
+        context
+        reversedApplication
+        expected
+
+doubleNegationEliminationProof
+    :: Eq global
+    => ProofContext global
+    -> ScopedCheckedCore global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+doubleNegationEliminationProof
+        context
+        target
+        doubleNegation = do
+    axiom <-
+        foundationProof
+            context
+            DoubleNegationElim
+    instanceProof <-
+        forallEliminationProof
+            context
+            axiom
+            target
+    implicationEliminationProof
+        context
+        instanceProof
+        doubleNegation
+
+conjunctionTerm
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+conjunctionTerm left right =
+    CImp
+        (CImp left
+            (CImp right CFalsum))
+        CFalsum
+
+conjunctionIntroductionProof
+    :: Eq global
+    => ProofContext global
+    -> BuiltProof global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+conjunctionIntroductionProof
+        context
+        left
+        right = do
+    let leftTerm =
+            scopedCoreTerm
+                (builtProofStatement left)
+        rightTerm =
+            scopedCoreTerm
+                (builtProofStatement right)
+    refuter <-
+        scopedTerm context
+            (CImp leftTerm
+                (CImp rightTerm CFalsum))
+    implicationIntroductionProof
+        context
+        refuter
+        (\extended refuterProof -> do
+            firstApplication <-
+                implicationEliminationProof
+                    extended
+                    refuterProof
+                    (weakenForHypothesis left)
+            implicationEliminationProof
+                extended
+                firstApplication
+                (weakenForHypothesis right))
+
+conjunctionLeftProof
+    :: Eq global
+    => ProofContext global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+conjunctionLeftProof context left right conjunction = do
+    leftProposition <-
+        scopedTerm context left
+    notLeft <-
+        scopedTerm context
+            (CImp left CFalsum)
+    doubleNegation <-
+        implicationIntroductionProof
+            context
+            notLeft
+            (\withNotLeft _notLeftProof -> do
+                leftAtRefuter <-
+                    scopedTerm withNotLeft left
+                refuterProof <-
+                    implicationIntroductionProof
+                        withNotLeft
+                        leftAtRefuter
+                        (\withLeft leftProof -> do
+                            rightProposition <-
+                                scopedTerm withLeft right
+                            implicationIntroductionProof
+                                withLeft
+                                rightProposition
+                                (\withBoth _rightProof -> do
+                                    notLeftCurrent <-
+                                        hypothesisProof
+                                            withBoth
+                                            notLeft
+                                    implicationEliminationProof
+                                        withBoth
+                                        notLeftCurrent
+                                        (weakenForHypothesis
+                                            leftProof)))
+                implicationEliminationProof
+                    withNotLeft
+                    (weakenForHypothesis conjunction)
+                    refuterProof)
+    doubleNegationEliminationProof
+        context
+        leftProposition
+        doubleNegation
+
+conjunctionRightProof
+    :: Eq global
+    => ProofContext global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+conjunctionRightProof context left right conjunction = do
+    rightProposition <-
+        scopedTerm context right
+    notRight <-
+        scopedTerm context
+            (CImp right CFalsum)
+    doubleNegation <-
+        implicationIntroductionProof
+            context
+            notRight
+            (\withNotRight _notRightProof -> do
+                leftAtRefuter <-
+                    scopedTerm withNotRight left
+                refuterProof <-
+                    implicationIntroductionProof
+                        withNotRight
+                        leftAtRefuter
+                        (\withLeft _leftProof -> do
+                            rightAtLeft <-
+                                scopedTerm
+                                    withLeft
+                                    right
+                            implicationIntroductionProof
+                                withLeft
+                                rightAtLeft
+                                (\withBoth rightProof -> do
+                                    notRightCurrent <-
+                                        hypothesisProof
+                                            withBoth
+                                            notRight
+                                    implicationEliminationProof
+                                        withBoth
+                                        notRightCurrent
+                                        rightProof))
+                implicationEliminationProof
+                    withNotRight
+                    (weakenForHypothesis conjunction)
+                    refuterProof)
+    doubleNegationEliminationProof
+        context
+        rightProposition
+        doubleNegation
+
+disjunctionTerm
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+disjunctionTerm left right =
+    CImp
+        (CImp left CFalsum)
+        right
+
+disjunctionLeftProof
+    :: Eq global
+    => ProofContext global
+    -> CanonicalTerm global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+disjunctionLeftProof context right leftProof = do
+    notLeft <-
+        scopedTerm context
+            (CImp
+                (scopedCoreTerm
+                    (builtProofStatement leftProof))
+                CFalsum)
+    rightTarget <-
+        scopedTerm context right
+    implicationIntroductionProof
+        context
+        notLeft
+        (\extended notLeftProof -> do
+            falsum <-
+                implicationEliminationProof
+                    extended
+                    notLeftProof
+                    (weakenForHypothesis
+                        leftProof)
+            falsumEliminationProof
+                extended
+                falsum
+                rightTarget)
+
+disjunctionRightProof
+    :: ProofContext global
+    -> CanonicalTerm global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+disjunctionRightProof context left rightProof = do
+    notLeft <-
+        scopedTerm context
+            (CImp left CFalsum)
+    implicationIntroductionProof
+        context
+        notLeft
+        (\_extended _notLeftProof ->
+            pure
+                (weakenForHypothesis
+                    rightProof))
+
+disjunctionEliminationProof
+    :: Eq global
+    => ProofContext global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+    -> BuiltProof global
+    -> ScopedCheckedCore global
+    -> ( ProofContext global
+         -> BuiltProof global
+         -> Either
+            KernelProofBuildError
+            (BuiltProof global)
+       )
+    -> ( ProofContext global
+         -> BuiltProof global
+         -> Either
+            KernelProofBuildError
+            (BuiltProof global)
+       )
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+disjunctionEliminationProof
+        context
+        left
+        right
+        disjunction
+        result
+        leftCase
+        rightCase = do
+    leftProposition <-
+        scopedTerm context left
+    rightProposition <-
+        scopedTerm context right
+    leftImplication <-
+        implicationIntroductionProof
+            context
+            leftProposition
+            leftCase
+    rightImplication <-
+        implicationIntroductionProof
+            context
+            rightProposition
+            rightCase
+    notResult <-
+        scopedTerm context
+            (CImp
+                (scopedCoreTerm result)
+                CFalsum)
+    doubleNegation <-
+        implicationIntroductionProof
+            context
+            notResult
+            (\extended notResultProof -> do
+                leftAtNotResult <-
+                    scopedTerm extended left
+                notLeftProof <-
+                    implicationIntroductionProof
+                        extended
+                        leftAtNotResult
+                        (\withLeft leftProof -> do
+                            resultProof <-
+                                implicationEliminationProof
+                                    withLeft
+                                    (weakenForHypothesis
+                                        (weakenForHypothesis
+                                            leftImplication))
+                                    leftProof
+                            implicationEliminationProof
+                                withLeft
+                                (weakenForHypothesis
+                                    notResultProof)
+                                resultProof)
+                rightProof <-
+                    implicationEliminationProof
+                        extended
+                        (weakenForHypothesis
+                            disjunction)
+                        notLeftProof
+                resultProof <-
+                    implicationEliminationProof
+                        extended
+                        (weakenForHypothesis
+                            rightImplication)
+                        rightProof
+                implicationEliminationProof
+                    extended
+                    notResultProof
+                    resultProof)
+    doubleNegationEliminationProof
+        context
+        result
+        doubleNegation
+
+-- | Validate the one structural rule used by exact source case analysis.
+-- The branch proofs and the exhaustive disjunction are represented here by
+-- exact hypotheses; the kernel combinators must derive the owned goal from
+-- precisely those propositions.  No derived proof escapes this check.
+validateCaseAnalysisComposition
+    :: Eq global
+    => CheckedFoundation
+    -> (global -> Maybe CoreType)
+    -> ScopedCheckedCore global
+    -> NonEmpty (ScopedCheckedCore global)
+    -> ScopedCheckedCore global
+    -> Either KernelProofBuildError ()
+validateCaseAnalysisComposition
+        foundation globalType goal cases exhaustive = do
+    validatePropositionContext "case goal" lexicalContext goal
+    traverse_
+        (validatePropositionContext "case assumption" lexicalContext)
+        cases
+    validatePropositionContext
+        "case exhaustiveness target" lexicalContext exhaustive
+    let expectedExhaustive =
+            foldl1
+                (\left right ->
+                    CImp
+                        (CImp left CFalsum)
+                        right)
+                (scopedCoreTerm <$> cases)
+    unless (scopedCoreTerm exhaustive == expectedExhaustive)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "case exhaustiveness is not the source-ordered disjunction"))
+    branchImplications <-
+        traverse
+            (checkedImplication lexicalContext goal)
+            cases
+    let context =
+            ProofContext
+                foundation
+                globalType
+                lexicalContext
+                (exhaustive : toList branchImplications)
+    exhaustiveProof <- hypothesisProof context exhaustive
+    result <-
+        eliminateCases
+            context goal cases exhaustiveProof
+    unless (builtProofStatement result == goal)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "case elimination did not derive the owned goal"))
+  where
+    lexicalContext = scopedCoreContext goal
+
+    checkedImplication expectedContext conclusion antecedent =
+        case implyScopedCore antecedent conclusion of
+            Just implication
+                | scopedCoreContext implication == expectedContext ->
+                    pure implication
+            _ ->
+                Left
+                    (ProofStructuralCompositionMismatch
+                        "case branch implication changed context")
+
+    eliminateCases context result (only :| []) caseProof = do
+        branchImplication <-
+            scopedTerm context
+                (CImp
+                    (scopedCoreTerm only)
+                    (scopedCoreTerm result))
+            >>= hypothesisProof context
+        implicationEliminationProof context branchImplication caseProof
+    eliminateCases context result (firstCase :| rest) disjunctionProof = do
+        let allCases = firstCase :| rest
+            leftCases = NonEmpty.fromList (NonEmpty.init allCases)
+            rightCase = NonEmpty.last allCases
+            leftTerm =
+                foldl1 disjunctionTerm
+                    (scopedCoreTerm <$> leftCases)
+        disjunctionEliminationProof
+            context
+            leftTerm
+            (scopedCoreTerm rightCase)
+            disjunctionProof
+            result
+            (\extended leftProof ->
+                eliminateCases extended result leftCases leftProof)
+            (\extended rightProof -> do
+                branchImplication <-
+                    scopedTerm extended
+                        (CImp
+                            (scopedCoreTerm rightCase)
+                            (scopedCoreTerm result))
+                        >>= hypothesisProof extended
+                implicationEliminationProof
+                    extended branchImplication rightProof)
+
+-- | Validate the exact classical closing step for a proof by contradiction.
+-- The only classical input is the confined 'DoubleNegationElim' foundation
+-- row already consumed by 'doubleNegationEliminationProof'.
+validateDoubleNegationComposition
+    :: Eq global
+    => CheckedFoundation
+    -> (global -> Maybe CoreType)
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Either KernelProofBuildError ()
+validateDoubleNegationComposition
+        foundation globalType goal negation falsum = do
+    let lexicalContext = scopedCoreContext goal
+    validatePropositionContext "contradiction goal" lexicalContext goal
+    validatePropositionContext
+        "contradiction negation" lexicalContext negation
+    validatePropositionContext "contradiction falsum" lexicalContext falsum
+    unless (scopedCoreTerm falsum == CFalsum)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "proof by contradiction did not target falsum"))
+    expectedNegation <-
+        checkedNegation lexicalContext goal
+    unless (negation == expectedNegation)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "proof by contradiction did not own the exact negated goal"))
+    doubleNegation <-
+        checkedNegation lexicalContext negation
+    let context =
+            ProofContext
+                foundation globalType lexicalContext [doubleNegation]
+    hypothesis <- hypothesisProof context doubleNegation
+    result <- doubleNegationEliminationProof context goal hypothesis
+    unless (builtProofStatement result == goal)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "double-negation elimination did not derive the owned goal"))
+
+-- | Validate the exact ex-falso closing step used after a terminal indirect
+-- contradiction discharge.
+validateFalsumEliminationComposition
+    :: Eq global
+    => CheckedFoundation
+    -> (global -> Maybe CoreType)
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Either KernelProofBuildError ()
+validateFalsumEliminationComposition foundation globalType goal falsum = do
+    let lexicalContext = scopedCoreContext goal
+    validatePropositionContext "contradiction goal" lexicalContext goal
+    validatePropositionContext "contradiction falsum" lexicalContext falsum
+    unless (scopedCoreTerm falsum == CFalsum)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "falsum elimination did not receive falsum"))
+    let context =
+            ProofContext foundation globalType lexicalContext [falsum]
+    hypothesis <- hypothesisProof context falsum
+    result <- falsumEliminationProof context hypothesis goal
+    unless (builtProofStatement result == goal)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "falsum elimination did not derive the owned goal"))
+
+-- | Validate the exact structural instance used by source set induction.
+-- The admitted child is represented by its generalized step proposition;
+-- the checked foundation row must specialize to that exact premise and the
+-- owned binder-level result. No induction principle becomes an ATP premise.
+validateSetInductionComposition
+    :: Eq global
+    => CheckedFoundation
+    -> (global -> Maybe CoreType)
+    -> Natural
+    -> ScopedCheckedCore global
+    -> [ScopedCheckedCore global]
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Either KernelProofBuildError ()
+validateSetInductionComposition
+        foundation globalType selected property antecedents childTarget
+        hypothesis result = do
+    let lexicalContext = scopedCoreContext property
+    traverse_
+        (validatePropositionContext
+            "set-induction antecedent" lexicalContext)
+        antecedents
+    validatePropositionContext
+        "set-induction property" lexicalContext property
+    validatePropositionContext
+        "set-induction child target" lexicalContext childTarget
+    validatePropositionContext
+        "set-induction hypothesis" lexicalContext hypothesis
+    validatePropositionContext
+        "set-induction result" lexicalContext result
+    expectedProperty <-
+        foldrM implyChecked childTarget antecedents
+    unless (property == expectedProperty)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "set-induction property does not own the child target and guards"))
+    (predicate, expectedHypothesis, step, expectedResult) <-
+        maybe
+            (Left
+                (ProofStructuralCompositionMismatch
+                    "set-induction focus is not a set-valued ambient binder"))
+            pure
+            (scopedSetInductionInstance selected property)
+    unless (hypothesis == expectedHypothesis)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "set-induction hypothesis does not match the owned property"))
+    unless (result == expectedResult)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "set-induction result does not close the owned property"))
+    let context =
+            ProofContext foundation globalType lexicalContext [step]
+    stepProof <- hypothesisProof context step
+    axiom <- foundationProof context SetInduction
+    instanceProof <- forallEliminationProof context axiom predicate
+    expectedInstance <-
+        maybe
+            (Left
+                (ProofStructuralCompositionMismatch
+                    "set-induction instance changed lexical context"))
+            pure
+            (implyScopedCore step result)
+    convertedInstance <-
+        conversionProof context instanceProof expectedInstance
+    resultProof <-
+        implicationEliminationProof context convertedInstance stepProof
+    unless (builtProofStatement resultProof == result)
+        (Left
+            (ProofStructuralCompositionMismatch
+                "set-induction foundation instance did not derive the owned result"))
+  where
+    implyChecked antecedent conclusion =
+        maybe
+            (Left
+                (ProofStructuralCompositionMismatch
+                    "set-induction guard changed lexical context"))
+            pure
+            (implyScopedCore antecedent conclusion)
+
+validatePropositionContext
+    :: Text
+    -> [CoreType]
+    -> ScopedCheckedCore global
+    -> Either KernelProofBuildError ()
+validatePropositionContext label expected proposition =
+    unless
+        ( scopedCoreType proposition == TyProp
+            && scopedCoreContext proposition == expected
+        )
+        (Left
+            (ProofStructuralCompositionMismatch
+                (label <> " has the wrong type or lexical context")))
+
+checkedNegation
+    :: [CoreType]
+    -> ScopedCheckedCore global
+    -> Either KernelProofBuildError (ScopedCheckedCore global)
+checkedNegation expectedContext proposition =
+    case negateScopedCore proposition of
+        Just negation
+            | scopedCoreContext negation == expectedContext ->
+                pure negation
+        _ ->
+            Left
+                (ProofStructuralCompositionMismatch
+                    "classical negation changed context")
+
+existentialTerm
+    :: CoreType
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+existentialTerm binderType body =
+    CImp
+        (CForall binderType
+            (CImp body CFalsum))
+        CFalsum
+
+existentialIntroductionProof
+    :: Eq global
+    => ProofContext global
+    -> CoreType
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+existentialIntroductionProof
+        context
+        binderType
+        bodyUnderBinder
+        witness
+        bodyAtWitness = do
+    unless
+        (proofContextTypes context
+            == drop 1
+                (scopedCoreContext
+                    bodyUnderBinder))
+        (Left ProofExpectedUnaryBinder)
+    universalNegation <-
+        scopedTerm context
+            (CForall binderType
+                (CImp
+                    (scopedCoreTerm
+                        bodyUnderBinder)
+                    CFalsum))
+    implicationIntroductionProof
+        context
+        universalNegation
+        (\extended universalProof -> do
+            negatedBody <-
+                forallEliminationProof
+                    extended
+                    universalProof
+                    witness
+            implicationEliminationProof
+                extended
+                negatedBody
+                (weakenForHypothesis
+                    bodyAtWitness))
+
+existentialEliminationProof
+    :: Eq global
+    => ProofContext global
+    -> CoreType
+    -> ScopedCheckedCore global
+    -> BuiltProof global
+    -> ScopedCheckedCore global
+    -> ( ProofContext global
+         -> ScopedCheckedCore global
+         -> BuiltProof global
+         -> Either
+            KernelProofBuildError
+            (BuiltProof global)
+       )
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+existentialEliminationProof
+        context
+        binderType
+        bodyUnderBinder
+        existential
+        result
+        bodyCase = do
+    notResult <-
+        scopedTerm context
+            (CImp
+                (scopedCoreTerm result)
+                CFalsum)
+    notResultUnderBinder <-
+        first ProofTermIllTyped
+            (weakenScopedCore
+                (contextGlobalType context)
+                binderType
+                notResult)
+    doubleNegation <-
+        implicationIntroductionProof
+            context
+            notResult
+            (\withNotResult _notResultProof -> do
+                universalNegation <-
+                    forallIntroductionProof
+                        withNotResult
+                        binderType
+                        (\withBinder variable -> do
+                            let body =
+                                    bodyUnderBinder
+                            implicationIntroductionProof
+                                withBinder
+                                body
+                                (\withBody bodyProof -> do
+                                    resultProof <-
+                                        bodyCase
+                                            withBody
+                                            variable
+                                            bodyProof
+                                    notResultCurrent <-
+                                        hypothesisProof
+                                            withBody
+                                            notResultUnderBinder
+                                    implicationEliminationProof
+                                        withBody
+                                        notResultCurrent
+                                        resultProof))
+                implicationEliminationProof
+                    withNotResult
+                    (weakenForHypothesis
+                        existential)
+                    universalNegation)
+    doubleNegationEliminationProof
+        context
+        result
+        doubleNegation
+
+setLfpBoundProof
+    :: ProofContext global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+setLfpBoundProof
+        (ProofContext
+            foundation
+            globalType
+            _types
+            _hypotheses)
+        domain
+        operator = do
+    result <-
+        first (ProofSetLfpRuleFailed . Text.pack . show)
+            (SetLfp.setLfpBound
+                foundation
+                globalType
+                domain
+                operator)
+    pure
+        (BuiltProof
+            result
+            (setLfpBoundDerivation
+                domain
+                operator))
+
+setLfpFixedProof
+    :: Eq global
+    => ProofContext global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+setLfpFixedProof
+        (ProofContext
+            foundation
+            globalType
+            _types
+            _hypotheses)
+        domain
+        operator
+        monotone = do
+    result <-
+        first (ProofSetLfpRuleFailed . Text.pack . show)
+            (SetLfp.setLfpFixed
+                foundation
+                globalType
+                domain
+                operator
+                (builtProofStatement
+                    monotone))
+    pure
+        (BuiltProof
+            result
+            (setLfpFixedDerivation
+                domain
+                operator
+                (builtProofDerivation
+                    monotone)))
+
+setLfpInductProof
+    :: Eq global
+    => ProofContext global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> BuiltProof global
+    -> BuiltProof global
+    -> BuiltProof global
+    -> Either
+        KernelProofBuildError
+        (BuiltProof global)
+setLfpInductProof
+        (ProofContext
+            foundation
+            globalType
+            _types
+            _hypotheses)
+        domain
+        operator
+        predicate
+        element
+        monotone
+        member
+        closure = do
+    result <-
+        first (ProofSetLfpRuleFailed . Text.pack . show)
+            (SetLfp.setLfpInduct
+                foundation
+                globalType
+                domain
+                operator
+                predicate
+                element
+                (builtProofStatement
+                    monotone)
+                (builtProofStatement
+                    member)
+                (builtProofStatement
+                    closure))
+    pure
+        (BuiltProof
+            result
+            (setLfpInductDerivation
+                domain
+                operator
+                predicate
+                element
+                (builtProofDerivation
+                    monotone)
+                (builtProofDerivation
+                    member)
+                (builtProofDerivation
+                    closure)))
+
+contextGlobalType
+    :: ProofContext global
+    -> (global -> Maybe CoreType)
+contextGlobalType
+        (ProofContext
+            _foundation
+            globalType
+            _types
+            _hypotheses) =
+    globalType
+
+equalityParts
+    :: ScopedCheckedCore global
+    -> Either
+        KernelProofBuildError
+        ( CoreType
+        , CanonicalTerm global
+        , CanonicalTerm global
+        )
+equalityParts equality =
+    case scopedCoreTerm equality of
+        CEq operandType left right ->
+            Right (operandType, left, right)
+        _ ->
+            Left ProofExpectedEquality
+
+weakenForHypothesis
+    :: BuiltProof global
+    -> BuiltProof global
+weakenForHypothesis
+        (BuiltProof statement derivation) =
+    BuiltProof
+        statement
+        (weakenDerivationHypotheses 1 derivation)