diff options
Diffstat (limited to 'source/Felix/Checking/Kernel/Proof.hs')
| -rw-r--r-- | source/Felix/Checking/Kernel/Proof.hs | 1443 |
1 files changed, 1443 insertions, 0 deletions
diff --git a/source/Felix/Checking/Kernel/Proof.hs b/source/Felix/Checking/Kernel/Proof.hs new file mode 100644 index 0000000..d4ccedc --- /dev/null +++ b/source/Felix/Checking/Kernel/Proof.hs @@ -0,0 +1,1443 @@ +{-# 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) |