summaryrefslogtreecommitdiff
path: root/source/Felix/Checking/Kernel
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2026-08-06 17:54:00 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2026-08-06 17:54:00 +0200
commit82328890108bae64b372b8d58620ebc62699de76 (patch)
tree575404c6b425c19259c0ded296f1c8ffb7ff0e2b /source/Felix/Checking/Kernel
parent1a25421c2a168d420581358c8733fcd8f36f379b (diff)
Migrate to `Felix` namespaceHEADhotg
Diffstat (limited to 'source/Felix/Checking/Kernel')
-rw-r--r--source/Felix/Checking/Kernel/Derivation.hs1264
-rw-r--r--source/Felix/Checking/Kernel/Proof.hs1443
-rw-r--r--source/Felix/Checking/Kernel/Semantics.hs436
-rw-r--r--source/Felix/Checking/Kernel/SetLfp.hs762
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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 21:05:24 +0000