diff options
Diffstat (limited to 'source/Checking/Kernel/Proof.hs')
| -rw-r--r-- | source/Checking/Kernel/Proof.hs | 1166 |
1 files changed, 0 insertions, 1166 deletions
diff --git a/source/Checking/Kernel/Proof.hs b/source/Checking/Kernel/Proof.hs deleted file mode 100644 index 42324d1..0000000 --- a/source/Checking/Kernel/Proof.hs +++ /dev/null @@ -1,1166 +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 - , 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.Text qualified as Text - - -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 - 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 - -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) |