summaryrefslogtreecommitdiff
path: root/source/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/Checking/Typed/Inductive.hs
parent1a25421c2a168d420581358c8733fcd8f36f379b (diff)
Migrate to `Felix` namespaceHEADhotg
Diffstat (limited to 'source/Checking/Typed/Inductive.hs')
-rw-r--r--source/Checking/Typed/Inductive.hs4732
1 files changed, 0 insertions, 4732 deletions
diff --git a/source/Checking/Typed/Inductive.hs b/source/Checking/Typed/Inductive.hs
deleted file mode 100644
index eb6c0f7..0000000
--- a/source/Checking/Typed/Inductive.hs
+++ /dev/null
@@ -1,4732 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Direct checked lowering of the current one-carrier set-valued inductive
--- declaration.
-module Checking.Typed.Inductive
- ( DirectInductive(..)
- , DirectInductiveClause(..)
- , DirectInductiveCondition(..)
- , 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 Checking.Core
-import Checking.Exact.Vocabulary
-import Checking.Foundation
-import Checking.Kernel.Derivation
-import Checking.Kernel.Proof
-import Report.Location (Location)
-import Syntax.Internal
-
-import Control.Monad ((<=<), foldM)
-import Data.Bifunctor (first)
-import Data.List qualified as List
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Data.Vector (Vector)
-import Data.Vector qualified as Vector
-import Numeric.Natural (Natural)
-import Bound.Scope (fromScope, instantiate)
-import Bound.Var (Var(..))
-
-
-data DirectInductive = DirectInductive
- { directInductiveParams :: ![VarSymbol]
- , directInductiveDomain :: !Term
- , directInductiveClauses
- :: !(NonEmpty DirectInductiveClause)
- }
-
-data DirectInductiveClause = DirectInductiveClause
- { directClauseVariables :: ![VarSymbol]
- , directClauseConditions
- :: ![DirectInductiveCondition]
- , directClauseResult :: !Term
- }
-
-data DirectInductiveCondition
- = DirectSideCondition !Formula
- | DirectRecursiveCondition !Term !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 18:42:01 +0000