diff options
Diffstat (limited to 'source/Felix/Checking/Kernel')
| -rw-r--r-- | source/Felix/Checking/Kernel/Derivation.hs | 1264 | ||||
| -rw-r--r-- | source/Felix/Checking/Kernel/Proof.hs | 1443 | ||||
| -rw-r--r-- | source/Felix/Checking/Kernel/Semantics.hs | 436 | ||||
| -rw-r--r-- | source/Felix/Checking/Kernel/SetLfp.hs | 762 |
4 files changed, 3905 insertions, 0 deletions
diff --git a/source/Felix/Checking/Kernel/Derivation.hs b/source/Felix/Checking/Kernel/Derivation.hs new file mode 100644 index 0000000..e83b376 --- /dev/null +++ b/source/Felix/Checking/Kernel/Derivation.hs @@ -0,0 +1,1264 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Private in-memory proof trees and independent kernel replay. +module Felix.Checking.Kernel.Derivation + ( ImportIx + , importIx + , importIxValue + , HypothesisIx + , hypothesisIx + , DerivationImportJudgment + , derivationImportJudgment + , derivationImportStatement + , KernelDerivation + , mapKernelDerivationGlobals + , importedFactDerivation + , localHypothesisDerivation + , foundationFactDerivation + , implicationEliminationDerivation + , forallEliminationDerivation + , falsumEliminationDerivation + , implicationIntroductionDerivation + , forallIntroductionDerivation + , ConversionPlan + , conversionPlan + , conversionPlanBudget + , ConversionPlanError(..) + , convertJudgmentDerivation + , equalityReflexivityDerivation + , scopedEqualityReflexivityDerivation + , equalityCongruenceApplicationDerivation + , equalityCongruenceLambdaDerivation + , equalityModusPonensDerivation + , setLfpBoundDerivation + , setLfpLeastDerivation + , setLfpFixedDerivation + , setLfpInductDerivation + , weakenDerivationHypotheses + , KernelReplayLimits + , kernelReplayLimits + , defaultKernelReplayLimits + , KernelReplayLimitError(..) + , ReplayedKernelDerivation + , replayKernelDerivation + , replayedKernelTarget + , replayedKernelImportUses + , replayedKernelFoundationUses + , replayedKernelRuleUses + , replayedKernelNodeCount + , replayedKernelMaximumDepth + , DerivationImportError(..) + , KernelReplayError(..) + ) where + +import Base +import Felix.Checking.Core +import Felix.Checking.Foundation +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.Set qualified as Set +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Numeric.Natural (Natural) + + +newtype ImportIx = ImportIx Natural + deriving stock (Show, Eq, Ord) + +importIx :: Natural -> ImportIx +importIx = ImportIx + +importIxValue :: ImportIx -> Natural +importIxValue (ImportIx index) = + index + +newtype HypothesisIx = HypothesisIx Natural + deriving stock (Show, Eq, Ord) + +hypothesisIx :: Natural -> HypothesisIx +hypothesisIx = HypothesisIx + +newtype DerivationImportJudgment global = + DerivationImportJudgment + (FrozenCheckedCore global) + deriving stock (Eq) + +data DerivationImportError = + DerivationImportIsNotProposition !CoreType + deriving stock (Show, Eq) + +derivationImportJudgment + :: FrozenCheckedCore global + -> Either + DerivationImportError + (DerivationImportJudgment global) +derivationImportJudgment statement + | frozenCoreType statement == TyProp = + Right (DerivationImportJudgment statement) + | otherwise = + Left + (DerivationImportIsNotProposition + (frozenCoreType statement)) + +derivationImportStatement + :: DerivationImportJudgment global + -> FrozenCheckedCore global +derivationImportStatement + (DerivationImportJudgment statement) = + statement + +data KernelDerivation global + = UseImportedFact !ImportIx + | UseLocalHypothesis !HypothesisIx + | UseFoundationFact !FoundationAxiomTag + | ImplicationElimination + !(KernelDerivation global) + !(KernelDerivation global) + | ForallElimination + !(KernelDerivation global) + !(ScopedCheckedCore global) + | FalsumElimination + !(KernelDerivation global) + !(ScopedCheckedCore global) + | ImplicationIntroduction + !(ScopedCheckedCore global) + !(KernelDerivation global) + | ForallIntroduction + !CoreType + !(KernelDerivation global) + | ConvertJudgment + !(KernelDerivation global) + !(ScopedCheckedCore global) + !ConversionPlan + | EqualityReflexivity + !(ScopedCheckedCore global) + | EqualityCongruenceApplication + !(KernelDerivation global) + !(KernelDerivation global) + | EqualityCongruenceLambda + !CoreType + !(KernelDerivation global) + | EqualityModusPonens + !(KernelDerivation global) + !(KernelDerivation global) + | ApplySetLfpBound + !(ScopedCheckedCore global) + !(ScopedCheckedCore global) + | ApplySetLfpLeast + !(ScopedCheckedCore global) + !(ScopedCheckedCore global) + !(ScopedCheckedCore global) + !(KernelDerivation global) + !(KernelDerivation global) + | ApplySetLfpFixed + !(ScopedCheckedCore global) + !(ScopedCheckedCore global) + !(KernelDerivation global) + | ApplySetLfpInduct + !(ScopedCheckedCore global) + !(ScopedCheckedCore global) + !(ScopedCheckedCore global) + !(ScopedCheckedCore global) + !(KernelDerivation global) + !(KernelDerivation global) + !(KernelDerivation global) + deriving stock (Eq) + +mapKernelDerivationGlobals + :: (left -> right) + -> KernelDerivation left + -> KernelDerivation right +mapKernelDerivationGlobals transform = go + where + scoped = mapScopedGlobals transform + go = \case + UseImportedFact index -> + UseImportedFact index + UseLocalHypothesis index -> + UseLocalHypothesis index + UseFoundationFact tag -> + UseFoundationFact tag + ImplicationElimination premise implication -> + ImplicationElimination (go premise) (go implication) + ForallElimination proof argument -> + ForallElimination (go proof) (scoped argument) + FalsumElimination proof target -> + FalsumElimination (go proof) (scoped target) + ImplicationIntroduction premise proof -> + ImplicationIntroduction (scoped premise) (go proof) + ForallIntroduction binderType proof -> + ForallIntroduction binderType (go proof) + ConvertJudgment proof target plan -> + ConvertJudgment (go proof) (scoped target) plan + EqualityReflexivity term -> + EqualityReflexivity (scoped term) + EqualityCongruenceApplication function argument -> + EqualityCongruenceApplication (go function) (go argument) + EqualityCongruenceLambda binderType proof -> + EqualityCongruenceLambda binderType (go proof) + EqualityModusPonens equality proof -> + EqualityModusPonens (go equality) (go proof) + ApplySetLfpBound domain operator -> + ApplySetLfpBound (scoped domain) (scoped operator) + ApplySetLfpLeast domain operator candidate bounded closed -> + ApplySetLfpLeast + (scoped domain) + (scoped operator) + (scoped candidate) + (go bounded) + (go closed) + ApplySetLfpFixed domain operator monotone -> + ApplySetLfpFixed + (scoped domain) + (scoped operator) + (go monotone) + ApplySetLfpInduct domain operator predicate element + monotone member closed -> + ApplySetLfpInduct + (scoped domain) + (scoped operator) + (scoped predicate) + (scoped element) + (go monotone) + (go member) + (go closed) + +importedFactDerivation + :: ImportIx + -> KernelDerivation global +importedFactDerivation = + UseImportedFact + +localHypothesisDerivation + :: HypothesisIx + -> KernelDerivation global +localHypothesisDerivation = + UseLocalHypothesis + +foundationFactDerivation + :: FoundationAxiomTag + -> KernelDerivation global +foundationFactDerivation = + UseFoundationFact + +implicationEliminationDerivation + :: KernelDerivation global + -> KernelDerivation global + -> KernelDerivation global +implicationEliminationDerivation = + ImplicationElimination + +forallEliminationDerivation + :: KernelDerivation global + -> ScopedCheckedCore global + -> KernelDerivation global +forallEliminationDerivation = + ForallElimination + +falsumEliminationDerivation + :: KernelDerivation global + -> ScopedCheckedCore global + -> KernelDerivation global +falsumEliminationDerivation = + FalsumElimination + +implicationIntroductionDerivation + :: ScopedCheckedCore global + -> KernelDerivation global + -> KernelDerivation global +implicationIntroductionDerivation = + ImplicationIntroduction + +forallIntroductionDerivation + :: CoreType + -> KernelDerivation global + -> KernelDerivation global +forallIntroductionDerivation = + ForallIntroduction + +newtype ConversionPlan = ConversionPlan Natural + deriving stock (Show, Eq, Ord) + +data ConversionPlanError = + ConversionPlanExceedsLimit !Natural + deriving stock (Show, Eq) + +conversionPlanLimit :: Natural +conversionPlanLimit = + 100000 + +conversionPlan + :: Natural + -> Either ConversionPlanError ConversionPlan +conversionPlan budget + | budget <= conversionPlanLimit = + Right (ConversionPlan budget) + | otherwise = + Left (ConversionPlanExceedsLimit budget) + +conversionPlanBudget :: ConversionPlan -> Natural +conversionPlanBudget (ConversionPlan budget) = + budget + +convertJudgmentDerivation + :: KernelDerivation global + -> ScopedCheckedCore global + -> ConversionPlan + -> KernelDerivation global +convertJudgmentDerivation = + ConvertJudgment + +equalityReflexivityDerivation + :: FrozenCheckedCore global + -> KernelDerivation global +equalityReflexivityDerivation = + EqualityReflexivity . embedClosedCore [] + +scopedEqualityReflexivityDerivation + :: ScopedCheckedCore global + -> KernelDerivation global +scopedEqualityReflexivityDerivation = + EqualityReflexivity + +equalityCongruenceApplicationDerivation + :: KernelDerivation global + -> KernelDerivation global + -> KernelDerivation global +equalityCongruenceApplicationDerivation = + EqualityCongruenceApplication + +equalityCongruenceLambdaDerivation + :: CoreType + -> KernelDerivation global + -> KernelDerivation global +equalityCongruenceLambdaDerivation = + EqualityCongruenceLambda + +equalityModusPonensDerivation + :: KernelDerivation global + -> KernelDerivation global + -> KernelDerivation global +equalityModusPonensDerivation = + EqualityModusPonens + +setLfpBoundDerivation + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> KernelDerivation global +setLfpBoundDerivation = + ApplySetLfpBound + +setLfpLeastDerivation + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> KernelDerivation global + -> KernelDerivation global + -> KernelDerivation global +setLfpLeastDerivation = + ApplySetLfpLeast + +setLfpFixedDerivation + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> KernelDerivation global + -> KernelDerivation global +setLfpFixedDerivation = + ApplySetLfpFixed + +setLfpInductDerivation + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> KernelDerivation global + -> KernelDerivation global + -> KernelDerivation global + -> KernelDerivation global +setLfpInductDerivation = + ApplySetLfpInduct + +-- | Add hypotheses outside a derivation while preserving hypotheses introduced +-- by implication nodes inside it. +weakenDerivationHypotheses + :: Natural + -> KernelDerivation global + -> KernelDerivation global +weakenDerivationHypotheses amount = + shift 0 + where + shift cutoff = \case + UseImportedFact index -> + UseImportedFact index + UseLocalHypothesis (HypothesisIx index) -> + UseLocalHypothesis + (HypothesisIx + (if index >= cutoff + then index + amount + else index)) + UseFoundationFact tag -> + UseFoundationFact tag + ImplicationElimination implication premise -> + ImplicationElimination + (shift cutoff implication) + (shift cutoff premise) + ForallElimination quantified argument -> + ForallElimination + (shift cutoff quantified) + argument + FalsumElimination falsum target -> + FalsumElimination + (shift cutoff falsum) + target + ImplicationIntroduction premise body -> + ImplicationIntroduction + premise + (shift (cutoff + 1) body) + ForallIntroduction binderType body -> + ForallIntroduction + binderType + (shift cutoff body) + ConvertJudgment source target plan -> + ConvertJudgment + (shift cutoff source) + target + plan + EqualityReflexivity operand -> + EqualityReflexivity operand + EqualityCongruenceApplication function argument -> + EqualityCongruenceApplication + (shift cutoff function) + (shift cutoff argument) + EqualityCongruenceLambda binderType body -> + EqualityCongruenceLambda + binderType + (shift cutoff body) + EqualityModusPonens equality premise -> + EqualityModusPonens + (shift cutoff equality) + (shift cutoff premise) + ApplySetLfpBound domain operator -> + ApplySetLfpBound domain operator + ApplySetLfpLeast + domain operator candidate + closed bounded -> + ApplySetLfpLeast + domain + operator + candidate + (shift cutoff closed) + (shift cutoff bounded) + ApplySetLfpFixed domain operator monotone -> + ApplySetLfpFixed + domain + operator + (shift cutoff monotone) + ApplySetLfpInduct + domain operator predicate element + monotone member closure -> + ApplySetLfpInduct + domain + operator + predicate + element + (shift cutoff monotone) + (shift cutoff member) + (shift cutoff closure) + +data KernelReplayLimits = KernelReplayLimits + !Natural + !Natural + deriving stock (Show, Eq) + +data KernelReplayLimitError + = KernelReplayNodeLimitIsZero + | KernelReplayNodeLimitTooLarge !Natural + | KernelReplayDepthLimitTooLarge !Natural + deriving stock (Show, Eq) + +maximumKernelReplayNodes :: Natural +maximumKernelReplayNodes = + 1000000 + +maximumKernelReplayDepth :: Natural +maximumKernelReplayDepth = + 4096 + +kernelReplayLimits + :: Natural + -> Natural + -> Either KernelReplayLimitError KernelReplayLimits +kernelReplayLimits nodeLimit depthLimit + | nodeLimit == 0 = + Left KernelReplayNodeLimitIsZero + | nodeLimit > maximumKernelReplayNodes = + Left (KernelReplayNodeLimitTooLarge nodeLimit) + | depthLimit > maximumKernelReplayDepth = + Left (KernelReplayDepthLimitTooLarge depthLimit) + | otherwise = + Right + (KernelReplayLimits + nodeLimit + depthLimit) + +defaultKernelReplayLimits :: KernelReplayLimits +defaultKernelReplayLimits = + KernelReplayLimits + 200000 + 2048 + +data ReplayedKernelDerivation global = + ReplayedKernelDerivation + !(FrozenCheckedCore global) + !(Set ImportIx) + !(Set FoundationAxiomTag) + !(Set KernelRuleTag) + !Natural + !Natural + deriving stock (Eq) + +replayedKernelTarget + :: ReplayedKernelDerivation global + -> FrozenCheckedCore global +replayedKernelTarget + (ReplayedKernelDerivation + target + _importUses + _foundationUses + _ruleUses + _nodeCount + _maximumDepth) = + target + +replayedKernelImportUses + :: ReplayedKernelDerivation global + -> Set ImportIx +replayedKernelImportUses + (ReplayedKernelDerivation + _target + importUses + _foundationUses + _ruleUses + _nodeCount + _maximumDepth) = + importUses + +replayedKernelFoundationUses + :: ReplayedKernelDerivation global + -> Set FoundationAxiomTag +replayedKernelFoundationUses + (ReplayedKernelDerivation + _target + _importUses + foundationUses + _ruleUses + _nodeCount + _maximumDepth) = + foundationUses + +replayedKernelRuleUses + :: ReplayedKernelDerivation global + -> Set KernelRuleTag +replayedKernelRuleUses + (ReplayedKernelDerivation + _target + _importUses + _foundationUses + ruleUses + _nodeCount + _maximumDepth) = + ruleUses + +replayedKernelNodeCount + :: ReplayedKernelDerivation global + -> Natural +replayedKernelNodeCount + (ReplayedKernelDerivation + _target + _importUses + _foundationUses + _ruleUses + nodeCount + _maximumDepth) = + nodeCount + +replayedKernelMaximumDepth + :: ReplayedKernelDerivation global + -> Natural +replayedKernelMaximumDepth + (ReplayedKernelDerivation + _target + _importUses + _foundationUses + _ruleUses + _nodeCount + maximumDepth) = + maximumDepth + +data ReplayStep global = ReplayStep + !(ScopedCheckedCore global) + !(Set ImportIx) + !(Set FoundationAxiomTag) + !(Set KernelRuleTag) + !Natural + !Natural + +data KernelReplayError + = KernelReplaySemanticsError + !Semantics.KernelSemanticsError + | KernelReplaySetLfpRuleError + !SetLfp.SetLfpRuleError + | KernelReplayImportOutOfBounds !ImportIx + | KernelReplayHypothesisOutOfBounds !HypothesisIx + | KernelReplayStoredContextMismatch + ![CoreType] + ![CoreType] + | KernelReplayStoredTermIllTyped !CoreCheckError + | KernelReplayStoredTypeMismatch + !CoreType + !CoreType + | KernelReplayWeakeningError !CoreCheckError + | KernelReplayNodeLimitExceeded !Natural + | KernelReplayDepthLimitExceeded !Natural + | KernelReplayRootRemainedOpen + | KernelReplayTargetMismatch + deriving stock (Show, Eq) + +replayKernelDerivation + :: Eq global + => CheckedFoundation + -> KernelReplayLimits + -> (global -> Maybe CoreType) + -> Vector (DerivationImportJudgment global) + -> FrozenCheckedCore global + -> KernelDerivation global + -> Either + KernelReplayError + (ReplayedKernelDerivation global) +replayKernelDerivation + checkedFoundationValue + limits + globalType + imports + expectedTarget + derivation = + checkedFoundationValue `seq` do + expectedTarget' <- + recheckClosed expectedTarget + ReplayStep + synthesized + importUses + foundationUses + ruleUses + nodeCount + maximumDepth <- + replay [] [] 0 derivation + closed <- + maybe + (Left KernelReplayRootRemainedOpen) + Right + (closeScopedCore synthesized) + unless + (closed == expectedTarget') + (Left KernelReplayTargetMismatch) + pure + (ReplayedKernelDerivation + closed + importUses + foundationUses + ruleUses + nodeCount + maximumDepth) + where + replay context hypotheses depth derivationNode + | depth > replayDepthLimit = + Left + (KernelReplayDepthLimitExceeded + replayDepthLimit) + | otherwise = do + step <- + replayWithin + context + hypotheses + depth + derivationNode + if stepNodeCount step > replayNodeLimit + then + Left + (KernelReplayNodeLimitExceeded + replayNodeLimit) + else + Right step + + replayWithin context hypotheses depth = \case + UseImportedFact index -> do + judgment <- + lookupImport index + statement <- + recheckStored + context + (embedClosedCore context + (derivationImportStatement + judgment)) + pure + (leaf + depth + statement + (Set.singleton index) + mempty) + UseLocalHypothesis index -> do + hypothesis <- + lookupHypothesis index hypotheses + checkedHypothesis <- + recheckStored context hypothesis + pure + (leaf + depth + checkedHypothesis + mempty + mempty) + UseFoundationFact tag -> do + statement <- + recheckStored + context + (embedClosedCore context + (mapFrozenGlobals + absurd + (foundationAxiomFrozen + checkedFoundationValue + tag))) + pure + (leaf + depth + statement + mempty + (Set.singleton tag)) + ImplicationElimination implication premise -> do + implicationStep <- + replay context hypotheses (depth + 1) implication + premiseStep <- + replay context hypotheses (depth + 1) premise + combine2 depth + (Semantics.implicationElimination + globalType + (stepValue implicationStep) + (stepValue premiseStep)) + implicationStep + premiseStep + ForallElimination quantified argument -> do + argument' <- + recheckStored context argument + quantifiedStep <- + replay context hypotheses (depth + 1) quantified + combine1 depth + (Semantics.forallElimination + globalType + (stepValue quantifiedStep) + argument') + quantifiedStep + FalsumElimination falsum target -> do + target' <- + recheckStored context target + falsumStep <- + replay context hypotheses (depth + 1) falsum + combine1 depth + (Semantics.falsumElimination + globalType + (stepValue falsumStep) + target') + falsumStep + ImplicationIntroduction premise body -> do + premise' <- + recheckStored context premise + bodyStep <- + replay + context + (premise' : hypotheses) + (depth + 1) + body + combine1 depth + (Semantics.implicationIntroduction + globalType + premise' + (stepValue bodyStep)) + bodyStep + ForallIntroduction binderType body -> do + weakenedHypotheses <- + traverse + (first KernelReplayWeakeningError + . weakenScopedCore + globalType + binderType) + hypotheses + bodyStep <- + replay + (binderType : context) + weakenedHypotheses + (depth + 1) + body + combine1 depth + (Semantics.forallIntroduction + globalType + binderType + (stepValue bodyStep)) + bodyStep + ConvertJudgment source target plan -> do + target' <- + recheckStored context target + sourceStep <- + replay + context + hypotheses + (depth + 1) + source + combine1 depth + (Semantics.convertJudgment + globalType + (conversionPlanBudget plan) + (stepValue sourceStep) + target') + sourceStep + EqualityReflexivity operand -> do + operand' <- + recheckStored context operand + value <- + first KernelReplaySemanticsError + (Semantics.equalityReflexivity + globalType + operand') + pure (leaf depth value mempty mempty) + EqualityCongruenceApplication + functionEquality + argumentEquality -> do + functionStep <- + replay + context + hypotheses + (depth + 1) + functionEquality + argumentStep <- + replay + context + hypotheses + (depth + 1) + argumentEquality + combine2 depth + (Semantics.equalityCongruenceApplication + globalType + (stepValue functionStep) + (stepValue argumentStep)) + functionStep + argumentStep + EqualityCongruenceLambda binderType bodyEquality -> do + weakenedHypotheses <- + traverse + (first KernelReplayWeakeningError + . weakenScopedCore + globalType + binderType) + hypotheses + bodyStep <- + replay + (binderType : context) + weakenedHypotheses + (depth + 1) + bodyEquality + combine1 depth + (Semantics.equalityCongruenceLambda + globalType + binderType + (stepValue bodyStep)) + bodyStep + EqualityModusPonens equality premise -> do + equalityStep <- + replay context hypotheses (depth + 1) equality + premiseStep <- + replay context hypotheses (depth + 1) premise + combine2 depth + (Semantics.equalityModusPonens + globalType + (stepValue equalityStep) + (stepValue premiseStep)) + equalityStep + premiseStep + ApplySetLfpBound domain operator -> do + domain' <- + recheckStored context domain + operator' <- + recheckStored context operator + value <- + first KernelReplaySetLfpRuleError + (SetLfp.setLfpBound + checkedFoundationValue + globalType + domain' + operator') + pure + (ruleLeaf + depth + SetLfpBound + value) + ApplySetLfpLeast + domain + operator + candidate + closedPremise + boundedPremise -> do + domain' <- + recheckStored context domain + operator' <- + recheckStored context operator + candidate' <- + recheckStored context candidate + closedStep <- + replay + context + hypotheses + (depth + 1) + closedPremise + boundedStep <- + replay + context + hypotheses + (depth + 1) + boundedPremise + combineRule depth SetLfpLeast + (SetLfp.setLfpLeast + checkedFoundationValue + globalType + domain' + operator' + candidate' + (stepValue closedStep) + (stepValue boundedStep)) + [closedStep, boundedStep] + ApplySetLfpFixed domain operator monotonePremise -> do + domain' <- + recheckStored context domain + operator' <- + recheckStored context operator + monotoneStep <- + replay + context + hypotheses + (depth + 1) + monotonePremise + combineRule depth SetLfpFixed + (SetLfp.setLfpFixed + checkedFoundationValue + globalType + domain' + operator' + (stepValue monotoneStep)) + [monotoneStep] + ApplySetLfpInduct + domain + operator + predicate + element + monotonePremise + memberPremise + closurePremise -> do + domain' <- + recheckStored context domain + operator' <- + recheckStored context operator + predicate' <- + recheckStored context predicate + element' <- + recheckStored context element + monotoneStep <- + replay + context + hypotheses + (depth + 1) + monotonePremise + memberStep <- + replay + context + hypotheses + (depth + 1) + memberPremise + closureStep <- + replay + context + hypotheses + (depth + 1) + closurePremise + combineRule depth SetLfpInduct + (SetLfp.setLfpInduct + checkedFoundationValue + globalType + domain' + operator' + predicate' + element' + (stepValue monotoneStep) + (stepValue memberStep) + (stepValue closureStep)) + [ monotoneStep + , memberStep + , closureStep + ] + + lookupImport index@(ImportIx naturalIndex) + | naturalIndex + > fromIntegral (maxBound :: Int) = + Left + (KernelReplayImportOutOfBounds + index) + | otherwise = + maybe + (Left + (KernelReplayImportOutOfBounds + index)) + Right + (imports + Vector.!? + (fromIntegral naturalIndex)) + + lookupHypothesis + index@(HypothesisIx naturalIndex) + hypotheses = + maybe + (Left + (KernelReplayHypothesisOutOfBounds + index)) + Right + (atNatural naturalIndex hypotheses) + + requireContext expected value + | scopedCoreContext value == expected = + Right () + | otherwise = + Left + (KernelReplayStoredContextMismatch + expected + (scopedCoreContext value)) + + recheckStored expectedContext stored = do + requireContext expectedContext stored + checked <- + first KernelReplayStoredTermIllTyped + (checkScopedCanonicalCore + globalType + expectedContext + (scopedCoreTerm stored)) + unless + (scopedCoreType checked + == scopedCoreType stored) + (Left + (KernelReplayStoredTypeMismatch + (scopedCoreType stored) + (scopedCoreType checked))) + pure checked + + recheckClosed stored = do + checked <- + first KernelReplayStoredTermIllTyped + (checkCanonicalCore + globalType + (frozenCoreTerm stored)) + unless + (frozenCoreType checked + == frozenCoreType stored) + (Left + (KernelReplayStoredTypeMismatch + (frozenCoreType stored) + (frozenCoreType checked))) + pure checked + + replayNodeLimit = + case limits of + KernelReplayLimits nodeLimit _depthLimit -> + nodeLimit + + replayDepthLimit = + case limits of + KernelReplayLimits _nodeLimit depthLimit -> + depthLimit + +leaf + :: Natural + -> ScopedCheckedCore global + -> Set ImportIx + -> Set FoundationAxiomTag + -> ReplayStep global +leaf depth value importUses foundationUses = + ReplayStep + value + importUses + foundationUses + mempty + 1 + depth + +ruleLeaf + :: Natural + -> KernelRuleTag + -> ScopedCheckedCore global + -> ReplayStep global +ruleLeaf depth tag value = + ReplayStep + value + mempty + mempty + (Set.singleton tag) + 1 + depth + +stepValue :: ReplayStep global -> ScopedCheckedCore global +stepValue + (ReplayStep + value + _importUses + _foundationUses + _ruleUses + _nodeCount + _maximumDepth) = + value + +combine1 + :: Natural + -> Either + Semantics.KernelSemanticsError + (ScopedCheckedCore global) + -> ReplayStep global + -> Either KernelReplayError (ReplayStep global) +combine1 depth synthesized child = do + value <- + first KernelReplaySemanticsError synthesized + pure + (ReplayStep + value + (stepImportUses child) + (stepFoundationUses child) + (stepRuleUses child) + (1 + stepNodeCount child) + (max depth + (stepMaximumDepth child))) + +combine2 + :: Natural + -> Either + Semantics.KernelSemanticsError + (ScopedCheckedCore global) + -> ReplayStep global + -> ReplayStep global + -> Either KernelReplayError (ReplayStep global) +combine2 depth synthesized left right = do + value <- + first KernelReplaySemanticsError synthesized + pure + (ReplayStep + value + (stepImportUses left + <> stepImportUses right) + (stepFoundationUses left + <> stepFoundationUses right) + (stepRuleUses left + <> stepRuleUses right) + (1 + + stepNodeCount left + + stepNodeCount right) + (maximum + [ depth + , stepMaximumDepth left + , stepMaximumDepth right + ])) + +combineRule + :: Natural + -> KernelRuleTag + -> Either + SetLfp.SetLfpRuleError + (ScopedCheckedCore global) + -> [ReplayStep global] + -> Either KernelReplayError (ReplayStep global) +combineRule depth tag synthesized children = do + value <- + first KernelReplaySetLfpRuleError synthesized + pure + (ReplayStep + value + (foldMap stepImportUses children) + (foldMap stepFoundationUses children) + (Set.insert tag + (foldMap stepRuleUses children)) + (1 + sum (stepNodeCount <$> children)) + (maximum + (depth + : (stepMaximumDepth <$> children)))) + +stepImportUses + :: ReplayStep global + -> Set ImportIx +stepImportUses + (ReplayStep + _value + importUses + _foundationUses + _ruleUses + _nodeCount + _maximumDepth) = + importUses + +stepFoundationUses + :: ReplayStep global + -> Set FoundationAxiomTag +stepFoundationUses + (ReplayStep + _value + _importUses + foundationUses + _ruleUses + _nodeCount + _maximumDepth) = + foundationUses + +stepRuleUses + :: ReplayStep global + -> Set KernelRuleTag +stepRuleUses + (ReplayStep + _value + _importUses + _foundationUses + ruleUses + _nodeCount + _maximumDepth) = + ruleUses + +stepNodeCount :: ReplayStep global -> Natural +stepNodeCount + (ReplayStep + _value + _importUses + _foundationUses + _ruleUses + nodeCount + _maximumDepth) = + nodeCount + +stepMaximumDepth :: ReplayStep global -> Natural +stepMaximumDepth + (ReplayStep + _value + _importUses + _foundationUses + _ruleUses + _nodeCount + maximumDepth) = + maximumDepth + +atNatural :: Natural -> [a] -> Maybe a +atNatural _index [] = + Nothing +atNatural 0 (value : _rest) = + Just value +atNatural index (_value : rest) = + atNatural (index - 1) rest 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) diff --git a/source/Felix/Checking/Kernel/Semantics.hs b/source/Felix/Checking/Kernel/Semantics.hs new file mode 100644 index 0000000..f9cfcfa --- /dev/null +++ b/source/Felix/Checking/Kernel/Semantics.hs @@ -0,0 +1,436 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Checked logical inference over scoped canonical HOL terms. +module Felix.Checking.Kernel.Semantics + ( implicationElimination + , implicationIntroduction + , forallElimination + , forallIntroduction + , falsumElimination + , equalityReflexivity + , equalityCongruenceApplication + , equalityCongruenceLambda + , equalityModusPonens + , convertJudgment + , KernelSemanticsError(..) + ) where + +import Base +import Felix.Checking.Core + +import Control.Monad (unless) +import Data.Bifunctor (first) +import Numeric.Natural (Natural) + + +data KernelSemanticsError + = KernelContextMismatch + ![CoreType] + ![CoreType] + | KernelBinderContextMismatch + !CoreType + ![CoreType] + | KernelExpectedProposition !CoreType + | KernelExpectedImplication + | KernelImplicationPremiseMismatch + | KernelExpectedForall + | KernelForallArgumentTypeMismatch + !CoreType + !CoreType + | KernelExpectedFalsum + | KernelExpectedEquality + | KernelEqualityOperandTypeMismatch + !CoreType + !CoreType + | KernelExpectedFunctionEquality !CoreType + | KernelEqualityPremiseMismatch + | KernelConversionBudgetExhausted + | KernelConversionMismatch + | KernelConclusionIllTyped !CoreCheckError + deriving stock (Show, Eq) + +implicationElimination + :: Eq global + => (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +implicationElimination globalType implication premise = do + requireSameContext implication premise + requireProposition implication + requireProposition premise + case scopedCoreTerm implication of + CImp expected conclusion + | scopedCoreTerm premise == expected -> + checkConclusion + globalType + (scopedCoreContext implication) + conclusion + | otherwise -> + Left KernelImplicationPremiseMismatch + _ -> + Left KernelExpectedImplication + +implicationIntroduction + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +implicationIntroduction globalType premise conclusion = do + requireSameContext premise conclusion + requireProposition premise + requireProposition conclusion + checkConclusion + globalType + (scopedCoreContext premise) + (CImp + (scopedCoreTerm premise) + (scopedCoreTerm conclusion)) + +forallElimination + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +forallElimination globalType quantified argument = do + requireSameContext quantified argument + requireProposition quantified + case scopedCoreTerm quantified of + CForall binderType body + | scopedCoreType argument == binderType -> + checkConclusion + globalType + (scopedCoreContext quantified) + (instantiateCanonical + (scopedCoreTerm argument) + body) + | otherwise -> + Left + (KernelForallArgumentTypeMismatch + binderType + (scopedCoreType argument)) + _ -> + Left KernelExpectedForall + +forallIntroduction + :: (global -> Maybe CoreType) + -> CoreType + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +forallIntroduction globalType binderType body = do + requireProposition body + outerContext <- + case scopedCoreContext body of + actualBinder : context + | actualBinder == binderType -> + Right context + | otherwise -> + Left + (KernelBinderContextMismatch + binderType + (scopedCoreContext body)) + [] -> + Left + (KernelBinderContextMismatch + binderType + []) + checkConclusion + globalType + outerContext + (CForall + binderType + (scopedCoreTerm body)) + +falsumElimination + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +falsumElimination _globalType falsum target = do + requireSameContext falsum target + requireProposition falsum + requireProposition target + case scopedCoreTerm falsum of + CFalsum -> + Right target + _ -> + Left KernelExpectedFalsum + +equalityReflexivity + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +equalityReflexivity globalType operand = + checkConclusion + globalType + (scopedCoreContext operand) + (CEq + (scopedCoreType operand) + (scopedCoreTerm operand) + (scopedCoreTerm operand)) + +equalityCongruenceApplication + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +equalityCongruenceApplication + globalType + functionEquality + argumentEquality = do + requireSameContext functionEquality argumentEquality + (functionType, leftFunction, rightFunction) <- + equalityOperands functionEquality + (argumentType, leftArgument, rightArgument) <- + equalityOperands argumentEquality + case functionType of + TyArrow expectedArgument resultType + | expectedArgument == argumentType -> + checkConclusion + globalType + (scopedCoreContext functionEquality) + (CEq + resultType + (CApp leftFunction leftArgument) + (CApp rightFunction rightArgument)) + | otherwise -> + Left + (KernelEqualityOperandTypeMismatch + expectedArgument + argumentType) + other -> + Left (KernelExpectedFunctionEquality other) + +equalityCongruenceLambda + :: (global -> Maybe CoreType) + -> CoreType + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +equalityCongruenceLambda + globalType + binderType + bodyEquality = do + (bodyType, leftBody, rightBody) <- + equalityOperands bodyEquality + outerContext <- + case scopedCoreContext bodyEquality of + actualBinder : context + | actualBinder == binderType -> + Right context + | otherwise -> + Left + (KernelBinderContextMismatch + binderType + (scopedCoreContext bodyEquality)) + [] -> + Left + (KernelBinderContextMismatch + binderType + []) + checkConclusion + globalType + outerContext + (CEq + (TyArrow binderType bodyType) + (CLam binderType leftBody) + (CLam binderType rightBody)) + +equalityModusPonens + :: Eq global + => (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +equalityModusPonens globalType propositionEquality premise = do + requireSameContext propositionEquality premise + requireProposition premise + (operandType, left, right) <- + equalityOperands propositionEquality + unless + (operandType == TyProp) + (Left + (KernelEqualityOperandTypeMismatch + TyProp + operandType)) + unless + (left == scopedCoreTerm premise) + (Left KernelEqualityPremiseMismatch) + checkConclusion + globalType + (scopedCoreContext premise) + right + +-- | Recheck a displayed proposition and independently establish beta +-- conversion within the supplied contraction budget. +convertJudgment + :: Eq global + => (global -> Maybe CoreType) + -> Natural + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +convertJudgment globalType budget source target = do + requireSameContext source target + requireProposition source + requireProposition target + sourceNormal <- + normalizeCanonical budget + (scopedCoreTerm source) + targetNormal <- + normalizeCanonical budget + (scopedCoreTerm target) + unless + (sourceNormal == targetNormal) + (Left KernelConversionMismatch) + checkConclusion + globalType + (scopedCoreContext target) + (scopedCoreTerm target) + +requireSameContext + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either KernelSemanticsError () +requireSameContext left right + | scopedCoreContext left + == scopedCoreContext right = + Right () + | otherwise = + Left + (KernelContextMismatch + (scopedCoreContext left) + (scopedCoreContext right)) + +requireProposition + :: ScopedCheckedCore global + -> Either KernelSemanticsError () +requireProposition value + | scopedCoreType value == TyProp = + Right () + | otherwise = + Left + (KernelExpectedProposition + (scopedCoreType value)) + +equalityOperands + :: ScopedCheckedCore global + -> Either + KernelSemanticsError + (CoreType, CanonicalTerm global, CanonicalTerm global) +equalityOperands equality = do + requireProposition equality + case scopedCoreTerm equality of + CEq operandType left right -> + Right (operandType, left, right) + _ -> + Left KernelExpectedEquality + +checkConclusion + :: (global -> Maybe CoreType) + -> [CoreType] + -> CanonicalTerm global + -> Either + KernelSemanticsError + (ScopedCheckedCore global) +checkConclusion globalType context = + first KernelConclusionIllTyped + . checkScopedCanonicalCore globalType context + +normalizeCanonical + :: Natural + -> CanonicalTerm global + -> Either + KernelSemanticsError + (CanonicalTerm global) +normalizeCanonical budget term = + fst <$> normalize budget term + where + normalize remaining = \case + CBound index -> + pure (CBound index, remaining) + CGlobal global -> + pure (CGlobal global, remaining) + CIntrinsic intrinsic -> + pure (CIntrinsic intrinsic, remaining) + COpaqueInteger integer -> + pure (COpaqueInteger integer, remaining) + CApp function argument -> do + (functionNormal, afterFunction) <- + normalize remaining function + case functionNormal of + CLam _binderType body -> do + afterContraction <- + consumeReduction afterFunction + normalize + afterContraction + (instantiateCanonical + argument + body) + _ -> do + (argumentNormal, afterArgument) <- + normalize afterFunction argument + pure + ( CApp + functionNormal + argumentNormal + , afterArgument + ) + CLam binderType body -> do + (bodyNormal, remaining') <- + normalize remaining body + pure + (CLam binderType bodyNormal, remaining') + CFalsum -> + pure (CFalsum, remaining) + CImp premise conclusion -> do + (premiseNormal, afterPremise) <- + normalize remaining premise + (conclusionNormal, afterConclusion) <- + normalize afterPremise conclusion + pure + ( CImp premiseNormal conclusionNormal + , afterConclusion + ) + CEq operandType left right -> do + (leftNormal, afterLeft) <- + normalize remaining left + (rightNormal, afterRight) <- + normalize afterLeft right + pure + ( CEq + operandType + leftNormal + rightNormal + , afterRight + ) + CForall binderType body -> do + (bodyNormal, remaining') <- + normalize remaining body + pure + (CForall binderType bodyNormal, remaining') + + consumeReduction 0 = + Left KernelConversionBudgetExhausted + consumeReduction remaining = + Right (remaining - 1) diff --git a/source/Felix/Checking/Kernel/SetLfp.hs b/source/Felix/Checking/Kernel/SetLfp.hs new file mode 100644 index 0000000..19f6714 --- /dev/null +++ b/source/Felix/Checking/Kernel/SetLfp.hs @@ -0,0 +1,762 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | The four checked rules for the bounded set-valued least fixed point. +module Felix.Checking.Kernel.SetLfp + ( setLfpBound + , setLfpLeast + , setLfpFixed + , setLfpInduct + , setLfpTerm + , memberProposition + , subsetProposition + , boundedMonoProposition + , inductionClosureProposition + , SetLfpRuleError(..) + ) where + +import Base +import Felix.Checking.Core +import Felix.Checking.Foundation + +import Data.Bifunctor (first) +import Numeric.Natural (Natural) + + +data SetLfpRuleError + = SetLfpRuleSignatureMismatch + !KernelRuleTag + !KernelRuleSignature + !KernelRuleSignature + | SetLfpRuleContextMismatch + !KernelRuleTag + ![CoreType] + ![CoreType] + | SetLfpRuleArgumentTypeMismatch + !KernelRuleTag + !Natural + !CoreType + !CoreType + | SetLfpRulePremiseIsNotProposition + !KernelRuleTag + !Natural + !CoreType + | SetLfpRulePremiseMismatch + !KernelRuleTag + !Natural + | SetLfpRuleConstructionIllTyped + !KernelRuleTag + !CoreCheckError + deriving stock (Show, Eq) + +setLfpBound + :: CheckedFoundation + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +setLfpBound foundation globalType domain operator = do + validateApplication + foundation + SetLfpBound + [domain, operator] + [] + fixedPoint <- + setLfpTermFor + SetLfpBound + globalType + domain + operator + subsetFor + SetLfpBound + globalType + fixedPoint + domain + +setLfpLeast + :: Eq global + => CheckedFoundation + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +setLfpLeast + foundation + globalType + domain + operator + candidate + closedPremise + boundedPremise = do + validateApplication + foundation + SetLfpLeast + [domain, operator, candidate] + [closedPremise, boundedPremise] + operatorCandidate <- + applyFor + SetLfpLeast + globalType + operator + candidate + expectedClosed <- + subsetFor + SetLfpLeast + globalType + operatorCandidate + candidate + expectedBounded <- + subsetFor + SetLfpLeast + globalType + candidate + domain + requirePremise + SetLfpLeast + 0 + expectedClosed + closedPremise + requirePremise + SetLfpLeast + 1 + expectedBounded + boundedPremise + fixedPoint <- + setLfpTermFor + SetLfpLeast + globalType + domain + operator + subsetFor + SetLfpLeast + globalType + fixedPoint + candidate + +setLfpFixed + :: Eq global + => CheckedFoundation + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +setLfpFixed + foundation + globalType + domain + operator + monotonePremise = do + validateApplication + foundation + SetLfpFixed + [domain, operator] + [monotonePremise] + expectedMonotone <- + boundedMonoFor + SetLfpFixed + globalType + domain + operator + requirePremise + SetLfpFixed + 0 + expectedMonotone + monotonePremise + fixedPoint <- + setLfpTermFor + SetLfpFixed + globalType + domain + operator + unfolded <- + applyFor + SetLfpFixed + globalType + operator + fixedPoint + checkedFor + SetLfpFixed + globalType + (scopedCoreContext domain) + (CEq + TySet + (scopedCoreTerm fixedPoint) + (scopedCoreTerm unfolded)) + +setLfpInduct + :: Eq global + => CheckedFoundation + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +setLfpInduct + foundation + globalType + domain + operator + predicate + element + monotonePremise + memberPremise + closurePremise = do + validateApplication + foundation + SetLfpInduct + [domain, operator, predicate, element] + [monotonePremise, memberPremise, closurePremise] + expectedMonotone <- + boundedMonoFor + SetLfpInduct + globalType + domain + operator + requirePremise + SetLfpInduct + 0 + expectedMonotone + monotonePremise + fixedPoint <- + setLfpTermFor + SetLfpInduct + globalType + domain + operator + expectedMember <- + memberFor + SetLfpInduct + globalType + element + fixedPoint + requirePremise + SetLfpInduct + 1 + expectedMember + memberPremise + expectedClosure <- + inductionClosureFor + SetLfpInduct + globalType + fixedPoint + operator + predicate + requirePremise + SetLfpInduct + 2 + expectedClosure + closurePremise + applyFor + SetLfpInduct + globalType + predicate + element + +setLfpTerm + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +setLfpTerm = + setLfpTermFor SetLfpBound + +memberProposition + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +memberProposition = + memberFor SetLfpInduct + +subsetProposition + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +subsetProposition = + subsetFor SetLfpBound + +boundedMonoProposition + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +boundedMonoProposition = + boundedMonoFor SetLfpFixed + +inductionClosureProposition + :: (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +inductionClosureProposition globalType domain operator predicate = do + fixedPoint <- + setLfpTermFor + SetLfpInduct + globalType + domain + operator + inductionClosureFor + SetLfpInduct + globalType + fixedPoint + operator + predicate + +validateApplication + :: CheckedFoundation + -> KernelRuleTag + -> [ScopedCheckedCore global] + -> [ScopedCheckedCore global] + -> Either SetLfpRuleError () +validateApplication foundation tag arguments premises = do + let expected = + expectedSignature tag + actual = + foundationRuleSignature foundation tag + if actual == expected + then pure () + else + Left + (SetLfpRuleSignatureMismatch + tag + expected + actual) + case arguments of + [] -> + pure () + firstArgument : remainingArguments -> do + traverse_ + (requireContext tag firstArgument) + remainingArguments + traverse_ + (requireContext tag firstArgument) + premises + traverse_ + (uncurry + (requireArgumentType tag)) + (zip [0 ..] arguments) + traverse_ + (uncurry + (requireProposition tag)) + (zip [0 ..] premises) + +expectedSignature :: KernelRuleTag -> KernelRuleSignature +expectedSignature = \case + SetLfpBound -> + KernelRuleSignature + [TySet, TySet `TyArrow` TySet] + 0 + SetLfpLeast -> + KernelRuleSignature + [TySet, TySet `TyArrow` TySet, TySet] + 2 + SetLfpFixed -> + KernelRuleSignature + [TySet, TySet `TyArrow` TySet] + 1 + SetLfpInduct -> + KernelRuleSignature + [ TySet + , TySet `TyArrow` TySet + , TySet `TyArrow` TyProp + , TySet + ] + 3 + +expectedArgumentTypes + :: KernelRuleTag + -> [CoreType] +expectedArgumentTypes tag = + case expectedSignature tag of + KernelRuleSignature argumentTypes _premiseCount -> + argumentTypes + +requireContext + :: KernelRuleTag + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either SetLfpRuleError () +requireContext tag expected actual + | scopedCoreContext expected + == scopedCoreContext actual = + Right () + | otherwise = + Left + (SetLfpRuleContextMismatch + tag + (scopedCoreContext expected) + (scopedCoreContext actual)) + +requireArgumentType + :: KernelRuleTag + -> Natural + -> ScopedCheckedCore global + -> Either SetLfpRuleError () +requireArgumentType tag index argument = + case atNatural index (expectedArgumentTypes tag) of + Nothing -> + impossible + "fixed-point rule argument inventory is inconsistent" + Just expected + | scopedCoreType argument == expected -> + Right () + | otherwise -> + Left + (SetLfpRuleArgumentTypeMismatch + tag + index + expected + (scopedCoreType argument)) + +requireProposition + :: KernelRuleTag + -> Natural + -> ScopedCheckedCore global + -> Either SetLfpRuleError () +requireProposition tag index premise + | scopedCoreType premise == TyProp = + Right () + | otherwise = + Left + (SetLfpRulePremiseIsNotProposition + tag + index + (scopedCoreType premise)) + +requirePremise + :: Eq global + => KernelRuleTag + -> Natural + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either SetLfpRuleError () +requirePremise tag index expected actual + | expected == actual = + Right () + | otherwise = + Left + (SetLfpRulePremiseMismatch + tag + index) + +setLfpTermFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +setLfpTermFor tag globalType domain operator = + checkedFor tag globalType + (scopedCoreContext domain) + (CApp + (CApp + (CIntrinsic ISetLfp) + (scopedCoreTerm domain)) + (scopedCoreTerm operator)) + +applyFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +applyFor tag globalType function argument = do + requireContext tag function argument + checkedFor tag globalType + (scopedCoreContext function) + (CApp + (scopedCoreTerm function) + (scopedCoreTerm argument)) + +memberFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +memberFor tag globalType element set = do + requireContext tag element set + checkedFor tag globalType + (scopedCoreContext element) + (CApp + (CApp + (CIntrinsic Member) + (scopedCoreTerm element)) + (scopedCoreTerm set)) + +subsetFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +subsetFor tag globalType left right = do + requireContext tag left right + left' <- weakenFor tag globalType TySet left + right' <- weakenFor tag globalType TySet right + element <- + checkedFor tag globalType + (TySet : scopedCoreContext left) + (CBound 0) + inLeft <- + memberFor tag globalType element left' + inRight <- + memberFor tag globalType element right' + checkedFor tag globalType + (scopedCoreContext left) + (CForall + TySet + (CImp + (scopedCoreTerm inLeft) + (scopedCoreTerm inRight))) + +boundedMonoFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +boundedMonoFor tag globalType domain operator = do + requireContext tag domain operator + operatorDomain <- + applyFor tag globalType operator domain + bounded <- + subsetFor tag globalType operatorDomain domain + + domainX <- + weakenFor tag globalType TySet domain + operatorX <- + weakenFor tag globalType TySet operator + domainXY <- + weakenFor tag globalType TySet domainX + operatorXY <- + weakenFor tag globalType TySet operatorX + let xyContext = + TySet : TySet : scopedCoreContext domain + x <- + checkedFor tag globalType + xyContext + (CBound 1) + y <- + checkedFor tag globalType + xyContext + (CBound 0) + xSubsetY <- + subsetFor tag globalType x y + ySubsetDomain <- + subsetFor tag globalType y domainXY + antecedent <- + conjunctionFor + tag + globalType + xSubsetY + ySubsetDomain + operatorXValue <- + applyFor tag globalType operatorXY x + operatorYValue <- + applyFor tag globalType operatorXY y + imageSubset <- + subsetFor + tag + globalType + operatorXValue + operatorYValue + monotoneBody <- + implicationFor + tag + globalType + antecedent + imageSubset + quantifiedY <- + closeForallFor tag globalType TySet monotoneBody + quantifiedXY <- + closeForallFor tag globalType TySet quantifiedY + conjunctionFor + tag + globalType + bounded + quantifiedXY + +inductionClosureFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +inductionClosureFor + tag + globalType + fixedPoint + operator + predicate = do + fixedPoint' <- + weakenFor tag globalType TySet fixedPoint + operator' <- + weakenFor tag globalType TySet operator + predicate' <- + weakenFor tag globalType TySet predicate + element <- + checkedFor tag globalType + (TySet : scopedCoreContext fixedPoint) + (CBound 0) + separated <- + checkedFor tag globalType + (scopedCoreContext fixedPoint') + (CApp + (CApp + (CIntrinsic Sep) + (scopedCoreTerm fixedPoint')) + (scopedCoreTerm predicate')) + unfolded <- + applyFor tag globalType operator' separated + memberUnfolded <- + memberFor tag globalType element unfolded + predicateElement <- + applyFor tag globalType predicate' element + body <- + implicationFor + tag + globalType + memberUnfolded + predicateElement + closeForallFor tag globalType TySet body + +conjunctionFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +conjunctionFor tag globalType left right = do + requireContext tag left right + checkedFor tag globalType + (scopedCoreContext left) + (CImp + (CImp + (scopedCoreTerm left) + (CImp + (scopedCoreTerm right) + CFalsum)) + CFalsum) + +implicationFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +implicationFor tag globalType premise conclusion = do + requireContext tag premise conclusion + checkedFor tag globalType + (scopedCoreContext premise) + (CImp + (scopedCoreTerm premise) + (scopedCoreTerm conclusion)) + +closeForallFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> CoreType + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +closeForallFor tag globalType binderType body = + case scopedCoreContext body of + actualBinder : outerContext + | actualBinder == binderType -> + checkedFor tag globalType + outerContext + (CForall + binderType + (scopedCoreTerm body)) + _ -> + Left + (SetLfpRuleContextMismatch + tag + (binderType : drop 1 + (scopedCoreContext body)) + (scopedCoreContext body)) + +weakenFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> CoreType + -> ScopedCheckedCore global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +weakenFor tag globalType binderType = + first + (SetLfpRuleConstructionIllTyped tag) + . weakenScopedCore + globalType + binderType + +checkedFor + :: KernelRuleTag + -> (global -> Maybe CoreType) + -> [CoreType] + -> CanonicalTerm global + -> Either + SetLfpRuleError + (ScopedCheckedCore global) +checkedFor tag globalType context = + first + (SetLfpRuleConstructionIllTyped tag) + . checkScopedCanonicalCore + globalType + context + +atNatural :: Natural -> [a] -> Maybe a +atNatural _index [] = + Nothing +atNatural 0 (value : _rest) = + Just value +atNatural index (_value : rest) = + atNatural (index - 1) rest |