diff options
Diffstat (limited to 'source/Checking/Kernel/Proof.hs')
| -rw-r--r-- | source/Checking/Kernel/Proof.hs | 277 |
1 files changed, 277 insertions, 0 deletions
diff --git a/source/Checking/Kernel/Proof.hs b/source/Checking/Kernel/Proof.hs index 42324d1..5fc0d96 100644 --- a/source/Checking/Kernel/Proof.hs +++ b/source/Checking/Kernel/Proof.hs @@ -33,6 +33,10 @@ module Checking.Kernel.Proof , disjunctionLeftProof , disjunctionRightProof , disjunctionEliminationProof + , validateCaseAnalysisComposition + , validateDoubleNegationComposition + , validateFalsumEliminationComposition + , validateSetInductionComposition , existentialTerm , existentialIntroductionProof , existentialEliminationProof @@ -52,7 +56,9 @@ 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 @@ -108,6 +114,7 @@ data KernelProofBuildError | ProofExpectedUnaryBinder | ProofSetLfpRuleFailed !Text | ProofConversionPlanFailed !Text + | ProofStructuralCompositionMismatch !Text deriving stock (Show, Eq) scopedTerm @@ -881,6 +888,276 @@ disjunctionEliminationProof 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 |