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