diff options
Diffstat (limited to 'source/Checking/Kernel/Proof.hs')
| -rw-r--r-- | source/Checking/Kernel/Proof.hs | 1443 |
1 files changed, 0 insertions, 1443 deletions
diff --git a/source/Checking/Kernel/Proof.hs b/source/Checking/Kernel/Proof.hs deleted file mode 100644 index 5fc0d96..0000000 --- a/source/Checking/Kernel/Proof.hs +++ /dev/null @@ -1,1443 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Small proof-producing natural-deduction combinators. Every resulting tree --- is still replayed independently before it can authorize a fact. -module 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 Checking.Core -import Checking.Foundation -import Checking.Kernel.Derivation -import Checking.Kernel.Semantics qualified as Semantics -import 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) |