summaryrefslogtreecommitdiff
path: root/source/Felix/Checking/Typed/Inductive.hs
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2026-08-06 17:54:00 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2026-08-06 17:54:00 +0200
commit82328890108bae64b372b8d58620ebc62699de76 (patch)
tree575404c6b425c19259c0ded296f1c8ffb7ff0e2b /source/Felix/Checking/Typed/Inductive.hs
parent1a25421c2a168d420581358c8733fcd8f36f379b (diff)
Migrate to `Felix` namespaceHEADhotg
Diffstat (limited to 'source/Felix/Checking/Typed/Inductive.hs')
-rw-r--r--source/Felix/Checking/Typed/Inductive.hs4732
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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 20:25:05 +0000