diff options
Diffstat (limited to 'source/Felix/Checking/Typed/Inductive.hs')
| -rw-r--r-- | source/Felix/Checking/Typed/Inductive.hs | 4732 |
1 files changed, 4732 insertions, 0 deletions
diff --git a/source/Felix/Checking/Typed/Inductive.hs b/source/Felix/Checking/Typed/Inductive.hs new file mode 100644 index 0000000..4094083 --- /dev/null +++ b/source/Felix/Checking/Typed/Inductive.hs @@ -0,0 +1,4732 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Direct checked lowering of the current one-carrier set-valued inductive +-- declaration. +module Felix.Checking.Typed.Inductive + ( DirectInductive(..) + , DirectInductiveClause(..) + , DirectInductiveCondition(..) + , RecursiveCarrierContext + , RecursiveCarrierContextError(..) + , prepareRecursiveCarrierContext + , directRecursiveCarrierContext + , recursiveCarrierContextSymbols + , SourceGlobal(..) + , PreparedTypedInductive + , typedInductiveCarrierType + , typedInductiveCarrierBody + , typedInductiveGuardTargets + , PreparedTypedInductiveMonotonicity + , typedInductiveMonotonicities + , typedInductiveMonotonicityLocation + , typedInductiveMonotonicityTarget + , typedInductiveContextInventory + , PreparedTypedInductiveFact + , typedInductiveFacts + , typedInductiveFactMarker + , typedInductiveFactTarget + , typedInductiveFactRules + , typedInductiveFactRequiresMonotonicities + , typedInductiveFactDerivation + , prepareTypedClosedTerm + , prepareTypedClosedFormula + , prepareTypedInductive + , TypedInductiveError(..) + ) where + +import Base hiding (Empty) +import Felix.Checking.Core +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Foundation +import Felix.Checking.Kernel.Derivation +import Felix.Checking.Kernel.Proof +import Felix.Report.Location (Location) +import Felix.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 !RecursiveCarrierContext + +data RecursiveCarrierVariable + = RecursiveCarrierHole + | RecursiveCarrierSourceVariable !VarSymbol + deriving stock (Show, Eq, Ord) + +-- | A validated, capture-free one-hole carrier context in the same +-- first-order set-term fragment lowered by this module. The source carrier +-- application itself has been replaced, so the inductive symbol cannot +-- survive inside this value. +data RecursiveCarrierContext = RecursiveCarrierContext + !Location + !(ExprOf RecursiveCarrierVariable) + deriving stock (Show, Eq, Ord) + +data RecursiveCarrierContextError + = RecursiveCarrierWrongArguments !Location + | RecursiveCarrierUnsupportedContext !Location + deriving stock (Show, Eq) + +prepareRecursiveCarrierContext + :: FunctionSymbol + -> [VarSymbol] + -> Term + -> Either RecursiveCarrierContextError RecursiveCarrierContext +prepareRecursiveCarrierContext carrier parameters source = + RecursiveCarrierContext (exprLocation source) <$> go source + where + carrierSymbol = SymbolMixfix carrier + + go = \case + TermVar variable -> + pure + (TermVar + (RecursiveCarrierSourceVariable variable)) + TermSymbol location symbol arguments + | symbol == carrierSymbol -> + if sameCarrierArguments arguments parameters + then pure (TermVar RecursiveCarrierHole) + else Left (RecursiveCarrierWrongArguments location) + | otherwise -> + TermSymbol location symbol <$> traverse go arguments + unsupported -> + Left + (RecursiveCarrierUnsupportedContext + (exprLocation unsupported)) + + sameCarrierArguments arguments variables = + length arguments == length variables + && and + (zipWith + (\argument variable -> + argument == TermVar variable) + arguments + variables) + +recursiveCarrierContextSymbols + :: RecursiveCarrierContext + -> Set Symbol +recursiveCarrierContextSymbols + (RecursiveCarrierContext _location source) = + mentionedSymbols source + +directRecursiveCarrierContext :: Location -> RecursiveCarrierContext +directRecursiveCarrierContext location = + RecursiveCarrierContext location (TermVar RecursiveCarrierHole) + +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)) + !(Vector (PreparedTypedInductiveMonotonicity global)) + !(Vector (FrozenCheckedCore global)) + !(NonEmpty (PreparedTypedInductiveFact global)) + +data PreparedTypedInductiveMonotonicity global = + PreparedTypedInductiveMonotonicity + !Location + !(FrozenCheckedCore global) + +typedInductiveMonotonicities + :: PreparedTypedInductive global + -> Vector (PreparedTypedInductiveMonotonicity global) +typedInductiveMonotonicities + (PreparedTypedInductive + _carrierType + _body + _guards + monotonicities + _contexts + _facts) = + monotonicities + +typedInductiveMonotonicityLocation + :: PreparedTypedInductiveMonotonicity global + -> Location +typedInductiveMonotonicityLocation + (PreparedTypedInductiveMonotonicity location _target) = + location + +typedInductiveMonotonicityTarget + :: PreparedTypedInductiveMonotonicity global + -> FrozenCheckedCore global +typedInductiveMonotonicityTarget + (PreparedTypedInductiveMonotonicity _location target) = + target + +typedInductiveContextInventory + :: PreparedTypedInductive global + -> Vector (FrozenCheckedCore global) +typedInductiveContextInventory + (PreparedTypedInductive + _carrierType _body _guards _monotonicities contexts _facts) = + contexts + +data CheckedRecursiveCarrierContext global = + CheckedRecursiveCarrierContext + ![VarSymbol] + !(FrozenCheckedCore global) + +data PreparedInductiveSource global = PreparedInductiveSource + { preparedInductiveParams :: ![VarSymbol] + , preparedInductiveDomain :: !Term + , preparedInductiveClauses + :: !(NonEmpty (PreparedInductiveClause global)) + } + +data PreparedInductiveClause global = PreparedInductiveClause + { preparedClauseVariables :: ![VarSymbol] + , preparedClauseConditions + :: ![PreparedInductiveCondition global] + , preparedClauseResult :: !Term + } + +data PreparedInductiveCondition global + = PreparedSideCondition !Formula + | PreparedDirectRecursiveCondition + !Term + !(CheckedRecursiveCarrierContext global) + | PreparedNestedRecursiveCondition + !Term + !(CheckedRecursiveCarrierContext global) + !ImportIx + !(FrozenCheckedCore global) + +data PreparedInductiveGuard global + = PreparedFoundationGuard !FoundationAxiomTag + | PreparedImportedGuard + !ImportIx + !(FrozenCheckedCore global) + +typedInductiveCarrierType + :: PreparedTypedInductive global + -> CoreType +typedInductiveCarrierType + (PreparedTypedInductive + carrierType + _body + _guards + _monotonicities + _contexts + _facts) = + carrierType + +typedInductiveCarrierBody + :: PreparedTypedInductive global + -> FrozenCheckedCore global +typedInductiveCarrierBody + (PreparedTypedInductive + _carrierType + body + _guards + _monotonicities + _contexts + _facts) = + body + +typedInductiveGuardTargets + :: PreparedTypedInductive global + -> Vector (FrozenCheckedCore global) +typedInductiveGuardTargets + (PreparedTypedInductive + _carrierType + _body + guards + _monotonicities + _contexts + _facts) = + guards + +newtype PreparedTypedInductiveFact global = + PreparedTypedInductiveFact + ( Marker + , FrozenCheckedCore global + , NonEmpty KernelRuleTag + , Bool + , KernelDerivation global + ) + +typedInductiveFacts + :: PreparedTypedInductive global + -> NonEmpty (PreparedTypedInductiveFact global) +typedInductiveFacts + (PreparedTypedInductive + _carrierType + _body + _guards + _monotonicities + _contexts + facts) = + facts + +typedInductiveFactMarker + :: PreparedTypedInductiveFact global + -> Marker +typedInductiveFactMarker + (PreparedTypedInductiveFact + (marker, _target, _rule, _monotonicities, _derivation)) = + marker + +typedInductiveFactTarget + :: PreparedTypedInductiveFact global + -> FrozenCheckedCore global +typedInductiveFactTarget + (PreparedTypedInductiveFact + (_marker, target, _rule, _monotonicities, _derivation)) = + target + +typedInductiveFactRules + :: PreparedTypedInductiveFact global + -> NonEmpty KernelRuleTag +typedInductiveFactRules + (PreparedTypedInductiveFact + (_marker, _target, rules, _monotonicities, _derivation)) = + rules + +typedInductiveFactRequiresMonotonicities + :: PreparedTypedInductiveFact global + -> Bool +typedInductiveFactRequiresMonotonicities + (PreparedTypedInductiveFact + (_marker, _target, _rules, required, _derivation)) = + required + +typedInductiveFactDerivation + :: PreparedTypedInductiveFact global + -> KernelDerivation global +typedInductiveFactDerivation + (PreparedTypedInductiveFact + (_marker, _target, _rule, _monotonicities, 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 + guards <- + traverse + (prepareDirectGuardTarget + resolveGlobal + inductive) + (directInductiveClauses + inductive) + let preparedGuards = + assignGuardSources foundation + (NonEmpty.toList guards) + nextImport = + fromIntegral + (length + [ () + | PreparedImportedGuard{} <- preparedGuards + ]) + (preparedSource, monotonicities, contexts) <- + prepareInductiveSource + resolveGlobal + nextImport + inductive + carrierBody <- + prepareCarrierBody + resolveGlobal + preparedSource + facts <- + prepareFacts + foundation + resolveGlobal + marker + preparedSource + (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 + ]) + (Vector.fromList monotonicities) + (Vector.fromList contexts) + 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 monotonicities contexts facts) = + PreparedTypedInductive + carrierType + (mapFrozenGlobals transform body) + (mapFrozenGlobals transform <$> guards) + (mapMonotonicity transform <$> monotonicities) + (mapFrozenGlobals transform <$> contexts) + (mapPreparedFact transform <$> facts) + where + mapMonotonicity mapGlobal + (PreparedTypedInductiveMonotonicity location target) = + PreparedTypedInductiveMonotonicity + location + (mapFrozenGlobals mapGlobal target) + + mapPreparedFact mapGlobal + (PreparedTypedInductiveFact + (marker, target, rule, requiresMonotonicities, derivation)) = + PreparedTypedInductiveFact + ( marker + , mapFrozenGlobals mapGlobal target + , rule + , requiresMonotonicities + , mapKernelDerivationGlobals mapGlobal derivation + ) + +data MonotonicityInventory global = MonotonicityInventory + ![(FrozenCheckedCore global, ImportIx)] + !Natural + ![PreparedTypedInductiveMonotonicity global] + ![FrozenCheckedCore global] + +prepareInductiveSource + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Natural + -> DirectInductive + -> Either + TypedInductiveError + ( PreparedInductiveSource (InductiveGlobal global) + , [PreparedTypedInductiveMonotonicity (InductiveGlobal global)] + , [FrozenCheckedCore (InductiveGlobal global)] + ) +prepareInductiveSource resolveGlobal firstImport inductive = do + (final, clauses) <- + prepareClauses + (MonotonicityInventory [] firstImport [] []) + (NonEmpty.toList (directInductiveClauses inductive)) + let MonotonicityInventory + _targets _next monotonicities contexts = final + pure + ( PreparedInductiveSource + (directInductiveParams inductive) + (directInductiveDomain inductive) + (NonEmpty.fromList clauses) + , reverse monotonicities + , reverse contexts + ) + where + variablesFor clause = + directInductiveParams inductive + <> directClauseVariables clause + + prepareClauses inventory = \case + [] -> pure (inventory, []) + clause : remaining -> do + (afterClause, preparedClause) <- + prepareClause inventory clause + (final, preparedRemaining) <- + prepareClauses afterClause remaining + pure (final, preparedClause : preparedRemaining) + + prepareClause inventory clause = do + (next, conditions) <- + prepareConditions inventory clause + (directClauseConditions clause) + pure + ( next + , PreparedInductiveClause + (directClauseVariables clause) + conditions + (directClauseResult clause) + ) + + prepareConditions inventory _clause [] = + pure (inventory, []) + prepareConditions inventory clause (condition : remaining) = do + (next, prepared) <- + prepareCondition inventory clause condition + (final, preparedRemaining) <- + prepareConditions next clause remaining + pure (final, prepared : preparedRemaining) + + prepareCondition inventory _clause (DirectSideCondition formula) = + pure (inventory, PreparedSideCondition formula) + prepareCondition + (MonotonicityInventory targets next facts contexts) + clause + (DirectRecursiveCondition recursiveTerm sourceContext) = do + checkedContext <- + prepareRecursiveCarrierTemplate + resolveGlobal + (variablesFor clause) + sourceContext + let template = checkedRecursiveCarrierTemplate checkedContext + withContext currentFacts = + MonotonicityInventory + targets next currentFacts (template : contexts) + if recursiveCarrierContextIsDirect sourceContext + then pure + ( withContext facts + , PreparedDirectRecursiveCondition + recursiveTerm checkedContext + ) + else do + target <- + prepareRecursiveCarrierMonotonicityTarget + checkedContext + let RecursiveCarrierContext location _source = sourceContext + case List.lookup target targets of + Just index -> + pure + ( MonotonicityInventory + targets next facts (template : contexts) + , PreparedNestedRecursiveCondition + recursiveTerm checkedContext index target + ) + Nothing -> + let index = importIx next + in pure + ( MonotonicityInventory + ((target, index) : targets) + (next + 1) + (PreparedTypedInductiveMonotonicity + location target : facts) + (template : contexts) + , PreparedNestedRecursiveCondition + recursiveTerm checkedContext index target + ) + +checkedRecursiveCarrierTemplate + :: CheckedRecursiveCarrierContext global + -> FrozenCheckedCore global +checkedRecursiveCarrierTemplate + (CheckedRecursiveCarrierContext _variables template) = + template + +recursiveCarrierContextIsDirect :: RecursiveCarrierContext -> Bool +recursiveCarrierContextIsDirect + (RecursiveCarrierContext _location source) = + source == TermVar RecursiveCarrierHole + +prepareRecursiveCarrierTemplate + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> [VarSymbol] + -> RecursiveCarrierContext + -> Either + TypedInductiveError + (CheckedRecursiveCarrierContext (InductiveGlobal global)) +prepareRecursiveCarrierTemplate resolveGlobal variables context = do + body <- + buildUnderVariables emptyEnvironment variables \environment -> do + underHole <- shiftEnvironment environment + lowerRecursiveCarrierContext + resolveGlobal underHole (CBound 0) context + checked <- + first TypedInductiveCoreError + (checkCanonicalCore + (Just . inductiveGlobalType) + -- Transparent expansion may leave beta redexes. Freeze one + -- normalized template so routing, generated laws, and kernel + -- transport all see the same first-order shape. + (betaNormalizeCanonical + (closeLambdas (length variables + 1) body))) + pure (CheckedRecursiveCarrierContext variables checked) + +prepareRecursiveCarrierMonotonicityTarget + :: CheckedRecursiveCarrierContext (InductiveGlobal global) + -> Either + TypedInductiveError + (FrozenCheckedCore (InductiveGlobal global)) +prepareRecursiveCarrierMonotonicityTarget + context@(CheckedRecursiveCarrierContext variables _template) = do + target <- + buildUnderVariables emptyEnvironment variables \environment -> do + underSets <- shiftEnvironment =<< shiftEnvironment environment + left <- + instantiateRecursiveCarrier + underSets (CBound 1) context + right <- + instantiateRecursiveCarrier + underSets (CBound 0) context + pure + (CImp + (subsetTerm (CBound 1) (CBound 0)) + (subsetTerm left right)) + freezeClosedTarget + (closeForalls (length variables + 2) target) + +instantiateRecursiveCarrier + :: InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> CheckedRecursiveCarrierContext (InductiveGlobal global) + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +instantiateRecursiveCarrier environment replacement + context@(CheckedRecursiveCarrierContext variables _template) = do + arguments <- traverse (`lookupEnvironment` environment) variables + foldM instantiateLambda + (frozenCoreTerm (checkedRecursiveCarrierTemplate context)) + (arguments <> [replacement]) + where + instantiateLambda term argument = + case term of + CLam TySet body -> + pure (instantiateCanonical argument body) + _ -> + Left + (TypedInductiveUnsupportedExpression + "a checked recursive carrier context lost its set telescope") + +lowerRecursiveCarrierContext + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> RecursiveCarrierContext + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerRecursiveCarrierContext resolveGlobal environment replacement + (RecursiveCarrierContext _location source) = + go source + where + go = \case + TermVar RecursiveCarrierHole -> + pure replacement + TermVar (RecursiveCarrierSourceVariable variable) -> + lookupEnvironment variable environment + TermSymbol _location symbol arguments -> do + lowered <- traverse go arguments + lowerApplicationTerms resolveGlobal symbol lowered + _ -> + Left + (TypedInductiveUnsupportedExpression + "a validated recursive carrier context left the supported set-term fragment") + +prepareCarrierBody + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> PreparedInductiveSource (InductiveGlobal global) + -> Either + TypedInductiveError + (FrozenCheckedCore (InductiveGlobal global)) +prepareCarrierBody resolveGlobal inductive = do + body <- + buildUnderVariables + emptyEnvironment + (preparedInductiveParams + inductive) + (\env -> fixedPointTerm + resolveGlobal + inductive + env) + let closed = + closeLambdas + (length + (preparedInductiveParams + inductive)) + body + checked <- + first TypedInductiveCoreError + (checkCanonicalCore + (Just . inductiveGlobalType) + closed) + pure checked + +prepareDirectGuardTarget + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> DirectInductive + -> DirectInductiveClause + -> Either + TypedInductiveError + (FrozenCheckedCore (InductiveGlobal global)) +prepareDirectGuardTarget + resolveGlobal + inductive + clause = do + target <- + buildUnderVariables + emptyEnvironment + (directInductiveParams inductive + <> directClauseVariables clause) + (\environment -> do + domain <- + lowerTerm + resolveGlobal + environment + (directInductiveDomain + inductive) + conditions <- + traverse + (directConditionTerm + 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 + -> PreparedInductiveSource (InductiveGlobal global) + -> 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 + (preparedInductiveClauses + 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 + -> PreparedInductiveSource (InductiveGlobal global) + -> Natural + -> (PreparedInductiveGuard (InductiveGlobal global), PreparedInductiveClause (InductiveGlobal global)) + -> Either + TypedInductiveError + (PreparedTypedInductiveFact (InductiveGlobal global)) +prepareIntroductionFact + foundation + resolveGlobal + marker + inductive + clauseIndex + (guardSource, clause) = do + proof <- + proveUnderVariables + (rootProofContext + foundation + (Just . inductiveGlobalType)) + emptyEnvironment + (preparedInductiveParams inductive + <> preparedClauseVariables clause) + (\context environment -> do + domain <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedInductiveDomain + 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)) + (preparedClauseConditions + clause) + result <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedClauseResult + 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 + (preparedInductiveParams + inductive + <> preparedClauseVariables + clause) + guardProof) + guardPremiseProofs <- + sequence + [ case condition of + PreparedSideCondition _formula -> + pure premiseProof + PreparedDirectRecursiveCondition + recursiveTerm _context -> 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) + nested@PreparedNestedRecursiveCondition{} -> do + bound <- + first TypedInductiveProofError + (setLfpBoundProof + context + domain + operator) + recursiveElement <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedRecursiveTerm + nested) + transportNestedRecursiveMembership + context + environment + nested + fixedPoint + domain + recursiveElement + bound + premiseProof + | (condition, premiseProof) <- + zip + (preparedClauseConditions + 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 + (preparedClauseConditions clause) + then SetLfpBound :| [SetLfpFixed] + else SetLfpFixed :| []) + True + proof + where + isRecursiveCondition = \case + PreparedDirectRecursiveCondition{} -> True + PreparedNestedRecursiveCondition{} -> True + PreparedSideCondition{} -> 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 + -> PreparedInductiveSource (InductiveGlobal global) + -> Either + TypedInductiveError + (PreparedTypedInductiveFact (InductiveGlobal global)) +prepareDomainSubsetFact + foundation + resolveGlobal + marker + inductive = do + proof <- + proveUnderVariables + (rootProofContext + foundation + (Just . inductiveGlobalType)) + emptyEnvironment + (preparedInductiveParams + inductive) + (\context environment -> do + domain <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedInductiveDomain + inductive) + operator <- + checkedTerm context + =<< operatorTerm + resolveGlobal + inductive + environment + first TypedInductiveProofError + (setLfpBoundProof + context + domain + operator)) + preparedFact + (derivedMarker marker "dom_subset") + (SetLfpBound :| []) + False + proof + +prepareCasesFact + :: CheckedFoundation + -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Marker + -> PreparedInductiveSource (InductiveGlobal global) + -> Either + TypedInductiveError + (PreparedTypedInductiveFact (InductiveGlobal global)) +prepareCasesFact + foundation + resolveGlobal + marker + inductive = do + proof <- + proveUnderVariables + (rootProofContext + foundation + (Just . inductiveGlobalType)) + emptyEnvironment + (preparedInductiveParams + inductive) + (\parameterContext parameterEnvironment -> + forallIntroductionTyped + parameterContext + TySet + (\context result -> do + environment <- + shiftEnvironment + parameterEnvironment + domain <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedInductiveDomain + 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 :| []) + True + proof + +prepareInductionFact + :: CheckedFoundation + -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Marker + -> PreparedInductiveSource (InductiveGlobal global) + -> Either + TypedInductiveError + (PreparedTypedInductiveFact (InductiveGlobal global)) +prepareInductionFact + foundation + resolveGlobal + marker + inductive = do + proof <- + proveUnderVariables + (rootProofContext + foundation + (Just . inductiveGlobalType)) + emptyEnvironment + (preparedInductiveParams + 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 + (preparedInductiveDomain + 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 :| []) + True + 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 + -> Bool + -> BuiltProof (InductiveGlobal global) + -> Either + TypedInductiveError + (PreparedTypedInductiveFact (InductiveGlobal global)) +preparedFact marker rules requiresMonotonicities proof = do + target <- + maybe + (Left TypedInductiveProofRemainedOpen) + Right + (closeScopedCore + (builtProofStatement proof)) + pure + (PreparedTypedInductiveFact + ( marker + , target + , canonicalRules rules + , requiresMonotonicities + , 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> PreparedInductiveClause (InductiveGlobal global) + -> 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 + (preparedClauseVariables 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))) + -> PreparedInductiveClause (InductiveGlobal global) + -> 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) + (preparedClauseConditions + clause) + clauseResult <- + lowerTerm + resolveGlobal + environment + (preparedClauseResult 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> Either + TypedInductiveError + [CanonicalTerm (InductiveGlobal global)] +closureTerms + resolveGlobal + inductive + environment + subset = + traverse closureFor + (NonEmpty.toList + (preparedInductiveClauses + inductive)) + where + closureFor clause = do + clauseEnvironment <- + extendVariables + environment + (preparedClauseVariables clause) + let binderCount = + fromIntegral + (length + (preparedClauseVariables + clause)) + subset' = + shiftCanonicalTerm + binderCount + 0 + subset + conditions <- + traverse + (conditionTerm + resolveGlobal + clauseEnvironment + subset') + (preparedClauseConditions + clause) + result <- + lowerTerm + resolveGlobal + clauseEnvironment + (preparedClauseResult clause) + pure + (closeForalls + (length + (preparedClauseVariables + clause)) + (impliesIfNeeded + (conjunctionList conditions) + (memberTerm + result + subset'))) + +proveBoundedMonotonicity + :: CheckedFoundation + -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> PreparedInductiveSource (InductiveGlobal global) + -> ProofContext (InductiveGlobal global) + -> InductiveEnvironment + -> Either + TypedInductiveError + (BuiltProof (InductiveGlobal global)) +proveBoundedMonotonicity + _foundation + resolveGlobal + inductive + context + environment = do + domain <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedInductiveDomain + 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 + (preparedInductiveDomain + 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 + (preparedInductiveDomain + 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 + (preparedInductiveDomain + 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> 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 + (preparedInductiveClauses + 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))) + -> PreparedInductiveClause (InductiveGlobal global) + -> 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) + (preparedClauseConditions + clause) + clauseResult <- + lowerTerm + resolveGlobal + environment + (preparedClauseResult 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 + PreparedSideCondition _formula -> + pure conditionProof + PreparedDirectRecursiveCondition + recursiveTerm _context -> 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) + nested@PreparedNestedRecursiveCondition{} -> do + recursiveElement <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedRecursiveTerm nested) + subsetProof <- + subsetRelationHypothesis + context + candidateX + candidateY + domain + left <- checkedTerm context candidateX + right <- checkedTerm context candidateY + transportNestedRecursiveMembership + context + environment + nested + left + right + recursiveElement + subsetProof + conditionProof + | (condition, conditionProof) <- + zip + (preparedClauseConditions 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) + +preparedRecursiveTerm + :: PreparedInductiveCondition global + -> Term +preparedRecursiveTerm = \case + PreparedDirectRecursiveCondition term _context -> term + PreparedNestedRecursiveCondition term _context _index _target -> term + PreparedSideCondition{} -> + impossible "a side condition has no recursive element" + +transportNestedRecursiveMembership + :: ProofContext (InductiveGlobal global) + -> InductiveEnvironment + -> PreparedInductiveCondition (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> BuiltProof (InductiveGlobal global) + -> BuiltProof (InductiveGlobal global) + -> Either + TypedInductiveError + (BuiltProof (InductiveGlobal global)) +transportNestedRecursiveMembership + context + environment + condition + left + right + element + subsetProof + membership = do + monotonicity <- + nestedRecursiveMonotonicityProof + context environment condition left right subsetProof + implication <- + first TypedInductiveProofError + (forallEliminationProof + context monotonicity element) + first TypedInductiveProofError + (implicationEliminationProof + context implication membership) + +nestedRecursiveMonotonicityProof + :: ProofContext (InductiveGlobal global) + -> InductiveEnvironment + -> PreparedInductiveCondition (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> BuiltProof (InductiveGlobal global) + -> Either + TypedInductiveError + (BuiltProof (InductiveGlobal global)) +nestedRecursiveMonotonicityProof + context + environment + (PreparedNestedRecursiveCondition + _term + (CheckedRecursiveCarrierContext variables _template) + index + target) + left + right + subsetProof = do + theorem <- + first TypedInductiveProofError + (importedProof context index target) + specialized <- + eliminateWrittenForalls + context environment variables theorem + atLeft <- + first TypedInductiveProofError + (forallEliminationProof context specialized left) + atRight <- + first TypedInductiveProofError + (forallEliminationProof context atLeft right) + first TypedInductiveProofError + (implicationEliminationProof + context atRight subsetProof) +nestedRecursiveMonotonicityProof + _context _environment _condition _left _right _subsetProof = + Left + (TypedInductiveUnsupportedExpression + "nested carrier transport requires a monotonicity import") + +proveInductionCandidateSubset + :: ProofContext (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> Either + TypedInductiveError + (BuiltProof (InductiveGlobal global)) +proveInductionCandidateSubset + context fixedPoint predicate candidate subset = + proveSubset + context candidate subset + (\elementContext element membership -> do + fixedPointAtElement <- + first TypedInductiveCoreError + (weakenScopedCore + (Just . inductiveGlobalType) + TySet + fixedPoint) + predicateAtElement <- + first TypedInductiveCoreError + (weakenScopedCore + (Just . inductiveGlobalType) + TySet + predicate) + explicitMembership <- + checkedTerm elementContext + (memberTerm + (scopedCoreTerm element) + (apply2 + (CIntrinsic Sep) + (scopedCoreTerm fixedPointAtElement) + (scopedCoreTerm predicateAtElement))) + membership' <- + first TypedInductiveProofError + (conversionProof + elementContext membership explicitMembership) + characteristic <- + separationForward + elementContext + fixedPointAtElement + predicateAtElement + element + membership' + satisfies <- + first TypedInductiveProofError + (conjunctionRightProof + elementContext + (memberTerm + (scopedCoreTerm element) + (scopedCoreTerm fixedPointAtElement)) + (CApp + (scopedCoreTerm predicateAtElement) + (scopedCoreTerm element)) + characteristic) + expected <- + first TypedInductiveCoreError + (weakenScopedCore + (Just . inductiveGlobalType) + TySet + subset) + target <- + checkedTerm elementContext + (memberTerm + (scopedCoreTerm element) + (scopedCoreTerm expected)) + first TypedInductiveProofError + (conversionProof + elementContext satisfies target)) + +eliminateClauseWitnesses + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> PreparedInductiveClause (InductiveGlobal global) + -> 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 + (preparedClauseVariables 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> 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 + (preparedInductiveDomain + 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 + (preparedInductiveClauses + 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> Natural + -> PreparedInductiveClause (InductiveGlobal global) + -> 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)) + (preparedClauseConditions + clause) + clauseResult <- + lowerTerm + resolveGlobal + environment + (preparedClauseResult 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 + PreparedSideCondition _formula -> + pure conditionProof + PreparedDirectRecursiveCondition + recursiveTerm _context -> 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) + nested@PreparedNestedRecursiveCondition{} -> do + recursiveElement <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedRecursiveTerm nested) + fixedPoint' <- checkedTerm context fixedPoint + predicate' <- checkedTerm context predicate + candidate <- + checkedTerm context + (apply2 + (CIntrinsic Sep) + fixedPoint + predicate) + subset' <- checkedTerm context subset + candidateSubset <- + proveInductionCandidateSubset + context + fixedPoint' + predicate' + candidate + subset' + transportNestedRecursiveMembership + context + environment + nested + candidate + subset' + recursiveElement + candidateSubset + conditionProof + | (condition, conditionProof) <- + zip + (preparedClauseConditions 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 + (preparedClauseVariables 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> 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 + (preparedInductiveClauses + inductive)) + +clauseFormulaAt + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> CanonicalTerm (InductiveGlobal global) + -> PreparedInductiveClause (InductiveGlobal global) + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +clauseFormulaAt + resolveGlobal + environment + candidate + result + clause = do + clauseEnvironment <- + extendVariables + environment + (preparedClauseVariables clause) + let binderCount = + fromIntegral + (length + (preparedClauseVariables + clause)) + candidate' = + shiftCanonicalTerm binderCount 0 candidate + result' = + shiftCanonicalTerm binderCount 0 result + conditions <- + traverse + (conditionTerm + resolveGlobal + clauseEnvironment + candidate') + (preparedClauseConditions + clause) + clauseResult <- + lowerTerm + resolveGlobal + clauseEnvironment + (preparedClauseResult clause) + pure + (closeExistentials + (length + (preparedClauseVariables + 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +separationSetAt + resolveGlobal + inductive + environment + candidate = do + domain <- + lowerTerm + resolveGlobal + environment + (preparedInductiveDomain + 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))) + -> PreparedInductiveSource (InductiveGlobal global) + -> InductiveEnvironment + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +fixedPointTerm resolveGlobal inductive environment = do + domain <- + lowerTerm + resolveGlobal + environment + (preparedInductiveDomain + inductive) + operator <- + operatorTerm + resolveGlobal + inductive + environment + pure + (CApp + (CApp + (CIntrinsic ISetLfp) + domain) + operator) + +operatorTerm + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> PreparedInductiveSource (InductiveGlobal global) + -> InductiveEnvironment + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +operatorTerm resolveGlobal inductive parameterEnvironment = do + candidateEnvironment <- + shiftEnvironment parameterEnvironment + domain <- + lowerTerm + resolveGlobal + candidateEnvironment + (preparedInductiveDomain + inductive) + resultEnvironment <- + shiftEnvironment candidateEnvironment + clauses <- + traverse + (clausePredicateTerm + resolveGlobal + resultEnvironment) + (preparedInductiveClauses + inductive) + pure + (CLam TySet + (CApp + (CApp + (CIntrinsic Sep) + domain) + (CLam TySet + (disjunctionList + (NonEmpty.toList + clauses))))) + +clausePredicateTerm + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> PreparedInductiveClause (InductiveGlobal global) + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +clausePredicateTerm + resolveGlobal + resultEnvironment + clause = do + clauseEnvironment <- + extendVariables + resultEnvironment + (preparedClauseVariables clause) + let variableCount = + fromIntegral + (length + (preparedClauseVariables + clause)) + resultVariable = + CBound variableCount + candidate = + CBound (variableCount + 1) + conditions <- + traverse + (conditionTerm + resolveGlobal + clauseEnvironment + candidate) + (preparedClauseConditions + clause) + result <- + lowerTerm + resolveGlobal + clauseEnvironment + (preparedClauseResult + clause) + pure + (closeExistentials + (length + (preparedClauseVariables clause)) + (fromMaybe + (CEq + TySet + resultVariable + result) + (conjunctionList + (conditions + <> [CEq + TySet + resultVariable + result])))) + +directConditionTerm + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> DirectInductiveCondition + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +directConditionTerm resolveGlobal environment candidate = \case + DirectSideCondition formula -> + lowerFormula resolveGlobal environment formula + DirectRecursiveCondition term context -> do + carrier <- + betaNormalizeCanonical + <$> lowerRecursiveCarrierContext + resolveGlobal environment candidate context + memberTerm + <$> lowerTerm resolveGlobal environment term + <*> pure carrier + +conditionTerm + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> PreparedInductiveCondition (InductiveGlobal global) + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +conditionTerm resolveGlobal environment candidate = \case + PreparedSideCondition formula -> + lowerFormula + resolveGlobal + environment + formula + PreparedDirectRecursiveCondition term context -> do + carrier <- + instantiateRecursiveCarrier environment candidate context + memberTerm + <$> lowerTerm + resolveGlobal + environment + term + <*> pure carrier + PreparedNestedRecursiveCondition term context _index _target -> do + carrier <- + instantiateRecursiveCarrier environment candidate context + memberTerm + <$> lowerTerm resolveGlobal environment term + <*> pure carrier + +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 -> + lowerPredicateApplication + 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 + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerPredicateApplication + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> Symbol + -> [Expr] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerPredicateApplication resolveGlobal environment symbol arguments = do + arguments' <- + traverse + (lowerTerm + resolveGlobal + environment) + arguments + case classifyExactSymbol symbol of + ExactFixedPrimitive meaning -> + maybe + (lowerApplicationTerms resolveGlobal symbol arguments') + Right + (lowerFixedEqualityPredicate meaning arguments') + _ -> + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerApplicationTerms + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Symbol + -> [CanonicalTerm (InductiveGlobal global)] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerApplicationTerms resolveGlobal symbol 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 |