path: root/source/Felix/Checking/Kernel/Proof.hs

{-# 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)