path: root/source/Felix/Checking/Typed/Inductive.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Direct checked lowering of the current one-carrier set-valued inductive
-- declaration.
module Felix.Checking.Typed.Inductive
    ( DirectInductive(..)
    , DirectInductiveClause(..)
    , DirectInductiveCondition(..)
    , RecursiveCarrierContext
    , RecursiveCarrierContextError(..)
    , prepareRecursiveCarrierContext
    , directRecursiveCarrierContext
    , recursiveCarrierContextSymbols
    , SourceGlobal(..)
    , PreparedTypedInductive
    , typedInductiveCarrierType
    , typedInductiveCarrierBody
    , typedInductiveGuardTargets
    , PreparedTypedInductiveMonotonicity
    , typedInductiveMonotonicities
    , typedInductiveMonotonicityLocation
    , typedInductiveMonotonicityTarget
    , typedInductiveContextInventory
    , PreparedTypedInductiveFact
    , typedInductiveFacts
    , typedInductiveFactMarker
    , typedInductiveFactTarget
    , typedInductiveFactRules
    , typedInductiveFactRequiresMonotonicities
    , typedInductiveFactDerivation
    , prepareTypedClosedTerm
    , prepareTypedClosedFormula
    , prepareTypedInductive
    , TypedInductiveError(..)
    ) where

import Base hiding (Empty)
import Felix.Checking.Core
import Felix.Checking.Exact.Vocabulary
import Felix.Checking.Foundation
import Felix.Checking.Kernel.Derivation
import Felix.Checking.Kernel.Proof
import Felix.Report.Location (Location)
import Felix.Syntax.Internal

import Control.Monad ((<=<), foldM)
import Data.Bifunctor (first)
import Data.List qualified as List
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Text qualified as Text
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)
import Bound.Scope (fromScope, instantiate)
import Bound.Var (Var(..))


data DirectInductive = DirectInductive
    { directInductiveParams :: ![VarSymbol]
    , directInductiveDomain :: !Term
    , directInductiveClauses
        :: !(NonEmpty DirectInductiveClause)
    }

data DirectInductiveClause = DirectInductiveClause
    { directClauseVariables :: ![VarSymbol]
    , directClauseConditions
        :: ![DirectInductiveCondition]
    , directClauseResult :: !Term
    }

data DirectInductiveCondition
    = DirectSideCondition !Formula
    | DirectRecursiveCondition !Term !RecursiveCarrierContext

data RecursiveCarrierVariable
    = RecursiveCarrierHole
    | RecursiveCarrierSourceVariable !VarSymbol
    deriving stock (Show, Eq, Ord)

-- | A validated, capture-free one-hole carrier context in the same
-- first-order set-term fragment lowered by this module.  The source carrier
-- application itself has been replaced, so the inductive symbol cannot
-- survive inside this value.
data RecursiveCarrierContext = RecursiveCarrierContext
    !Location
    !(ExprOf RecursiveCarrierVariable)
    deriving stock (Show, Eq, Ord)

data RecursiveCarrierContextError
    = RecursiveCarrierWrongArguments !Location
    | RecursiveCarrierUnsupportedContext !Location
    deriving stock (Show, Eq)

prepareRecursiveCarrierContext
    :: FunctionSymbol
    -> [VarSymbol]
    -> Term
    -> Either RecursiveCarrierContextError RecursiveCarrierContext
prepareRecursiveCarrierContext carrier parameters source =
    RecursiveCarrierContext (exprLocation source) <$> go source
  where
    carrierSymbol = SymbolMixfix carrier

    go = \case
        TermVar variable ->
            pure
                (TermVar
                    (RecursiveCarrierSourceVariable variable))
        TermSymbol location symbol arguments
            | symbol == carrierSymbol ->
                if sameCarrierArguments arguments parameters
                    then pure (TermVar RecursiveCarrierHole)
                    else Left (RecursiveCarrierWrongArguments location)
            | otherwise ->
                TermSymbol location symbol <$> traverse go arguments
        unsupported ->
            Left
                (RecursiveCarrierUnsupportedContext
                    (exprLocation unsupported))

    sameCarrierArguments arguments variables =
        length arguments == length variables
            && and
                (zipWith
                    (\argument variable ->
                        argument == TermVar variable)
                    arguments
                    variables)

recursiveCarrierContextSymbols
    :: RecursiveCarrierContext
    -> Set Symbol
recursiveCarrierContextSymbols
        (RecursiveCarrierContext _location source) =
    mentionedSymbols source

directRecursiveCarrierContext :: Location -> RecursiveCarrierContext
directRecursiveCarrierContext location =
    RecursiveCarrierContext location (TermVar RecursiveCarrierHole)

data SourceGlobal global = SourceGlobal
    !global
    !(Maybe (FrozenCheckedCore global))

data InductiveGlobal global where
    InductiveGlobal
        :: Eq global
        => !global
        -> !CoreType
        -> InductiveGlobal global

instance Eq (InductiveGlobal global) where
    InductiveGlobal left _leftType
        == InductiveGlobal right _rightType =
            left == right

inductiveGlobalIdentity :: InductiveGlobal global -> global
inductiveGlobalIdentity (InductiveGlobal identity _coreType) =
    identity

inductiveGlobalType :: InductiveGlobal global -> CoreType
inductiveGlobalType (InductiveGlobal _identity coreType) =
    coreType

data PreparedTypedInductive global = PreparedTypedInductive
    !CoreType
    !(FrozenCheckedCore global)
    !(Vector (FrozenCheckedCore global))
    !(Vector (PreparedTypedInductiveMonotonicity global))
    !(Vector (FrozenCheckedCore global))
    !(NonEmpty (PreparedTypedInductiveFact global))

data PreparedTypedInductiveMonotonicity global =
    PreparedTypedInductiveMonotonicity
        !Location
        !(FrozenCheckedCore global)

typedInductiveMonotonicities
    :: PreparedTypedInductive global
    -> Vector (PreparedTypedInductiveMonotonicity global)
typedInductiveMonotonicities
        (PreparedTypedInductive
            _carrierType
            _body
            _guards
            monotonicities
            _contexts
            _facts) =
    monotonicities

typedInductiveMonotonicityLocation
    :: PreparedTypedInductiveMonotonicity global
    -> Location
typedInductiveMonotonicityLocation
        (PreparedTypedInductiveMonotonicity location _target) =
    location

typedInductiveMonotonicityTarget
    :: PreparedTypedInductiveMonotonicity global
    -> FrozenCheckedCore global
typedInductiveMonotonicityTarget
        (PreparedTypedInductiveMonotonicity _location target) =
    target

typedInductiveContextInventory
    :: PreparedTypedInductive global
    -> Vector (FrozenCheckedCore global)
typedInductiveContextInventory
        (PreparedTypedInductive
            _carrierType _body _guards _monotonicities contexts _facts) =
    contexts

data CheckedRecursiveCarrierContext global =
    CheckedRecursiveCarrierContext
        ![VarSymbol]
        !(FrozenCheckedCore global)

data PreparedInductiveSource global = PreparedInductiveSource
    { preparedInductiveParams :: ![VarSymbol]
    , preparedInductiveDomain :: !Term
    , preparedInductiveClauses
        :: !(NonEmpty (PreparedInductiveClause global))
    }

data PreparedInductiveClause global = PreparedInductiveClause
    { preparedClauseVariables :: ![VarSymbol]
    , preparedClauseConditions
        :: ![PreparedInductiveCondition global]
    , preparedClauseResult :: !Term
    }

data PreparedInductiveCondition global
    = PreparedSideCondition !Formula
    | PreparedDirectRecursiveCondition
        !Term
        !(CheckedRecursiveCarrierContext global)
    | PreparedNestedRecursiveCondition
        !Term
        !(CheckedRecursiveCarrierContext global)
        !ImportIx
        !(FrozenCheckedCore global)

data PreparedInductiveGuard global
    = PreparedFoundationGuard !FoundationAxiomTag
    | PreparedImportedGuard
        !ImportIx
        !(FrozenCheckedCore global)

typedInductiveCarrierType
    :: PreparedTypedInductive global
    -> CoreType
typedInductiveCarrierType
        (PreparedTypedInductive
            carrierType
            _body
            _guards
            _monotonicities
            _contexts
            _facts) =
    carrierType

typedInductiveCarrierBody
    :: PreparedTypedInductive global
    -> FrozenCheckedCore global
typedInductiveCarrierBody
        (PreparedTypedInductive
            _carrierType
            body
            _guards
            _monotonicities
            _contexts
            _facts) =
    body

typedInductiveGuardTargets
    :: PreparedTypedInductive global
    -> Vector (FrozenCheckedCore global)
typedInductiveGuardTargets
        (PreparedTypedInductive
            _carrierType
            _body
            guards
            _monotonicities
            _contexts
            _facts) =
    guards

newtype PreparedTypedInductiveFact global =
    PreparedTypedInductiveFact
        ( Marker
        , FrozenCheckedCore global
        , NonEmpty KernelRuleTag
        , Bool
        , KernelDerivation global
        )

typedInductiveFacts
    :: PreparedTypedInductive global
    -> NonEmpty (PreparedTypedInductiveFact global)
typedInductiveFacts
        (PreparedTypedInductive
            _carrierType
            _body
            _guards
            _monotonicities
            _contexts
            facts) =
    facts

typedInductiveFactMarker
    :: PreparedTypedInductiveFact global
    -> Marker
typedInductiveFactMarker
        (PreparedTypedInductiveFact
            (marker, _target, _rule, _monotonicities, _derivation)) =
    marker

typedInductiveFactTarget
    :: PreparedTypedInductiveFact global
    -> FrozenCheckedCore global
typedInductiveFactTarget
        (PreparedTypedInductiveFact
            (_marker, target, _rule, _monotonicities, _derivation)) =
    target

typedInductiveFactRules
    :: PreparedTypedInductiveFact global
    -> NonEmpty KernelRuleTag
typedInductiveFactRules
        (PreparedTypedInductiveFact
            (_marker, _target, rules, _monotonicities, _derivation)) =
    rules

typedInductiveFactRequiresMonotonicities
    :: PreparedTypedInductiveFact global
    -> Bool
typedInductiveFactRequiresMonotonicities
        (PreparedTypedInductiveFact
            (_marker, _target, _rules, required, _derivation)) =
    required

typedInductiveFactDerivation
    :: PreparedTypedInductiveFact global
    -> KernelDerivation global
typedInductiveFactDerivation
        (PreparedTypedInductiveFact
            (_marker, _target, _rule, _monotonicities, derivation)) =
    derivation

-- | Lower one closed source formula through the exact primitive/global
-- policy used by the direct-inductive compiler.
prepareTypedClosedFormula
    :: Eq global
    => (global -> CoreType)
    -> (Symbol -> Maybe (SourceGlobal global))
    -> Formula
    -> Either TypedInductiveError (FrozenCheckedCore global)
prepareTypedClosedFormula globalType resolveGlobal formula = do
    term <-
        lowerFormulaWith
            True
            (fmap (mapSourceGlobal wrapGlobal) . resolveGlobal)
            emptyEnvironment
            formula
    checked <-
        first TypedInductiveCoreError
            (checkCanonicalCore
                (Just . inductiveGlobalType)
                term)
    pure (mapFrozenGlobals inductiveGlobalIdentity checked)
  where
    wrapGlobal identity =
        InductiveGlobal identity (globalType identity)

prepareTypedClosedTerm
    :: Eq global
    => (global -> CoreType)
    -> (Symbol -> Maybe (SourceGlobal global))
    -> Term
    -> Either TypedInductiveError (FrozenCheckedCore global)
prepareTypedClosedTerm globalType resolveGlobal term = do
    canonical <-
        lowerTerm
            (fmap (mapSourceGlobal wrapGlobal) . resolveGlobal)
            emptyEnvironment
            term
    checked <-
        first TypedInductiveCoreError
            (checkCanonicalCore
                (Just . inductiveGlobalType)
                canonical)
    pure (mapFrozenGlobals inductiveGlobalIdentity checked)
  where
    wrapGlobal identity =
        InductiveGlobal identity (globalType identity)

data TypedInductiveError
    = TypedInductiveDuplicateBinder !VarSymbol
    | TypedInductiveUnknownLocal !VarSymbol
    | TypedInductiveUnsupportedExpression !Text
    | TypedInductiveCoreError !CoreCheckError
    | TypedInductiveProofError !KernelProofBuildError
    | TypedInductiveProofRemainedOpen
    | TypedInductiveFactPreparationFailed
        !Marker
        !TypedInductiveError
    | TypedInductivePreparationContext
        !Text
        !TypedInductiveError
    deriving stock (Show, Eq)

data InductiveEnvironment = InductiveEnvironment
    !(Map VarSymbol Natural)

emptyEnvironment :: InductiveEnvironment
emptyEnvironment =
    InductiveEnvironment Map.empty

extendEnvironment
    :: VarSymbol
    -> InductiveEnvironment
    -> Either
        TypedInductiveError
        InductiveEnvironment
extendEnvironment variable
        (InductiveEnvironment variables)
    | Map.member variable variables =
        Left
            (TypedInductiveDuplicateBinder
                variable)
    | otherwise =
        Right
            (InductiveEnvironment
                (Map.insert variable 0
                    (succ <$> variables)))

lookupEnvironment
    :: VarSymbol
    -> InductiveEnvironment
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lookupEnvironment variable
        (InductiveEnvironment variables) =
    maybe
        (Left
            (TypedInductiveUnknownLocal
                variable))
        (Right . CBound)
        (Map.lookup variable variables)

prepareTypedInductive
    :: Eq global
    => (global -> CoreType)
    -> CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal global))
    -> Marker
    -> DirectInductive
    -> Either
        TypedInductiveError
        (PreparedTypedInductive global)
prepareTypedInductive
        globalType
        foundation
        resolveGlobal
        marker
        inductive =
    mapPreparedTypedInductive inductiveGlobalIdentity
        <$> prepareTypedInductiveInternal
            foundation
            (fmap (mapSourceGlobal wrapGlobal) . resolveGlobal)
            marker
            inductive
  where
    wrapGlobal identity =
        InductiveGlobal identity (globalType identity)

prepareTypedInductiveInternal
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Marker
    -> DirectInductive
    -> Either
        TypedInductiveError
        (PreparedTypedInductive (InductiveGlobal global))
prepareTypedInductiveInternal
        foundation
        resolveGlobal
        marker
        inductive = do
    guards <-
        traverse
            (prepareDirectGuardTarget
                resolveGlobal
                inductive)
            (directInductiveClauses
                inductive)
    let preparedGuards =
            assignGuardSources foundation
                (NonEmpty.toList guards)
        nextImport =
            fromIntegral
                (length
                    [ ()
                    | PreparedImportedGuard{} <- preparedGuards
                    ])
    (preparedSource, monotonicities, contexts) <-
        prepareInductiveSource
            resolveGlobal
            nextImport
            inductive
    carrierBody <-
        prepareCarrierBody
            resolveGlobal
            preparedSource
    facts <-
        prepareFacts
            foundation
            resolveGlobal
            marker
            preparedSource
            (case preparedGuards of
                firstGuard : remainingGuards ->
                    firstGuard :| remainingGuards
                [] ->
                    impossible
                        "a nonempty inductive declaration produced no guards")
    pure
        (PreparedTypedInductive
            carrierType
            carrierBody
            (Vector.fromList
                [ target
                | PreparedImportedGuard
                    _index target <- preparedGuards
                ])
            (Vector.fromList monotonicities)
            (Vector.fromList contexts)
            facts)
  where
    carrierType =
        foldr
            TyArrow
            TySet
            (TySet
                <$ directInductiveParams
                    inductive)

mapSourceGlobal
    :: (left -> right)
    -> SourceGlobal left
    -> SourceGlobal right
mapSourceGlobal transform (SourceGlobal identity body) =
    SourceGlobal
        (transform identity)
        (mapFrozenGlobals transform <$> body)

mapPreparedTypedInductive
    :: (left -> right)
    -> PreparedTypedInductive left
    -> PreparedTypedInductive right
mapPreparedTypedInductive transform
        (PreparedTypedInductive
            carrierType body guards monotonicities contexts facts) =
    PreparedTypedInductive
        carrierType
        (mapFrozenGlobals transform body)
        (mapFrozenGlobals transform <$> guards)
        (mapMonotonicity transform <$> monotonicities)
        (mapFrozenGlobals transform <$> contexts)
        (mapPreparedFact transform <$> facts)
  where
    mapMonotonicity mapGlobal
            (PreparedTypedInductiveMonotonicity location target) =
        PreparedTypedInductiveMonotonicity
            location
            (mapFrozenGlobals mapGlobal target)

    mapPreparedFact mapGlobal
            (PreparedTypedInductiveFact
                (marker, target, rule, requiresMonotonicities, derivation)) =
        PreparedTypedInductiveFact
            ( marker
            , mapFrozenGlobals mapGlobal target
            , rule
            , requiresMonotonicities
            , mapKernelDerivationGlobals mapGlobal derivation
            )

data MonotonicityInventory global = MonotonicityInventory
    ![(FrozenCheckedCore global, ImportIx)]
    !Natural
    ![PreparedTypedInductiveMonotonicity global]
    ![FrozenCheckedCore global]

prepareInductiveSource
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Natural
    -> DirectInductive
    -> Either
        TypedInductiveError
        ( PreparedInductiveSource (InductiveGlobal global)
        , [PreparedTypedInductiveMonotonicity (InductiveGlobal global)]
        , [FrozenCheckedCore (InductiveGlobal global)]
        )
prepareInductiveSource resolveGlobal firstImport inductive = do
    (final, clauses) <-
        prepareClauses
            (MonotonicityInventory [] firstImport [] [])
            (NonEmpty.toList (directInductiveClauses inductive))
    let MonotonicityInventory
            _targets _next monotonicities contexts = final
    pure
        ( PreparedInductiveSource
            (directInductiveParams inductive)
            (directInductiveDomain inductive)
            (NonEmpty.fromList clauses)
        , reverse monotonicities
        , reverse contexts
        )
  where
    variablesFor clause =
        directInductiveParams inductive
            <> directClauseVariables clause

    prepareClauses inventory = \case
        [] -> pure (inventory, [])
        clause : remaining -> do
            (afterClause, preparedClause) <-
                prepareClause inventory clause
            (final, preparedRemaining) <-
                prepareClauses afterClause remaining
            pure (final, preparedClause : preparedRemaining)

    prepareClause inventory clause = do
        (next, conditions) <-
            prepareConditions inventory clause
                (directClauseConditions clause)
        pure
            ( next
            , PreparedInductiveClause
                (directClauseVariables clause)
                conditions
                (directClauseResult clause)
            )

    prepareConditions inventory _clause [] =
        pure (inventory, [])
    prepareConditions inventory clause (condition : remaining) = do
        (next, prepared) <-
            prepareCondition inventory clause condition
        (final, preparedRemaining) <-
            prepareConditions next clause remaining
        pure (final, prepared : preparedRemaining)

    prepareCondition inventory _clause (DirectSideCondition formula) =
        pure (inventory, PreparedSideCondition formula)
    prepareCondition
            (MonotonicityInventory targets next facts contexts)
            clause
            (DirectRecursiveCondition recursiveTerm sourceContext) = do
        checkedContext <-
            prepareRecursiveCarrierTemplate
                resolveGlobal
                (variablesFor clause)
                sourceContext
        let template = checkedRecursiveCarrierTemplate checkedContext
            withContext currentFacts =
                MonotonicityInventory
                    targets next currentFacts (template : contexts)
        if recursiveCarrierContextIsDirect sourceContext
            then pure
                ( withContext facts
                , PreparedDirectRecursiveCondition
                    recursiveTerm checkedContext
                )
            else do
                target <-
                    prepareRecursiveCarrierMonotonicityTarget
                        checkedContext
                let RecursiveCarrierContext location _source = sourceContext
                case List.lookup target targets of
                    Just index ->
                        pure
                            ( MonotonicityInventory
                                targets next facts (template : contexts)
                            , PreparedNestedRecursiveCondition
                                recursiveTerm checkedContext index target
                            )
                    Nothing ->
                        let index = importIx next
                        in pure
                            ( MonotonicityInventory
                                ((target, index) : targets)
                                (next + 1)
                                (PreparedTypedInductiveMonotonicity
                                    location target : facts)
                                (template : contexts)
                            , PreparedNestedRecursiveCondition
                                recursiveTerm checkedContext index target
                            )

checkedRecursiveCarrierTemplate
    :: CheckedRecursiveCarrierContext global
    -> FrozenCheckedCore global
checkedRecursiveCarrierTemplate
        (CheckedRecursiveCarrierContext _variables template) =
    template

recursiveCarrierContextIsDirect :: RecursiveCarrierContext -> Bool
recursiveCarrierContextIsDirect
        (RecursiveCarrierContext _location source) =
    source == TermVar RecursiveCarrierHole

prepareRecursiveCarrierTemplate
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> [VarSymbol]
    -> RecursiveCarrierContext
    -> Either
        TypedInductiveError
        (CheckedRecursiveCarrierContext (InductiveGlobal global))
prepareRecursiveCarrierTemplate resolveGlobal variables context = do
    body <-
        buildUnderVariables emptyEnvironment variables \environment -> do
            underHole <- shiftEnvironment environment
            lowerRecursiveCarrierContext
                resolveGlobal underHole (CBound 0) context
    checked <-
        first TypedInductiveCoreError
            (checkCanonicalCore
                (Just . inductiveGlobalType)
                -- Transparent expansion may leave beta redexes.  Freeze one
                -- normalized template so routing, generated laws, and kernel
                -- transport all see the same first-order shape.
                (betaNormalizeCanonical
                    (closeLambdas (length variables + 1) body)))
    pure (CheckedRecursiveCarrierContext variables checked)

prepareRecursiveCarrierMonotonicityTarget
    :: CheckedRecursiveCarrierContext (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (FrozenCheckedCore (InductiveGlobal global))
prepareRecursiveCarrierMonotonicityTarget
        context@(CheckedRecursiveCarrierContext variables _template) = do
    target <-
        buildUnderVariables emptyEnvironment variables \environment -> do
            underSets <- shiftEnvironment =<< shiftEnvironment environment
            left <-
                instantiateRecursiveCarrier
                    underSets (CBound 1) context
            right <-
                instantiateRecursiveCarrier
                    underSets (CBound 0) context
            pure
                (CImp
                    (subsetTerm (CBound 1) (CBound 0))
                    (subsetTerm left right))
    freezeClosedTarget
        (closeForalls (length variables + 2) target)

instantiateRecursiveCarrier
    :: InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CheckedRecursiveCarrierContext (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
instantiateRecursiveCarrier environment replacement
        context@(CheckedRecursiveCarrierContext variables _template) = do
    arguments <- traverse (`lookupEnvironment` environment) variables
    foldM instantiateLambda
        (frozenCoreTerm (checkedRecursiveCarrierTemplate context))
        (arguments <> [replacement])
  where
    instantiateLambda term argument =
        case term of
            CLam TySet body ->
                pure (instantiateCanonical argument body)
            _ ->
                Left
                    (TypedInductiveUnsupportedExpression
                        "a checked recursive carrier context lost its set telescope")

lowerRecursiveCarrierContext
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> RecursiveCarrierContext
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lowerRecursiveCarrierContext resolveGlobal environment replacement
        (RecursiveCarrierContext _location source) =
    go source
  where
    go = \case
        TermVar RecursiveCarrierHole ->
            pure replacement
        TermVar (RecursiveCarrierSourceVariable variable) ->
            lookupEnvironment variable environment
        TermSymbol _location symbol arguments -> do
            lowered <- traverse go arguments
            lowerApplicationTerms resolveGlobal symbol lowered
        _ ->
            Left
                (TypedInductiveUnsupportedExpression
                    "a validated recursive carrier context left the supported set-term fragment")

prepareCarrierBody
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (FrozenCheckedCore (InductiveGlobal global))
prepareCarrierBody resolveGlobal inductive = do
    body <-
        buildUnderVariables
            emptyEnvironment
            (preparedInductiveParams
                inductive)
            (\env -> fixedPointTerm
                resolveGlobal
                inductive
                env)
    let closed =
            closeLambdas
                    (length
                    (preparedInductiveParams
                        inductive))
                body
    checked <-
        first TypedInductiveCoreError
            (checkCanonicalCore
                (Just . inductiveGlobalType)
                closed)
    pure checked

prepareDirectGuardTarget
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> DirectInductive
    -> DirectInductiveClause
    -> Either
        TypedInductiveError
        (FrozenCheckedCore (InductiveGlobal global))
prepareDirectGuardTarget
        resolveGlobal
        inductive
        clause = do
    target <-
        buildUnderVariables
            emptyEnvironment
            (directInductiveParams inductive
                <> directClauseVariables clause)
            (\environment -> do
                domain <-
                    lowerTerm
                        resolveGlobal
                        environment
                        (directInductiveDomain
                            inductive)
                conditions <-
                    traverse
                        (directConditionTerm
                            resolveGlobal
                            environment
                            domain)
                        (directClauseConditions
                            clause)
                result <-
                    lowerTerm
                        resolveGlobal
                        environment
                        (directClauseResult
                            clause)
                pure
                    (impliesIfNeeded
                        (conjunctionList
                            conditions)
                        (memberTerm
                            result
                            domain)))
    freezeClosedTarget
        (closeForalls
            (length
                (directInductiveParams inductive
                    <> directClauseVariables clause))
            target)

assignGuardSources
    :: CheckedFoundation
    -> [FrozenCheckedCore (InductiveGlobal global)]
    -> [PreparedInductiveGuard (InductiveGlobal global)]
assignGuardSources foundation =
    snd . List.mapAccumL assign 0
  where
    assign nextImport target =
        case matchingFoundationAxiom target of
            Just tag ->
                (nextImport, PreparedFoundationGuard tag)
            Nothing ->
                ( nextImport + 1
                , PreparedImportedGuard
                    (importIx nextImport)
                    target
                )

    matchingFoundationAxiom target =
        List.find
            (\tag ->
                mapFrozenGlobals
                    absurd
                    (foundationAxiomFrozen
                        foundation
                        tag)
                    == target)
            [minBound .. maxBound]

prepareFacts
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Marker
    -> PreparedInductiveSource (InductiveGlobal global)
    -> NonEmpty (PreparedInductiveGuard (InductiveGlobal global))
    -> Either
        TypedInductiveError
        (NonEmpty (PreparedTypedInductiveFact (InductiveGlobal global)))
prepareFacts
        foundation
        resolveGlobal
        marker
        inductive
        guards = do
    introductions <-
        sequence
            (NonEmpty.zipWith
                (\clauseIndex pair ->
                    first
                        (TypedInductiveFactPreparationFailed
                            (introMarker
                                marker
                                (clauseIndex + 1)))
                        (prepareIntroductionFact
                            foundation
                            resolveGlobal
                            marker
                            inductive
                            clauseIndex
                            pair))
                (0 :| [1 ..])
                (NonEmpty.zip
                    guards
                    (preparedInductiveClauses
                        inductive)))
    domainSubset <-
        first
            (TypedInductiveFactPreparationFailed
                (derivedMarker marker "dom_subset"))
            (prepareDomainSubsetFact
                foundation
                resolveGlobal
                marker
                inductive)
    cases <-
        first
            (TypedInductiveFactPreparationFailed
                (derivedMarker marker "cases"))
            (prepareCasesFact
                foundation
                resolveGlobal
                marker
                inductive)
    induction <-
        first
            (TypedInductiveFactPreparationFailed
                (derivedMarker marker "induct"))
            (prepareInductionFact
                foundation
                resolveGlobal
                marker
                inductive)
    pure
        (introductions
            <> (domainSubset
                :| [cases, induction]))

prepareIntroductionFact
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Marker
    -> PreparedInductiveSource (InductiveGlobal global)
    -> Natural
    -> (PreparedInductiveGuard (InductiveGlobal global), PreparedInductiveClause (InductiveGlobal global))
    -> Either
        TypedInductiveError
        (PreparedTypedInductiveFact (InductiveGlobal global))
prepareIntroductionFact
        foundation
        resolveGlobal
        marker
        inductive
        clauseIndex
        (guardSource, clause) = do
    proof <-
        proveUnderVariables
            (rootProofContext
                foundation
                (Just . inductiveGlobalType))
            emptyEnvironment
            (preparedInductiveParams inductive
                <> preparedClauseVariables clause)
            (\context environment -> do
                domain <-
                    checkedTerm context
                        =<< lowerTerm
                            resolveGlobal
                            environment
                            (preparedInductiveDomain
                                inductive)
                operator <-
                    checkedTerm context
                        =<< operatorTerm
                            resolveGlobal
                            inductive
                            environment
                fixedPoint <-
                    checkedTerm context
                        =<< fixedPointTerm
                            resolveGlobal
                            inductive
                            environment
                predicate <-
                    checkedTerm context
                        =<< operatorPredicateAt
                            resolveGlobal
                            inductive
                            environment
                            (scopedCoreTerm
                                fixedPoint)
                appliedOperatorSet <-
                    checkedTerm context
                        (CApp
                            (scopedCoreTerm operator)
                            (scopedCoreTerm
                                fixedPoint))
                conditions <-
                    traverse
                        (checkedTerm context <=<
                            conditionTerm
                                resolveGlobal
                                environment
                                (scopedCoreTerm
                                    fixedPoint))
                        (preparedClauseConditions
                            clause)
                result <-
                    checkedTerm context
                        =<< lowerTerm
                            resolveGlobal
                            environment
                            (preparedClauseResult
                                clause)
                let conditionTerms =
                        scopedCoreTerm <$> conditions
                first
                    (TypedInductivePreparationContext
                        "introduction premises")
                    (provePremises
                        context
                        conditionTerms
                        (\premiseProofs -> do
                        guardProof <-
                            preparedGuardProof
                                context
                                guardSource
                        specializedGuard <-
                            first
                                (TypedInductivePreparationContext
                                    "introduction guard specialization")
                                (eliminateWrittenForalls
                                    context
                                    environment
                                    (preparedInductiveParams
                                        inductive
                                        <> preparedClauseVariables
                                            clause)
                                    guardProof)
                        guardPremiseProofs <-
                            sequence
                                [ case condition of
                                    PreparedSideCondition _formula ->
                                        pure premiseProof
                                    PreparedDirectRecursiveCondition
                                            recursiveTerm _context -> do
                                        bound <-
                                            first
                                                TypedInductiveProofError
                                                (setLfpBoundProof
                                                    context
                                                    domain
                                                    operator)
                                        recursiveElement <-
                                            checkedTerm context
                                                =<< lowerTerm
                                                    resolveGlobal
                                                    environment
                                                    recursiveTerm
                                        implication <-
                                            first
                                                TypedInductiveProofError
                                                (forallEliminationProof
                                                    context
                                                    bound
                                                    recursiveElement)
                                        first
                                            TypedInductiveProofError
                                            (implicationEliminationProof
                                                context
                                                implication
                                                premiseProof)
                                    nested@PreparedNestedRecursiveCondition{} -> do
                                        bound <-
                                            first TypedInductiveProofError
                                                (setLfpBoundProof
                                                    context
                                                    domain
                                                    operator)
                                        recursiveElement <-
                                            checkedTerm context
                                                =<< lowerTerm
                                                    resolveGlobal
                                                    environment
                                                    (preparedRecursiveTerm
                                                        nested)
                                        transportNestedRecursiveMembership
                                            context
                                            environment
                                            nested
                                            fixedPoint
                                            domain
                                            recursiveElement
                                            bound
                                            premiseProof
                                | (condition, premiseProof) <-
                                    zip
                                        (preparedClauseConditions
                                            clause)
                                        premiseProofs
                                ]
                        inDomain <-
                            case conjunctionList
                                    conditionTerms of
                                Nothing ->
                                    pure specializedGuard
                                Just _condition -> do
                                    conjunction <-
                                        conjunctionIntroductionList
                                            context
                                            guardPremiseProofs
                                    first
                                        (TypedInductivePreparationContext
                                            "introduction guard application")
                                        (first TypedInductiveProofError
                                            (implicationEliminationProof
                                                context
                                                specializedGuard
                                                conjunction))
                        equality <-
                            first TypedInductiveProofError
                                (equalityReflexivityProof
                                    context
                                    result)
                        clauseProof <-
                            conjunctionIntroductionList
                                context
                                (premiseProofs
                                    <> [equality])
                        clauseExists <-
                            first
                                (TypedInductivePreparationContext
                                    "introduction witnesses")
                                (introduceClauseWitnesses
                                    resolveGlobal
                                    inductive
                                    clause
                                    context
                                    environment
                                    (scopedCoreTerm
                                        fixedPoint)
                                    result
                                    clauseProof)
                        alternatives <-
                            clauseFormulaTerms
                                resolveGlobal
                                inductive
                                environment
                                (scopedCoreTerm
                                    fixedPoint)
                                (scopedCoreTerm
                                    result)
                        disjunction <-
                            first
                                (TypedInductivePreparationContext
                                    "introduction disjunction")
                                (injectDisjunction
                                    context
                                    clauseIndex
                                    alternatives
                                    clauseExists)
                        inOperator <-
                            first
                                (TypedInductivePreparationContext
                                    "introduction separation")
                                (separationBackward
                                    context
                                    domain
                                    predicate
                                    result
                                    inDomain
                                    disjunction)
                        inAppliedTarget <-
                            checkedTerm context
                                (memberTerm
                                    (scopedCoreTerm
                                        result)
                                    (scopedCoreTerm
                                        appliedOperatorSet))
                        inAppliedOperator <-
                            first TypedInductiveProofError
                                (conversionProof
                                    context
                                    inOperator
                                    inAppliedTarget)
                        monotone <-
                            first
                                (TypedInductivePreparationContext
                                    "introduction bounded monotonicity")
                                (proveBoundedMonotonicity
                                    foundation
                                    resolveGlobal
                                    inductive
                                    context
                                    environment)
                        fixed <-
                            first TypedInductiveProofError
                                (setLfpFixedProof
                                    context
                                    domain
                                    operator
                                    monotone)
                        reversedFixed <-
                            first
                                (TypedInductivePreparationContext
                                    "introduction fixed-point symmetry")
                                (first TypedInductiveProofError
                                    (equalityReverseProof
                                        context
                                        fixed))
                        first
                            (TypedInductivePreparationContext
                                "introduction fixed-point transport")
                            (transportMembership
                                context
                                result
                                reversedFixed
                                inAppliedOperator))))
    preparedFact
        (introMarker
            marker
            (clauseIndex + 1))
        (if any isRecursiveCondition
                (preparedClauseConditions clause)
            then SetLfpBound :| [SetLfpFixed]
            else SetLfpFixed :| [])
        True
        proof
  where
    isRecursiveCondition = \case
        PreparedDirectRecursiveCondition{} -> True
        PreparedNestedRecursiveCondition{} -> True
        PreparedSideCondition{} -> False

preparedGuardProof
    :: ProofContext (InductiveGlobal global)
    -> PreparedInductiveGuard (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
preparedGuardProof context = \case
    PreparedFoundationGuard tag ->
        first TypedInductiveProofError
            (foundationProof context tag)
    PreparedImportedGuard index target ->
        first TypedInductiveProofError
            (importedProof context index target)

prepareDomainSubsetFact
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Marker
    -> PreparedInductiveSource (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (PreparedTypedInductiveFact (InductiveGlobal global))
prepareDomainSubsetFact
        foundation
        resolveGlobal
        marker
        inductive = do
    proof <-
        proveUnderVariables
            (rootProofContext
                foundation
                (Just . inductiveGlobalType))
            emptyEnvironment
            (preparedInductiveParams
                inductive)
            (\context environment -> do
                domain <-
                    checkedTerm context
                        =<< lowerTerm
                            resolveGlobal
                            environment
                            (preparedInductiveDomain
                                inductive)
                operator <-
                    checkedTerm context
                        =<< operatorTerm
                            resolveGlobal
                            inductive
                            environment
                first TypedInductiveProofError
                    (setLfpBoundProof
                        context
                        domain
                        operator))
    preparedFact
        (derivedMarker marker "dom_subset")
        (SetLfpBound :| [])
        False
        proof

prepareCasesFact
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Marker
    -> PreparedInductiveSource (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (PreparedTypedInductiveFact (InductiveGlobal global))
prepareCasesFact
        foundation
        resolveGlobal
        marker
        inductive = do
    proof <-
        proveUnderVariables
            (rootProofContext
                foundation
                (Just . inductiveGlobalType))
            emptyEnvironment
            (preparedInductiveParams
                inductive)
            (\parameterContext parameterEnvironment ->
                forallIntroductionTyped
                    parameterContext
                    TySet
                    (\context result -> do
                        environment <-
                            shiftEnvironment
                                parameterEnvironment
                        domain <-
                            checkedTerm context
                                =<< lowerTerm
                                    resolveGlobal
                                    environment
                                    (preparedInductiveDomain
                                        inductive)
                        operator <-
                            checkedTerm context
                                =<< operatorTerm
                                    resolveGlobal
                                    inductive
                                    environment
                        fixedPoint <-
                            checkedTerm context
                                =<< fixedPointTerm
                                    resolveGlobal
                                    inductive
                                    environment
                        predicate <-
                            checkedTerm context
                                =<< operatorPredicateAt
                                    resolveGlobal
                                    inductive
                                    environment
                                    (scopedCoreTerm
                                        fixedPoint)
                        explicitOperatorSet <-
                            checkedTerm context
                                =<< separationSetAt
                                    resolveGlobal
                                    inductive
                                    environment
                                    (scopedCoreTerm
                                        fixedPoint)
                        member <-
                            checkedTerm context
                                (memberTerm
                                    (scopedCoreTerm result)
                                    (scopedCoreTerm
                                        fixedPoint))
                        implicationIntroductionTyped
                            context
                            member
                            (\withMember memberProof -> do
                                monotone <-
                                    proveBoundedMonotonicity
                                        foundation
                                        resolveGlobal
                                        inductive
                                        withMember
                                        environment
                                fixed <-
                                    first TypedInductiveProofError
                                        (setLfpFixedProof
                                            withMember
                                            domain
                                            operator
                                            monotone)
                                inOperator <-
                                    transportMembership
                                        withMember
                                        result
                                        fixed
                                        memberProof
                                explicitMembership <-
                                    checkedTerm withMember
                                        (memberTerm
                                            (scopedCoreTerm
                                                result)
                                            (scopedCoreTerm
                                                explicitOperatorSet))
                                inSeparation <-
                                    first TypedInductiveProofError
                                        (conversionProof
                                            withMember
                                            inOperator
                                            explicitMembership)
                                separation <-
                                    separationForward
                                        withMember
                                        domain
                                        predicate
                                        result
                                        inSeparation
                                predicateResult <-
                                    predicateAt
                                        resolveGlobal
                                        inductive
                                        environment
                                        (scopedCoreTerm
                                            fixedPoint)
                                        (scopedCoreTerm
                                            result)
                                predicateProof <-
                                    first TypedInductiveProofError
                                        (conjunctionRightProof
                                            withMember
                                            (memberTerm
                                                (scopedCoreTerm result)
                                                (scopedCoreTerm
                                                    domain))
                                            (CApp
                                                (scopedCoreTerm
                                                    predicate)
                                                (scopedCoreTerm
                                                    result))
                                            separation)
                                predicateTarget <-
                                    checkedTerm
                                        withMember
                                        predicateResult
                                first TypedInductiveProofError
                                    (conversionProof
                                        withMember
                                        predicateProof
                                        predicateTarget))))
    preparedFact
        (derivedMarker marker "cases")
        (SetLfpFixed :| [])
        True
        proof

prepareInductionFact
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Marker
    -> PreparedInductiveSource (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (PreparedTypedInductiveFact (InductiveGlobal global))
prepareInductionFact
        foundation
        resolveGlobal
        marker
        inductive = do
    proof <-
        proveUnderVariables
            (rootProofContext
                foundation
                (Just . inductiveGlobalType))
            emptyEnvironment
            (preparedInductiveParams
                inductive)
            (\parameterContext parameterEnvironment ->
                forallIntroductionTyped
                    parameterContext
                    TySet
                    (\subsetContext subset -> do
                        environment <-
                            shiftEnvironment
                                parameterEnvironment
                        closures <-
                            closureTerms
                                resolveGlobal
                                inductive
                                environment
                                (scopedCoreTerm subset)
                        closureConjunction <-
                            checkedTerm subsetContext
                                (fromMaybe
                                    (CImp CFalsum CFalsum)
                                    (conjunctionList
                                        closures))
                        implicationIntroductionTyped
                            subsetContext
                            closureConjunction
                            (\withClosures closuresProof -> do
                                fixedPoint <-
                                    checkedTerm withClosures
                                        =<< fixedPointTerm
                                            resolveGlobal
                                            inductive
                                            environment
                                proveSubset
                                    withClosures
                                    fixedPoint
                                    subset
                                    (\elementContext element memberProof -> do
                                        elementEnvironment <-
                                            shiftEnvironment environment
                                        domain <-
                                            checkedTerm elementContext
                                                =<< lowerTerm
                                                    resolveGlobal
                                                    elementEnvironment
                                                    (preparedInductiveDomain
                                                        inductive)
                                        operator <-
                                            checkedTerm elementContext
                                                =<< operatorTerm
                                                    resolveGlobal
                                                    inductive
                                                    elementEnvironment
                                        fixedPointAtElement <-
                                            checkedTerm elementContext
                                                =<< fixedPointTerm
                                                    resolveGlobal
                                                    inductive
                                                    elementEnvironment
                                        subsetAtElement <-
                                            first TypedInductiveCoreError
                                                (weakenScopedCore
                                                    (Just . inductiveGlobalType)
                                                    TySet
                                                    subset)
                                        predicate <-
                                            membershipPredicate
                                                elementContext
                                                subsetAtElement
                                        monotone <-
                                            first
                                                (TypedInductivePreparationContext
                                                    "induction bounded monotonicity")
                                                (proveBoundedMonotonicity
                                                    foundation
                                                    resolveGlobal
                                                    inductive
                                                    elementContext
                                                    elementEnvironment)
                                        closure <-
                                            first
                                                (TypedInductivePreparationContext
                                                    "induction closure")
                                                (proveInductionClosure
                                                    foundation
                                                    resolveGlobal
                                                    inductive
                                                    elementContext
                                                    elementEnvironment
                                                    fixedPointAtElement
                                                    operator
                                                    subsetAtElement
                                                    closures
                                                    closuresProof)
                                        inducted <-
                                            first
                                            (TypedInductivePreparationContext
                                                "induction fixed-point rule")
                                            (first TypedInductiveProofError
                                                (setLfpInductProof
                                                elementContext
                                                domain
                                                operator
                                                predicate
                                                element
                                                monotone
                                                memberProof
                                                closure))
                                        expected <-
                                            checkedTerm elementContext
                                                (memberTerm
                                                    (scopedCoreTerm
                                                        element)
                                                    (scopedCoreTerm
                                                        subsetAtElement))
                                        first TypedInductiveProofError
                                            (conversionProof
                                                elementContext
                                                inducted
                                                expected)))))
    preparedFact
        (derivedMarker marker "induct")
        (SetLfpInduct :| [])
        True
        proof

proveUnderVariables
    :: ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> [VarSymbol]
    -> ( ProofContext (InductiveGlobal global)
         -> InductiveEnvironment
         -> Either
            TypedInductiveError
            (BuiltProof (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
proveUnderVariables context environment variables build =
    case variables of
        [] ->
            build context environment
        variable : remaining -> do
            extendedEnvironment <-
                extendEnvironment
                    variable
                    environment
            forallIntroductionTyped
                context
                TySet
                (\extended _bound ->
                    proveUnderVariables
                        extended
                        extendedEnvironment
                        remaining
                        build)

checkedTerm
    :: ProofContext (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (ScopedCheckedCore (InductiveGlobal global))
checkedTerm context =
    first TypedInductiveProofError
        . scopedTerm context

preparedFact
    :: Marker
    -> NonEmpty KernelRuleTag
    -> Bool
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (PreparedTypedInductiveFact (InductiveGlobal global))
preparedFact marker rules requiresMonotonicities proof = do
    target <-
        maybe
            (Left TypedInductiveProofRemainedOpen)
            Right
            (closeScopedCore
                (builtProofStatement proof))
    pure
        (PreparedTypedInductiveFact
            ( marker
            , target
            , canonicalRules rules
            , requiresMonotonicities
            , builtProofDerivation proof
            ))
  where
    canonicalRules supplied =
        case Set.toAscList
                (Set.fromList (NonEmpty.toList supplied)) of
            firstRule : remainingRules ->
                firstRule :| remainingRules
            [] ->
                impossible "a nonempty guarded-rule set became empty"

introMarker :: Marker -> Natural -> Marker
introMarker (Marker marker) index =
    Marker
        (marker
            <> "_intro_"
            <> Text.pack (show index))

derivedMarker :: Marker -> Text -> Marker
derivedMarker (Marker marker) suffix =
    Marker
        (marker <> "_" <> suffix)

eliminateWrittenForalls
    :: ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> [VarSymbol]
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
eliminateWrittenForalls
        context
        environment
        variables
        initial =
    foldM
        (\proof variable -> do
            argument <-
                checkedTerm context
                    =<< lookupEnvironment
                        variable
                        environment
            first TypedInductiveProofError
                (forallEliminationProof
                    context
                    proof
                    argument))
        initial
        variables

provePremises
    :: ProofContext (InductiveGlobal global)
    -> [CanonicalTerm (InductiveGlobal global)]
    -> ( [BuiltProof (InductiveGlobal global)]
         -> Either
            TypedInductiveError
            (BuiltProof (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
provePremises context premises build =
    case conjunctionList premises of
        Nothing ->
            build []
        Just conjunction -> do
            proposition <-
                checkedTerm context conjunction
            implicationIntroductionTyped
                context
                proposition
                (\extended conjunctionProof -> do
                    projections <-
                        projectConjunctionList
                            extended
                            premises
                            conjunctionProof
                    build projections)

conjunctionIntroductionList
    :: ProofContext (InductiveGlobal global)
    -> [BuiltProof (InductiveGlobal global)]
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
conjunctionIntroductionList _context [] =
    Left
        (TypedInductiveUnsupportedExpression
            "an empty conjunction has no introduction proof")
conjunctionIntroductionList context (firstProof : remaining) =
    foldM
        (\left right ->
            first TypedInductiveProofError
                (conjunctionIntroductionProof
                    context
                    left
                    right))
        firstProof
        remaining

projectConjunctionList
    :: ProofContext (InductiveGlobal global)
    -> [CanonicalTerm (InductiveGlobal global)]
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        [BuiltProof (InductiveGlobal global)]
projectConjunctionList _context [] _proof =
    pure []
projectConjunctionList _context [_only] proof =
    pure [proof]
projectConjunctionList context terms proof = do
    let preceding =
            List.init terms
        final =
            List.last terms
        precedingTerm =
            fromMaybe
                CFalsum
                (conjunctionList preceding)
    precedingProof <-
        first TypedInductiveProofError
            (conjunctionLeftProof
                context
                precedingTerm
                final
                proof)
    finalProof <-
        first TypedInductiveProofError
            (conjunctionRightProof
                context
                precedingTerm
                final
                proof)
    (<> [finalProof])
        <$> projectConjunctionList
            context
            preceding
            precedingProof

introduceClauseWitnesses
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> PreparedInductiveClause (InductiveGlobal global)
    -> ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
introduceClauseWitnesses
        resolveGlobal
        _inductive
        clause
        context
        environment
        candidate
        result
        bodyProof =
    introduce
        (preparedClauseVariables clause)
  where
    introduce [] =
        pure bodyProof
    introduce (variable : remaining) = do
        inner <-
            introduce remaining
        witness <-
            checkedTerm context
                =<< lookupEnvironment
                    variable
                    environment
        underBinderEnvironment <-
            rebindEnvironment
                variable
                =<< shiftEnvironment
                    environment
        let candidate' =
                shiftCanonicalTerm 1 0 candidate
            result' =
                shiftCanonicalTerm
                    1
                    0
                    (scopedCoreTerm result)
        bodyUnderBinderTerm <-
            clauseFormulaWithBinders
                resolveGlobal
                clause
                underBinderEnvironment
                candidate'
                result'
                remaining
        bodyUnderBinder <-
            first TypedInductiveCoreError
                (checkScopedCanonicalCore
                    (Just . inductiveGlobalType)
                    (TySet
                        : proofContextTypes
                            context)
                    bodyUnderBinderTerm)
        first TypedInductiveProofError
            (existentialIntroductionProof
                context
                TySet
                bodyUnderBinder
                witness
                inner)

clauseFormulaWithBinders
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveClause (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> [VarSymbol]
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
clauseFormulaWithBinders
        resolveGlobal
        clause
        environment
        candidate
        result = \case
    [] -> do
        conditions <-
            traverse
                (conditionTerm
                    resolveGlobal
                    environment
                    candidate)
                (preparedClauseConditions
                    clause)
        clauseResult <-
            lowerTerm
                resolveGlobal
                environment
                (preparedClauseResult clause)
        pure
            (fromMaybe
                (CEq TySet result clauseResult)
                (conjunctionList
                    (conditions
                        <> [CEq
                            TySet
                            result
                            clauseResult])))
    variable : remaining -> do
        extended <-
            rebindEnvironment
                variable
                =<< shiftEnvironment
                    environment
        body <-
            clauseFormulaWithBinders
                resolveGlobal
                clause
                extended
                (shiftCanonicalTerm
                    1
                    0
                    candidate)
                (shiftCanonicalTerm
                    1
                    0
                    result)
                remaining
        pure (existentialTerm TySet body)

rebindEnvironment
    :: VarSymbol
    -> InductiveEnvironment
    -> Either
        TypedInductiveError
        InductiveEnvironment
rebindEnvironment variable
        (InductiveEnvironment variables) =
    pure
        (InductiveEnvironment
            (Map.insert variable 0 variables))

injectDisjunction
    :: ProofContext (InductiveGlobal global)
    -> Natural
    -> [CanonicalTerm (InductiveGlobal global)]
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
injectDisjunction context index alternatives proof =
    case splitAtNatural index alternatives of
        Nothing ->
            Left
                (TypedInductiveUnsupportedExpression
                    "inductive clause index is outside the source-ordered alternatives")
        Just (preceding, _selected, following) -> do
            selectedProof <-
                case preceding of
                    [] ->
                        pure proof
                    _ -> do
                        let precedingTerm =
                                disjunctionList preceding
                        first TypedInductiveProofError
                            (disjunctionRightProof
                                context
                                precedingTerm
                                proof)
            foldM
                (\current followingTerm ->
                    first TypedInductiveProofError
                        (disjunctionLeftProof
                            context
                            followingTerm
                            current))
                selectedProof
                following
  where
    splitAtNatural
        :: Natural
        -> [a]
        -> Maybe ([a], a, [a])
    splitAtNatural =
        go []
      where
        go _preceding _index [] =
            Nothing
        go preceding 0 (selected : rest) =
            Just
                ( reverse preceding
                , selected
                , rest
                )
        go preceding current (item : rest) =
            go
                (item : preceding)
                (current - 1)
                rest

closureTerms
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        [CanonicalTerm (InductiveGlobal global)]
closureTerms
        resolveGlobal
        inductive
        environment
        subset =
    traverse closureFor
        (NonEmpty.toList
            (preparedInductiveClauses
                inductive))
  where
    closureFor clause = do
        clauseEnvironment <-
            extendVariables
                environment
                (preparedClauseVariables clause)
        let binderCount =
                fromIntegral
                    (length
                        (preparedClauseVariables
                            clause))
            subset' =
                shiftCanonicalTerm
                    binderCount
                    0
                    subset
        conditions <-
            traverse
                (conditionTerm
                    resolveGlobal
                    clauseEnvironment
                    subset')
                (preparedClauseConditions
                    clause)
        result <-
            lowerTerm
                resolveGlobal
                clauseEnvironment
                (preparedClauseResult clause)
        pure
            (closeForalls
                (length
                    (preparedClauseVariables
                        clause))
                (impliesIfNeeded
                    (conjunctionList conditions)
                    (memberTerm
                        result
                        subset')))

proveBoundedMonotonicity
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
proveBoundedMonotonicity
        _foundation
        resolveGlobal
        inductive
        context
        environment = do
    domain <-
        checkedTerm context
            =<< lowerTerm
                resolveGlobal
                environment
                (preparedInductiveDomain
                    inductive)
    operator <-
        checkedTerm context
            =<< operatorTerm
                resolveGlobal
                inductive
                environment
    operatorDomain <-
        checkedTerm context
            (CApp
                (scopedCoreTerm operator)
                (scopedCoreTerm domain))
    bounded <-
        first
            (TypedInductivePreparationContext
                "bounded monotonicity range")
            (proveSubset
                context
                operatorDomain
                domain
                (\elementContext element membership -> do
                    elementEnvironment <-
                        shiftEnvironment environment
                    domainAtElement <-
                        checkedTerm elementContext
                            =<< lowerTerm
                                resolveGlobal
                                elementEnvironment
                                (preparedInductiveDomain
                                    inductive)
                    predicate <-
                        checkedTerm elementContext
                            =<< operatorPredicateAt
                                resolveGlobal
                                inductive
                                elementEnvironment
                                (scopedCoreTerm
                                    domainAtElement)
                    explicitOperator <-
                        checkedTerm elementContext
                            =<< separationSetAt
                                resolveGlobal
                                inductive
                                elementEnvironment
                                (scopedCoreTerm
                                    domainAtElement)
                    explicitMembership <-
                        checkedTerm elementContext
                            (memberTerm
                                (scopedCoreTerm element)
                                (scopedCoreTerm
                                    explicitOperator))
                    separatedMembership <-
                        first TypedInductiveProofError
                            (conversionProof
                                elementContext
                                membership
                                explicitMembership)
                    characteristic <-
                        separationForward
                            elementContext
                            domainAtElement
                            predicate
                            element
                            separatedMembership
                    first TypedInductiveProofError
                        (conjunctionLeftProof
                            elementContext
                            (memberTerm
                                (scopedCoreTerm element)
                                (scopedCoreTerm
                                    domainAtElement))
                            (CApp
                                (scopedCoreTerm predicate)
                                (scopedCoreTerm element))
                            characteristic)))
    monotone <-
        first
            (TypedInductivePreparationContext
                "bounded monotonicity relation")
            (forallIntroductionTyped
                context
                TySet
                (\xContext _x ->
                forallIntroductionTyped
                    xContext
                    TySet
                    (\xyContext _y -> do
                        xyEnvironment <-
                            shiftEnvironment
                                =<< shiftEnvironment
                                    environment
                        x <-
                            checkedTerm xyContext
                                (CBound 1)
                        y <-
                            checkedTerm xyContext
                                (CBound 0)
                        domainXY <-
                            checkedTerm xyContext
                                =<< lowerTerm
                                    resolveGlobal
                                    xyEnvironment
                                    (preparedInductiveDomain
                                        inductive)
                        relation <-
                            checkedTerm xyContext
                                (conjunctionTerm
                                    (subsetTerm
                                        (scopedCoreTerm x)
                                        (scopedCoreTerm y))
                                    (subsetTerm
                                        (scopedCoreTerm y)
                                        (scopedCoreTerm
                                            domainXY)))
                        implicationIntroductionTyped
                            xyContext
                            relation
                            (\relatedContext _relationProof -> do
                                operatorXY <-
                                    checkedTerm relatedContext
                                        =<< operatorTerm
                                            resolveGlobal
                                            inductive
                                            xyEnvironment
                                operatorX <-
                                    checkedTerm relatedContext
                                        (CApp
                                            (scopedCoreTerm
                                                operatorXY)
                                            (scopedCoreTerm x))
                                operatorY <-
                                    checkedTerm relatedContext
                                        (CApp
                                            (scopedCoreTerm
                                                operatorXY)
                                            (scopedCoreTerm y))
                                proveSubset
                                    relatedContext
                                    operatorX
                                    operatorY
                                    (\elementContext element membership -> do
                                        elementEnvironment <-
                                            shiftEnvironment
                                                xyEnvironment
                                        xAtElement <-
                                            checkedTerm
                                                elementContext
                                                (CBound 2)
                                        yAtElement <-
                                            checkedTerm
                                                elementContext
                                                (CBound 1)
                                        domainAtElement <-
                                            checkedTerm
                                                elementContext
                                                =<< lowerTerm
                                                    resolveGlobal
                                                    elementEnvironment
                                                    (preparedInductiveDomain
                                                        inductive)
                                        predicateX <-
                                            checkedTerm
                                                elementContext
                                                =<< operatorPredicateAt
                                                    resolveGlobal
                                                    inductive
                                                    elementEnvironment
                                                    (scopedCoreTerm
                                                        xAtElement)
                                        predicateY <-
                                            checkedTerm
                                                elementContext
                                                =<< operatorPredicateAt
                                                    resolveGlobal
                                                    inductive
                                                    elementEnvironment
                                                    (scopedCoreTerm
                                                        yAtElement)
                                        explicitX <-
                                            checkedTerm
                                                elementContext
                                                =<< separationSetAt
                                                    resolveGlobal
                                                    inductive
                                                    elementEnvironment
                                                    (scopedCoreTerm
                                                        xAtElement)
                                        memberExplicitX <-
                                            checkedTerm
                                                elementContext
                                                (memberTerm
                                                    (scopedCoreTerm
                                                        element)
                                                    (scopedCoreTerm
                                                        explicitX))
                                        separatedX <-
                                            first TypedInductiveProofError
                                                (conversionProof
                                                    elementContext
                                                    membership
                                                    memberExplicitX)
                                        characteristicX <-
                                            separationForward
                                                elementContext
                                                domainAtElement
                                                predicateX
                                                element
                                                separatedX
                                        inDomain <-
                                            first
                                                (TypedInductivePreparationContext
                                                    "monotonicity domain projection")
                                                (first TypedInductiveProofError
                                                    (conjunctionLeftProof
                                                        elementContext
                                                        (memberTerm
                                                            (scopedCoreTerm
                                                                element)
                                                            (scopedCoreTerm
                                                                domainAtElement))
                                                        (CApp
                                                            (scopedCoreTerm
                                                                predicateX)
                                                            (scopedCoreTerm
                                                                element))
                                                        characteristicX))
                                        satisfiesX <-
                                            first
                                                (TypedInductivePreparationContext
                                                    "monotonicity predicate projection")
                                                (first TypedInductiveProofError
                                                    (conjunctionRightProof
                                                        elementContext
                                                        (memberTerm
                                                            (scopedCoreTerm
                                                                element)
                                                            (scopedCoreTerm
                                                                domainAtElement))
                                                        (CApp
                                                            (scopedCoreTerm
                                                                predicateX)
                                                            (scopedCoreTerm
                                                                element))
                                                        characteristicX))
                                        alternativesX <-
                                            clauseFormulaTerms
                                                resolveGlobal
                                                inductive
                                                elementEnvironment
                                                (scopedCoreTerm
                                                    xAtElement)
                                                (scopedCoreTerm
                                                    element)
                                        alternativesY <-
                                            clauseFormulaTerms
                                                resolveGlobal
                                                inductive
                                                elementEnvironment
                                                (scopedCoreTerm
                                                    yAtElement)
                                                (scopedCoreTerm
                                                    element)
                                        predicateXTarget <-
                                            checkedTerm
                                                elementContext
                                                (disjunctionList
                                                    alternativesX)
                                        satisfiesX' <-
                                            first TypedInductiveProofError
                                                (conversionProof
                                                    elementContext
                                                    satisfiesX
                                                    predicateXTarget)
                                        satisfiesY <-
                                            first
                                                (TypedInductivePreparationContext
                                                    "monotonicity predicate transport")
                                                (transformPredicateProof
                                                    resolveGlobal
                                                    inductive
                                                    elementContext
                                                    elementEnvironment
                                                    (scopedCoreTerm
                                                        xAtElement)
                                                    (scopedCoreTerm
                                                        yAtElement)
                                                    (scopedCoreTerm
                                                        domainAtElement)
                                                    (scopedCoreTerm
                                                        element)
                                                    alternativesX
                                                    alternativesY
                                                    satisfiesX')
                                        separatedY <-
                                            first
                                                (TypedInductivePreparationContext
                                                    "monotonicity separation")
                                                (separationBackward
                                                    elementContext
                                                    domainAtElement
                                                    predicateY
                                                    element
                                                    inDomain
                                                    satisfiesY)
                                        operatorYAtElement <-
                                            first
                                                TypedInductiveCoreError
                                                (weakenScopedCore
                                                    (Just
                                                        . inductiveGlobalType)
                                                    TySet
                                                    operatorY)
                                        explicitMembershipY <-
                                            checkedTerm
                                                elementContext
                                                (memberTerm
                                                    (scopedCoreTerm
                                                        element)
                                                    (scopedCoreTerm
                                                        operatorYAtElement))
                                        first TypedInductiveProofError
                                            (conversionProof
                                                elementContext
                                                separatedY
                                                explicitMembershipY))))))
    first
        (TypedInductivePreparationContext
            "bounded monotonicity conjunction")
        (first TypedInductiveProofError
            (conjunctionIntroductionProof
                context
                bounded
                monotone))

transformPredicateProof
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> [CanonicalTerm (InductiveGlobal global)]
    -> [CanonicalTerm (InductiveGlobal global)]
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
transformPredicateProof
        resolveGlobal
        inductive
        context
        environment
        candidateX
        candidateY
        domain
        result
        alternativesX
        alternativesY
        proof = do
    target <-
        checkedTerm context
            (disjunctionList alternativesY)
    first
        (TypedInductivePreparationContext
            "predicate disjunction elimination")
        (eliminateDisjunctionAlternatives
            context
            alternativesX
            proof
            target
            (\caseContext clauseIndex clauseProof -> do
                clause <-
                    maybe
                        (Left
                            (TypedInductiveUnsupportedExpression
                                "inductive clause inventory changed during proof construction"))
                        Right
                        (atNatural
                            clauseIndex
                            (NonEmpty.toList
                                (preparedInductiveClauses
                                    inductive)))
                first
                    (TypedInductivePreparationContext
                        "predicate witness elimination")
                    (eliminateClauseWitnesses
                        resolveGlobal
                        clause
                        caseContext
                        environment
                        candidateX
                        result
                        clauseProof
                        target
                        (\depth
                            leafContext
                            leafEnvironment
                            candidateXAtLeaf
                            resultAtLeaf
                            bodyProof -> do
                            let candidateYAtLeaf =
                                    shiftCanonicalTerm
                                        depth
                                        0
                                        candidateY
                                domainAtLeaf =
                                    shiftCanonicalTerm
                                        depth
                                        0
                                        domain
                                alternativesYAtLeaf =
                                    shiftCanonicalTerm
                                        depth
                                        0
                                        <$> alternativesY
                            bodyY <-
                                first
                                    (TypedInductivePreparationContext
                                        "predicate clause body")
                                    (transformClauseBody
                                        resolveGlobal
                                        clause
                                        leafContext
                                        leafEnvironment
                                        candidateXAtLeaf
                                        candidateYAtLeaf
                                        domainAtLeaf
                                        resultAtLeaf
                                        bodyProof)
                            resultAtLeaf' <-
                                checkedTerm
                                    leafContext
                                    resultAtLeaf
                            alternativeY <-
                                introduceClauseWitnesses
                                    resolveGlobal
                                    inductive
                                    clause
                                    leafContext
                                    leafEnvironment
                                    candidateYAtLeaf
                                    resultAtLeaf'
                                    bodyY
                            first
                                (TypedInductivePreparationContext
                                    "predicate disjunction injection")
                                (injectDisjunction
                                    leafContext
                                    clauseIndex
                                    alternativesYAtLeaf
                                    alternativeY)))))

transformClauseBody
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveClause (InductiveGlobal global)
    -> ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
transformClauseBody
        resolveGlobal
        clause
        context
        environment
        candidateX
        candidateY
        domain
        result
        proof = do
    conditionsX <-
        traverse
            (conditionTerm
                resolveGlobal
                environment
                candidateX)
            (preparedClauseConditions
                clause)
    clauseResult <-
        lowerTerm
            resolveGlobal
            environment
            (preparedClauseResult clause)
    let equality =
            CEq TySet result clauseResult
        bodyTermsX =
            conditionsX <> [equality]
    projections <-
        projectConjunctionList
            context
            bodyTermsX
            proof
    let (conditionProofs, equalityProofs) =
            splitAt
                (length conditionsX)
                projections
    transformedConditions <-
        sequence
            [ case condition of
                PreparedSideCondition _formula ->
                    pure conditionProof
                PreparedDirectRecursiveCondition
                        recursiveTerm _context -> do
                    recursiveElement <-
                        checkedTerm context
                            =<< lowerTerm
                                resolveGlobal
                                environment
                                recursiveTerm
                    subsetProof <-
                        subsetRelationHypothesis
                            context
                            candidateX
                            candidateY
                            domain
                    implication <-
                        first TypedInductiveProofError
                            (forallEliminationProof
                                context
                                subsetProof
                                recursiveElement)
                    first TypedInductiveProofError
                        (implicationEliminationProof
                            context
                            implication
                            conditionProof)
                nested@PreparedNestedRecursiveCondition{} -> do
                    recursiveElement <-
                        checkedTerm context
                            =<< lowerTerm
                                resolveGlobal
                                environment
                                (preparedRecursiveTerm nested)
                    subsetProof <-
                        subsetRelationHypothesis
                            context
                            candidateX
                            candidateY
                            domain
                    left <- checkedTerm context candidateX
                    right <- checkedTerm context candidateY
                    transportNestedRecursiveMembership
                        context
                        environment
                        nested
                        left
                        right
                        recursiveElement
                        subsetProof
                        conditionProof
            | (condition, conditionProof) <-
                zip
                    (preparedClauseConditions clause)
                    conditionProofs
            ]
    equalityProof <-
        case equalityProofs of
            [only] ->
                pure only
            _ ->
                Left
                    (TypedInductiveUnsupportedExpression
                        "inductive clause equality projection is inconsistent")
    conjunctionIntroductionList
        context
        (transformedConditions
            <> [equalityProof])

subsetRelationHypothesis
    :: ProofContext (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
subsetRelationHypothesis
        context
        left
        right
        domain = do
    let leftSubsetRight =
            subsetTerm left right
        rightSubsetDomain =
            subsetTerm right domain
        relation =
            conjunctionTerm
                leftSubsetRight
                rightSubsetDomain
    relationTerm <-
        checkedTerm context relation
    relationProof <-
        first TypedInductiveProofError
            (hypothesisProof
                context
                relationTerm)
    first TypedInductiveProofError
        (conjunctionLeftProof
            context
            leftSubsetRight
            rightSubsetDomain
            relationProof)

preparedRecursiveTerm
    :: PreparedInductiveCondition global
    -> Term
preparedRecursiveTerm = \case
    PreparedDirectRecursiveCondition term _context -> term
    PreparedNestedRecursiveCondition term _context _index _target -> term
    PreparedSideCondition{} ->
        impossible "a side condition has no recursive element"

transportNestedRecursiveMembership
    :: ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> PreparedInductiveCondition (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
transportNestedRecursiveMembership
        context
        environment
        condition
        left
        right
        element
        subsetProof
        membership = do
    monotonicity <-
        nestedRecursiveMonotonicityProof
            context environment condition left right subsetProof
    implication <-
        first TypedInductiveProofError
            (forallEliminationProof
                context monotonicity element)
    first TypedInductiveProofError
        (implicationEliminationProof
            context implication membership)

nestedRecursiveMonotonicityProof
    :: ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> PreparedInductiveCondition (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
nestedRecursiveMonotonicityProof
        context
        environment
        (PreparedNestedRecursiveCondition
            _term
            (CheckedRecursiveCarrierContext variables _template)
            index
            target)
        left
        right
        subsetProof = do
    theorem <-
        first TypedInductiveProofError
            (importedProof context index target)
    specialized <-
        eliminateWrittenForalls
            context environment variables theorem
    atLeft <-
        first TypedInductiveProofError
            (forallEliminationProof context specialized left)
    atRight <-
        first TypedInductiveProofError
            (forallEliminationProof context atLeft right)
    first TypedInductiveProofError
        (implicationEliminationProof
            context atRight subsetProof)
nestedRecursiveMonotonicityProof
        _context _environment _condition _left _right _subsetProof =
    Left
        (TypedInductiveUnsupportedExpression
            "nested carrier transport requires a monotonicity import")

proveInductionCandidateSubset
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
proveInductionCandidateSubset
        context fixedPoint predicate candidate subset =
    proveSubset
        context candidate subset
        (\elementContext element membership -> do
            fixedPointAtElement <-
                first TypedInductiveCoreError
                    (weakenScopedCore
                        (Just . inductiveGlobalType)
                        TySet
                        fixedPoint)
            predicateAtElement <-
                first TypedInductiveCoreError
                    (weakenScopedCore
                        (Just . inductiveGlobalType)
                        TySet
                        predicate)
            explicitMembership <-
                checkedTerm elementContext
                    (memberTerm
                        (scopedCoreTerm element)
                        (apply2
                            (CIntrinsic Sep)
                            (scopedCoreTerm fixedPointAtElement)
                            (scopedCoreTerm predicateAtElement)))
            membership' <-
                first TypedInductiveProofError
                    (conversionProof
                        elementContext membership explicitMembership)
            characteristic <-
                separationForward
                    elementContext
                    fixedPointAtElement
                    predicateAtElement
                    element
                    membership'
            satisfies <-
                first TypedInductiveProofError
                    (conjunctionRightProof
                        elementContext
                        (memberTerm
                            (scopedCoreTerm element)
                            (scopedCoreTerm fixedPointAtElement))
                        (CApp
                            (scopedCoreTerm predicateAtElement)
                            (scopedCoreTerm element))
                        characteristic)
            expected <-
                first TypedInductiveCoreError
                    (weakenScopedCore
                        (Just . inductiveGlobalType)
                        TySet
                        subset)
            target <-
                checkedTerm elementContext
                    (memberTerm
                        (scopedCoreTerm element)
                        (scopedCoreTerm expected))
            first TypedInductiveProofError
                (conversionProof
                    elementContext satisfies target))

eliminateClauseWitnesses
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveClause (InductiveGlobal global)
    -> ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ( Natural
         -> ProofContext (InductiveGlobal global)
         -> InductiveEnvironment
         -> CanonicalTerm (InductiveGlobal global)
         -> CanonicalTerm (InductiveGlobal global)
         -> BuiltProof (InductiveGlobal global)
         -> Either
            TypedInductiveError
            (BuiltProof (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
eliminateClauseWitnesses
        resolveGlobal
        clause
        initialContext
        initialEnvironment
        initialCandidate
        initialResult
        initialProof
        initialTarget
        finish =
    go
        0
        initialContext
        initialEnvironment
        initialCandidate
        initialResult
        initialProof
        initialTarget
        (preparedClauseVariables clause)
  where
    go depth context environment candidate result proof target = \case
        [] ->
            finish
                depth
                context
                environment
                candidate
                result
                proof
        variable : remaining -> do
            underBinderEnvironment <-
                rebindEnvironment
                    variable
                    =<< shiftEnvironment
                        environment
            let candidate' =
                    shiftCanonicalTerm
                        1
                        0
                        candidate
                result' =
                    shiftCanonicalTerm
                        1
                        0
                        result
            bodyUnderBinderTerm <-
                clauseFormulaWithBinders
                    resolveGlobal
                    clause
                    underBinderEnvironment
                    candidate'
                    result'
                    remaining
            bodyUnderBinder <-
                first TypedInductiveCoreError
                    (checkScopedCanonicalCore
                        (Just . inductiveGlobalType)
                        (TySet
                            : proofContextTypes
                                context)
                        bodyUnderBinderTerm)
            targetUnderBinder <-
                first TypedInductiveCoreError
                    (weakenScopedCore
                        (Just . inductiveGlobalType)
                        TySet
                        target)
            first TypedInductiveProofError
                (existentialEliminationProof
                    context
                    TySet
                    bodyUnderBinder
                    proof
                    target
                    (\underBinderContext _witness bodyProof ->
                        first typedAsProofError
                            (go
                                (depth + 1)
                                underBinderContext
                                underBinderEnvironment
                                candidate'
                                result'
                                bodyProof
                                targetUnderBinder
                                remaining)))

eliminateDisjunctionAlternatives
    :: ProofContext (InductiveGlobal global)
    -> [CanonicalTerm (InductiveGlobal global)]
    -> BuiltProof (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ( ProofContext (InductiveGlobal global)
         -> Natural
         -> BuiltProof (InductiveGlobal global)
         -> Either
            TypedInductiveError
            (BuiltProof (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
eliminateDisjunctionAlternatives
        initialContext
        alternatives
        proof
        target
        handle =
    go initialContext 0 alternatives proof
  where
    go _context _offset [] _proof =
        Left
            (TypedInductiveUnsupportedExpression
                "an inductive predicate has no alternatives")
    go context offset [_only] onlyProof =
        handle context offset onlyProof
    go context offset current currentProof = do
        let preceding =
                List.init current
            final =
                List.last current
            precedingTerm =
                disjunctionList preceding
            finalIndex =
                offset
                    + fromIntegral
                        (length preceding)
        first TypedInductiveProofError
            (disjunctionEliminationProof
                context
                precedingTerm
                final
                currentProof
                target
                (\leftContext leftProof ->
                    first typedAsProofError
                        (go
                            leftContext
                            offset
                            preceding
                            leftProof))
                (\rightContext rightProof ->
                    first typedAsProofError
                        (handle
                            rightContext
                            finalIndex
                            rightProof)))

proveInductionClosure
    :: CheckedFoundation
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> [CanonicalTerm (InductiveGlobal global)]
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
proveInductionClosure
        _foundation
        resolveGlobal
        inductive
        context
        environment
        fixedPoint
        operator
        subset
        closures
        _closuresProof =
    forallIntroductionTyped
        context
        TySet
        (\elementContext element -> do
            elementEnvironment <-
                shiftEnvironment environment
            fixedPointAtElement <-
                first TypedInductiveCoreError
                    (weakenScopedCore
                        (Just . inductiveGlobalType)
                        TySet
                        fixedPoint)
            operatorAtElement <-
                first TypedInductiveCoreError
                    (weakenScopedCore
                        (Just . inductiveGlobalType)
                        TySet
                        operator)
            subsetAtElement <-
                first TypedInductiveCoreError
                    (weakenScopedCore
                        (Just . inductiveGlobalType)
                        TySet
                        subset)
            inductionPredicate <-
                membershipPredicate
                    elementContext
                    subsetAtElement
            candidate <-
                checkedTerm elementContext
                    (apply2
                        (CIntrinsic Sep)
                        (scopedCoreTerm
                            fixedPointAtElement)
                        (scopedCoreTerm
                            inductionPredicate))
            unfolded <-
                checkedTerm elementContext
                    (CApp
                        (scopedCoreTerm
                            operatorAtElement)
                        (scopedCoreTerm
                            candidate))
            premise <-
                checkedTerm elementContext
                    (memberTerm
                        (scopedCoreTerm element)
                        (scopedCoreTerm unfolded))
            implicationIntroductionTyped
                elementContext
                premise
                (\withMember memberProof -> do
                    domain <-
                        checkedTerm withMember
                            =<< lowerTerm
                                resolveGlobal
                                elementEnvironment
                                (preparedInductiveDomain
                                    inductive)
                    operatorPredicate <-
                        checkedTerm withMember
                            =<< operatorPredicateAt
                                resolveGlobal
                                inductive
                                elementEnvironment
                                (scopedCoreTerm
                                    candidate)
                    explicitOperator <-
                        checkedTerm withMember
                            =<< separationSetAt
                                resolveGlobal
                                inductive
                                elementEnvironment
                                (scopedCoreTerm
                                    candidate)
                    explicitMembership <-
                        checkedTerm withMember
                            (memberTerm
                                (scopedCoreTerm
                                    element)
                                (scopedCoreTerm
                                    explicitOperator))
                    separated <-
                        first TypedInductiveProofError
                            (conversionProof
                                withMember
                                memberProof
                                explicitMembership)
                    characteristic <-
                        separationForward
                            withMember
                            domain
                            operatorPredicate
                            element
                            separated
                    predicateProof <-
                        first TypedInductiveProofError
                            (conjunctionRightProof
                                withMember
                                (memberTerm
                                    (scopedCoreTerm
                                        element)
                                    (scopedCoreTerm
                                        domain))
                                (CApp
                                    (scopedCoreTerm
                                        operatorPredicate)
                                    (scopedCoreTerm
                                        element))
                                characteristic)
                    alternatives <-
                        clauseFormulaTerms
                            resolveGlobal
                            inductive
                            elementEnvironment
                            (scopedCoreTerm
                                candidate)
                            (scopedCoreTerm
                                element)
                    predicateTarget <-
                        checkedTerm
                            withMember
                            (disjunctionList
                                alternatives)
                    predicateProof' <-
                        first TypedInductiveProofError
                            (conversionProof
                                withMember
                                predicateProof
                                predicateTarget)
                    result <-
                        checkedTerm withMember
                            (memberTerm
                                (scopedCoreTerm
                                    element)
                                (scopedCoreTerm
                                    subsetAtElement))
                    subsetMembership <-
                        first
                        (TypedInductivePreparationContext
                            "induction clause alternatives")
                        (eliminateDisjunctionAlternatives
                            withMember
                            alternatives
                            predicateProof'
                            result
                            (\caseContext clauseIndex clauseProof -> do
                                clause <-
                                    maybe
                                        (Left
                                            (TypedInductiveUnsupportedExpression
                                                "inductive closure clause index is outside the source inventory"))
                                        Right
                                        (atNatural
                                            clauseIndex
                                            (NonEmpty.toList
                                                (preparedInductiveClauses
                                                    inductive)))
                                first
                                    (TypedInductivePreparationContext
                                        "induction clause witnesses")
                                    (eliminateClauseWitnesses
                                        resolveGlobal
                                        clause
                                        caseContext
                                        elementEnvironment
                                        (scopedCoreTerm
                                            candidate)
                                        (scopedCoreTerm
                                            element)
                                        clauseProof
                                        result
                                        (\depth
                                            leafContext
                                            leafEnvironment
                                            _candidateAtLeaf
                                            resultAtLeaf
                                            bodyProof ->
                                                first
                                                    (TypedInductivePreparationContext
                                                        "induction clause proof")
                                                    (proveInductionClause
                                                        resolveGlobal
                                                        inductive
                                                        clauseIndex
                                                        clause
                                                        leafContext
                                                        leafEnvironment
                                                        (shiftCanonicalTerm
                                                            depth
                                                            0
                                                            (scopedCoreTerm
                                                                fixedPointAtElement))
                                                        (shiftCanonicalTerm
                                                            depth
                                                            0
                                                            (scopedCoreTerm
                                                                inductionPredicate))
                                                        (shiftCanonicalTerm
                                                            depth
                                                            0
                                                            (scopedCoreTerm
                                                                subsetAtElement))
                                                        (shiftCanonicalTerm
                                                            (depth + 2)
                                                            0
                                                            <$> closures)
                                                        resultAtLeaf
                                                        bodyProof)))))
                    appliedPredicate <-
                        checkedTerm withMember
                            (CApp
                                (scopedCoreTerm
                                    inductionPredicate)
                                (scopedCoreTerm
                                    element))
                    first TypedInductiveProofError
                        (conversionProof
                            withMember
                            subsetMembership
                            appliedPredicate)))

proveInductionClause
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> Natural
    -> PreparedInductiveClause (InductiveGlobal global)
    -> ProofContext (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> [CanonicalTerm (InductiveGlobal global)]
    -> CanonicalTerm (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
proveInductionClause
        resolveGlobal
        _inductive
        clauseIndex
        clause
        context
        environment
        fixedPoint
        predicate
        subset
        closures
        result
        bodyProof = do
    conditions <-
        traverse
            (conditionTerm
                resolveGlobal
                environment
                (apply2
                    (CIntrinsic Sep)
                    fixedPoint
                    predicate))
            (preparedClauseConditions
                clause)
    clauseResult <-
        lowerTerm
            resolveGlobal
            environment
            (preparedClauseResult clause)
    let equality =
            CEq TySet result clauseResult
        bodyTerms =
            conditions <> [equality]
    projections <-
        first
            (TypedInductivePreparationContext
                "induction clause body projections")
            (projectConjunctionList
                context
                bodyTerms
                bodyProof)
    let (conditionProofs, equalityProofs) =
            splitAt
                (length conditions)
                projections
    closureConditionProofs <-
        sequence
            [ case condition of
                PreparedSideCondition _formula ->
                    pure conditionProof
                PreparedDirectRecursiveCondition
                        recursiveTerm _context -> do
                    recursiveElement <-
                        checkedTerm context
                            =<< lowerTerm
                                resolveGlobal
                                environment
                                recursiveTerm
                    fixedPoint' <-
                        checkedTerm context fixedPoint
                    predicate' <-
                        checkedTerm context predicate
                    separated <-
                        separationForward
                            context
                            fixedPoint'
                            predicate'
                            recursiveElement
                            conditionProof
                    predicateMembership <-
                        first TypedInductiveProofError
                            (conjunctionRightProof
                                context
                                (memberTerm
                                    (scopedCoreTerm
                                        recursiveElement)
                                    fixedPoint)
                                (CApp
                                    predicate
                                    (scopedCoreTerm
                                        recursiveElement))
                                separated)
                    expected <-
                        checkedTerm context
                            (memberTerm
                                (scopedCoreTerm
                                    recursiveElement)
                                subset)
                    first TypedInductiveProofError
                        (conversionProof
                            context
                            predicateMembership
                            expected)
                nested@PreparedNestedRecursiveCondition{} -> do
                    recursiveElement <-
                        checkedTerm context
                            =<< lowerTerm
                                resolveGlobal
                                environment
                                (preparedRecursiveTerm nested)
                    fixedPoint' <- checkedTerm context fixedPoint
                    predicate' <- checkedTerm context predicate
                    candidate <-
                        checkedTerm context
                            (apply2
                                (CIntrinsic Sep)
                                fixedPoint
                                predicate)
                    subset' <- checkedTerm context subset
                    candidateSubset <-
                        proveInductionCandidateSubset
                            context
                            fixedPoint'
                            predicate'
                            candidate
                            subset'
                    transportNestedRecursiveMembership
                        context
                        environment
                        nested
                        candidate
                        subset'
                        recursiveElement
                        candidateSubset
                        conditionProof
            | (condition, conditionProof) <-
                zip
                    (preparedClauseConditions clause)
                    conditionProofs
            ]
    closureConjunction <-
        case conjunctionList closures of
            Nothing ->
                Left
                    (TypedInductiveUnsupportedExpression
                        "inductive closure inventory is empty")
            Just conjunction ->
                first
                    (TypedInductivePreparationContext
                        "induction closure conjunction")
                    (checkedTerm context conjunction)
    allClosures <-
        first
            (TypedInductivePreparationContext
                "induction closure hypothesis")
            (first TypedInductiveProofError
                (hypothesisProof
                    context
                    closureConjunction))
    closureProofs <-
        first
            (TypedInductivePreparationContext
                "induction closure projections")
            (projectConjunctionList
                context
                closures
                allClosures)
    selectedClosure <-
        maybe
            (Left
                (TypedInductiveUnsupportedExpression
                    "inductive closure projection is outside the source inventory"))
            Right
            (atNatural clauseIndex closureProofs)
    specializedClosure <-
        first
            (TypedInductivePreparationContext
                "induction closure specialization")
            (eliminateWrittenForalls
                context
                environment
                (preparedClauseVariables clause)
                selectedClosure)
    resultMembership <-
        case closureConditionProofs of
            [] ->
                pure specializedClosure
            _ -> do
                conjunction <-
                    conjunctionIntroductionList
                        context
                        closureConditionProofs
                first TypedInductiveProofError
                    (implicationEliminationProof
                        context
                        specializedClosure
                        conjunction)
    equalityProof <-
        case equalityProofs of
            [only] ->
                pure only
            _ ->
                Left
                    (TypedInductiveUnsupportedExpression
                        "inductive closure equality projection is inconsistent")
    subset' <-
        first
            (TypedInductivePreparationContext
                "induction subset target")
            (checkedTerm context subset)
    first
        (TypedInductivePreparationContext
            "induction result transport")
        (transportElementMembership
            context
            subset'
            equalityProof
            resultMembership)

transportElementMembership
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
transportElementMembership
        context
        set
        equality
        membership = do
    (sourceElement, targetElement) <-
        case scopedCoreTerm
                (builtProofStatement
                    equality) of
            CEq TySet source target ->
                Right (source, target)
            _ ->
                Left
                    (TypedInductiveUnsupportedExpression
                        "element transport requires set equality")
    predicate <-
        membershipPredicate
            context
            set
    predicateReflexivity <-
        first TypedInductiveProofError
            (equalityReflexivityProof
                context
                predicate)
    propositionEquality <-
        first TypedInductiveProofError
            (equalityCongruenceApplicationProof
                context
                predicateReflexivity
                equality)
    reversed <-
        first TypedInductiveProofError
            (equalityReverseProof
                context
                propositionEquality)
    appliedTarget <-
        checkedTerm context
            (CApp
                (scopedCoreTerm predicate)
                targetElement)
    targetMembership <-
        first TypedInductiveProofError
            (conversionProof
                context
                membership
                appliedTarget)
    transported <-
        first TypedInductiveProofError
            (equalityModusPonensProof
                context
                reversed
                targetMembership)
    sourceMembership <-
        checkedTerm context
            (memberTerm
                sourceElement
                (scopedCoreTerm set))
    first TypedInductiveProofError
        (conversionProof
            context
            transported
            sourceMembership)

predicateAt
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
predicateAt
        resolveGlobal
        inductive
        environment
        candidate
        result =
    disjunctionList
        <$> clauseFormulaTerms
            resolveGlobal
            inductive
            environment
            candidate
            result

clauseFormulaTerms
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        [CanonicalTerm (InductiveGlobal global)]
clauseFormulaTerms
        resolveGlobal
        inductive
        environment
        candidate
        result =
    traverse
        (clauseFormulaAt
            resolveGlobal
            environment
            candidate
            result)
        (NonEmpty.toList
            (preparedInductiveClauses
                inductive))

clauseFormulaAt
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> CanonicalTerm (InductiveGlobal global)
    -> PreparedInductiveClause (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
clauseFormulaAt
        resolveGlobal
        environment
        candidate
        result
        clause = do
    clauseEnvironment <-
        extendVariables
            environment
            (preparedClauseVariables clause)
    let binderCount =
            fromIntegral
                (length
                    (preparedClauseVariables
                        clause))
        candidate' =
            shiftCanonicalTerm binderCount 0 candidate
        result' =
            shiftCanonicalTerm binderCount 0 result
    conditions <-
        traverse
            (conditionTerm
                resolveGlobal
                clauseEnvironment
                candidate')
            (preparedClauseConditions
                clause)
    clauseResult <-
        lowerTerm
            resolveGlobal
            clauseEnvironment
            (preparedClauseResult clause)
    pure
        (closeExistentials
            (length
                (preparedClauseVariables
                    clause))
            (fromMaybe
                (CEq TySet result' clauseResult)
                (conjunctionList
                    (conditions
                        <> [CEq
                            TySet
                            result'
                            clauseResult]))))

extendVariables
    :: InductiveEnvironment
    -> [VarSymbol]
    -> Either
        TypedInductiveError
        InductiveEnvironment
extendVariables =
    go []
  where
    go _seen environment [] =
        Right environment
    go seen environment (variable : remaining)
        | variable `elem` seen =
            Left
                (TypedInductiveDuplicateBinder
                    variable)
        | otherwise = do
            extended <-
                rebindEnvironment
                    variable
                    =<< shiftEnvironment
                        environment
            go
                (variable : seen)
                extended
                remaining

membershipPredicate
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (ScopedCheckedCore (InductiveGlobal global))
membershipPredicate context set = do
    weakenedSet <-
        first TypedInductiveCoreError
            (weakenScopedCore
                (Just . inductiveGlobalType)
                TySet
                set)
    checkedTerm context
        (CLam TySet
            (memberTerm
                (CBound 0)
                (scopedCoreTerm
                    weakenedSet)))

operatorPredicateAt
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
operatorPredicateAt
        resolveGlobal
        inductive
        environment
        candidate = do
    extended <-
        shiftEnvironment environment
    body <-
        predicateAt
            resolveGlobal
            inductive
            extended
            (shiftCanonicalTerm
                1
                0
                candidate)
            (CBound 0)
    pure (CLam TySet body)

separationSetAt
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
separationSetAt
        resolveGlobal
        inductive
        environment
        candidate = do
    domain <-
        lowerTerm
            resolveGlobal
            environment
            (preparedInductiveDomain
                inductive)
    predicate <-
        operatorPredicateAt
            resolveGlobal
            inductive
            environment
            candidate
    pure
        (apply2
            (CIntrinsic Sep)
            domain
            predicate)

foundationInstance
    :: ProofContext (InductiveGlobal global)
    -> FoundationAxiomTag
    -> [ScopedCheckedCore (InductiveGlobal global)]
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
foundationInstance context tag arguments = do
    initial <-
        first TypedInductiveProofError
            (foundationProof context tag)
    foldM
        (\proof argument ->
            first TypedInductiveProofError
                (forallEliminationProof
                    context
                    proof
                    argument))
        initial
        arguments

separationForward
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
separationForward
        context
        domain
        predicate
        element
        membership = do
    characteristic <-
        foundationInstance
            context
            SeparationCharacteristic
            [domain, predicate, element]
    first TypedInductiveProofError
        (equalityModusPonensProof
            context
            characteristic
            membership)

separationBackward
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
separationBackward
        context
        domain
        predicate
        element
        inDomain
        satisfies = do
    characteristic <-
        foundationInstance
            context
            SeparationCharacteristic
            [domain, predicate, element]
    reversed <-
        first TypedInductiveProofError
            (equalityReverseProof
                context
                characteristic)
    expectedSatisfies <-
        checkedTerm context
            (CApp
                (scopedCoreTerm predicate)
                (scopedCoreTerm element))
    satisfies' <-
        first TypedInductiveProofError
            (conversionProof
                context
                satisfies
                expectedSatisfies)
    conjunction <-
        first TypedInductiveProofError
            (conjunctionIntroductionProof
                context
                inDomain
                satisfies')
    first TypedInductiveProofError
        (equalityModusPonensProof
            context
            reversed
            conjunction)

transportMembership
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> BuiltProof (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
transportMembership
        context
        element
        setEquality
        membership = do
    (sourceSet, targetSet) <-
        case scopedCoreTerm
                (builtProofStatement
                    setEquality) of
            CEq TySet source target ->
                Right (source, target)
            _ ->
                Left
                    (TypedInductiveUnsupportedExpression
                        "membership transport requires set equality")
    weakenedElement <-
        first TypedInductiveCoreError
            (weakenScopedCore
                (Just . inductiveGlobalType)
                TySet
                element)
    function <-
        checkedTerm context
            (CLam TySet
                (memberTerm
                    (scopedCoreTerm
                        weakenedElement)
                    (CBound 0)))
    functionReflexivity <-
        first TypedInductiveProofError
            (equalityReflexivityProof
                context
                function)
    propositionEquality <-
        first TypedInductiveProofError
            (equalityCongruenceApplicationProof
                context
                functionReflexivity
                setEquality)
    appliedSource <-
        checkedTerm context
            (CApp
                (scopedCoreTerm function)
                sourceSet)
    sourceMembership <-
        first TypedInductiveProofError
            (conversionProof
                context
                membership
                appliedSource)
    transported <-
        first TypedInductiveProofError
            (equalityModusPonensProof
                context
                propositionEquality
                sourceMembership)
    targetMembership <-
        checkedTerm context
            (memberTerm
                (scopedCoreTerm element)
                targetSet)
    first TypedInductiveProofError
        (conversionProof
            context
            transported
            targetMembership)

proveSubset
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ( ProofContext (InductiveGlobal global)
         -> ScopedCheckedCore (InductiveGlobal global)
         -> BuiltProof (InductiveGlobal global)
         -> Either
            TypedInductiveError
            (BuiltProof (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
proveSubset context left right proveElement =
    forallIntroductionTyped
        context
        TySet
        (\extended element -> do
                left' <-
                    first TypedInductiveCoreError
                        (weakenScopedCore
                            (Just . inductiveGlobalType)
                            TySet
                            left)
                right' <-
                    first TypedInductiveCoreError
                        (weakenScopedCore
                            (Just . inductiveGlobalType)
                            TySet
                            right)
                memberLeft <-
                    checkedTerm extended
                        (memberTerm
                            (scopedCoreTerm element)
                            (scopedCoreTerm left'))
                implicationIntroductionTyped
                    extended
                    memberLeft
                    (\withMember memberProof ->
                        proveElement
                            withMember
                            element
                            memberProof
                            >>= \result -> do
                                expected <-
                                    checkedTerm withMember
                                        (memberTerm
                                            (scopedCoreTerm
                                                element)
                                            (scopedCoreTerm
                                                right'))
                                if builtProofStatement result
                                    == expected
                                    then pure result
                                    else
                                        Left
                                            (TypedInductiveUnsupportedExpression
                                                "subset proof produced the wrong membership target")))

typedAsProofError
    :: TypedInductiveError
    -> KernelProofBuildError
typedAsProofError = \case
    TypedInductiveProofError err ->
        err
    err ->
        ProofSetLfpRuleFailed
            (Text.pack (show err))

implicationIntroductionTyped
    :: ProofContext (InductiveGlobal global)
    -> ScopedCheckedCore (InductiveGlobal global)
    -> ( ProofContext (InductiveGlobal global)
         -> BuiltProof (InductiveGlobal global)
         -> Either
            TypedInductiveError
            (BuiltProof (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
implicationIntroductionTyped context premise build =
    first TypedInductiveProofError
        (implicationIntroductionProof
            context
            premise
            (\extended proof ->
                first typedAsProofError
                    (build extended proof)))

forallIntroductionTyped
    :: ProofContext (InductiveGlobal global)
    -> CoreType
    -> ( ProofContext (InductiveGlobal global)
         -> ScopedCheckedCore (InductiveGlobal global)
         -> Either
            TypedInductiveError
            (BuiltProof (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (BuiltProof (InductiveGlobal global))
forallIntroductionTyped context binderType build =
    first TypedInductiveProofError
        (forallIntroductionProof
            context
            binderType
            (\extended variable ->
                first typedAsProofError
                    (build extended variable)))

buildUnderVariables
    :: InductiveEnvironment
    -> [VarSymbol]
    -> ( InductiveEnvironment
         -> Either
            TypedInductiveError
            (CanonicalTerm (InductiveGlobal global))
       )
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
buildUnderVariables
        environment
        []
        build =
    build environment
buildUnderVariables
        environment
        (variable : remaining)
        build = do
    extended <-
        extendEnvironment
            variable
            environment
    buildUnderVariables
        extended
        remaining
        build

fixedPointTerm
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> InductiveEnvironment
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
fixedPointTerm resolveGlobal inductive environment = do
    domain <-
        lowerTerm
            resolveGlobal
            environment
            (preparedInductiveDomain
                inductive)
    operator <-
        operatorTerm
            resolveGlobal
            inductive
            environment
    pure
        (CApp
            (CApp
                (CIntrinsic ISetLfp)
                domain)
            operator)

operatorTerm
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> PreparedInductiveSource (InductiveGlobal global)
    -> InductiveEnvironment
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
operatorTerm resolveGlobal inductive parameterEnvironment = do
    candidateEnvironment <-
        shiftEnvironment parameterEnvironment
    domain <-
        lowerTerm
            resolveGlobal
            candidateEnvironment
            (preparedInductiveDomain
                inductive)
    resultEnvironment <-
        shiftEnvironment candidateEnvironment
    clauses <-
        traverse
            (clausePredicateTerm
                resolveGlobal
                resultEnvironment)
            (preparedInductiveClauses
                inductive)
    pure
        (CLam TySet
            (CApp
                (CApp
                    (CIntrinsic Sep)
                    domain)
                (CLam TySet
                    (disjunctionList
                        (NonEmpty.toList
                            clauses)))))

clausePredicateTerm
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> PreparedInductiveClause (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
clausePredicateTerm
        resolveGlobal
        resultEnvironment
        clause = do
    clauseEnvironment <-
        extendVariables
            resultEnvironment
            (preparedClauseVariables clause)
    let variableCount =
            fromIntegral
                (length
                    (preparedClauseVariables
                        clause))
        resultVariable =
            CBound variableCount
        candidate =
            CBound (variableCount + 1)
    conditions <-
        traverse
            (conditionTerm
                resolveGlobal
                clauseEnvironment
                candidate)
            (preparedClauseConditions
                clause)
    result <-
        lowerTerm
            resolveGlobal
            clauseEnvironment
            (preparedClauseResult
                clause)
    pure
        (closeExistentials
            (length
                (preparedClauseVariables clause))
            (fromMaybe
                (CEq
                    TySet
                    resultVariable
                    result)
                (conjunctionList
                    (conditions
                        <> [CEq
                            TySet
                            resultVariable
                            result]))))

directConditionTerm
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> DirectInductiveCondition
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
directConditionTerm resolveGlobal environment candidate = \case
    DirectSideCondition formula ->
        lowerFormula resolveGlobal environment formula
    DirectRecursiveCondition term context -> do
        carrier <-
            betaNormalizeCanonical
                <$> lowerRecursiveCarrierContext
                    resolveGlobal environment candidate context
        memberTerm
            <$> lowerTerm resolveGlobal environment term
            <*> pure carrier

conditionTerm
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> CanonicalTerm (InductiveGlobal global)
    -> PreparedInductiveCondition (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
conditionTerm resolveGlobal environment candidate = \case
    PreparedSideCondition formula ->
        lowerFormula
            resolveGlobal
            environment
            formula
    PreparedDirectRecursiveCondition term context -> do
        carrier <-
            instantiateRecursiveCarrier environment candidate context
        memberTerm
            <$> lowerTerm
                resolveGlobal
                environment
                term
            <*> pure carrier
    PreparedNestedRecursiveCondition term context _index _target -> do
        carrier <-
            instantiateRecursiveCarrier environment candidate context
        memberTerm
            <$> lowerTerm resolveGlobal environment term
            <*> pure carrier

shiftEnvironment
    :: InductiveEnvironment
    -> Either
        TypedInductiveError
        InductiveEnvironment
shiftEnvironment
        (InductiveEnvironment variables) =
    pure
        (InductiveEnvironment
            (succ <$> variables))

lowerFormula
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> Formula
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lowerFormula =
    lowerFormulaWith False

lowerFormulaWith
    :: Bool
    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> Formula
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lowerFormulaWith allowQuantified resolveGlobal environment = \case
    IsElementOf _location element set ->
        memberTerm
            <$> lowerTerm
                resolveGlobal
                environment
                element
            <*> lowerTerm
                resolveGlobal
                environment
                set
    Equals _location left right ->
        CEq TySet
            <$> lowerTerm resolveGlobal environment left
            <*> lowerTerm resolveGlobal environment right
    NotEquals _location left right ->
        notTerm
            <$> (CEq TySet
                <$> lowerTerm resolveGlobal environment left
                <*> lowerTerm resolveGlobal environment right)
    IsSubsetOf _location left right -> do
        extended <-
            shiftEnvironment environment
        left' <-
            lowerTerm resolveGlobal extended left
        right' <-
            lowerTerm resolveGlobal extended right
        pure
            (CForall TySet
                (CImp
                    (memberTerm
                        (CBound 0)
                        left')
                    (memberTerm
                        (CBound 0)
                        right')))
    Bottom ->
        pure CFalsum
    Top ->
        pure (CImp CFalsum CFalsum)
    Not _location proposition ->
        notTerm
            <$> lowerFormulaWith allowQuantified
                resolveGlobal
                environment
                proposition
    left `Implies` right ->
        CImp
            <$> lowerFormulaWith allowQuantified
                resolveGlobal environment left
            <*> lowerFormulaWith allowQuantified
                resolveGlobal environment right
    left `And` right ->
        conjunctionTerm
            <$> lowerFormulaWith allowQuantified
                resolveGlobal environment left
            <*> lowerFormulaWith allowQuantified
                resolveGlobal environment right
    left `Or` right ->
        disjunctionTerm
            <$> lowerFormulaWith allowQuantified
                resolveGlobal environment left
            <*> lowerFormulaWith allowQuantified
                resolveGlobal environment right
    left `Iff` right ->
        CEq TyProp
            <$> lowerFormulaWith allowQuantified
                resolveGlobal environment left
            <*> lowerFormulaWith allowQuantified
                resolveGlobal environment right
    Atomic _location predicate arguments ->
        lowerPredicateApplication
            resolveGlobal
            environment
            (SymbolPredicate predicate)
            arguments
    Quantified quantifier scope
        | allowQuantified -> do
            let variables =
                    nubOrd
                        [ variable
                        | B variable <- toList (fromScope scope)
                        ]
                body = instantiate TermVar scope
            extended <- extendVariables environment variables
            lowered <-
                lowerFormulaWith
                    allowQuantified
                    resolveGlobal
                    extended
                    body
            pure
                (case quantifier of
                    Universally ->
                        closeForalls (length variables) lowered
                    Existentially ->
                        closeExistentials (length variables) lowered)
    _ ->
        Left
            (TypedInductiveUnsupportedExpression
                "quantified and higher-order side conditions are not supported by the typed inductive slice")

lowerTerm
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> Term
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lowerTerm resolveGlobal environment = \case
    TermVar variable ->
        lookupEnvironment
            variable
            environment
    EmptySet _location ->
        pure (CIntrinsic Empty)
    TermSymbol _location (SymbolInteger integer) [] ->
        pure
            (COpaqueInteger
                (toInteger integer))
    TermSymbol _location symbol arguments ->
        lowerApplication
            resolveGlobal
            environment
            symbol
            arguments
    _ ->
        Left
            (TypedInductiveUnsupportedExpression
                "higher-order source terms are not supported by the typed inductive slice")

lowerApplication
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> Symbol
    -> [Expr]
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lowerApplication resolveGlobal environment symbol arguments = do
    arguments' <-
        traverse
            (lowerTerm
                resolveGlobal
                environment)
            arguments
    lowerApplicationTerms resolveGlobal symbol arguments'

lowerPredicateApplication
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> InductiveEnvironment
    -> Symbol
    -> [Expr]
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lowerPredicateApplication resolveGlobal environment symbol arguments = do
    arguments' <-
        traverse
            (lowerTerm
                resolveGlobal
                environment)
            arguments
    case classifyExactSymbol symbol of
        ExactFixedPrimitive meaning ->
            maybe
                (lowerApplicationTerms resolveGlobal symbol arguments')
                Right
                (lowerFixedEqualityPredicate meaning arguments')
        _ ->
            lowerApplicationTerms resolveGlobal symbol arguments'

lowerApplicationTerms
    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
    -> Symbol
    -> [CanonicalTerm (InductiveGlobal global)]
    -> Either
        TypedInductiveError
        (CanonicalTerm (InductiveGlobal global))
lowerApplicationTerms resolveGlobal symbol arguments' =
    case dispatchFixedSetTerm symbol arguments' of
        LoweredFixedSetTerm term ->
            pure term
        RejectedFixedSetTerm ->
            Left
                (TypedInductiveUnsupportedExpression
                    ("fixed source symbol is not a supported set term: "
                        <> symbolText symbol))
        NotFixedSetTerm -> do
            SourceGlobal reference body <-
                maybe
                    (Left
                        (TypedInductiveUnsupportedExpression
                            ("source symbol is not typed: "
                                <> symbolText symbol)))
                    Right
                    (resolveGlobal symbol)
            pure
                (foldl'
                    CApp
                    (maybe
                        (CGlobal reference)
                        frozenCoreTerm
                        body)
                    arguments')

memberTerm
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
memberTerm =
    apply2 (CIntrinsic Member)

subsetTerm
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
subsetTerm left right =
    CForall TySet
        (CImp
            (memberTerm
                (CBound 0)
                (shiftCanonicalTerm
                    1
                    0
                    left))
            (memberTerm
                (CBound 0)
                (shiftCanonicalTerm
                    1
                    0
                    right)))

apply2
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
apply2 function firstArgument secondArgument =
    CApp
        (CApp function firstArgument)
        secondArgument

notTerm
    :: CanonicalTerm global
    -> CanonicalTerm global
notTerm proposition =
    CImp proposition CFalsum

conjunctionList
    :: [CanonicalTerm global]
    -> Maybe (CanonicalTerm global)
conjunctionList = \case
    [] ->
        Nothing
    firstTerm : remaining ->
        Just
            (foldl'
                conjunctionTerm
                firstTerm
                remaining)

disjunctionList
    :: [CanonicalTerm global]
    -> CanonicalTerm global
disjunctionList = \case
    [] ->
        CFalsum
    firstTerm : remaining ->
        foldl'
            disjunctionTerm
            firstTerm
            remaining

impliesIfNeeded
    :: Maybe (CanonicalTerm global)
    -> CanonicalTerm global
    -> CanonicalTerm global
impliesIfNeeded = \case
    Nothing ->
        id
    Just premise ->
        CImp premise

closeLambdas
    :: Int
    -> CanonicalTerm global
    -> CanonicalTerm global
closeLambdas binderCount body =
    foldl'
        (\current _ ->
            CLam TySet current)
        body
        [1 .. binderCount]

closeForalls
    :: Int
    -> CanonicalTerm global
    -> CanonicalTerm global
closeForalls binderCount body =
    foldl'
        (\current _ ->
            CForall TySet current)
        body
        [1 .. binderCount]

closeExistentials
    :: Int
    -> CanonicalTerm global
    -> CanonicalTerm global
closeExistentials binderCount body =
    foldl'
        (\current _ ->
            existentialTerm TySet current)
        body
        [1 .. binderCount]

shiftCanonicalTerm
    :: Natural
    -> Natural
    -> CanonicalTerm global
    -> CanonicalTerm global
shiftCanonicalTerm amount cutoff = \case
    CBound index
        | index >= cutoff ->
            CBound (index + amount)
        | otherwise ->
            CBound index
    CGlobal global ->
        CGlobal global
    CIntrinsic intrinsic ->
        CIntrinsic intrinsic
    COpaqueInteger integer ->
        COpaqueInteger integer
    CApp function argument ->
        CApp
            (shiftCanonicalTerm
                amount
                cutoff
                function)
            (shiftCanonicalTerm
                amount
                cutoff
                argument)
    CLam binderType body ->
        CLam binderType
            (shiftCanonicalTerm
                amount
                (cutoff + 1)
                body)
    CFalsum ->
        CFalsum
    CImp premise conclusion ->
        CImp
            (shiftCanonicalTerm
                amount
                cutoff
                premise)
            (shiftCanonicalTerm
                amount
                cutoff
                conclusion)
    CEq operandType left right ->
        CEq operandType
            (shiftCanonicalTerm
                amount
                cutoff
                left)
            (shiftCanonicalTerm
                amount
                cutoff
                right)
    CForall binderType body ->
        CForall binderType
            (shiftCanonicalTerm
                amount
                (cutoff + 1)
                body)

atNatural :: Natural -> [a] -> Maybe a
atNatural _index [] =
    Nothing
atNatural 0 (value : _rest) =
    Just value
atNatural index (_value : rest) =
    atNatural (index - 1) rest

freezeClosedTarget
    :: CanonicalTerm (InductiveGlobal global)
    -> Either
        TypedInductiveError
        (FrozenCheckedCore (InductiveGlobal global))
freezeClosedTarget =
    first TypedInductiveCoreError
        . checkCanonicalCore
            (Just . inductiveGlobalType)

symbolText :: Symbol -> Text
symbolText = \case
    SymbolMixfix symbol ->
        case mixfixMarker symbol of
            Marker text ->
                text
    SymbolFun symbol ->
        case lexicalItemSgPlMarker symbol of
            Marker text ->
                text
    SymbolInteger integer ->
        Text.pack (show integer)
    SymbolPredicate predicate ->
        case predicateObjectMarker predicate of
            Marker text ->
                text