{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -- | Exact lowering for the first ordinary theorem/proof fragment. -- -- This module is the trusted owner of structural local-proof composition. Its -- private prepared tree controls when assumptions and proved local claims -- become available and executes discharges depth-first. The declaration -- boundary validates typed tasks and authority; it does not reconstruct this -- derivation. module Felix.Checking.Exact.Proof ( PreparedExactProof , preparedExactProofSyntaxId , preparedExactProofFirstOmission , prepareExactProof , CheckedExactProofAuthorization , lowerPreparedExactProof , authorizeCheckedExactProof , PreparedFinalPreludeFoundationClaim , prepareFinalPreludeFoundationClaim , CheckedFinalPreludeFoundationAuthorization , lowerPreparedFinalPreludeFoundationClaim , authorizeCheckedFinalPreludeFoundationClaim , ExactProofError(..) , exactProofErrorLocation , renderExactProofError ) where import Base import Felix.Checking.Authority qualified as Authority import Felix.Checking.Backend.Problem qualified as Backend import Felix.Checking.Core import Felix.Checking.Declaration qualified as Declaration import Felix.Checking.Exact qualified as Exact import Felix.Checking.Foundation import Felix.Checking.Identity import Felix.Checking.Kernel.Derivation (foundationFactDerivation) import Felix.Checking.Kernel.Proof qualified as KernelProof import Felix.Checking.SetConstruction import Felix.Checking.Semantic import Felix.Cache.Codec import Felix.Report.Location import Felix.Syntax.Abstract qualified as Raw import Control.Monad.Except (ExceptT) import Control.Monad.Except qualified as Except import Control.Monad (foldM, unless, when) import Control.Monad.State.Strict (StateT) import Control.Monad.State.Strict qualified as State import Data.ByteString (ByteString) 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) data ExactProofError = ExactProofUnsupportedClaim !Location | ExactProofUnsupportedStep !Location | ExactProofSetInductionVariableRequired !Location | ExactProofSetInductionVariableNotActive !Location !Raw.VarSymbol | ExactProofSetInductionFocusAmbiguous !Location | ExactProofSetInductionActiveBinderIneligible !Location !Raw.VarSymbol | ExactProofSetInductionBinderConflict !Location !Raw.VarSymbol | ExactProofSetInductionGoalMismatch !Location | ExactProofSetExtensionalityGoalMismatch !Location | ExactProofSetExtensionalityDirectionsUnavailable !Location | ExactProofExpectedUniversalGoal !Location | ExactProofExpectedImplicationGoal !Location | ExactProofGoalStatementMismatch !Location | ExactProofEmptyCaseSplit !Location | ExactProofStructuralCompositionFailed !Location !KernelProof.KernelProofBuildError | ExactProofLocalFunctionBinderMismatch !Location | ExactProofLocalFunctionNameConflict !Location | ExactProofUnknownReference !Location !Raw.Marker | ExactProofElaborationFailed !Exact.ExactCompileError | ExactProofObligationPreparationFailed !Location !(Declaration.VampireObligationPreparationError Exact.ExactLocalId) | ExactProofFoundationLeafRequiresImplicitAuto !Location | ExactProofFoundationLeafTargetMismatch !Location | ExactProofFoundationLeafTargetAmbiguous !Location deriving stock (Show, Eq) exactProofErrorLocation :: ExactProofError -> Location exactProofErrorLocation = \case ExactProofUnsupportedClaim location -> location ExactProofUnsupportedStep location -> location ExactProofSetInductionVariableRequired location -> location ExactProofSetInductionVariableNotActive location _variable -> location ExactProofSetInductionFocusAmbiguous location -> location ExactProofSetInductionActiveBinderIneligible location _variable -> location ExactProofSetInductionBinderConflict location _variable -> location ExactProofSetInductionGoalMismatch location -> location ExactProofSetExtensionalityGoalMismatch location -> location ExactProofSetExtensionalityDirectionsUnavailable location -> location ExactProofExpectedUniversalGoal location -> location ExactProofExpectedImplicationGoal location -> location ExactProofGoalStatementMismatch location -> location ExactProofEmptyCaseSplit location -> location ExactProofStructuralCompositionFailed location _failure -> location ExactProofLocalFunctionBinderMismatch location -> location ExactProofLocalFunctionNameConflict location -> location ExactProofUnknownReference location _marker -> location ExactProofElaborationFailed failure -> Exact.exactCompileErrorLocation failure ExactProofObligationPreparationFailed location _failure -> location ExactProofFoundationLeafRequiresImplicitAuto location -> location ExactProofFoundationLeafTargetMismatch location -> location ExactProofFoundationLeafTargetAmbiguous location -> location renderExactProofError :: ExactProofError -> Text renderExactProofError = \case ExactProofUnsupportedClaim location -> at location <> "this claim is not yet supported by the typed checker" ExactProofUnsupportedStep location -> at location <> "this proof step is not yet supported by the typed checker" ExactProofSetInductionVariableRequired location -> at location <> "exact set induction requires a named set variable" ExactProofSetInductionVariableNotActive location variable -> at location <> "the set-induction variable " <> shown variable <> " is not an eligible exact focus" ExactProofSetInductionFocusAmbiguous location -> at location <> "set induction without an explicit variable has no unique focus" ExactProofSetInductionActiveBinderIneligible location variable -> at location <> "the active binder " <> shown variable <> " is not an eligible set-induction focus" ExactProofSetInductionBinderConflict location variable -> at location <> "the leading set-induction binder " <> shown variable <> " conflicts with an active exact binder" ExactProofSetInductionGoalMismatch location -> at location <> "the set-induction variable does not belong to this goal" ExactProofSetExtensionalityGoalMismatch location -> at location <> "set extensionality requires a set-equality goal" ExactProofSetExtensionalityDirectionsUnavailable location -> at location <> "set extensionality requires both directions as proved local claims" ExactProofExpectedUniversalGoal location -> at location <> "this fix step requires a universal goal" ExactProofExpectedImplicationGoal location -> at location <> "this assume step requires an implication goal" ExactProofGoalStatementMismatch location -> at location <> "the proof step does not match the current goal" ExactProofEmptyCaseSplit location -> at location <> "case analysis requires at least one case" ExactProofStructuralCompositionFailed location failure -> at location <> "invalid structural proof composition: " <> shown failure ExactProofLocalFunctionBinderMismatch location -> at location <> "the function argument must match its domain binder" ExactProofLocalFunctionNameConflict location -> at location <> "the function and argument names must be distinct" ExactProofUnknownReference location marker -> at location <> "the cited fact " <> shown marker <> " is not visible" ExactProofElaborationFailed failure -> Exact.renderExactCompileError failure ExactProofObligationPreparationFailed location failure -> at location <> "the exact proof obligation is invalid: " <> shown failure ExactProofFoundationLeafRequiresImplicitAuto location -> at location <> "a confined foundation claim requires an implicit Auto proof" ExactProofFoundationLeafTargetMismatch location -> at location <> "the claim does not exactly match a foundation axiom" ExactProofFoundationLeafTargetAmbiguous location -> at location <> "the claim matches more than one foundation axiom" where at location = locationToText location <> ": " shown :: Show value => value -> Text shown = Text.pack . show data ExactLocalOrigin = ExactAssumption | ExactDerivedClaim | ExactLocalDefinition | ExactLocalConstructionExtensional | ExactLocalConstructionEquation deriving stock (Show, Eq, Ord) data PreparedLocal = PreparedLocal !Backend.LocalPremiseOrdinal !ExactLocalOrigin !(Vector (Exact.ExactLocalId, CoreType)) !(ScopedCheckedCore ObjectId) data PreparedJustification = PreparedAuto | PreparedReferences !(NonEmpty SemanticFactOccurrenceFingerprint) | PreparedLocalOnly data PreparedDischarge = PreparedVampireDischarge !Location !PreparedJustification !(ScopedCheckedCore ObjectId) !(Declaration.PreparedVampireObligation Exact.ExactLocalId ExactLocalOrigin) | PreparedSetExtensionality !Location !(ScopedCheckedCore ObjectId) data PreparedCalculationLink = PreparedCalculationLink !(ScopedCheckedCore ObjectId) !PreparedDischarge -- The private constructor stores every destination with the discharge derived -- from its immediately preceding endpoint. Planning and admission can -- therefore traverse one immutable sequence without re-associating shapes. data PreparedCalculation = PreparedCheckedCalculation !CoreType ![Exact.ExactLocalId] !(Maybe (ScopedCheckedCore ObjectId)) !(ScopedCheckedCore ObjectId) !(NonEmpty PreparedCalculationLink) !(ScopedCheckedCore ObjectId) data PreparedSinceEvidence = PreparedSinceExisting !PreparedLocal | PreparedSinceDischarged !PreparedDischarge !PreparedLocal data PreparedCase = PreparedCase !(ScopedCheckedCore ObjectId) !PreparedProof data PreparedCaseAnalysis = PreparedCaseAnalysis !(ScopedCheckedCore ObjectId) !(NonEmpty PreparedCase) !(ScopedCheckedCore ObjectId) !PreparedDischarge data InitialSetInductionFocus = InitialSetInductionFocus !Raw.VarSymbol !Exact.ExactLocalId !Natural data InitialSetInductionView = InitialSetInductionView ![InitialSetInductionFocus] !(Vector (Exact.ExactLocalId, CoreType)) !(ScopedCheckedCore ObjectId) ![ScopedCheckedCore ObjectId] !(ScopedCheckedCore ObjectId) !(Maybe Raw.VarSymbol) data SetInductionBoundary = InitialClaimInduction !InitialSetInductionView -- A direct source-statement goal may retain only its leading binder name. -- Recursive proof transformations deliberately discard this hint. | SourceStatementInduction !(Maybe Raw.VarSymbol) | RecursiveProofInduction data SelectedSetInductionFocus = SelectedInitialSetInduction !InitialSetInductionFocus | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol) data PreparedSetInductionFocus = PreparedInitialSetInductionFocus !Exact.ExactLocalId !Natural | PreparedLeadingSetInductionFocus !Exact.ExactLocalId data PreparedSetInduction = PreparedCheckedSetInduction !PreparedSetInductionFocus !(ScopedCheckedCore ObjectId) ![ScopedCheckedCore ObjectId] !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedProof data PreparedProof = PreparedImplicitAuto !PreparedDischarge | PreparedQed !PreparedDischarge | PreparedOmitted !Location !(ScopedCheckedCore ObjectId) | PreparedFix ![Exact.ExactLocalId] !PreparedProof | PreparedAssume !(ScopedCheckedCore ObjectId) !PreparedProof | PreparedTake ![Exact.ExactLocalId] !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof | PreparedSetInduction !PreparedSetInduction | PreparedHave !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof | PreparedSuffices !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof | PreparedCalculate !PreparedCalculation !PreparedProof | PreparedSince !(ScopedCheckedCore ObjectId) !PreparedSinceEvidence !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof | PreparedSubclaim !(ScopedCheckedCore ObjectId) !PreparedProof !PreparedProof | PreparedDefine !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) !(NonEmpty (ScopedCheckedCore ObjectId)) !PreparedProof | PreparedDefineRelational !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) !PreparedDischarge !(NonEmpty (ScopedCheckedCore ObjectId)) !PreparedProof | PreparedDefineFunction !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedProof | PreparedByCase !PreparedCaseAnalysis | PreparedByContradiction !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedProof | PreparedContradiction !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedDischarge data PreparedExactProof = PreparedExactProof !Location !SemanticName !(ScopedCheckedCore ObjectId) !PreparedProof !ProofSyntaxId data PreparedFinalPreludeFoundationClaim = PreparedFinalPreludeFoundationClaim !Location !SemanticName !(ScopedCheckedCore ObjectId) !FoundationAxiomTag !ProofSyntaxId preparedExactProofSyntaxId :: PreparedExactProof -> ProofSyntaxId preparedExactProofSyntaxId (PreparedExactProof _location _alias _target _proof syntax) = syntax preparedExactProofFirstOmission :: PreparedExactProof -> Maybe Location preparedExactProofFirstOmission (PreparedExactProof _location _alias _target proof _syntax) = preparedProofFirstOmission proof data PrepareState = PrepareState { prepareNextLocal :: !Natural , prepareNextPremise :: !Natural } type Prepare = StateT PrepareState (ExceptT ExactProofError (Declaration.LoweringDriver)) prepareExactProof :: Raw.Block -> Maybe Raw.Proof -> Declaration.LoweringDriver (Either ExactProofError PreparedExactProof) prepareExactProof block explicitProof = Except.runExceptT (State.evalStateT prepare initialState) where initialState = PrepareState 0 0 prepare = case block of Raw.BlockClaim _kind location _title (Raw.Marker marker) (Raw.Claim assumptions statement) -> do envelope <- liftDriver (Exact.prepareExactClaimEnvelope assumptions statement) >>= either (throwProof . ExactProofElaborationFailed) pure let targetCore = Exact.preparedExactClaimTarget envelope unless (null (scopedCoreContext targetCore)) (throwProof (ExactProofUnsupportedClaim location)) (context, openedGoal, identities) <- openEnvelopeVariables targetCore (Exact.preparedExactClaimVariables envelope) (Exact.preparedExactClaimContext envelope) (locals, bodyGoal, antecedents) <- openEnvelopeAntecedents context openedGoal (Exact.preparedExactClaimAntecedentCount envelope) initialInduction <- prepareInitialSetInductionView statement context (Exact.preparedExactClaimVariables envelope) identities antecedents bodyGoal bodyProof <- case explicitProof of Nothing -> PreparedImplicitAuto <$> prepareDischarge location context locals bodyGoal Raw.JustificationEmpty Just sourceProof -> prepareProof location context locals (InitialClaimInduction initialInduction) bodyGoal sourceProof let withAssumptions = foldr PreparedAssume bodyProof antecedents proof = case identities of [] -> withAssumptions _ -> PreparedFix identities withAssumptions pure (PreparedExactProof location (semanticName marker) targetCore proof (proofSyntaxId (encodePreparedProof proof))) _ -> throwProof (ExactProofUnsupportedClaim (locate block)) prepareFinalPreludeFoundationClaim :: CheckedFoundation -> Raw.Block -> Maybe Raw.Proof -> Declaration.LoweringDriver (Either ExactProofError PreparedFinalPreludeFoundationClaim) prepareFinalPreludeFoundationClaim foundation block explicitProof = Except.runExceptT do case (block, explicitProof) of ( Raw.BlockClaim _kind location _title (Raw.Marker marker) (Raw.Claim assumptions statement) , Nothing ) -> do envelope <- Except.lift (Exact.prepareExactClaimEnvelope assumptions statement) >>= either (Except.throwError . ExactProofElaborationFailed) pure unless ( null (Exact.preparedExactClaimVariables envelope) && Exact.preparedExactClaimAntecedentCount envelope == 0 ) (Except.throwError (ExactProofFoundationLeafRequiresImplicitAuto location)) let target = Exact.preparedExactClaimTarget envelope matches = [ tag | tag <- [minBound .. maxBound] , target == foundationTarget tag ] tag <- case matches of [] -> Except.throwError (ExactProofFoundationLeafTargetMismatch location) [only] -> pure only _ -> Except.throwError (ExactProofFoundationLeafTargetAmbiguous location) pure (PreparedFinalPreludeFoundationClaim location (semanticName marker) target tag (implicitAutoProofSyntaxId target)) (Raw.BlockClaim _kind location _title _marker _claim, Just{}) -> Except.throwError (ExactProofFoundationLeafRequiresImplicitAuto location) _ -> Except.throwError (ExactProofUnsupportedClaim (locate block)) where foundationTarget tag = embedClosedCore [] (mapFrozenGlobals absurd (foundationAxiomFrozen foundation tag)) openEnvelopeVariables :: ScopedCheckedCore ObjectId -> [Raw.VarSymbol] -> Exact.ExactBinderContext -> Prepare ( Exact.ExactBinderContext , ScopedCheckedCore ObjectId , [Exact.ExactLocalId] ) openEnvelopeVariables target variables preparedContext = case NonEmpty.nonEmpty variables of Nothing -> pure (preparedContext, target, []) Just nonempty -> do (_unannotated, opened, identities) <- openFixedVariables Exact.emptyExactBinderContext target nonempty let expected = reverse (fst <$> toList (Exact.exactBinderContextSupport preparedContext)) unless (identities == expected) (impossible "prepared claim annotations do not match opened binders") pure (preparedContext, opened, identities) openEnvelopeAntecedents :: Exact.ExactBinderContext -> ScopedCheckedCore ObjectId -> Natural -> Prepare ( [PreparedLocal] , ScopedCheckedCore ObjectId , [ScopedCheckedCore ObjectId] ) openEnvelopeAntecedents context initialGoal initialCount = go [] [] initialGoal initialCount where go locals antecedents goal 0 = pure (locals, goal, antecedents) go locals antecedents goal remaining = do (antecedent, conclusion) <- maybe (impossible "a prepared claim envelope has too few implications") pure (openScopedImplication goal) local <- allocateLocal ExactAssumption context antecedent go (locals <> [local]) (antecedents <> [antecedent]) conclusion (remaining - 1) prepareInitialSetInductionView :: Raw.Stmt -> Exact.ExactBinderContext -> [Raw.VarSymbol] -> [Exact.ExactLocalId] -> [ScopedCheckedCore ObjectId] -> ScopedCheckedCore ObjectId -> Prepare InitialSetInductionView prepareInitialSetInductionView statement context variables identities antecedents bodyGoal = do unless (length variables == length identities) (impossible "opened claim binders lost their source identity association") foci <- traverse checkedFocus (zip variables identities) let property = foldr implyChecked bodyGoal antecedents support = Exact.exactBinderContextSupport context unless ( scopedCoreContext property == (snd <$> Vector.toList support) ) (impossible "initial set-induction property changed its checked context") pure (InitialSetInductionView foci support property antecedents bodyGoal (claimLeadingUniversalName statement)) where checkedFocus (variable, identity) = do index <- maybe (impossible "an opened claim binder is absent from its exact context") pure (Exact.exactBinderContextIndex variable context) case Exact.exactBinderContextSupport context Vector.!? (fromIntegral index) of Just (actualIdentity, TySet) | actualIdentity == identity -> pure (InitialSetInductionFocus variable identity index) _ -> impossible "an initial set-induction focus changed identity or type" implyChecked antecedent conclusion = fromMaybe (impossible "an exact claim antecedent changed context") (implyScopedCore antecedent conclusion) claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol claimLeadingUniversalName = \case Raw.StmtFormula (Raw.FormulaQuantified _location Raw.Universally (variable :| _rest) _bound _formula) -> Just variable Raw.SymbolicForall _location (variable :| _rest) _bound _suchThat _statement -> Just variable Raw.StmtQuantPhrase _location (Raw.QuantPhrase Raw.Universally (Raw.NounPhrase _left _noun variables _right _suchThat)) _statement -> listToMaybe variables Raw.StmtVerbPhrase (Raw.TermQuantified Raw.Universally _location (Raw.NounPhrase _left _noun variable _right _suchThat) :| []) _verb -> variable Raw.StmtNoun (Raw.TermQuantified Raw.Universally _location (Raw.NounPhrase _left _noun variable _right _suchThat) :| []) _nounPhrase -> variable _statement -> Nothing prepareProof :: Location -> Exact.ExactBinderContext -> [PreparedLocal] -> SetInductionBoundary -> ScopedCheckedCore ObjectId -> Raw.Proof -> Prepare PreparedProof prepareProof fallback context locals inductionBoundary goal = \case Raw.Omitted location -> pure (PreparedOmitted location goal) Raw.Qed maybeLocation justification -> PreparedQed <$> prepareDischarge (fromMaybe fallback maybeLocation) context locals goal justification Raw.FixSymbolic location variables bound continuation -> do (context', goal', identities) <- openFixedVariables context goal variables case bound of Raw.Unbounded -> PreparedFix identities <$> prepareProof fallback context' locals RecursiveProofInduction goal' continuation _ -> do constraint <- prepareSymbolicBoundConstraints context' variables bound prepareGuardedFix fallback location context' locals goal' identities constraint continuation Raw.FixSuchThat location variables statement continuation -> do (context', goal', identities) <- openFixedVariables context goal variables constraint <- Exact.preparedExactPropositionCore <$> prepareStatement context' statement prepareGuardedFix fallback location context' locals goal' identities constraint continuation Raw.Assume location statement continuation -> do supplied <- prepareStatement context statement when (isNothing (openScopedImplication goal)) (throwProof (ExactProofExpectedImplicationGoal location)) (assumption, conclusion) <- maybe (throwProof (ExactProofGoalStatementMismatch location)) pure (openScopedAssumption (Exact.preparedExactPropositionCore supplied) goal) local <- allocateLocal ExactAssumption context assumption PreparedAssume assumption <$> prepareProof fallback context (locals <> [local]) RecursiveProofInduction conclusion continuation Raw.TakeVar location variables bound statement justification continuation -> do prepareSymbolicTake fallback location context locals goal variables bound statement justification continuation Raw.TakeNoun location nounPhrase justification continuation -> prepareNounTake fallback location context locals goal nounPhrase justification continuation Raw.BySetInduction location variable continuation -> prepareSetInduction fallback location context locals inductionBoundary goal variable continuation Raw.Have location Nothing (Raw.SymbolicExists _existential variables bound statement) justification continuation -> prepareSymbolicTake fallback location context locals goal variables bound statement justification continuation Raw.Have location Nothing statement justification continuation -> do claim <- Exact.preparedExactPropositionCore <$> prepareStatement context statement discharge <- prepareDischarge location context locals claim justification local <- allocateLocal ExactDerivedClaim context claim PreparedHave claim discharge <$> prepareProof fallback context (locals <> [local]) RecursiveProofInduction goal continuation Raw.Have location (Just sinceStatement) statement justification continuation -> do sinceProposition <- Exact.preparedExactPropositionCore <$> prepareStatement context sinceStatement claim <- Exact.preparedExactPropositionCore <$> prepareStatement context statement (evidence, sinceLocals) <- case find (localMatches sinceProposition) locals of Just existing -> pure (PreparedSinceExisting existing, locals) Nothing -> do discharge <- prepareDischarge location context locals sinceProposition Raw.JustificationLocal local <- allocateLocal ExactDerivedClaim context sinceProposition pure ( PreparedSinceDischarged discharge local , locals <> [local] ) claimDischarge <- prepareDischarge location context sinceLocals claim justification claimLocal <- allocateLocal ExactDerivedClaim context claim PreparedSince sinceProposition evidence claim claimDischarge <$> prepareProof fallback context (sinceLocals <> [claimLocal]) RecursiveProofInduction goal continuation Raw.Suffices location statement justification continuation -> do reduction <- Exact.preparedExactPropositionCore <$> prepareStatement context statement implication <- maybe (impossible "a checked suffices reduction changed lexical context") pure (implyScopedCore reduction goal) discharge <- prepareDischarge location context locals implication justification PreparedSuffices goal reduction implication discharge <$> prepareProof fallback context locals (SourceStatementInduction (claimLeadingUniversalName statement)) reduction continuation Raw.Calc location quantifier calculation continuation -> do prepared <- prepareCalculation location context locals quantifier calculation local <- allocateLocal ExactDerivedClaim context (preparedCalculationResult prepared) PreparedCalculate prepared <$> prepareProof fallback context (locals <> [local]) RecursiveProofInduction goal continuation Raw.Subclaim location statement subproof continuation -> do claim <- Exact.preparedExactPropositionCore <$> prepareStatement context statement preparedSubproof <- prepareProof location context locals (SourceStatementInduction (claimLeadingUniversalName statement)) claim subproof local <- allocateLocal ExactDerivedClaim context claim PreparedSubclaim claim preparedSubproof <$> prepareProof fallback context (locals <> [local]) RecursiveProofInduction goal continuation Raw.Define location variable expression continuation -> do preparedBody <- liftDriver (Exact.prepareExactSetExpression context expression) >>= either (throwProof . ExactProofElaborationFailed) pure let body = Exact.preparedExactSetExpressionCore preparedBody identity <- allocateLocalIdentity context' <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactBinderContext ((identity, variable) :| []) context) case Exact.preparedExactSetExpressionConstruction preparedBody of Nothing -> do separationCharacteristic <- liftDriver (Declaration.currentFoundationAxiomLowering SeparationCharacteristic) definition <- maybe (impossible "an exact set expression did not form a local definition") pure (scopedSetDefinition separationCharacteristic body) local <- allocateLocal ExactLocalDefinition context' definition PreparedDefine identity body (definition :| []) <$> prepareProof fallback context' (locals <> [local]) RecursiveProofInduction (weakenCheckedScopedCore TySet goal) continuation Just (Exact.PreparedUnconditionalSetConstruction construction) -> do characteristics <- prepareConstructionFoundation (extensional, equation) <- maybe (impossible "a checked named construction has no definition views") pure (namedSetConstructionLocalViews characteristics construction) extensionalLocal <- allocateLocal ExactLocalConstructionExtensional context' extensional equationLocal <- allocateLocal ExactLocalConstructionEquation context' equation PreparedDefine identity body (extensional :| [equation]) <$> prepareProof fallback context' (locals <> [extensionalLocal, equationLocal]) RecursiveProofInduction (weakenCheckedScopedCore TySet goal) continuation Just (Exact.PreparedRelationalSetConstruction construction) -> do characteristics <- prepareConstructionFoundation let functionality = relationalSetConstructionFunctionality construction discharge <- prepareDischarge location context locals functionality Raw.JustificationEmpty (extensional, equation) <- maybe (impossible "a checked relational construction has no admitted definition views") pure (relationalSetConstructionLocalViews characteristics construction functionality) extensionalLocal <- allocateLocal ExactLocalConstructionExtensional context' extensional equationLocal <- allocateLocal ExactLocalConstructionEquation context' equation PreparedDefineRelational identity body discharge (extensional :| [equation]) <$> prepareProof fallback context' (locals <> [extensionalLocal, equationLocal]) RecursiveProofInduction (weakenCheckedScopedCore TySet goal) continuation Raw.DefineFunction location function argument value bound domain continuation -> do unless (argument == bound) (throwProof (ExactProofLocalFunctionBinderMismatch (locate bound))) when (function == argument) (throwProof (ExactProofLocalFunctionNameConflict (locate function))) argumentIdentity <- allocateLocalIdentity argumentContext <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactBinderContext ((argumentIdentity, argument) :| []) context) graph <- liftDriver (Exact.prepareExactLocalFunctionGraph location context argumentContext domain value) >>= either (throwProof . ExactProofElaborationFailed) pure functionIdentity <- allocateLocalIdentity functionContext <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactBinderContext ((functionIdentity, function) :| []) context) replacementCharacteristic <- liftDriver (Declaration.currentFoundationAxiomLowering ReplacementCharacteristic) definition <- maybe (impossible "a checked replacement graph did not form a local definition") pure (scopedCharacteristicDefinition replacementCharacteristic (Exact.preparedExactLocalFunctionGraphCore graph) ( Exact.preparedExactLocalFunctionGraphDomain graph :| [Exact.preparedExactLocalFunctionGraphMap graph] )) local <- allocateLocal ExactLocalDefinition functionContext definition PreparedDefineFunction functionIdentity (Exact.preparedExactLocalFunctionGraphCore graph) definition <$> prepareProof fallback functionContext (locals <> [local]) RecursiveProofInduction (weakenCheckedScopedCore TySet goal) continuation Raw.ByCase location sourceCases -> prepareByCase location context locals goal sourceCases Raw.ByContradiction location continuation -> do let falsum = falsumScopedCore (scopedCoreContext goal) negation <- maybe (structuralFailure location "proof by contradiction requires a proposition goal") pure (negateScopedCore goal) local <- allocateLocal ExactAssumption context negation prepared <- prepareProof location context (locals <> [local]) RecursiveProofInduction falsum continuation validateStructuralComposition location [goal, negation, falsum] (\foundation globalType -> KernelProof.validateDoubleNegationComposition foundation globalType goal negation falsum) pure (PreparedByContradiction goal negation falsum prepared) Raw.Contradiction location justification -> do let falsum = falsumScopedCore (scopedCoreContext goal) discharge <- prepareDischarge location context locals falsum justification validateStructuralComposition location [goal, falsum] (\foundation globalType -> KernelProof.validateFalsumEliminationComposition foundation globalType goal falsum) pure (PreparedContradiction goal falsum discharge) proof -> throwProof (ExactProofUnsupportedStep (proofLocation fallback proof)) where localMatches proposition (PreparedLocal _ordinal _origin _support local) = local == proposition prepareSetInduction :: Location -> Location -> Exact.ExactBinderContext -> [PreparedLocal] -> SetInductionBoundary -> ScopedCheckedCore ObjectId -> Maybe Raw.Term -> Raw.Proof -> Prepare PreparedProof prepareSetInduction fallback location context locals boundary goal sourceFocus continuation = do selected <- selectSetInductionFocus location context boundary goal sourceFocus case selected of SelectedInitialSetInduction (InitialSetInductionFocus _variable identity index) -> do (foci, expectedSupport, property, antecedents, childTarget) <- case boundary of InitialClaimInduction (InitialSetInductionView foundFoci support foundProperty foundAntecedents foundTarget _leadingName) -> pure ( foundFoci , support , foundProperty , foundAntecedents , foundTarget ) RecursiveProofInduction -> impossible "an initial induction focus escaped its claim boundary" SourceStatementInduction _leadingName -> impossible "an initial induction focus escaped its claim boundary" unless ( Exact.exactBinderContextSupport context == expectedSupport && goal == childTarget && any (sameInitialFocus identity index) foci ) (throwProof (ExactProofSetInductionGoalMismatch location)) PreparedSetInduction <$> prepareCheckedSetInduction fallback location context locals (PreparedInitialSetInductionFocus identity index) index property antecedents childTarget continuation SelectedLeadingSetInduction sourceName -> do (binderType, property) <- maybe (throwProof (ExactProofSetInductionGoalMismatch location)) pure (openScopedForall goal) unless (binderType == TySet) (throwProof (ExactProofSetInductionGoalMismatch location)) identity <- allocateLocalIdentity extendedContext <- either (throwProof . ExactProofElaborationFailed) pure (case sourceName of Just variable -> Exact.extendExactBinderContext ((identity, variable) :| []) context Nothing -> Exact.extendExactAnonymousBinderContext identity context) let expectedResult = weakenCheckedScopedCore TySet goal prepared <- prepareCheckedSetInduction fallback location extendedContext locals (PreparedLeadingSetInductionFocus identity) 0 property [] property continuation unless (preparedSetInductionResult prepared == expectedResult) (throwProof (ExactProofSetInductionGoalMismatch location)) pure (PreparedSetInduction prepared) where sameInitialFocus expectedIdentity expectedIndex (InitialSetInductionFocus _variable identity index) = identity == expectedIdentity && index == expectedIndex prepareCheckedSetInduction :: Location -> Location -> Exact.ExactBinderContext -> [PreparedLocal] -> PreparedSetInductionFocus -> Natural -> ScopedCheckedCore ObjectId -> [ScopedCheckedCore ObjectId] -> ScopedCheckedCore ObjectId -> Raw.Proof -> Prepare PreparedSetInduction prepareCheckedSetInduction fallback location context locals focus selected property antecedents childTarget continuation = do (_predicate, hypothesis, _step, result) <- maybe (throwProof (ExactProofSetInductionGoalMismatch location)) pure (scopedSetInductionInstance selected property) validateStructuralComposition location (property : hypothesis : result : childTarget : antecedents) (\foundation globalType -> KernelProof.validateSetInductionComposition foundation globalType selected property antecedents childTarget hypothesis result) local <- allocateLocal ExactAssumption context hypothesis child <- prepareProof fallback context (locals <> [local]) RecursiveProofInduction childTarget continuation pure (PreparedCheckedSetInduction focus property antecedents childTarget hypothesis result child) preparedSetInductionResult :: PreparedSetInduction -> ScopedCheckedCore ObjectId preparedSetInductionResult (PreparedCheckedSetInduction _focus _property _antecedents _target _hypothesis result _child) = result selectSetInductionFocus :: Location -> Exact.ExactBinderContext -> SetInductionBoundary -> ScopedCheckedCore ObjectId -> Maybe Raw.Term -> Prepare SelectedSetInductionFocus selectSetInductionFocus location context boundary goal sourceFocus = do explicit <- traverse simpleVariable sourceFocus let (initialFoci, retainedLeadingName) = case boundary of InitialClaimInduction (InitialSetInductionView foci _support _property _antecedents _target leadingName) -> (foci, leadingName) SourceStatementInduction leadingName -> ([], leadingName) RecursiveProofInduction -> ([], Nothing) leadingAvailable = case openScopedForall goal of Just (TySet, _body) -> True _ -> False case explicit of Just variable -> case find (initialNamed variable) initialFoci of Just focus -> pure (SelectedInitialSetInduction focus) Nothing | leadingAvailable , isJust (Exact.exactBinderContextIndex variable context) -> throwProof (ExactProofSetInductionBinderConflict location variable) | leadingAvailable -> pure (SelectedLeadingSetInduction (Just variable)) | isJust (Exact.exactBinderContextIndex variable context) -> throwProof (ExactProofSetInductionActiveBinderIneligible location variable) | otherwise -> throwProof (ExactProofSetInductionVariableNotActive location variable) Nothing -> case ( (SelectedInitialSetInduction <$> initialFoci) <> [ SelectedLeadingSetInduction retainedLeadingName | leadingAvailable ] ) of [only] -> pure only _ -> throwProof (ExactProofSetInductionFocusAmbiguous location) where simpleVariable = \case Raw.TermExpr (Raw.ExprVar variable) -> pure variable _term -> throwProof (ExactProofSetInductionVariableRequired location) initialNamed variable (InitialSetInductionFocus candidate _identity _index) = candidate == variable prepareByCase :: Location -> Exact.ExactBinderContext -> [PreparedLocal] -> ScopedCheckedCore ObjectId -> [Raw.Case] -> Prepare PreparedProof prepareByCase location context locals goal sourceCases = do cases <- maybe (throwProof (ExactProofEmptyCaseSplit location)) (traverse prepareCase) (NonEmpty.nonEmpty sourceCases) exhaustive <- foldM disjoin (preparedCaseAssumption (NonEmpty.head cases)) (preparedCaseAssumption <$> NonEmpty.tail cases) discharge <- prepareDischarge location context locals exhaustive Raw.JustificationEmpty validateStructuralComposition location (goal : exhaustive : (preparedCaseAssumption <$> toList cases)) (\foundation globalType -> KernelProof.validateCaseAnalysisComposition foundation globalType goal (preparedCaseAssumption <$> cases) exhaustive) pure (PreparedByCase (PreparedCaseAnalysis goal cases exhaustive discharge)) where prepareCase (Raw.Case statement child) = do assumption <- Exact.preparedExactPropositionCore <$> prepareStatement context statement local <- allocateLocal ExactAssumption context assumption prepared <- prepareProof (locate statement) context (locals <> [local]) RecursiveProofInduction goal child pure (PreparedCase assumption prepared) disjoin left right = maybe (structuralFailure location "case assumptions changed type or lexical context") pure (disjoinScopedCore left right) preparedCaseAssumption :: PreparedCase -> ScopedCheckedCore ObjectId preparedCaseAssumption (PreparedCase assumption _proof) = assumption preparedCaseProof :: PreparedCase -> PreparedProof preparedCaseProof (PreparedCase _assumption proof) = proof prepareGuardedFix :: Location -> Location -> Exact.ExactBinderContext -> [PreparedLocal] -> ScopedCheckedCore ObjectId -> [Exact.ExactLocalId] -> ScopedCheckedCore ObjectId -> Raw.Proof -> Prepare PreparedProof prepareGuardedFix fallback location context locals goal identities constraint continuation = do (antecedent, conclusion) <- maybe (throwProof (ExactProofExpectedImplicationGoal location)) pure (openScopedImplication goal) unless (constraint == antecedent) (throwProof (ExactProofGoalStatementMismatch location)) local <- allocateLocal ExactAssumption context constraint prepared <- prepareProof fallback context (locals <> [local]) RecursiveProofInduction conclusion continuation pure (PreparedFix identities (PreparedAssume constraint prepared)) prepareCalculation :: Location -> Exact.ExactBinderContext -> [PreparedLocal] -> Maybe Raw.CalcQuantifier -> Raw.Calc -> Prepare PreparedCalculation prepareCalculation location context locals quantifier calculation = do (identities, calculationContext, calculationGuard) <- prepareCalculationScope context quantifier case calculation of Raw.Equation first destinations -> do firstChecked <- prepareSetEndpoint calculationContext first checkedDestinations <- traverse (\(destination, justification) -> do checked <- prepareSetEndpoint calculationContext destination pure ( locate destination , checked , justification )) destinations finishCalculation location context locals TySet identities calculationGuard firstChecked checkedDestinations Raw.Biconditionals first destinations -> do firstChecked <- preparePropositionEndpoint calculationContext first checkedDestinations <- traverse (\(destination, justification) -> do checked <- preparePropositionEndpoint calculationContext destination pure ( locate destination , checked , justification )) destinations finishCalculation location context locals TyProp identities calculationGuard firstChecked checkedDestinations where prepareSetEndpoint endpointContext expression = Exact.preparedExactSetExpressionCore <$> ( liftDriver (Exact.prepareExactSetExpression endpointContext expression) >>= either (throwProof . ExactProofElaborationFailed) pure ) preparePropositionEndpoint endpointContext formula = Exact.preparedExactPropositionCore <$> prepareStatement endpointContext (Raw.StmtFormula formula) prepareCalculationScope :: Exact.ExactBinderContext -> Maybe Raw.CalcQuantifier -> Prepare ( [Exact.ExactLocalId] , Exact.ExactBinderContext , Maybe (ScopedCheckedCore ObjectId) ) prepareCalculationScope context = \case Nothing -> pure ([], context, Nothing) Just (Raw.CalcQuantifier variables bound suchThat) -> do identities <- traverse (const allocateLocalIdentity) variables calculationContext <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactBinderContext (NonEmpty.zip identities variables) context) boundGuard <- prepareSymbolicBoundConstraints calculationContext variables bound suchThatGuard <- traverse (fmap Exact.preparedExactPropositionCore . prepareStatement calculationContext) suchThat calculationGuard <- normalizeCalculationGuard (boundGuard : maybeToList suchThatGuard) pure (toList identities, calculationContext, calculationGuard) normalizeCalculationGuard :: [ScopedCheckedCore ObjectId] -> Prepare (Maybe (ScopedCheckedCore ObjectId)) normalizeCalculationGuard guards = foldM add Nothing guards where add accumulated constraint | isScopedTruth constraint = pure accumulated | otherwise = case accumulated of Nothing -> pure (Just constraint) Just previous -> Just <$> maybe (impossible "checked calculation guards changed context") pure (conjoinScopedCore previous constraint) isScopedTruth proposition = scopedCoreType proposition == TyProp && scopedCoreTerm proposition == CImp CFalsum CFalsum finishCalculation :: Location -> Exact.ExactBinderContext -> [PreparedLocal] -> CoreType -> [Exact.ExactLocalId] -> Maybe (ScopedCheckedCore ObjectId) -> ScopedCheckedCore ObjectId -> NonEmpty ( Location , ScopedCheckedCore ObjectId , Raw.Justification ) -> Prepare PreparedCalculation finishCalculation fallback context locals operandType identities calculationGuard first destinations = do links <- prepareCalculationLinks first destinations let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links) resultOpen <- calculationEquality first finalEndpoint result <- closeCalculationProposition identities calculationGuard resultOpen pure (PreparedCheckedCalculation operandType identities calculationGuard first links result) where prepareCalculationLinks previous (destination :| rest) = do (next, firstLink) <- prepareCalculationLink previous destination later <- prepareRemainingCalculationLinks next rest pure (firstLink :| later) prepareRemainingCalculationLinks _previous [] = pure [] prepareRemainingCalculationLinks previous (destination : rest) = do (next, link) <- prepareCalculationLink previous destination (link :) <$> prepareRemainingCalculationLinks next rest prepareCalculationLink previous (destinationLocation, destination, justification) = do linkOpen <- calculationEquality previous destination link <- closeCalculationProposition identities calculationGuard linkOpen discharge <- prepareDischarge (if destinationLocation == Nowhere then fallback else destinationLocation) context locals link justification pure ( destination , PreparedCalculationLink destination discharge ) calculationEquality left right = maybe (impossible "checked calculation endpoints changed type or context") pure (equalScopedCore left right) closeCalculationProposition :: [Exact.ExactLocalId] -> Maybe (ScopedCheckedCore ObjectId) -> ScopedCheckedCore ObjectId -> Prepare (ScopedCheckedCore ObjectId) closeCalculationProposition identities calculationGuard proposition = do guarded <- case calculationGuard of Nothing -> pure proposition Just constraint -> maybe (impossible "a checked calculation guard changed context") pure (implyScopedCore constraint proposition) pure (closeBinders (length identities) guarded) where closeBinders 0 closed = closed closeBinders remaining open = closeBinders (remaining - 1) (fromMaybe (impossible "a checked calculation lost a quantified binder") (closeScopedForall open)) preparedCalculationResult :: PreparedCalculation -> ScopedCheckedCore ObjectId preparedCalculationResult (PreparedCheckedCalculation _operandType _identities _guard _first _links result) = result preparedCalculationLinkDestination :: PreparedCalculationLink -> ScopedCheckedCore ObjectId preparedCalculationLinkDestination (PreparedCalculationLink destination _discharge) = destination preparedCalculationLinkDischarge :: PreparedCalculationLink -> PreparedDischarge preparedCalculationLinkDischarge (PreparedCalculationLink _destination discharge) = discharge preparedDischargeGoal :: PreparedDischarge -> ScopedCheckedCore ObjectId preparedDischargeGoal = \case PreparedVampireDischarge _location _justification goal _obligation -> goal PreparedSetExtensionality _location goal -> goal prepareSymbolicBoundConstraints :: Exact.ExactBinderContext -> NonEmpty Raw.VarSymbol -> Raw.Bound -> Prepare (ScopedCheckedCore ObjectId) prepareSymbolicBoundConstraints context variables bound = Exact.preparedExactPropositionCore <$> ( liftDriver (Exact.prepareExactSymbolicBoundConstraints context variables bound) >>= either (throwProof . ExactProofElaborationFailed) pure ) prepareSymbolicTake :: Location -> Location -> Exact.ExactBinderContext -> [PreparedLocal] -> ScopedCheckedCore ObjectId -> NonEmpty Raw.VarSymbol -> Raw.Bound -> Raw.Stmt -> Raw.Justification -> Raw.Proof -> Prepare PreparedProof prepareSymbolicTake fallback location context locals goal variables bound statement justification continuation = do identities <- traverse (const allocateLocalIdentity) variables context' <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactBinderContext (NonEmpty.zip identities variables) context) witness <- Exact.preparedExactPropositionCore <$> ( liftDriver (Exact.prepareExactSymbolicWitnessConstraints context' variables bound statement) >>= either (throwProof . ExactProofElaborationFailed) pure ) prepareTake fallback location context locals goal context' (toList identities) witness justification continuation prepareNounTake :: Location -> Location -> Exact.ExactBinderContext -> [PreparedLocal] -> ScopedCheckedCore ObjectId -> Raw.NounPhrase [] -> Raw.Justification -> Raw.Proof -> Prepare PreparedProof prepareNounTake fallback location context locals goal nounPhrase justification continuation = do (identities, context') <- case nounPhrase of Raw.NounPhrase _left _noun variables _right _suchThat -> case NonEmpty.nonEmpty variables of Just binders -> do identities <- traverse (const allocateLocalIdentity) binders context' <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactBinderContext (NonEmpty.zip identities binders) context) pure (toList identities, context') Nothing -> do identity <- allocateLocalIdentity context' <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactAnonymousBinderContext identity context) pure ([identity], context') witness <- Exact.preparedExactPropositionCore <$> ( liftDriver (Exact.prepareExactNounWitnessConstraints context' nounPhrase) >>= either (throwProof . ExactProofElaborationFailed) pure ) prepareTake fallback location context locals goal context' identities witness justification continuation prepareTake :: Location -> Location -> Exact.ExactBinderContext -> [PreparedLocal] -> ScopedCheckedCore ObjectId -> Exact.ExactBinderContext -> [Exact.ExactLocalId] -> ScopedCheckedCore ObjectId -> Raw.Justification -> Raw.Proof -> Prepare PreparedProof prepareTake fallback location context locals goal witnessContext identities witness justification continuation = do let witnessCount = length identities existence = closeTakenWitnesses witnessCount witness goal' = weakenForTakenWitnesses witnessCount goal discharge <- prepareDischarge location context locals existence justification local <- allocateLocal ExactAssumption witnessContext witness PreparedTake identities witness discharge <$> prepareProof fallback witnessContext (locals <> [local]) RecursiveProofInduction goal' continuation -- The discharged existential and the opened witness premise are the same -- checked proposition viewed on opposite sides of existential elimination. closeTakenWitnesses :: Int -> ScopedCheckedCore ObjectId -> ScopedCheckedCore ObjectId closeTakenWitnesses binderCount = go binderCount where go 0 proposition = proposition go remaining proposition = go (remaining - 1) (fromMaybe (impossible "a taken witness has no checked binder") (closeScopedExists proposition)) weakenForTakenWitnesses :: Int -> ScopedCheckedCore ObjectId -> ScopedCheckedCore ObjectId weakenForTakenWitnesses binderCount = go binderCount where go 0 proposition = proposition go remaining proposition = go (remaining - 1) (weakenCheckedScopedCore TySet proposition) openFixedVariables :: Exact.ExactBinderContext -> ScopedCheckedCore ObjectId -> NonEmpty Raw.VarSymbol -> Prepare ( Exact.ExactBinderContext , ScopedCheckedCore ObjectId , [Exact.ExactLocalId] ) openFixedVariables initialContext initialGoal variables = foldM openOne (initialContext, initialGoal, []) (toList variables) where openOne (context, goal, identities) variable = do (binderType, body) <- maybe (throwProof (ExactProofExpectedUniversalGoal (locate variable))) pure (openScopedForall goal) unless (binderType == TySet) (throwProof (ExactProofExpectedUniversalGoal (locate variable))) identity <- allocateLocalIdentity context' <- either (throwProof . ExactProofElaborationFailed) pure (Exact.extendExactBinderContext ((identity, variable) :| []) context) pure (context', body, identities <> [identity]) allocateLocalIdentity :: Prepare Exact.ExactLocalId allocateLocalIdentity = do state <- State.get State.put state { prepareNextLocal = prepareNextLocal state + 1 } pure (Exact.exactLocalId (prepareNextLocal state)) allocateLocal :: ExactLocalOrigin -> Exact.ExactBinderContext -> ScopedCheckedCore ObjectId -> Prepare PreparedLocal allocateLocal origin context proposition = do state <- State.get State.put state { prepareNextPremise = prepareNextPremise state + 1 } pure (PreparedLocal (Backend.localPremiseOrdinal (prepareNextPremise state)) origin (Exact.exactBinderContextSupport context) proposition) prepareConstructionFoundation :: Prepare SetConstructionFoundation prepareConstructionFoundation = do familyUnion <- foundation FamilyUnionCharacteristic separation <- foundation SeparationCharacteristic replacement <- foundation ReplacementCharacteristic setChoose <- foundation SetChooseWitness pure (setConstructionFoundation familyUnion separation replacement setChoose) where foundation tag = liftDriver (Declaration.currentFoundationAxiomLowering tag) prepareDischarge :: Location -> Exact.ExactBinderContext -> [PreparedLocal] -> ScopedCheckedCore ObjectId -> Raw.Justification -> Prepare PreparedDischarge prepareDischarge location context locals goal justification = prepareDischargeWith (dischargeModeFor goal) [] Nothing location context locals goal justification -- A contradictory-axioms answer can establish falsum, but never an unrelated -- proposition directly. Derive that distinction from the checked target so -- every surface proof spelling reaches the same guarded request path. dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode dischargeModeFor goal | scopedCoreType goal == TyProp , scopedCoreTerm goal == CFalsum = IndirectContradictionDischarge | otherwise = DirectDischarge data DischargeMode = DirectDischarge | IndirectContradictionDischarge prepareDischargeWith :: DischargeMode -> [FoundationAxiomTag] -> Maybe Declaration.VampirePremiseSelection -> Location -> Exact.ExactBinderContext -> [PreparedLocal] -> ScopedCheckedCore ObjectId -> Raw.Justification -> Prepare PreparedDischarge prepareDischargeWith dischargeMode auxiliaries selectionOverride location context locals goal justification = case justification of Raw.JustificationSetExt -> do (leftToRight, rightToLeft) <- maybe (throwProof (ExactProofSetExtensionalityGoalMismatch location)) pure (splitScopedSetEquality goal) unless ( hasDerivedLocal leftToRight && hasDerivedLocal rightToLeft ) (throwProof (ExactProofSetExtensionalityDirectionsUnavailable location)) pure (PreparedSetExtensionality location goal) _ -> do preparedJustification <- prepareJustification location justification prepared <- liftDriver (prepareObligation (Exact.exactBinderContextSupport context) goal (toScopedPremise <$> locals) auxiliaries (fromMaybe (vampirePremiseSelection preparedJustification) selectionOverride)) >>= either (throwProof . ExactProofObligationPreparationFailed location) pure pure (PreparedVampireDischarge location preparedJustification goal prepared) where prepareObligation = case dischargeMode of DirectDischarge -> Declaration.prepareScopedVampireObligationLowering IndirectContradictionDischarge -> Declaration.prepareScopedContradictionObligationLowering hasDerivedLocal proposition = any (\case PreparedLocal _ordinal ExactDerivedClaim _support local -> local == proposition PreparedLocal{} -> False) locals toScopedPremise (PreparedLocal ordinal origin support proposition) = Declaration.scopedVampirePremise ordinal origin support proposition prepareJustification :: Location -> Raw.Justification -> Prepare PreparedJustification prepareJustification _location Raw.JustificationEmpty = pure PreparedAuto prepareJustification location (Raw.JustificationRef markers) = do resolved <- traverse (resolveReference location) (toList markers) let unique = stableUnique resolved case unique of [] -> impossible "a nonempty citation list resolved to no facts" first : rest -> pure (PreparedReferences (first :| rest)) prepareJustification _location Raw.JustificationLocal = pure PreparedLocalOnly prepareJustification location Raw.JustificationSetExt = throwProof (ExactProofUnsupportedStep location) vampirePremiseSelection :: PreparedJustification -> Declaration.VampirePremiseSelection vampirePremiseSelection = \case PreparedAuto -> Declaration.VampireImplicitPremises PreparedReferences fingerprints -> Declaration.VampireExplicitPremises fingerprints PreparedLocalOnly -> Declaration.VampireLocalPremises resolveReference :: Location -> Raw.Marker -> Prepare SemanticFactOccurrenceFingerprint resolveReference location marker@(Raw.Marker name) = do resolved <- liftDriver (Declaration.resolveVisibleFactAliasLowering (semanticName name)) maybe (throwProof (ExactProofUnknownReference location marker)) pure resolved prepareStatement :: Exact.ExactBinderContext -> Raw.Stmt -> Prepare Exact.PreparedExactProposition prepareStatement context statement = liftDriver (Exact.prepareExactProposition context statement) >>= either (throwProof . ExactProofElaborationFailed) pure validateStructuralComposition :: Location -> [ScopedCheckedCore ObjectId] -> ( CheckedFoundation -> (ObjectId -> Maybe CoreType) -> Either KernelProof.KernelProofBuildError () ) -> Prepare () validateStructuralComposition location propositions validate = do foundation <- liftDriver Declaration.currentFoundationLowering let identities = Set.toAscList (Set.unions ( canonicalTermGlobals . scopedCoreTerm <$> propositions )) types <- traverse (\identity -> do coreType <- liftDriver (Declaration.objectTypeLowering identity) maybe (impossible "a checked structural proof lost a global object") (\availableType -> pure (identity, availableType)) coreType) identities either (throwProof . ExactProofStructuralCompositionFailed location) pure (validate foundation (\identity -> Map.lookup identity (Map.fromList types))) structuralFailure :: Location -> Text -> Prepare value structuralFailure location message = throwProof (ExactProofStructuralCompositionFailed location (KernelProof.ProofStructuralCompositionMismatch message)) data CheckedExactProofAuthorization = CheckedExactProofAuthorization !PreparedProof !Bool lowerPreparedExactProof :: PreparedExactProof -> Declaration.LoweringDriver (Either Declaration.DeclarationError (Declaration.CheckedDeclaration CheckedExactProofAuthorization)) lowerPreparedExactProof (PreparedExactProof _location alias target proof syntax) = fmap checked <$> Declaration.prepareCandidateSpecLowering [] target SearchEligible [alias] where checked spec = Declaration.checkedProofDeclaration syntax [] [] [] [] [Declaration.checkedCandidate spec planning :| []] (CheckedExactProofAuthorization proof (isJust (preparedProofFirstOmission proof))) where requests = plannedProofRequests proof planning | isJust (preparedProofFirstOmission proof) = Declaration.checkedOmittedPlanning requests [] | otherwise = Declaration.checkedSourceProofPlanning requests [] authorizeCheckedExactProof :: CheckedExactProofAuthorization -> [NonEmpty Declaration.ReservedCandidate] -> Declaration.Declaration () authorizeCheckedExactProof (CheckedExactProofAuthorization proof hasOmission) = \case [candidate :| []] | hasOmission -> Declaration.authorizeOmittedCandidate candidate (executePreparedProof proof) | otherwise -> Declaration.authorizeVampireCandidate candidate (executePreparedProof proof) stages -> Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch 1 (length stages)) data CheckedFinalPreludeFoundationAuthorization = CheckedFinalPreludeFoundationAuthorization !FoundationAxiomTag lowerPreparedFinalPreludeFoundationClaim :: PreparedFinalPreludeFoundationClaim -> Declaration.LoweringDriver (Either Declaration.DeclarationError (Declaration.CheckedDeclaration CheckedFinalPreludeFoundationAuthorization)) lowerPreparedFinalPreludeFoundationClaim (PreparedFinalPreludeFoundationClaim _location alias target tag syntax) = fmap checked <$> Declaration.prepareCandidateSpecLowering [] target SearchEligible [alias] where checked spec = Declaration.checkedProofDeclaration syntax [] [] [] [] [ Declaration.checkedCandidate spec (Declaration.checkedKernelPlanning (Authority.FoundationLeaf tag) []) :| [] ] (CheckedFinalPreludeFoundationAuthorization tag) authorizeCheckedFinalPreludeFoundationClaim :: CheckedFinalPreludeFoundationAuthorization -> [NonEmpty Declaration.ReservedCandidate] -> Declaration.Declaration () authorizeCheckedFinalPreludeFoundationClaim (CheckedFinalPreludeFoundationAuthorization tag) = \case [candidate :| []] -> Declaration.authorizeKernelConstructionCandidate (Authority.FoundationLeaf tag) candidate (pure (foundationFactDerivation tag)) stages -> Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch 1 (length stages)) preparedProofFirstOmission :: PreparedProof -> Maybe Location preparedProofFirstOmission = \case PreparedImplicitAuto{} -> Nothing PreparedQed{} -> Nothing PreparedOmitted location _goal -> Just location PreparedFix _identities continuation -> preparedProofFirstOmission continuation PreparedAssume _antecedent continuation -> preparedProofFirstOmission continuation PreparedTake _identities _witness _discharge continuation -> preparedProofFirstOmission continuation PreparedSetInduction (PreparedCheckedSetInduction _focus _property _antecedents _target _hypothesis _result child) -> preparedProofFirstOmission child PreparedHave _claim _discharge continuation -> preparedProofFirstOmission continuation PreparedSuffices _goal _reduction _implication _discharge continuation -> preparedProofFirstOmission continuation PreparedCalculate _calculation continuation -> preparedProofFirstOmission continuation PreparedSince _since _evidence _claim _discharge continuation -> preparedProofFirstOmission continuation PreparedSubclaim _claim subproof continuation -> preparedProofFirstOmission subproof <|> preparedProofFirstOmission continuation PreparedDefine _identity _body _definition continuation -> preparedProofFirstOmission continuation PreparedDefineRelational _identity _body _functionality _definitions continuation -> preparedProofFirstOmission continuation PreparedDefineFunction _identity _graph _definition continuation -> preparedProofFirstOmission continuation PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) -> foldr ((<|>) . preparedProofFirstOmission . preparedCaseProof) Nothing cases PreparedByContradiction _goal _negation _falsum child -> preparedProofFirstOmission child PreparedContradiction{} -> Nothing plannedProofRequests :: PreparedProof -> [Declaration.CheckedPlannedVampireRequest] plannedProofRequests = \case PreparedImplicitAuto discharge -> plannedDischargeRequests discharge PreparedQed discharge -> plannedDischargeRequests discharge PreparedOmitted{} -> [] PreparedFix _identities continuation -> plannedProofRequests continuation PreparedAssume _antecedent continuation -> plannedProofRequests continuation PreparedTake _identities _witness discharge continuation -> plannedDischargeRequests discharge <> plannedProofRequests continuation PreparedSetInduction (PreparedCheckedSetInduction _focus _property _antecedents _target _hypothesis _result child) -> plannedProofRequests child PreparedHave _claim discharge continuation -> plannedDischargeRequests discharge <> plannedProofRequests continuation PreparedSuffices _goal _reduction _implication discharge continuation -> plannedDischargeRequests discharge <> plannedProofRequests continuation PreparedCalculate calculation continuation -> plannedCalculationRequests calculation <> plannedProofRequests continuation PreparedSince _since evidence _claim discharge continuation -> plannedSinceEvidenceRequests evidence <> plannedDischargeRequests discharge <> plannedProofRequests continuation PreparedSubclaim _claim subproof continuation -> plannedProofRequests subproof <> plannedProofRequests continuation PreparedDefine _identity _body _definition continuation -> plannedProofRequests continuation PreparedDefineRelational _identity _body functionality _definitions continuation -> plannedDischargeRequests functionality <> plannedProofRequests continuation PreparedDefineFunction _identity _graph _definition continuation -> plannedProofRequests continuation PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> concatMap (plannedProofRequests . preparedCaseProof) (toList cases) <> plannedDischargeRequests discharge PreparedByContradiction _goal _negation _falsum child -> plannedProofRequests child PreparedContradiction _goal _falsum discharge -> plannedDischargeRequests discharge plannedDischargeRequests :: PreparedDischarge -> [Declaration.CheckedPlannedVampireRequest] plannedDischargeRequests = \case PreparedVampireDischarge location _justification _goal obligation -> [Declaration.checkedPlannedVampireRequest location obligation] PreparedSetExtensionality{} -> [] plannedCalculationRequests :: PreparedCalculation -> [Declaration.CheckedPlannedVampireRequest] plannedCalculationRequests (PreparedCheckedCalculation _operandType _identities _guard _first links _result) = concatMap (plannedDischargeRequests . preparedCalculationLinkDischarge) (toList links) plannedSinceEvidenceRequests :: PreparedSinceEvidence -> [Declaration.CheckedPlannedVampireRequest] plannedSinceEvidenceRequests = \case PreparedSinceExisting{} -> [] PreparedSinceDischarged discharge _local -> plannedDischargeRequests discharge executePreparedProof :: PreparedProof -> Declaration.CandidateProof () executePreparedProof = \case PreparedImplicitAuto discharge -> executeDischarge discharge PreparedQed discharge -> executeDischarge discharge PreparedOmitted _location _goal -> Declaration.recordOmittedUse PreparedFix _identities continuation -> executePreparedProof continuation PreparedAssume _antecedent continuation -> executePreparedProof continuation PreparedTake _identities _witness discharge continuation -> do executeDischarge discharge executePreparedProof continuation PreparedSetInduction (PreparedCheckedSetInduction _focus _property _antecedents _target _hypothesis _result child) -> executePreparedProof child PreparedHave _claim discharge continuation -> do executeDischarge discharge executePreparedProof continuation PreparedSuffices goal reduction implication discharge continuation -> do executeDischarge discharge executePreparedProof continuation unless (implyScopedCore reduction goal == Just implication) (impossible "a prepared suffices implication diverged") PreparedCalculate calculation continuation -> do executePreparedCalculation calculation executePreparedProof continuation PreparedSince sinceProposition evidence _claim discharge continuation -> do executeSinceEvidence sinceProposition evidence executeDischarge discharge executePreparedProof continuation PreparedSubclaim _claim subproof continuation -> do executePreparedProof subproof executePreparedProof continuation PreparedDefine _identity _body _definition continuation -> executePreparedProof continuation PreparedDefineRelational _identity _body functionality _definitions continuation -> do executeDischarge functionality executePreparedProof continuation PreparedDefineFunction _identity _graph _definition continuation -> executePreparedProof continuation PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do traverse_ (executePreparedProof . preparedCaseProof) cases executeDischarge discharge PreparedByContradiction _goal _negation _falsum child -> executePreparedProof child PreparedContradiction _goal _falsum discharge -> executeDischarge discharge executeDischarge :: PreparedDischarge -> Declaration.CandidateProof () executeDischarge (PreparedVampireDischarge location _justification _goal obligation) = Declaration.locateProofObligation location (Declaration.acceptPreparedVampireObligation obligation) executeDischarge PreparedSetExtensionality{} = pure () executePreparedCalculation :: PreparedCalculation -> Declaration.CandidateProof () executePreparedCalculation (PreparedCheckedCalculation _operandType _identities _guard _first links _result) = traverse_ (executeDischarge . preparedCalculationLinkDischarge) links executeSinceEvidence :: ScopedCheckedCore ObjectId -> PreparedSinceEvidence -> Declaration.CandidateProof () executeSinceEvidence proposition = \case PreparedSinceExisting local -> unless (preparedLocalProposition local == proposition) (impossible "a structural since premise diverged") PreparedSinceDischarged discharge local -> do executeDischarge discharge unless ( preparedDischargeGoal discharge == proposition && preparedLocalProposition local == proposition ) (impossible "a discharged since premise diverged") preparedLocalProposition :: PreparedLocal -> ScopedCheckedCore ObjectId preparedLocalProposition (PreparedLocal _ordinal _origin _support proposition) = proposition encodePreparedProof :: PreparedProof -> ByteString encodePreparedProof = encodeCache . putPreparedProof putPreparedProof :: PreparedProof -> CachePut putPreparedProof = \case PreparedImplicitAuto discharge -> do putCacheTag 0x00 putPreparedDischarge discharge PreparedQed discharge -> do putCacheTag 0x01 putPreparedDischarge discharge PreparedOmitted _location goal -> do putCacheTag 0x06 putScopedProposition goal PreparedFix identities continuation -> do putCacheTag 0x02 putCacheList (putCacheNatural . Exact.exactLocalIdValue) identities putPreparedProof continuation PreparedAssume antecedent continuation -> do putCacheTag 0x03 putScopedProposition antecedent putPreparedProof continuation PreparedTake identities witness discharge continuation -> do putCacheTag 0x08 putCacheList (putCacheNatural . Exact.exactLocalIdValue) identities putScopedProposition witness putPreparedDischarge discharge putPreparedProof continuation PreparedSetInduction (PreparedCheckedSetInduction focus property antecedents target hypothesis result child) -> do putCacheTag 0x07 putPreparedSetInductionFocus focus putScopedProposition property putCacheList putScopedProposition antecedents putScopedProposition target putScopedProposition hypothesis putScopedProposition result putPreparedProof child PreparedHave claim discharge continuation -> do putCacheTag 0x04 putScopedProposition claim putPreparedDischarge discharge putPreparedProof continuation PreparedSuffices goal reduction implication discharge continuation -> do putCacheTag 0x0c putScopedProposition goal putScopedProposition reduction putScopedProposition implication putPreparedDischarge discharge putPreparedProof continuation PreparedCalculate calculation continuation -> do putCacheTag 0x0d putPreparedCalculation calculation putPreparedProof continuation PreparedSince sinceProposition evidence claim discharge continuation -> do putCacheTag 0x0e putScopedProposition sinceProposition putPreparedSinceEvidence evidence putScopedProposition claim putPreparedDischarge discharge putPreparedProof continuation PreparedSubclaim claim subproof continuation -> do putCacheTag 0x05 putScopedProposition claim putPreparedProof subproof putPreparedProof continuation PreparedDefine identity body definitions continuation -> do putCacheTag 0x09 putCacheNatural (Exact.exactLocalIdValue identity) putScopedTerm body putCacheList putScopedProposition (toList definitions) putPreparedProof continuation PreparedDefineRelational identity body functionality definitions continuation -> do putCacheTag 0x11 putCacheNatural (Exact.exactLocalIdValue identity) putScopedTerm body putPreparedDischarge functionality putCacheList putScopedProposition (toList definitions) putPreparedProof continuation PreparedByCase caseAnalysis -> do putCacheTag 0x0f putPreparedCaseAnalysis caseAnalysis PreparedByContradiction goal negation falsum child -> do putCacheTag 0x10 putScopedProposition goal putScopedProposition negation putScopedProposition falsum putPreparedProof child PreparedContradiction goal falsum discharge -> do putCacheTag 0x0a putScopedProposition goal putScopedProposition falsum putPreparedDischarge discharge PreparedDefineFunction identity graph definition continuation -> do putCacheTag 0x0b putCacheNatural (Exact.exactLocalIdValue identity) putScopedTerm graph putScopedProposition definition putPreparedProof continuation putPreparedSetInductionFocus :: PreparedSetInductionFocus -> CachePut putPreparedSetInductionFocus = \case PreparedInitialSetInductionFocus identity index -> do putCacheTag 0x00 putCacheNatural (Exact.exactLocalIdValue identity) putCacheNatural index PreparedLeadingSetInductionFocus identity -> do putCacheTag 0x01 putCacheNatural (Exact.exactLocalIdValue identity) putPreparedDischarge :: PreparedDischarge -> CachePut putPreparedDischarge (PreparedVampireDischarge _location justification goal _obligation) = do putPreparedDischargeSyntax justification goal putPreparedDischarge (PreparedSetExtensionality _location goal) = do putCacheTag 0x03 putScopedProposition goal putPreparedDischargeSyntax :: PreparedJustification -> ScopedCheckedCore ObjectId -> CachePut putPreparedDischargeSyntax justification goal = do putPreparedJustification justification putScopedProposition goal putPreparedCalculation :: PreparedCalculation -> CachePut putPreparedCalculation (PreparedCheckedCalculation operandType identities calculationGuard first links result) = do putCoreTypeCache operandType putCacheList (putCacheNatural . Exact.exactLocalIdValue) identities putCacheMaybe putScopedProposition calculationGuard putCacheList putScopedTerm (first : (preparedCalculationLinkDestination <$> toList links)) putCacheList putPreparedDischarge (preparedCalculationLinkDischarge <$> toList links) putScopedProposition result putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut putPreparedSinceEvidence = \case PreparedSinceExisting local -> do putCacheTag 0x00 putPreparedLocalEvidence local PreparedSinceDischarged discharge local -> do putCacheTag 0x01 putPreparedDischarge discharge putPreparedLocalEvidence local putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut putPreparedCaseAnalysis (PreparedCaseAnalysis goal cases exhaustive discharge) = do putScopedProposition goal putCacheList putPreparedCase (toList cases) putScopedProposition exhaustive putPreparedDischarge discharge putPreparedCase :: PreparedCase -> CachePut putPreparedCase (PreparedCase assumption proof) = do putScopedProposition assumption putPreparedProof proof putPreparedLocalEvidence :: PreparedLocal -> CachePut putPreparedLocalEvidence (PreparedLocal ordinal _origin support proposition) = do putCacheNatural (Backend.localPremiseOrdinalValue ordinal) putCacheList (\(identity, coreType) -> do putCacheNatural (Exact.exactLocalIdValue identity) putCoreTypeCache coreType) (Vector.toList support) putScopedProposition proposition implicitAutoProofSyntaxId :: ScopedCheckedCore ObjectId -> ProofSyntaxId implicitAutoProofSyntaxId goal = proofSyntaxId (encodeCache do putCacheTag 0x00 putPreparedDischargeSyntax PreparedAuto goal) putPreparedJustification :: PreparedJustification -> CachePut putPreparedJustification = \case PreparedAuto -> putCacheTag 0x00 PreparedReferences fingerprints -> do putCacheTag 0x01 putCacheList putSemanticFactOccurrenceFingerprintCache (toList fingerprints) PreparedLocalOnly -> putCacheTag 0x02 putScopedProposition :: ScopedCheckedCore ObjectId -> CachePut putScopedProposition proposition = do putCacheList putCoreTypeCache (scopedCoreContext proposition) putCanonicalTermCache putObjectIdCache (scopedCoreTerm proposition) putScopedTerm :: ScopedCheckedCore ObjectId -> CachePut putScopedTerm term = do putCacheList putCoreTypeCache (scopedCoreContext term) putCoreTypeCache (scopedCoreType term) putCanonicalTermCache putObjectIdCache (scopedCoreTerm term) proofLocation :: Location -> Raw.Proof -> Location proofLocation fallback = \case Raw.Omitted location -> location Raw.Qed maybeLocation _justification -> fromMaybe fallback maybeLocation Raw.Contradiction location _justification -> location Raw.ByCase location _cases -> location Raw.ByContradiction location _proof -> location Raw.BySetInduction location _term _proof -> location Raw.ByOrdInduction location _proof -> location Raw.Assume location _statement _proof -> location Raw.FixSymbolic location _variables _bound _proof -> location Raw.FixSuchThat location _variables _statement _proof -> location Raw.Calc location _quantifier _calculation _proof -> location Raw.TakeVar location _variables _bound _statement _justification _proof -> location Raw.TakeNoun location _noun _justification _proof -> location Raw.Have location _since _statement _justification _proof -> location Raw.Suffices location _statement _justification _proof -> location Raw.Subclaim location _statement _subproof _proof -> location Raw.Define location _variable _expression _proof -> location Raw.DefineFunction location _function _argument _value _bound _domain _proof -> location Raw.DefineFunctionLocal location _function _argument _value _bound _target _rules _proof -> location throwProof :: ExactProofError -> Prepare value throwProof = State.lift . Except.throwError liftDriver :: Declaration.LoweringDriver value -> Prepare value liftDriver = State.lift . Except.lift stableUnique :: Ord value => [value] -> [value] stableUnique = reverse . snd . foldl' (\(seen, reversed) value -> if value `Set.member` seen then (seen, reversed) else ( Set.insert value seen , value : reversed )) (Set.empty, [])