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