diff options
Diffstat (limited to 'source/Checking/Typed/Inductive.hs')
| -rw-r--r-- | source/Checking/Typed/Inductive.hs | 4018 |
1 files changed, 0 insertions, 4018 deletions
diff --git a/source/Checking/Typed/Inductive.hs b/source/Checking/Typed/Inductive.hs deleted file mode 100644 index 7a895c6..0000000 --- a/source/Checking/Typed/Inductive.hs +++ /dev/null @@ -1,4018 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Direct checked lowering of the current one-carrier set-valued inductive --- declaration. -module Checking.Typed.Inductive - ( DirectInductive(..) - , DirectInductiveClause(..) - , DirectInductiveCondition(..) - , SourceGlobal(..) - , PreparedTypedInductive - , typedInductiveCarrierType - , typedInductiveCarrierBody - , typedInductiveGuardTargets - , PreparedTypedInductiveFact - , typedInductiveFacts - , typedInductiveFactMarker - , typedInductiveFactTarget - , typedInductiveFactRules - , typedInductiveFactDerivation - , prepareTypedClosedTerm - , prepareTypedClosedFormula - , prepareTypedInductive - , TypedInductiveError(..) - ) where - -import Base hiding (Empty) -import Checking.Core -import Checking.Exact.Vocabulary -import Checking.Foundation -import Checking.Kernel.Derivation -import Checking.Kernel.Proof -import Syntax.Internal - -import Control.Monad ((<=<), foldM) -import Data.Bifunctor (first) -import Data.List qualified as List -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import Numeric.Natural (Natural) -import Bound.Scope (fromScope, instantiate) -import Bound.Var (Var(..)) - - -data DirectInductive = DirectInductive - { directInductiveParams :: ![VarSymbol] - , directInductiveDomain :: !Term - , directInductiveClauses - :: !(NonEmpty DirectInductiveClause) - } - -data DirectInductiveClause = DirectInductiveClause - { directClauseVariables :: ![VarSymbol] - , directClauseConditions - :: ![DirectInductiveCondition] - , directClauseResult :: !Term - } - -data DirectInductiveCondition - = DirectSideCondition !Formula - | DirectRecursiveCondition !Term - -data SourceGlobal global = SourceGlobal - !global - !(Maybe (FrozenCheckedCore global)) - -data InductiveGlobal global where - InductiveGlobal - :: Eq global - => !global - -> !CoreType - -> InductiveGlobal global - -instance Eq (InductiveGlobal global) where - InductiveGlobal left _leftType - == InductiveGlobal right _rightType = - left == right - -inductiveGlobalIdentity :: InductiveGlobal global -> global -inductiveGlobalIdentity (InductiveGlobal identity _coreType) = - identity - -inductiveGlobalType :: InductiveGlobal global -> CoreType -inductiveGlobalType (InductiveGlobal _identity coreType) = - coreType - -data PreparedTypedInductive global = PreparedTypedInductive - !CoreType - !(FrozenCheckedCore global) - !(Vector (FrozenCheckedCore global)) - !(NonEmpty (PreparedTypedInductiveFact global)) - -data PreparedInductiveGuard global - = PreparedFoundationGuard !FoundationAxiomTag - | PreparedImportedGuard - !ImportIx - !(FrozenCheckedCore global) - -typedInductiveCarrierType - :: PreparedTypedInductive global - -> CoreType -typedInductiveCarrierType - (PreparedTypedInductive - carrierType - _body - _guards - _facts) = - carrierType - -typedInductiveCarrierBody - :: PreparedTypedInductive global - -> FrozenCheckedCore global -typedInductiveCarrierBody - (PreparedTypedInductive - _carrierType - body - _guards - _facts) = - body - -typedInductiveGuardTargets - :: PreparedTypedInductive global - -> Vector (FrozenCheckedCore global) -typedInductiveGuardTargets - (PreparedTypedInductive - _carrierType - _body - guards - _facts) = - guards - -newtype PreparedTypedInductiveFact global = - PreparedTypedInductiveFact - ( Marker - , FrozenCheckedCore global - , NonEmpty KernelRuleTag - , KernelDerivation global - ) - -typedInductiveFacts - :: PreparedTypedInductive global - -> NonEmpty (PreparedTypedInductiveFact global) -typedInductiveFacts - (PreparedTypedInductive - _carrierType - _body - _guards - facts) = - facts - -typedInductiveFactMarker - :: PreparedTypedInductiveFact global - -> Marker -typedInductiveFactMarker - (PreparedTypedInductiveFact - (marker, _target, _rule, _derivation)) = - marker - -typedInductiveFactTarget - :: PreparedTypedInductiveFact global - -> FrozenCheckedCore global -typedInductiveFactTarget - (PreparedTypedInductiveFact - (_marker, target, _rule, _derivation)) = - target - -typedInductiveFactRules - :: PreparedTypedInductiveFact global - -> NonEmpty KernelRuleTag -typedInductiveFactRules - (PreparedTypedInductiveFact - (_marker, _target, rules, _derivation)) = - rules - -typedInductiveFactDerivation - :: PreparedTypedInductiveFact global - -> KernelDerivation global -typedInductiveFactDerivation - (PreparedTypedInductiveFact - (_marker, _target, _rule, derivation)) = - derivation - --- | Lower one closed source formula through the exact primitive/global --- policy used by the direct-inductive compiler. -prepareTypedClosedFormula - :: Eq global - => (global -> CoreType) - -> (Symbol -> Maybe (SourceGlobal global)) - -> Formula - -> Either TypedInductiveError (FrozenCheckedCore global) -prepareTypedClosedFormula globalType resolveGlobal formula = do - term <- - lowerFormulaWith - True - (fmap (mapSourceGlobal wrapGlobal) . resolveGlobal) - emptyEnvironment - formula - checked <- - first TypedInductiveCoreError - (checkCanonicalCore - (Just . inductiveGlobalType) - term) - pure (mapFrozenGlobals inductiveGlobalIdentity checked) - where - wrapGlobal identity = - InductiveGlobal identity (globalType identity) - -prepareTypedClosedTerm - :: Eq global - => (global -> CoreType) - -> (Symbol -> Maybe (SourceGlobal global)) - -> Term - -> Either TypedInductiveError (FrozenCheckedCore global) -prepareTypedClosedTerm globalType resolveGlobal term = do - canonical <- - lowerTerm - (fmap (mapSourceGlobal wrapGlobal) . resolveGlobal) - emptyEnvironment - term - checked <- - first TypedInductiveCoreError - (checkCanonicalCore - (Just . inductiveGlobalType) - canonical) - pure (mapFrozenGlobals inductiveGlobalIdentity checked) - where - wrapGlobal identity = - InductiveGlobal identity (globalType identity) - -data TypedInductiveError - = TypedInductiveDuplicateBinder !VarSymbol - | TypedInductiveUnknownLocal !VarSymbol - | TypedInductiveUnsupportedExpression !Text - | TypedInductiveCoreError !CoreCheckError - | TypedInductiveProofError !KernelProofBuildError - | TypedInductiveProofRemainedOpen - | TypedInductiveFactPreparationFailed - !Marker - !TypedInductiveError - | TypedInductivePreparationContext - !Text - !TypedInductiveError - deriving stock (Show, Eq) - -data InductiveEnvironment = InductiveEnvironment - !(Map VarSymbol Natural) - -emptyEnvironment :: InductiveEnvironment -emptyEnvironment = - InductiveEnvironment Map.empty - -extendEnvironment - :: VarSymbol - -> InductiveEnvironment - -> Either - TypedInductiveError - InductiveEnvironment -extendEnvironment variable - (InductiveEnvironment variables) - | Map.member variable variables = - Left - (TypedInductiveDuplicateBinder - variable) - | otherwise = - Right - (InductiveEnvironment - (Map.insert variable 0 - (succ <$> variables))) - -lookupEnvironment - :: VarSymbol - -> InductiveEnvironment - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -lookupEnvironment variable - (InductiveEnvironment variables) = - maybe - (Left - (TypedInductiveUnknownLocal - variable)) - (Right . CBound) - (Map.lookup variable variables) - -prepareTypedInductive - :: Eq global - => (global -> CoreType) - -> CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal global)) - -> Marker - -> DirectInductive - -> Either - TypedInductiveError - (PreparedTypedInductive global) -prepareTypedInductive - globalType - foundation - resolveGlobal - marker - inductive = - mapPreparedTypedInductive inductiveGlobalIdentity - <$> prepareTypedInductiveInternal - foundation - (fmap (mapSourceGlobal wrapGlobal) . resolveGlobal) - marker - inductive - where - wrapGlobal identity = - InductiveGlobal identity (globalType identity) - -prepareTypedInductiveInternal - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> Marker - -> DirectInductive - -> Either - TypedInductiveError - (PreparedTypedInductive (InductiveGlobal global)) -prepareTypedInductiveInternal - foundation - resolveGlobal - marker - inductive = do - carrierBody <- - prepareCarrierBody - resolveGlobal - inductive - guards <- - traverse - (prepareGuardTarget - resolveGlobal - inductive) - (directInductiveClauses - inductive) - let preparedGuards = - assignGuardSources foundation - (NonEmpty.toList guards) - facts <- - prepareFacts - foundation - resolveGlobal - marker - inductive - (case preparedGuards of - firstGuard : remainingGuards -> - firstGuard :| remainingGuards - [] -> - impossible - "a nonempty inductive declaration produced no guards") - pure - (PreparedTypedInductive - carrierType - carrierBody - (Vector.fromList - [ target - | PreparedImportedGuard - _index target <- preparedGuards - ]) - facts) - where - carrierType = - foldr - TyArrow - TySet - (TySet - <$ directInductiveParams - inductive) - -mapSourceGlobal - :: (left -> right) - -> SourceGlobal left - -> SourceGlobal right -mapSourceGlobal transform (SourceGlobal identity body) = - SourceGlobal - (transform identity) - (mapFrozenGlobals transform <$> body) - -mapPreparedTypedInductive - :: (left -> right) - -> PreparedTypedInductive left - -> PreparedTypedInductive right -mapPreparedTypedInductive transform - (PreparedTypedInductive carrierType body guards facts) = - PreparedTypedInductive - carrierType - (mapFrozenGlobals transform body) - (mapFrozenGlobals transform <$> guards) - (mapPreparedFact transform <$> facts) - where - mapPreparedFact mapGlobal - (PreparedTypedInductiveFact - (marker, target, rule, derivation)) = - PreparedTypedInductiveFact - ( marker - , mapFrozenGlobals mapGlobal target - , rule - , mapKernelDerivationGlobals mapGlobal derivation - ) - -prepareCarrierBody - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> Either - TypedInductiveError - (FrozenCheckedCore (InductiveGlobal global)) -prepareCarrierBody resolveGlobal inductive = do - body <- - buildUnderVariables - emptyEnvironment - (directInductiveParams - inductive) - (\env -> fixedPointTerm - resolveGlobal - inductive - env) - let closed = - closeLambdas - (length - (directInductiveParams - inductive)) - body - checked <- - first TypedInductiveCoreError - (checkCanonicalCore - (Just . inductiveGlobalType) - closed) - pure checked - -prepareGuardTarget - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> DirectInductiveClause - -> Either - TypedInductiveError - (FrozenCheckedCore (InductiveGlobal global)) -prepareGuardTarget - resolveGlobal - inductive - clause = do - target <- - buildUnderVariables - emptyEnvironment - (directInductiveParams inductive - <> directClauseVariables clause) - (\environment -> do - domain <- - lowerTerm - resolveGlobal - environment - (directInductiveDomain - inductive) - conditions <- - traverse - (conditionTerm - resolveGlobal - environment - domain) - (directClauseConditions - clause) - result <- - lowerTerm - resolveGlobal - environment - (directClauseResult - clause) - pure - (impliesIfNeeded - (conjunctionList - conditions) - (memberTerm - result - domain))) - freezeClosedTarget - (closeForalls - (length - (directInductiveParams inductive - <> directClauseVariables clause)) - target) - -assignGuardSources - :: CheckedFoundation - -> [FrozenCheckedCore (InductiveGlobal global)] - -> [PreparedInductiveGuard (InductiveGlobal global)] -assignGuardSources foundation = - snd . List.mapAccumL assign 0 - where - assign nextImport target = - case matchingFoundationAxiom target of - Just tag -> - (nextImport, PreparedFoundationGuard tag) - Nothing -> - ( nextImport + 1 - , PreparedImportedGuard - (importIx nextImport) - target - ) - - matchingFoundationAxiom target = - List.find - (\tag -> - mapFrozenGlobals - absurd - (foundationAxiomFrozen - foundation - tag) - == target) - [minBound .. maxBound] - -prepareFacts - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> Marker - -> DirectInductive - -> NonEmpty (PreparedInductiveGuard (InductiveGlobal global)) - -> Either - TypedInductiveError - (NonEmpty (PreparedTypedInductiveFact (InductiveGlobal global))) -prepareFacts - foundation - resolveGlobal - marker - inductive - guards = do - introductions <- - sequence - (NonEmpty.zipWith - (\clauseIndex pair -> - first - (TypedInductiveFactPreparationFailed - (introMarker - marker - (clauseIndex + 1))) - (prepareIntroductionFact - foundation - resolveGlobal - marker - inductive - clauseIndex - pair)) - (0 :| [1 ..]) - (NonEmpty.zip - guards - (directInductiveClauses - inductive))) - domainSubset <- - first - (TypedInductiveFactPreparationFailed - (derivedMarker marker "dom_subset")) - (prepareDomainSubsetFact - foundation - resolveGlobal - marker - inductive) - cases <- - first - (TypedInductiveFactPreparationFailed - (derivedMarker marker "cases")) - (prepareCasesFact - foundation - resolveGlobal - marker - inductive) - induction <- - first - (TypedInductiveFactPreparationFailed - (derivedMarker marker "induct")) - (prepareInductionFact - foundation - resolveGlobal - marker - inductive) - pure - (introductions - <> (domainSubset - :| [cases, induction])) - -prepareIntroductionFact - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> Marker - -> DirectInductive - -> Natural - -> (PreparedInductiveGuard (InductiveGlobal global), DirectInductiveClause) - -> Either - TypedInductiveError - (PreparedTypedInductiveFact (InductiveGlobal global)) -prepareIntroductionFact - foundation - resolveGlobal - marker - inductive - clauseIndex - (guardSource, clause) = do - proof <- - proveUnderVariables - (rootProofContext - foundation - (Just . inductiveGlobalType)) - emptyEnvironment - (directInductiveParams inductive - <> directClauseVariables clause) - (\context environment -> do - domain <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - (directInductiveDomain - inductive) - operator <- - checkedTerm context - =<< operatorTerm - resolveGlobal - inductive - environment - fixedPoint <- - checkedTerm context - =<< fixedPointTerm - resolveGlobal - inductive - environment - predicate <- - checkedTerm context - =<< operatorPredicateAt - resolveGlobal - inductive - environment - (scopedCoreTerm - fixedPoint) - appliedOperatorSet <- - checkedTerm context - (CApp - (scopedCoreTerm operator) - (scopedCoreTerm - fixedPoint)) - conditions <- - traverse - (checkedTerm context <=< - conditionTerm - resolveGlobal - environment - (scopedCoreTerm - fixedPoint)) - (directClauseConditions - clause) - result <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - (directClauseResult - clause) - let conditionTerms = - scopedCoreTerm <$> conditions - first - (TypedInductivePreparationContext - "introduction premises") - (provePremises - context - conditionTerms - (\premiseProofs -> do - guardProof <- - preparedGuardProof - context - guardSource - specializedGuard <- - first - (TypedInductivePreparationContext - "introduction guard specialization") - (eliminateWrittenForalls - context - environment - (directInductiveParams - inductive - <> directClauseVariables - clause) - guardProof) - guardPremiseProofs <- - sequence - [ case condition of - DirectSideCondition _formula -> - pure premiseProof - DirectRecursiveCondition - recursiveTerm -> do - bound <- - first - TypedInductiveProofError - (setLfpBoundProof - context - domain - operator) - recursiveElement <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - recursiveTerm - implication <- - first - TypedInductiveProofError - (forallEliminationProof - context - bound - recursiveElement) - first - TypedInductiveProofError - (implicationEliminationProof - context - implication - premiseProof) - | (condition, premiseProof) <- - zip - (directClauseConditions - clause) - premiseProofs - ] - inDomain <- - case conjunctionList - conditionTerms of - Nothing -> - pure specializedGuard - Just _condition -> do - conjunction <- - conjunctionIntroductionList - context - guardPremiseProofs - first - (TypedInductivePreparationContext - "introduction guard application") - (first TypedInductiveProofError - (implicationEliminationProof - context - specializedGuard - conjunction)) - equality <- - first TypedInductiveProofError - (equalityReflexivityProof - context - result) - clauseProof <- - conjunctionIntroductionList - context - (premiseProofs - <> [equality]) - clauseExists <- - first - (TypedInductivePreparationContext - "introduction witnesses") - (introduceClauseWitnesses - resolveGlobal - inductive - clause - context - environment - (scopedCoreTerm - fixedPoint) - result - clauseProof) - alternatives <- - clauseFormulaTerms - resolveGlobal - inductive - environment - (scopedCoreTerm - fixedPoint) - (scopedCoreTerm - result) - disjunction <- - first - (TypedInductivePreparationContext - "introduction disjunction") - (injectDisjunction - context - clauseIndex - alternatives - clauseExists) - inOperator <- - first - (TypedInductivePreparationContext - "introduction separation") - (separationBackward - context - domain - predicate - result - inDomain - disjunction) - inAppliedTarget <- - checkedTerm context - (memberTerm - (scopedCoreTerm - result) - (scopedCoreTerm - appliedOperatorSet)) - inAppliedOperator <- - first TypedInductiveProofError - (conversionProof - context - inOperator - inAppliedTarget) - monotone <- - first - (TypedInductivePreparationContext - "introduction bounded monotonicity") - (proveBoundedMonotonicity - foundation - resolveGlobal - inductive - context - environment) - fixed <- - first TypedInductiveProofError - (setLfpFixedProof - context - domain - operator - monotone) - reversedFixed <- - first - (TypedInductivePreparationContext - "introduction fixed-point symmetry") - (first TypedInductiveProofError - (equalityReverseProof - context - fixed)) - first - (TypedInductivePreparationContext - "introduction fixed-point transport") - (transportMembership - context - result - reversedFixed - inAppliedOperator)))) - preparedFact - (introMarker - marker - (clauseIndex + 1)) - (if any isRecursiveCondition - (directClauseConditions clause) - then SetLfpBound :| [SetLfpFixed] - else SetLfpFixed :| []) - proof - where - isRecursiveCondition = \case - DirectRecursiveCondition{} -> True - DirectSideCondition{} -> False - -preparedGuardProof - :: ProofContext (InductiveGlobal global) - -> PreparedInductiveGuard (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -preparedGuardProof context = \case - PreparedFoundationGuard tag -> - first TypedInductiveProofError - (foundationProof context tag) - PreparedImportedGuard index target -> - first TypedInductiveProofError - (importedProof context index target) - -prepareDomainSubsetFact - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> Marker - -> DirectInductive - -> Either - TypedInductiveError - (PreparedTypedInductiveFact (InductiveGlobal global)) -prepareDomainSubsetFact - foundation - resolveGlobal - marker - inductive = do - proof <- - proveUnderVariables - (rootProofContext - foundation - (Just . inductiveGlobalType)) - emptyEnvironment - (directInductiveParams - inductive) - (\context environment -> do - domain <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - (directInductiveDomain - inductive) - operator <- - checkedTerm context - =<< operatorTerm - resolveGlobal - inductive - environment - first TypedInductiveProofError - (setLfpBoundProof - context - domain - operator)) - preparedFact - (derivedMarker marker "dom_subset") - (SetLfpBound :| []) - proof - -prepareCasesFact - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> Marker - -> DirectInductive - -> Either - TypedInductiveError - (PreparedTypedInductiveFact (InductiveGlobal global)) -prepareCasesFact - foundation - resolveGlobal - marker - inductive = do - proof <- - proveUnderVariables - (rootProofContext - foundation - (Just . inductiveGlobalType)) - emptyEnvironment - (directInductiveParams - inductive) - (\parameterContext parameterEnvironment -> - forallIntroductionTyped - parameterContext - TySet - (\context result -> do - environment <- - shiftEnvironment - parameterEnvironment - domain <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - (directInductiveDomain - inductive) - operator <- - checkedTerm context - =<< operatorTerm - resolveGlobal - inductive - environment - fixedPoint <- - checkedTerm context - =<< fixedPointTerm - resolveGlobal - inductive - environment - predicate <- - checkedTerm context - =<< operatorPredicateAt - resolveGlobal - inductive - environment - (scopedCoreTerm - fixedPoint) - explicitOperatorSet <- - checkedTerm context - =<< separationSetAt - resolveGlobal - inductive - environment - (scopedCoreTerm - fixedPoint) - member <- - checkedTerm context - (memberTerm - (scopedCoreTerm result) - (scopedCoreTerm - fixedPoint)) - implicationIntroductionTyped - context - member - (\withMember memberProof -> do - monotone <- - proveBoundedMonotonicity - foundation - resolveGlobal - inductive - withMember - environment - fixed <- - first TypedInductiveProofError - (setLfpFixedProof - withMember - domain - operator - monotone) - inOperator <- - transportMembership - withMember - result - fixed - memberProof - explicitMembership <- - checkedTerm withMember - (memberTerm - (scopedCoreTerm - result) - (scopedCoreTerm - explicitOperatorSet)) - inSeparation <- - first TypedInductiveProofError - (conversionProof - withMember - inOperator - explicitMembership) - separation <- - separationForward - withMember - domain - predicate - result - inSeparation - predicateResult <- - predicateAt - resolveGlobal - inductive - environment - (scopedCoreTerm - fixedPoint) - (scopedCoreTerm - result) - predicateProof <- - first TypedInductiveProofError - (conjunctionRightProof - withMember - (memberTerm - (scopedCoreTerm result) - (scopedCoreTerm - domain)) - (CApp - (scopedCoreTerm - predicate) - (scopedCoreTerm - result)) - separation) - predicateTarget <- - checkedTerm - withMember - predicateResult - first TypedInductiveProofError - (conversionProof - withMember - predicateProof - predicateTarget)))) - preparedFact - (derivedMarker marker "cases") - (SetLfpFixed :| []) - proof - -prepareInductionFact - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> Marker - -> DirectInductive - -> Either - TypedInductiveError - (PreparedTypedInductiveFact (InductiveGlobal global)) -prepareInductionFact - foundation - resolveGlobal - marker - inductive = do - proof <- - proveUnderVariables - (rootProofContext - foundation - (Just . inductiveGlobalType)) - emptyEnvironment - (directInductiveParams - inductive) - (\parameterContext parameterEnvironment -> - forallIntroductionTyped - parameterContext - TySet - (\subsetContext subset -> do - environment <- - shiftEnvironment - parameterEnvironment - closures <- - closureTerms - resolveGlobal - inductive - environment - (scopedCoreTerm subset) - closureConjunction <- - checkedTerm subsetContext - (fromMaybe - (CImp CFalsum CFalsum) - (conjunctionList - closures)) - implicationIntroductionTyped - subsetContext - closureConjunction - (\withClosures closuresProof -> do - fixedPoint <- - checkedTerm withClosures - =<< fixedPointTerm - resolveGlobal - inductive - environment - proveSubset - withClosures - fixedPoint - subset - (\elementContext element memberProof -> do - elementEnvironment <- - shiftEnvironment environment - domain <- - checkedTerm elementContext - =<< lowerTerm - resolveGlobal - elementEnvironment - (directInductiveDomain - inductive) - operator <- - checkedTerm elementContext - =<< operatorTerm - resolveGlobal - inductive - elementEnvironment - fixedPointAtElement <- - checkedTerm elementContext - =<< fixedPointTerm - resolveGlobal - inductive - elementEnvironment - subsetAtElement <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - subset) - predicate <- - membershipPredicate - elementContext - subsetAtElement - monotone <- - first - (TypedInductivePreparationContext - "induction bounded monotonicity") - (proveBoundedMonotonicity - foundation - resolveGlobal - inductive - elementContext - elementEnvironment) - closure <- - first - (TypedInductivePreparationContext - "induction closure") - (proveInductionClosure - foundation - resolveGlobal - inductive - elementContext - elementEnvironment - fixedPointAtElement - operator - subsetAtElement - closures - closuresProof) - inducted <- - first - (TypedInductivePreparationContext - "induction fixed-point rule") - (first TypedInductiveProofError - (setLfpInductProof - elementContext - domain - operator - predicate - element - monotone - memberProof - closure)) - expected <- - checkedTerm elementContext - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - subsetAtElement)) - first TypedInductiveProofError - (conversionProof - elementContext - inducted - expected))))) - preparedFact - (derivedMarker marker "induct") - (SetLfpInduct :| []) - proof - -proveUnderVariables - :: ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> [VarSymbol] - -> ( ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -proveUnderVariables context environment variables build = - case variables of - [] -> - build context environment - variable : remaining -> do - extendedEnvironment <- - extendEnvironment - variable - environment - forallIntroductionTyped - context - TySet - (\extended _bound -> - proveUnderVariables - extended - extendedEnvironment - remaining - build) - -checkedTerm - :: ProofContext (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - (ScopedCheckedCore (InductiveGlobal global)) -checkedTerm context = - first TypedInductiveProofError - . scopedTerm context - -preparedFact - :: Marker - -> NonEmpty KernelRuleTag - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (PreparedTypedInductiveFact (InductiveGlobal global)) -preparedFact marker rules proof = do - target <- - maybe - (Left TypedInductiveProofRemainedOpen) - Right - (closeScopedCore - (builtProofStatement proof)) - pure - (PreparedTypedInductiveFact - ( marker - , target - , canonicalRules rules - , builtProofDerivation proof - )) - where - canonicalRules supplied = - case Set.toAscList - (Set.fromList (NonEmpty.toList supplied)) of - firstRule : remainingRules -> - firstRule :| remainingRules - [] -> - impossible "a nonempty guarded-rule set became empty" - -introMarker :: Marker -> Natural -> Marker -introMarker (Marker marker) index = - Marker - (marker - <> "_intro_" - <> Text.pack (show index)) - -derivedMarker :: Marker -> Text -> Marker -derivedMarker (Marker marker) suffix = - Marker - (marker <> "_" <> suffix) - -eliminateWrittenForalls - :: ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> [VarSymbol] - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -eliminateWrittenForalls - context - environment - variables - initial = - foldM - (\proof variable -> do - argument <- - checkedTerm context - =<< lookupEnvironment - variable - environment - first TypedInductiveProofError - (forallEliminationProof - context - proof - argument)) - initial - variables - -provePremises - :: ProofContext (InductiveGlobal global) - -> [CanonicalTerm (InductiveGlobal global)] - -> ( [BuiltProof (InductiveGlobal global)] - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -provePremises context premises build = - case conjunctionList premises of - Nothing -> - build [] - Just conjunction -> do - proposition <- - checkedTerm context conjunction - implicationIntroductionTyped - context - proposition - (\extended conjunctionProof -> do - projections <- - projectConjunctionList - extended - premises - conjunctionProof - build projections) - -conjunctionIntroductionList - :: ProofContext (InductiveGlobal global) - -> [BuiltProof (InductiveGlobal global)] - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -conjunctionIntroductionList _context [] = - Left - (TypedInductiveUnsupportedExpression - "an empty conjunction has no introduction proof") -conjunctionIntroductionList context (firstProof : remaining) = - foldM - (\left right -> - first TypedInductiveProofError - (conjunctionIntroductionProof - context - left - right)) - firstProof - remaining - -projectConjunctionList - :: ProofContext (InductiveGlobal global) - -> [CanonicalTerm (InductiveGlobal global)] - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - [BuiltProof (InductiveGlobal global)] -projectConjunctionList _context [] _proof = - pure [] -projectConjunctionList _context [_only] proof = - pure [proof] -projectConjunctionList context terms proof = do - let preceding = - List.init terms - final = - List.last terms - precedingTerm = - fromMaybe - CFalsum - (conjunctionList preceding) - precedingProof <- - first TypedInductiveProofError - (conjunctionLeftProof - context - precedingTerm - final - proof) - finalProof <- - first TypedInductiveProofError - (conjunctionRightProof - context - precedingTerm - final - proof) - (<> [finalProof]) - <$> projectConjunctionList - context - preceding - precedingProof - -introduceClauseWitnesses - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> DirectInductiveClause - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -introduceClauseWitnesses - resolveGlobal - _inductive - clause - context - environment - candidate - result - bodyProof = - introduce - (directClauseVariables clause) - where - introduce [] = - pure bodyProof - introduce (variable : remaining) = do - inner <- - introduce remaining - witness <- - checkedTerm context - =<< lookupEnvironment - variable - environment - underBinderEnvironment <- - rebindEnvironment - variable - =<< shiftEnvironment - environment - let candidate' = - shiftCanonicalTerm 1 0 candidate - result' = - shiftCanonicalTerm - 1 - 0 - (scopedCoreTerm result) - bodyUnderBinderTerm <- - clauseFormulaWithBinders - resolveGlobal - clause - underBinderEnvironment - candidate' - result' - remaining - bodyUnderBinder <- - first TypedInductiveCoreError - (checkScopedCanonicalCore - (Just . inductiveGlobalType) - (TySet - : proofContextTypes - context) - bodyUnderBinderTerm) - first TypedInductiveProofError - (existentialIntroductionProof - context - TySet - bodyUnderBinder - witness - inner) - -clauseFormulaWithBinders - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductiveClause - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> [VarSymbol] - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -clauseFormulaWithBinders - resolveGlobal - clause - environment - candidate - result = \case - [] -> do - conditions <- - traverse - (conditionTerm - resolveGlobal - environment - candidate) - (directClauseConditions - clause) - clauseResult <- - lowerTerm - resolveGlobal - environment - (directClauseResult clause) - pure - (fromMaybe - (CEq TySet result clauseResult) - (conjunctionList - (conditions - <> [CEq - TySet - result - clauseResult]))) - variable : remaining -> do - extended <- - rebindEnvironment - variable - =<< shiftEnvironment - environment - body <- - clauseFormulaWithBinders - resolveGlobal - clause - extended - (shiftCanonicalTerm - 1 - 0 - candidate) - (shiftCanonicalTerm - 1 - 0 - result) - remaining - pure (existentialTerm TySet body) - -rebindEnvironment - :: VarSymbol - -> InductiveEnvironment - -> Either - TypedInductiveError - InductiveEnvironment -rebindEnvironment variable - (InductiveEnvironment variables) = - pure - (InductiveEnvironment - (Map.insert variable 0 variables)) - -injectDisjunction - :: ProofContext (InductiveGlobal global) - -> Natural - -> [CanonicalTerm (InductiveGlobal global)] - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -injectDisjunction context index alternatives proof = - case splitAtNatural index alternatives of - Nothing -> - Left - (TypedInductiveUnsupportedExpression - "inductive clause index is outside the source-ordered alternatives") - Just (preceding, _selected, following) -> do - selectedProof <- - case preceding of - [] -> - pure proof - _ -> do - let precedingTerm = - disjunctionList preceding - first TypedInductiveProofError - (disjunctionRightProof - context - precedingTerm - proof) - foldM - (\current followingTerm -> - first TypedInductiveProofError - (disjunctionLeftProof - context - followingTerm - current)) - selectedProof - following - where - splitAtNatural - :: Natural - -> [a] - -> Maybe ([a], a, [a]) - splitAtNatural = - go [] - where - go _preceding _index [] = - Nothing - go preceding 0 (selected : rest) = - Just - ( reverse preceding - , selected - , rest - ) - go preceding current (item : rest) = - go - (item : preceding) - (current - 1) - rest - -closureTerms - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - [CanonicalTerm (InductiveGlobal global)] -closureTerms - resolveGlobal - inductive - environment - subset = - traverse closureFor - (NonEmpty.toList - (directInductiveClauses - inductive)) - where - closureFor clause = do - clauseEnvironment <- - extendVariables - environment - (directClauseVariables clause) - let binderCount = - fromIntegral - (length - (directClauseVariables - clause)) - subset' = - shiftCanonicalTerm - binderCount - 0 - subset - conditions <- - traverse - (conditionTerm - resolveGlobal - clauseEnvironment - subset') - (directClauseConditions - clause) - result <- - lowerTerm - resolveGlobal - clauseEnvironment - (directClauseResult clause) - pure - (closeForalls - (length - (directClauseVariables - clause)) - (impliesIfNeeded - (conjunctionList conditions) - (memberTerm - result - subset'))) - -proveBoundedMonotonicity - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -proveBoundedMonotonicity - _foundation - resolveGlobal - inductive - context - environment = do - domain <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - (directInductiveDomain - inductive) - operator <- - checkedTerm context - =<< operatorTerm - resolveGlobal - inductive - environment - operatorDomain <- - checkedTerm context - (CApp - (scopedCoreTerm operator) - (scopedCoreTerm domain)) - bounded <- - first - (TypedInductivePreparationContext - "bounded monotonicity range") - (proveSubset - context - operatorDomain - domain - (\elementContext element membership -> do - elementEnvironment <- - shiftEnvironment environment - domainAtElement <- - checkedTerm elementContext - =<< lowerTerm - resolveGlobal - elementEnvironment - (directInductiveDomain - inductive) - predicate <- - checkedTerm elementContext - =<< operatorPredicateAt - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - domainAtElement) - explicitOperator <- - checkedTerm elementContext - =<< separationSetAt - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - domainAtElement) - explicitMembership <- - checkedTerm elementContext - (memberTerm - (scopedCoreTerm element) - (scopedCoreTerm - explicitOperator)) - separatedMembership <- - first TypedInductiveProofError - (conversionProof - elementContext - membership - explicitMembership) - characteristic <- - separationForward - elementContext - domainAtElement - predicate - element - separatedMembership - first TypedInductiveProofError - (conjunctionLeftProof - elementContext - (memberTerm - (scopedCoreTerm element) - (scopedCoreTerm - domainAtElement)) - (CApp - (scopedCoreTerm predicate) - (scopedCoreTerm element)) - characteristic))) - monotone <- - first - (TypedInductivePreparationContext - "bounded monotonicity relation") - (forallIntroductionTyped - context - TySet - (\xContext _x -> - forallIntroductionTyped - xContext - TySet - (\xyContext _y -> do - xyEnvironment <- - shiftEnvironment - =<< shiftEnvironment - environment - x <- - checkedTerm xyContext - (CBound 1) - y <- - checkedTerm xyContext - (CBound 0) - domainXY <- - checkedTerm xyContext - =<< lowerTerm - resolveGlobal - xyEnvironment - (directInductiveDomain - inductive) - relation <- - checkedTerm xyContext - (conjunctionTerm - (subsetTerm - (scopedCoreTerm x) - (scopedCoreTerm y)) - (subsetTerm - (scopedCoreTerm y) - (scopedCoreTerm - domainXY))) - implicationIntroductionTyped - xyContext - relation - (\relatedContext _relationProof -> do - operatorXY <- - checkedTerm relatedContext - =<< operatorTerm - resolveGlobal - inductive - xyEnvironment - operatorX <- - checkedTerm relatedContext - (CApp - (scopedCoreTerm - operatorXY) - (scopedCoreTerm x)) - operatorY <- - checkedTerm relatedContext - (CApp - (scopedCoreTerm - operatorXY) - (scopedCoreTerm y)) - proveSubset - relatedContext - operatorX - operatorY - (\elementContext element membership -> do - elementEnvironment <- - shiftEnvironment - xyEnvironment - xAtElement <- - checkedTerm - elementContext - (CBound 2) - yAtElement <- - checkedTerm - elementContext - (CBound 1) - domainAtElement <- - checkedTerm - elementContext - =<< lowerTerm - resolveGlobal - elementEnvironment - (directInductiveDomain - inductive) - predicateX <- - checkedTerm - elementContext - =<< operatorPredicateAt - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - xAtElement) - predicateY <- - checkedTerm - elementContext - =<< operatorPredicateAt - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - yAtElement) - explicitX <- - checkedTerm - elementContext - =<< separationSetAt - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - xAtElement) - memberExplicitX <- - checkedTerm - elementContext - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - explicitX)) - separatedX <- - first TypedInductiveProofError - (conversionProof - elementContext - membership - memberExplicitX) - characteristicX <- - separationForward - elementContext - domainAtElement - predicateX - element - separatedX - inDomain <- - first - (TypedInductivePreparationContext - "monotonicity domain projection") - (first TypedInductiveProofError - (conjunctionLeftProof - elementContext - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - domainAtElement)) - (CApp - (scopedCoreTerm - predicateX) - (scopedCoreTerm - element)) - characteristicX)) - satisfiesX <- - first - (TypedInductivePreparationContext - "monotonicity predicate projection") - (first TypedInductiveProofError - (conjunctionRightProof - elementContext - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - domainAtElement)) - (CApp - (scopedCoreTerm - predicateX) - (scopedCoreTerm - element)) - characteristicX)) - alternativesX <- - clauseFormulaTerms - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - xAtElement) - (scopedCoreTerm - element) - alternativesY <- - clauseFormulaTerms - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - yAtElement) - (scopedCoreTerm - element) - predicateXTarget <- - checkedTerm - elementContext - (disjunctionList - alternativesX) - satisfiesX' <- - first TypedInductiveProofError - (conversionProof - elementContext - satisfiesX - predicateXTarget) - satisfiesY <- - first - (TypedInductivePreparationContext - "monotonicity predicate transport") - (transformPredicateProof - resolveGlobal - inductive - elementContext - elementEnvironment - (scopedCoreTerm - xAtElement) - (scopedCoreTerm - yAtElement) - (scopedCoreTerm - domainAtElement) - (scopedCoreTerm - element) - alternativesX - alternativesY - satisfiesX') - separatedY <- - first - (TypedInductivePreparationContext - "monotonicity separation") - (separationBackward - elementContext - domainAtElement - predicateY - element - inDomain - satisfiesY) - operatorYAtElement <- - first - TypedInductiveCoreError - (weakenScopedCore - (Just - . inductiveGlobalType) - TySet - operatorY) - explicitMembershipY <- - checkedTerm - elementContext - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - operatorYAtElement)) - first TypedInductiveProofError - (conversionProof - elementContext - separatedY - explicitMembershipY)))))) - first - (TypedInductivePreparationContext - "bounded monotonicity conjunction") - (first TypedInductiveProofError - (conjunctionIntroductionProof - context - bounded - monotone)) - -transformPredicateProof - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> [CanonicalTerm (InductiveGlobal global)] - -> [CanonicalTerm (InductiveGlobal global)] - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -transformPredicateProof - resolveGlobal - inductive - context - environment - candidateX - candidateY - domain - result - alternativesX - alternativesY - proof = do - target <- - checkedTerm context - (disjunctionList alternativesY) - first - (TypedInductivePreparationContext - "predicate disjunction elimination") - (eliminateDisjunctionAlternatives - context - alternativesX - proof - target - (\caseContext clauseIndex clauseProof -> do - clause <- - maybe - (Left - (TypedInductiveUnsupportedExpression - "inductive clause inventory changed during proof construction")) - Right - (atNatural - clauseIndex - (NonEmpty.toList - (directInductiveClauses - inductive))) - first - (TypedInductivePreparationContext - "predicate witness elimination") - (eliminateClauseWitnesses - resolveGlobal - clause - caseContext - environment - candidateX - result - clauseProof - target - (\depth - leafContext - leafEnvironment - candidateXAtLeaf - resultAtLeaf - bodyProof -> do - let candidateYAtLeaf = - shiftCanonicalTerm - depth - 0 - candidateY - domainAtLeaf = - shiftCanonicalTerm - depth - 0 - domain - alternativesYAtLeaf = - shiftCanonicalTerm - depth - 0 - <$> alternativesY - bodyY <- - first - (TypedInductivePreparationContext - "predicate clause body") - (transformClauseBody - resolveGlobal - clause - leafContext - leafEnvironment - candidateXAtLeaf - candidateYAtLeaf - domainAtLeaf - resultAtLeaf - bodyProof) - resultAtLeaf' <- - checkedTerm - leafContext - resultAtLeaf - alternativeY <- - introduceClauseWitnesses - resolveGlobal - inductive - clause - leafContext - leafEnvironment - candidateYAtLeaf - resultAtLeaf' - bodyY - first - (TypedInductivePreparationContext - "predicate disjunction injection") - (injectDisjunction - leafContext - clauseIndex - alternativesYAtLeaf - alternativeY))))) - -transformClauseBody - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductiveClause - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -transformClauseBody - resolveGlobal - clause - context - environment - candidateX - candidateY - domain - result - proof = do - conditionsX <- - traverse - (conditionTerm - resolveGlobal - environment - candidateX) - (directClauseConditions - clause) - clauseResult <- - lowerTerm - resolveGlobal - environment - (directClauseResult clause) - let equality = - CEq TySet result clauseResult - bodyTermsX = - conditionsX <> [equality] - projections <- - projectConjunctionList - context - bodyTermsX - proof - let (conditionProofs, equalityProofs) = - splitAt - (length conditionsX) - projections - transformedConditions <- - sequence - [ case condition of - DirectSideCondition _formula -> - pure conditionProof - DirectRecursiveCondition recursiveTerm -> do - recursiveElement <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - recursiveTerm - subsetProof <- - subsetRelationHypothesis - context - candidateX - candidateY - domain - implication <- - first TypedInductiveProofError - (forallEliminationProof - context - subsetProof - recursiveElement) - first TypedInductiveProofError - (implicationEliminationProof - context - implication - conditionProof) - | (condition, conditionProof) <- - zip - (directClauseConditions clause) - conditionProofs - ] - equalityProof <- - case equalityProofs of - [only] -> - pure only - _ -> - Left - (TypedInductiveUnsupportedExpression - "inductive clause equality projection is inconsistent") - conjunctionIntroductionList - context - (transformedConditions - <> [equalityProof]) - -subsetRelationHypothesis - :: ProofContext (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -subsetRelationHypothesis - context - left - right - domain = do - let leftSubsetRight = - subsetTerm left right - rightSubsetDomain = - subsetTerm right domain - relation = - conjunctionTerm - leftSubsetRight - rightSubsetDomain - relationTerm <- - checkedTerm context relation - relationProof <- - first TypedInductiveProofError - (hypothesisProof - context - relationTerm) - first TypedInductiveProofError - (conjunctionLeftProof - context - leftSubsetRight - rightSubsetDomain - relationProof) - -eliminateClauseWitnesses - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductiveClause - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ( Natural - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -eliminateClauseWitnesses - resolveGlobal - clause - initialContext - initialEnvironment - initialCandidate - initialResult - initialProof - initialTarget - finish = - go - 0 - initialContext - initialEnvironment - initialCandidate - initialResult - initialProof - initialTarget - (directClauseVariables clause) - where - go depth context environment candidate result proof target = \case - [] -> - finish - depth - context - environment - candidate - result - proof - variable : remaining -> do - underBinderEnvironment <- - rebindEnvironment - variable - =<< shiftEnvironment - environment - let candidate' = - shiftCanonicalTerm - 1 - 0 - candidate - result' = - shiftCanonicalTerm - 1 - 0 - result - bodyUnderBinderTerm <- - clauseFormulaWithBinders - resolveGlobal - clause - underBinderEnvironment - candidate' - result' - remaining - bodyUnderBinder <- - first TypedInductiveCoreError - (checkScopedCanonicalCore - (Just . inductiveGlobalType) - (TySet - : proofContextTypes - context) - bodyUnderBinderTerm) - targetUnderBinder <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - target) - first TypedInductiveProofError - (existentialEliminationProof - context - TySet - bodyUnderBinder - proof - target - (\underBinderContext _witness bodyProof -> - first typedAsProofError - (go - (depth + 1) - underBinderContext - underBinderEnvironment - candidate' - result' - bodyProof - targetUnderBinder - remaining))) - -eliminateDisjunctionAlternatives - :: ProofContext (InductiveGlobal global) - -> [CanonicalTerm (InductiveGlobal global)] - -> BuiltProof (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ( ProofContext (InductiveGlobal global) - -> Natural - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -eliminateDisjunctionAlternatives - initialContext - alternatives - proof - target - handle = - go initialContext 0 alternatives proof - where - go _context _offset [] _proof = - Left - (TypedInductiveUnsupportedExpression - "an inductive predicate has no alternatives") - go context offset [_only] onlyProof = - handle context offset onlyProof - go context offset current currentProof = do - let preceding = - List.init current - final = - List.last current - precedingTerm = - disjunctionList preceding - finalIndex = - offset - + fromIntegral - (length preceding) - first TypedInductiveProofError - (disjunctionEliminationProof - context - precedingTerm - final - currentProof - target - (\leftContext leftProof -> - first typedAsProofError - (go - leftContext - offset - preceding - leftProof)) - (\rightContext rightProof -> - first typedAsProofError - (handle - rightContext - finalIndex - rightProof))) - -proveInductionClosure - :: CheckedFoundation - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> ScopedCheckedCore (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> [CanonicalTerm (InductiveGlobal global)] - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -proveInductionClosure - _foundation - resolveGlobal - inductive - context - environment - fixedPoint - operator - subset - closures - _closuresProof = - forallIntroductionTyped - context - TySet - (\elementContext element -> do - elementEnvironment <- - shiftEnvironment environment - fixedPointAtElement <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - fixedPoint) - operatorAtElement <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - operator) - subsetAtElement <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - subset) - inductionPredicate <- - membershipPredicate - elementContext - subsetAtElement - candidate <- - checkedTerm elementContext - (apply2 - (CIntrinsic Sep) - (scopedCoreTerm - fixedPointAtElement) - (scopedCoreTerm - inductionPredicate)) - unfolded <- - checkedTerm elementContext - (CApp - (scopedCoreTerm - operatorAtElement) - (scopedCoreTerm - candidate)) - premise <- - checkedTerm elementContext - (memberTerm - (scopedCoreTerm element) - (scopedCoreTerm unfolded)) - implicationIntroductionTyped - elementContext - premise - (\withMember memberProof -> do - domain <- - checkedTerm withMember - =<< lowerTerm - resolveGlobal - elementEnvironment - (directInductiveDomain - inductive) - operatorPredicate <- - checkedTerm withMember - =<< operatorPredicateAt - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - candidate) - explicitOperator <- - checkedTerm withMember - =<< separationSetAt - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - candidate) - explicitMembership <- - checkedTerm withMember - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - explicitOperator)) - separated <- - first TypedInductiveProofError - (conversionProof - withMember - memberProof - explicitMembership) - characteristic <- - separationForward - withMember - domain - operatorPredicate - element - separated - predicateProof <- - first TypedInductiveProofError - (conjunctionRightProof - withMember - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - domain)) - (CApp - (scopedCoreTerm - operatorPredicate) - (scopedCoreTerm - element)) - characteristic) - alternatives <- - clauseFormulaTerms - resolveGlobal - inductive - elementEnvironment - (scopedCoreTerm - candidate) - (scopedCoreTerm - element) - predicateTarget <- - checkedTerm - withMember - (disjunctionList - alternatives) - predicateProof' <- - first TypedInductiveProofError - (conversionProof - withMember - predicateProof - predicateTarget) - result <- - checkedTerm withMember - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - subsetAtElement)) - subsetMembership <- - first - (TypedInductivePreparationContext - "induction clause alternatives") - (eliminateDisjunctionAlternatives - withMember - alternatives - predicateProof' - result - (\caseContext clauseIndex clauseProof -> do - clause <- - maybe - (Left - (TypedInductiveUnsupportedExpression - "inductive closure clause index is outside the source inventory")) - Right - (atNatural - clauseIndex - (NonEmpty.toList - (directInductiveClauses - inductive))) - first - (TypedInductivePreparationContext - "induction clause witnesses") - (eliminateClauseWitnesses - resolveGlobal - clause - caseContext - elementEnvironment - (scopedCoreTerm - candidate) - (scopedCoreTerm - element) - clauseProof - result - (\depth - leafContext - leafEnvironment - _candidateAtLeaf - resultAtLeaf - bodyProof -> - first - (TypedInductivePreparationContext - "induction clause proof") - (proveInductionClause - resolveGlobal - inductive - clauseIndex - clause - leafContext - leafEnvironment - (shiftCanonicalTerm - depth - 0 - (scopedCoreTerm - fixedPointAtElement)) - (shiftCanonicalTerm - depth - 0 - (scopedCoreTerm - inductionPredicate)) - (shiftCanonicalTerm - depth - 0 - (scopedCoreTerm - subsetAtElement)) - (shiftCanonicalTerm - (depth + 2) - 0 - <$> closures) - resultAtLeaf - bodyProof))))) - appliedPredicate <- - checkedTerm withMember - (CApp - (scopedCoreTerm - inductionPredicate) - (scopedCoreTerm - element)) - first TypedInductiveProofError - (conversionProof - withMember - subsetMembership - appliedPredicate))) - -proveInductionClause - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> Natural - -> DirectInductiveClause - -> ProofContext (InductiveGlobal global) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> [CanonicalTerm (InductiveGlobal global)] - -> CanonicalTerm (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -proveInductionClause - resolveGlobal - _inductive - clauseIndex - clause - context - environment - fixedPoint - predicate - subset - closures - result - bodyProof = do - conditions <- - traverse - (conditionTerm - resolveGlobal - environment - (apply2 - (CIntrinsic Sep) - fixedPoint - predicate)) - (directClauseConditions - clause) - clauseResult <- - lowerTerm - resolveGlobal - environment - (directClauseResult clause) - let equality = - CEq TySet result clauseResult - bodyTerms = - conditions <> [equality] - projections <- - first - (TypedInductivePreparationContext - "induction clause body projections") - (projectConjunctionList - context - bodyTerms - bodyProof) - let (conditionProofs, equalityProofs) = - splitAt - (length conditions) - projections - closureConditionProofs <- - sequence - [ case condition of - DirectSideCondition _formula -> - pure conditionProof - DirectRecursiveCondition recursiveTerm -> do - recursiveElement <- - checkedTerm context - =<< lowerTerm - resolveGlobal - environment - recursiveTerm - fixedPoint' <- - checkedTerm context fixedPoint - predicate' <- - checkedTerm context predicate - separated <- - separationForward - context - fixedPoint' - predicate' - recursiveElement - conditionProof - predicateMembership <- - first TypedInductiveProofError - (conjunctionRightProof - context - (memberTerm - (scopedCoreTerm - recursiveElement) - fixedPoint) - (CApp - predicate - (scopedCoreTerm - recursiveElement)) - separated) - expected <- - checkedTerm context - (memberTerm - (scopedCoreTerm - recursiveElement) - subset) - first TypedInductiveProofError - (conversionProof - context - predicateMembership - expected) - | (condition, conditionProof) <- - zip - (directClauseConditions clause) - conditionProofs - ] - closureConjunction <- - case conjunctionList closures of - Nothing -> - Left - (TypedInductiveUnsupportedExpression - "inductive closure inventory is empty") - Just conjunction -> - first - (TypedInductivePreparationContext - "induction closure conjunction") - (checkedTerm context conjunction) - allClosures <- - first - (TypedInductivePreparationContext - "induction closure hypothesis") - (first TypedInductiveProofError - (hypothesisProof - context - closureConjunction)) - closureProofs <- - first - (TypedInductivePreparationContext - "induction closure projections") - (projectConjunctionList - context - closures - allClosures) - selectedClosure <- - maybe - (Left - (TypedInductiveUnsupportedExpression - "inductive closure projection is outside the source inventory")) - Right - (atNatural clauseIndex closureProofs) - specializedClosure <- - first - (TypedInductivePreparationContext - "induction closure specialization") - (eliminateWrittenForalls - context - environment - (directClauseVariables clause) - selectedClosure) - resultMembership <- - case closureConditionProofs of - [] -> - pure specializedClosure - _ -> do - conjunction <- - conjunctionIntroductionList - context - closureConditionProofs - first TypedInductiveProofError - (implicationEliminationProof - context - specializedClosure - conjunction) - equalityProof <- - case equalityProofs of - [only] -> - pure only - _ -> - Left - (TypedInductiveUnsupportedExpression - "inductive closure equality projection is inconsistent") - subset' <- - first - (TypedInductivePreparationContext - "induction subset target") - (checkedTerm context subset) - first - (TypedInductivePreparationContext - "induction result transport") - (transportElementMembership - context - subset' - equalityProof - resultMembership) - -transportElementMembership - :: ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -transportElementMembership - context - set - equality - membership = do - (sourceElement, targetElement) <- - case scopedCoreTerm - (builtProofStatement - equality) of - CEq TySet source target -> - Right (source, target) - _ -> - Left - (TypedInductiveUnsupportedExpression - "element transport requires set equality") - predicate <- - membershipPredicate - context - set - predicateReflexivity <- - first TypedInductiveProofError - (equalityReflexivityProof - context - predicate) - propositionEquality <- - first TypedInductiveProofError - (equalityCongruenceApplicationProof - context - predicateReflexivity - equality) - reversed <- - first TypedInductiveProofError - (equalityReverseProof - context - propositionEquality) - appliedTarget <- - checkedTerm context - (CApp - (scopedCoreTerm predicate) - targetElement) - targetMembership <- - first TypedInductiveProofError - (conversionProof - context - membership - appliedTarget) - transported <- - first TypedInductiveProofError - (equalityModusPonensProof - context - reversed - targetMembership) - sourceMembership <- - checkedTerm context - (memberTerm - sourceElement - (scopedCoreTerm set)) - first TypedInductiveProofError - (conversionProof - context - transported - sourceMembership) - -predicateAt - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -predicateAt - resolveGlobal - inductive - environment - candidate - result = - disjunctionList - <$> clauseFormulaTerms - resolveGlobal - inductive - environment - candidate - result - -clauseFormulaTerms - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - [CanonicalTerm (InductiveGlobal global)] -clauseFormulaTerms - resolveGlobal - inductive - environment - candidate - result = - traverse - (clauseFormulaAt - resolveGlobal - environment - candidate - result) - (NonEmpty.toList - (directInductiveClauses - inductive)) - -clauseFormulaAt - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> CanonicalTerm (InductiveGlobal global) - -> DirectInductiveClause - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -clauseFormulaAt - resolveGlobal - environment - candidate - result - clause = do - clauseEnvironment <- - extendVariables - environment - (directClauseVariables clause) - let binderCount = - fromIntegral - (length - (directClauseVariables - clause)) - candidate' = - shiftCanonicalTerm binderCount 0 candidate - result' = - shiftCanonicalTerm binderCount 0 result - conditions <- - traverse - (conditionTerm - resolveGlobal - clauseEnvironment - candidate') - (directClauseConditions - clause) - clauseResult <- - lowerTerm - resolveGlobal - clauseEnvironment - (directClauseResult clause) - pure - (closeExistentials - (length - (directClauseVariables - clause)) - (fromMaybe - (CEq TySet result' clauseResult) - (conjunctionList - (conditions - <> [CEq - TySet - result' - clauseResult])))) - -extendVariables - :: InductiveEnvironment - -> [VarSymbol] - -> Either - TypedInductiveError - InductiveEnvironment -extendVariables = - go [] - where - go _seen environment [] = - Right environment - go seen environment (variable : remaining) - | variable `elem` seen = - Left - (TypedInductiveDuplicateBinder - variable) - | otherwise = do - extended <- - rebindEnvironment - variable - =<< shiftEnvironment - environment - go - (variable : seen) - extended - remaining - -membershipPredicate - :: ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> Either - TypedInductiveError - (ScopedCheckedCore (InductiveGlobal global)) -membershipPredicate context set = do - weakenedSet <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - set) - checkedTerm context - (CLam TySet - (memberTerm - (CBound 0) - (scopedCoreTerm - weakenedSet))) - -operatorPredicateAt - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -operatorPredicateAt - resolveGlobal - inductive - environment - candidate = do - extended <- - shiftEnvironment environment - body <- - predicateAt - resolveGlobal - inductive - extended - (shiftCanonicalTerm - 1 - 0 - candidate) - (CBound 0) - pure (CLam TySet body) - -separationSetAt - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -separationSetAt - resolveGlobal - inductive - environment - candidate = do - domain <- - lowerTerm - resolveGlobal - environment - (directInductiveDomain - inductive) - predicate <- - operatorPredicateAt - resolveGlobal - inductive - environment - candidate - pure - (apply2 - (CIntrinsic Sep) - domain - predicate) - -foundationInstance - :: ProofContext (InductiveGlobal global) - -> FoundationAxiomTag - -> [ScopedCheckedCore (InductiveGlobal global)] - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -foundationInstance context tag arguments = do - initial <- - first TypedInductiveProofError - (foundationProof context tag) - foldM - (\proof argument -> - first TypedInductiveProofError - (forallEliminationProof - context - proof - argument)) - initial - arguments - -separationForward - :: ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -separationForward - context - domain - predicate - element - membership = do - characteristic <- - foundationInstance - context - SeparationCharacteristic - [domain, predicate, element] - first TypedInductiveProofError - (equalityModusPonensProof - context - characteristic - membership) - -separationBackward - :: ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -separationBackward - context - domain - predicate - element - inDomain - satisfies = do - characteristic <- - foundationInstance - context - SeparationCharacteristic - [domain, predicate, element] - reversed <- - first TypedInductiveProofError - (equalityReverseProof - context - characteristic) - expectedSatisfies <- - checkedTerm context - (CApp - (scopedCoreTerm predicate) - (scopedCoreTerm element)) - satisfies' <- - first TypedInductiveProofError - (conversionProof - context - satisfies - expectedSatisfies) - conjunction <- - first TypedInductiveProofError - (conjunctionIntroductionProof - context - inDomain - satisfies') - first TypedInductiveProofError - (equalityModusPonensProof - context - reversed - conjunction) - -transportMembership - :: ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -transportMembership - context - element - setEquality - membership = do - (sourceSet, targetSet) <- - case scopedCoreTerm - (builtProofStatement - setEquality) of - CEq TySet source target -> - Right (source, target) - _ -> - Left - (TypedInductiveUnsupportedExpression - "membership transport requires set equality") - weakenedElement <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - element) - function <- - checkedTerm context - (CLam TySet - (memberTerm - (scopedCoreTerm - weakenedElement) - (CBound 0))) - functionReflexivity <- - first TypedInductiveProofError - (equalityReflexivityProof - context - function) - propositionEquality <- - first TypedInductiveProofError - (equalityCongruenceApplicationProof - context - functionReflexivity - setEquality) - appliedSource <- - checkedTerm context - (CApp - (scopedCoreTerm function) - sourceSet) - sourceMembership <- - first TypedInductiveProofError - (conversionProof - context - membership - appliedSource) - transported <- - first TypedInductiveProofError - (equalityModusPonensProof - context - propositionEquality - sourceMembership) - targetMembership <- - checkedTerm context - (memberTerm - (scopedCoreTerm element) - targetSet) - first TypedInductiveProofError - (conversionProof - context - transported - targetMembership) - -proveSubset - :: ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ( ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -proveSubset context left right proveElement = - forallIntroductionTyped - context - TySet - (\extended element -> do - left' <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - left) - right' <- - first TypedInductiveCoreError - (weakenScopedCore - (Just . inductiveGlobalType) - TySet - right) - memberLeft <- - checkedTerm extended - (memberTerm - (scopedCoreTerm element) - (scopedCoreTerm left')) - implicationIntroductionTyped - extended - memberLeft - (\withMember memberProof -> - proveElement - withMember - element - memberProof - >>= \result -> do - expected <- - checkedTerm withMember - (memberTerm - (scopedCoreTerm - element) - (scopedCoreTerm - right')) - if builtProofStatement result - == expected - then pure result - else - Left - (TypedInductiveUnsupportedExpression - "subset proof produced the wrong membership target"))) - -typedAsProofError - :: TypedInductiveError - -> KernelProofBuildError -typedAsProofError = \case - TypedInductiveProofError err -> - err - err -> - ProofSetLfpRuleFailed - (Text.pack (show err)) - -implicationIntroductionTyped - :: ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> ( ProofContext (InductiveGlobal global) - -> BuiltProof (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -implicationIntroductionTyped context premise build = - first TypedInductiveProofError - (implicationIntroductionProof - context - premise - (\extended proof -> - first typedAsProofError - (build extended proof))) - -forallIntroductionTyped - :: ProofContext (InductiveGlobal global) - -> CoreType - -> ( ProofContext (InductiveGlobal global) - -> ScopedCheckedCore (InductiveGlobal global) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (BuiltProof (InductiveGlobal global)) -forallIntroductionTyped context binderType build = - first TypedInductiveProofError - (forallIntroductionProof - context - binderType - (\extended variable -> - first typedAsProofError - (build extended variable))) - -buildUnderVariables - :: InductiveEnvironment - -> [VarSymbol] - -> ( InductiveEnvironment - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) - ) - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -buildUnderVariables - environment - [] - build = - build environment -buildUnderVariables - environment - (variable : remaining) - build = do - extended <- - extendEnvironment - variable - environment - buildUnderVariables - extended - remaining - build - -fixedPointTerm - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> InductiveEnvironment - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -fixedPointTerm resolveGlobal inductive environment = do - domain <- - lowerTerm - resolveGlobal - environment - (directInductiveDomain - inductive) - operator <- - operatorTerm - resolveGlobal - inductive - environment - pure - (CApp - (CApp - (CIntrinsic ISetLfp) - domain) - operator) - -operatorTerm - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> InductiveEnvironment - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -operatorTerm resolveGlobal inductive parameterEnvironment = do - candidateEnvironment <- - shiftEnvironment parameterEnvironment - domain <- - lowerTerm - resolveGlobal - candidateEnvironment - (directInductiveDomain - inductive) - resultEnvironment <- - shiftEnvironment candidateEnvironment - clauses <- - traverse - (clausePredicateTerm - resolveGlobal - resultEnvironment) - (directInductiveClauses - inductive) - pure - (CLam TySet - (CApp - (CApp - (CIntrinsic Sep) - domain) - (CLam TySet - (disjunctionList - (NonEmpty.toList - clauses))))) - -clausePredicateTerm - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> InductiveEnvironment - -> DirectInductiveClause - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -clausePredicateTerm - resolveGlobal - resultEnvironment - clause = do - clauseEnvironment <- - extendVariables - resultEnvironment - (directClauseVariables clause) - let variableCount = - fromIntegral - (length - (directClauseVariables - clause)) - resultVariable = - CBound variableCount - candidate = - CBound (variableCount + 1) - conditions <- - traverse - (conditionTerm - resolveGlobal - clauseEnvironment - candidate) - (directClauseConditions - clause) - result <- - lowerTerm - resolveGlobal - clauseEnvironment - (directClauseResult - clause) - pure - (closeExistentials - (length - (directClauseVariables clause)) - (fromMaybe - (CEq - TySet - resultVariable - result) - (conjunctionList - (conditions - <> [CEq - TySet - resultVariable - result])))) - -conditionTerm - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> InductiveEnvironment - -> CanonicalTerm (InductiveGlobal global) - -> DirectInductiveCondition - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -conditionTerm resolveGlobal environment candidate = \case - DirectSideCondition formula -> - lowerFormula - resolveGlobal - environment - formula - DirectRecursiveCondition term -> - memberTerm - <$> lowerTerm - resolveGlobal - environment - term - <*> pure candidate - -shiftEnvironment - :: InductiveEnvironment - -> Either - TypedInductiveError - InductiveEnvironment -shiftEnvironment - (InductiveEnvironment variables) = - pure - (InductiveEnvironment - (succ <$> variables)) - -lowerFormula - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> InductiveEnvironment - -> Formula - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -lowerFormula = - lowerFormulaWith False - -lowerFormulaWith - :: Bool - -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> InductiveEnvironment - -> Formula - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -lowerFormulaWith allowQuantified resolveGlobal environment = \case - IsElementOf _location element set -> - memberTerm - <$> lowerTerm - resolveGlobal - environment - element - <*> lowerTerm - resolveGlobal - environment - set - Equals _location left right -> - CEq TySet - <$> lowerTerm resolveGlobal environment left - <*> lowerTerm resolveGlobal environment right - NotEquals _location left right -> - notTerm - <$> (CEq TySet - <$> lowerTerm resolveGlobal environment left - <*> lowerTerm resolveGlobal environment right) - IsSubsetOf _location left right -> do - extended <- - shiftEnvironment environment - left' <- - lowerTerm resolveGlobal extended left - right' <- - lowerTerm resolveGlobal extended right - pure - (CForall TySet - (CImp - (memberTerm - (CBound 0) - left') - (memberTerm - (CBound 0) - right'))) - Bottom -> - pure CFalsum - Top -> - pure (CImp CFalsum CFalsum) - Not _location proposition -> - notTerm - <$> lowerFormulaWith allowQuantified - resolveGlobal - environment - proposition - left `Implies` right -> - CImp - <$> lowerFormulaWith allowQuantified - resolveGlobal environment left - <*> lowerFormulaWith allowQuantified - resolveGlobal environment right - left `And` right -> - conjunctionTerm - <$> lowerFormulaWith allowQuantified - resolveGlobal environment left - <*> lowerFormulaWith allowQuantified - resolveGlobal environment right - left `Or` right -> - disjunctionTerm - <$> lowerFormulaWith allowQuantified - resolveGlobal environment left - <*> lowerFormulaWith allowQuantified - resolveGlobal environment right - left `Iff` right -> - CEq TyProp - <$> lowerFormulaWith allowQuantified - resolveGlobal environment left - <*> lowerFormulaWith allowQuantified - resolveGlobal environment right - Atomic _location predicate arguments -> - lowerApplication - resolveGlobal - environment - (SymbolPredicate predicate) - arguments - Quantified quantifier scope - | allowQuantified -> do - let variables = - nubOrd - [ variable - | B variable <- toList (fromScope scope) - ] - body = instantiate TermVar scope - extended <- extendVariables environment variables - lowered <- - lowerFormulaWith - allowQuantified - resolveGlobal - extended - body - pure - (case quantifier of - Universally -> - closeForalls (length variables) lowered - Existentially -> - closeExistentials (length variables) lowered) - _ -> - Left - (TypedInductiveUnsupportedExpression - "quantified and higher-order side conditions are not supported by the typed inductive slice") - -lowerTerm - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> InductiveEnvironment - -> Term - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -lowerTerm resolveGlobal environment = \case - TermVar variable -> - lookupEnvironment - variable - environment - EmptySet _location -> - pure (CIntrinsic Empty) - TermSymbol _location (SymbolInteger integer) [] -> - pure - (COpaqueInteger - (toInteger integer)) - TermSymbol _location symbol arguments -> - lowerApplication - resolveGlobal - environment - symbol - arguments - _ -> - Left - (TypedInductiveUnsupportedExpression - "higher-order source terms are not supported by the typed inductive slice") - -lowerApplication - :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> InductiveEnvironment - -> Symbol - -> [Expr] - -> Either - TypedInductiveError - (CanonicalTerm (InductiveGlobal global)) -lowerApplication resolveGlobal environment symbol arguments = do - arguments' <- - traverse - (lowerTerm - resolveGlobal - environment) - arguments - case dispatchFixedSetTerm symbol arguments' of - LoweredFixedSetTerm term -> - pure term - RejectedFixedSetTerm -> - Left - (TypedInductiveUnsupportedExpression - ("fixed source symbol is not a supported set term: " - <> symbolText symbol)) - NotFixedSetTerm -> do - SourceGlobal reference body <- - maybe - (Left - (TypedInductiveUnsupportedExpression - ("source symbol is not typed: " - <> symbolText symbol))) - Right - (resolveGlobal symbol) - pure - (foldl' - CApp - (maybe - (CGlobal reference) - frozenCoreTerm - body) - arguments') - -memberTerm - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -memberTerm = - apply2 (CIntrinsic Member) - -subsetTerm - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -subsetTerm left right = - CForall TySet - (CImp - (memberTerm - (CBound 0) - (shiftCanonicalTerm - 1 - 0 - left)) - (memberTerm - (CBound 0) - (shiftCanonicalTerm - 1 - 0 - right))) - -apply2 - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -apply2 function firstArgument secondArgument = - CApp - (CApp function firstArgument) - secondArgument - -notTerm - :: CanonicalTerm global - -> CanonicalTerm global -notTerm proposition = - CImp proposition CFalsum - -conjunctionList - :: [CanonicalTerm global] - -> Maybe (CanonicalTerm global) -conjunctionList = \case - [] -> - Nothing - firstTerm : remaining -> - Just - (foldl' - conjunctionTerm - firstTerm - remaining) - -disjunctionList - :: [CanonicalTerm global] - -> CanonicalTerm global -disjunctionList = \case - [] -> - CFalsum - firstTerm : remaining -> - foldl' - disjunctionTerm - firstTerm - remaining - -impliesIfNeeded - :: Maybe (CanonicalTerm global) - -> CanonicalTerm global - -> CanonicalTerm global -impliesIfNeeded = \case - Nothing -> - id - Just premise -> - CImp premise - -closeLambdas - :: Int - -> CanonicalTerm global - -> CanonicalTerm global -closeLambdas binderCount body = - foldl' - (\current _ -> - CLam TySet current) - body - [1 .. binderCount] - -closeForalls - :: Int - -> CanonicalTerm global - -> CanonicalTerm global -closeForalls binderCount body = - foldl' - (\current _ -> - CForall TySet current) - body - [1 .. binderCount] - -closeExistentials - :: Int - -> CanonicalTerm global - -> CanonicalTerm global -closeExistentials binderCount body = - foldl' - (\current _ -> - existentialTerm TySet current) - body - [1 .. binderCount] - -shiftCanonicalTerm - :: Natural - -> Natural - -> CanonicalTerm global - -> CanonicalTerm global -shiftCanonicalTerm amount cutoff = \case - CBound index - | index >= cutoff -> - CBound (index + amount) - | otherwise -> - CBound index - CGlobal global -> - CGlobal global - CIntrinsic intrinsic -> - CIntrinsic intrinsic - COpaqueInteger integer -> - COpaqueInteger integer - CApp function argument -> - CApp - (shiftCanonicalTerm - amount - cutoff - function) - (shiftCanonicalTerm - amount - cutoff - argument) - CLam binderType body -> - CLam binderType - (shiftCanonicalTerm - amount - (cutoff + 1) - body) - CFalsum -> - CFalsum - CImp premise conclusion -> - CImp - (shiftCanonicalTerm - amount - cutoff - premise) - (shiftCanonicalTerm - amount - cutoff - conclusion) - CEq operandType left right -> - CEq operandType - (shiftCanonicalTerm - amount - cutoff - left) - (shiftCanonicalTerm - amount - cutoff - right) - CForall binderType body -> - CForall binderType - (shiftCanonicalTerm - amount - (cutoff + 1) - body) - -atNatural :: Natural -> [a] -> Maybe a -atNatural _index [] = - Nothing -atNatural 0 (value : _rest) = - Just value -atNatural index (_value : rest) = - atNatural (index - 1) rest - -freezeClosedTarget - :: CanonicalTerm (InductiveGlobal global) - -> Either - TypedInductiveError - (FrozenCheckedCore (InductiveGlobal global)) -freezeClosedTarget = - first TypedInductiveCoreError - . checkCanonicalCore - (Just . inductiveGlobalType) - -symbolText :: Symbol -> Text -symbolText = \case - SymbolMixfix symbol -> - case mixfixMarker symbol of - Marker text -> - text - SymbolFun symbol -> - case lexicalItemSgPlMarker symbol of - Marker text -> - text - SymbolInteger integer -> - Text.pack (show integer) - SymbolPredicate predicate -> - case predicateObjectMarker predicate of - Marker text -> - text |