Lean.Meta.IndPredBelow

Type

motives : Array (Lean.Name × Lean.Expr)
typeInfos : Array Lean.InductiveVal
belowNames : Array Lean.Name
headers : Array Lean.Expr
numParams : Nat

The context used in the creation of the below scheme for inductive predicates.

structure Lean.Meta.IndPredBelow.Variables:

Type

target : Array Lean.Expr
indVal : Array Lean.Expr
params : Array Lean.Expr
args : Array Lean.Expr
motives : Array Lean.Expr
innerType : Lean.Expr

Collection of variables used to keep track of the positions of binders in the construction of below motives and constructors.

source

instance Lean.Meta.IndPredBelow.instInhabitedVariables:

Inhabited Lean.Meta.IndPredBelow.Variables

Equations

Lean.Meta.IndPredBelow.instInhabitedVariables = { default := { target := default, indVal := default, params := default, args := default, motives := default, innerType := default } }

source

structure Lean.Meta.IndPredBelow.BrecOnVariables:

Type

params : Array Lean.FVarId
motives : Array Lean.FVarId
indices : Array Lean.FVarId
witness : Lean.FVarId
indHyps : Array Lean.FVarId

Collection of variables used to keep track of the local context used in the brecOn proof.

source

def Lean.Meta.IndPredBelow.mkContext (declName : Lean.Name) :

Lean.MetaM Lean.Meta.IndPredBelow.Context

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkContext.motiveName (motiveTypes : Array Lean.Expr) (i : Nat) :

Lean.MetaM Lean.Name

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkContext.mkHeader (motives : Array (Lean.Name × Lean.Expr)) (numParams : Nat) (indVal : Lean.InductiveVal) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkContext.addMotives (motives : Array (Lean.Name × Lean.Expr)) (numParams : Nat) (init : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkContext.motiveType (indVal : Lean.InductiveVal) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkContext.mkIndValConst (indVal : Lean.InductiveVal) :

Lean.Expr

Equations

Lean.Meta.IndPredBelow.mkContext.mkIndValConst indVal = Lean.mkConst indVal.toConstantVal.name (List.map Lean.mkLevelParam indVal.toConstantVal.levelParams)

source

def Lean.Meta.IndPredBelow.mkCtorType (ctx : Lean.Meta.IndPredBelow.Context) (belowIdx : Nat) (originalCtor : Lean.ConstructorVal) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkCtorType.addHeaderVars (ctx : Lean.Meta.IndPredBelow.Context) (belowIdx : Nat) (originalCtor : Lean.ConstructorVal) (vars : Lean.Meta.IndPredBelow.Variables) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkCtorType.addMotives (ctx : Lean.Meta.IndPredBelow.Context) (belowIdx : Nat) (originalCtor : Lean.ConstructorVal) (vars : Lean.Meta.IndPredBelow.Variables) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

partial def Lean.Meta.IndPredBelow.mkCtorType.modifyBinders (ctx : Lean.Meta.IndPredBelow.Context) (belowIdx : Nat) (originalCtor : Lean.ConstructorVal) (vars : Lean.Meta.IndPredBelow.Variables) (i : Nat) :

Lean.MetaM Lean.Expr

source

def Lean.Meta.IndPredBelow.mkCtorType.rebuild (ctx : Lean.Meta.IndPredBelow.Context) (belowIdx : Nat) (originalCtor : Lean.ConstructorVal) (vars : Lean.Meta.IndPredBelow.Variables) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkCtorType.replaceTempVars (ctx : Lean.Meta.IndPredBelow.Context) (vars : Lean.Meta.IndPredBelow.Variables) (ctor : Lean.Expr) :

Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkCtorType.checkCount (ctx : Lean.Meta.IndPredBelow.Context) (domain : Lean.Expr) :

Lean.MetaM Bool

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkCtorType.mkBelowBinder (ctx : Lean.Meta.IndPredBelow.Context) (vars : Lean.Meta.IndPredBelow.Variables) (binder : Lean.Expr) (domain : Lean.Expr) {α : Type} (k : Nat → Lean.Expr → Lean.MetaM α) :

Lean.MetaM α

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkCtorType.mkMotiveBinder (ctx : Lean.Meta.IndPredBelow.Context) (vars : Lean.Meta.IndPredBelow.Variables) (indValIdx : Nat) (binder : Lean.Expr) (domain : Lean.Expr) {α : Type} (k : Lean.Expr → Lean.MetaM α) :

Lean.MetaM α

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkCtorType.copyVarName (oldName : Lean.FVarId) :

Lean.MetaM Lean.Name

Equations

Lean.Meta.IndPredBelow.mkCtorType.copyVarName oldName = do let binderDecl ← Lean.Meta.getLocalDecl oldName liftM (Lean.mkFreshUserName (Lean.LocalDecl.userName binderDecl))

source

def Lean.Meta.IndPredBelow.mkConstructor (ctx : Lean.Meta.IndPredBelow.Context) (i : Nat) (ctor : Lean.Name) :

Lean.MetaM Lean.Constructor

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkInductiveType (ctx : Lean.Meta.IndPredBelow.Context) (i : Fin (Array.size ctx.typeInfos)) (indVal : Lean.InductiveVal) :

Lean.MetaM Lean.InductiveType

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkBelowDecl (ctx : Lean.Meta.IndPredBelow.Context) :

Lean.MetaM Lean.Declaration

Equations

One or more equations did not get rendered due to their size.

source

partial def Lean.Meta.IndPredBelow.backwardsChaining (m : Lean.MVarId) (depth : Nat) :

Lean.MetaM Bool

source

def Lean.Meta.IndPredBelow.proveBrecOn (ctx : Lean.Meta.IndPredBelow.Context) (indVal : Lean.InductiveVal) (type : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.proveBrecOn.intros (ctx : Lean.Meta.IndPredBelow.Context) (indVal : Lean.InductiveVal) (m : Lean.MVarId) :

Lean.MetaM (Lean.MVarId × Lean.Meta.IndPredBelow.BrecOnVariables)

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.proveBrecOn.applyIH (m : Lean.MVarId) (vars : Lean.Meta.IndPredBelow.BrecOnVariables) :

Lean.MetaM (List Lean.MVarId)

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.proveBrecOn.induction (ctx : Lean.Meta.IndPredBelow.Context) (indVal : Lean.InductiveVal) (m : Lean.MVarId) (vars : Lean.Meta.IndPredBelow.BrecOnVariables) :

Lean.MetaM (List Lean.MVarId)

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.proveBrecOn.applyCtors (ms : List Lean.MVarId) :

Lean.MetaM (List Lean.MVarId)

Equations

One or more equations did not get rendered due to their size.

source

partial def Lean.Meta.IndPredBelow.proveBrecOn.introNPRec (m : Lean.MVarId) :

Lean.MetaM Lean.MVarId

source

def Lean.Meta.IndPredBelow.proveBrecOn.closeGoal (maxDepth : Nat) (m : Lean.MVarId) :

Lean.MetaM Unit

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkBrecOnDecl (ctx : Lean.Meta.IndPredBelow.Context) (idx : Nat) :

Lean.MetaM Lean.Declaration

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkBrecOnDecl.mkType (ctx : Lean.Meta.IndPredBelow.Context) (idx : Nat) :

Lean.MetaM Lean.Expr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkBrecOnDecl.mkIH (ctx : Lean.Meta.IndPredBelow.Context) (params : Array Lean.Expr) (motives : Array Lean.Expr) (idx : Fin (Array.size ctx.motives)) (motive : Lean.Name × Lean.Expr) :

Lean.MetaM (Lean.Name × (Array Lean.Expr → Lean.MetaM Lean.Expr))

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.getBelowIndices (ctorName : Lean.Name) :

Lean.MetaM (Array Nat)

Given a constructor name, find the indices of the corresponding below version thereof.

Equations

One or more equations did not get rendered due to their size.

source

partial def Lean.Meta.IndPredBelow.getBelowIndices.loop (xs : Array Lean.Expr) (rest : Lean.Expr) (belowIndices : Array Nat) (xIdx : Nat) (yIdx : Nat) :

Lean.MetaM (Array Nat)

source

def Lean.Meta.IndPredBelow.mkBelowMatcher (matcherApp : Lean.Meta.MatcherApp) (belowMotive : Lean.Expr) (below : Lean.Expr) (idx : Nat) :

Lean.MetaM (Lean.Expr × Lean.MetaM Unit)

This function adds an additional below discriminant to a matcher application. It is used for modifying the patterns, such that the structural recursion can use the new below predicate instead of the original one and thus be used prove structural recursion.

It takes as parameters:
- matcherApp: a matcher application
- belowMotive: the motive, that the `below` type should carry
- below: an expression from the local context that is the `below` version of a predicate
         and can be used for structural recursion
- idx: the index of the original predicate discriminant.

It returns:
- A matcher application as an expression
- A side-effect for adding the matcher to the environment

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Meta.IndPredBelow.mkBelowMatcher.addBelowPattern (belowMotive : Lean.Expr) (idx : Nat) (indName : Lean.Name) (lhs : Lean.Meta.Match.AltLHS) :

Lean.MetaM Lean.Meta.Match.AltLHS

Equations

One or more equations did not get rendered due to their size.

source

partial def Lean.Meta.IndPredBelow.mkBelowMatcher.convertToBelow (belowMotive : Lean.Expr) (indName : Lean.Name) (originalPattern : Lean.Meta.Match.Pattern) :

Lean.MetaM (Array Lean.LocalDecl × Lean.Meta.Match.Pattern)

this function changes the type of the pattern from the original type to the below version thereof. Most of the cases don't apply. In order to change the type and the pattern to be type correct, we don't simply recursively change all occurrences, but rather, we recursively change occurences of the constructor. As such there are only a few cases: - the pattern is a constructor from the original type. Here we need to: - replace the constructor - copy original recursive patterns and convert them to below and reintroduce them in the correct position - turn original recursive patterns inaccessible - introduce free variables as needed. - it is an as pattern. Here the contstructor could be hidden inside of it. - it is a variable. Here you we need to introduce a fresh variable of a different type.

source