opaque Lean.Meta.IndPredBelow.maxBackwardChainingDepth : Lean.Option Nat

structure Lean.Meta.IndPredBelow.Context : Type

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

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

structure Lean.Meta.IndPredBelow.Variables : Type

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

• target : Array Expr
• indVal : Array Expr
• params : Array Expr
• args : Array Expr
• motives : Array Expr
• innerType : Expr

instance Lean.Meta.IndPredBelow.instInhabitedVariables : Inhabited Variables

Equations

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

structure Lean.Meta.IndPredBelow.BrecOnVariables : Type

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

• params : Array FVarId
• motives : Array FVarId
• indices : Array FVarId
• witness : FVarId
• indHyps : Array FVarId

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.IndPredBelow.mkInductiveType (ctx : Context) (i : Nat) (indVal : InductiveVal) : MetaM InductiveType

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.IndPredBelow.getBelowIndices (ctorName : Name) : 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.

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

def Lean.Meta.IndPredBelow.mkBelowMatcher (matcherApp : MatcherApp) (belowMotive below : Expr) (idx : Nat) : MetaM (Expr × 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.

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

Equations

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

partial def Lean.Meta.IndPredBelow.mkBelowMatcher.convertToBelow (belowMotive : Expr) (indName : Name) (originalPattern : Match.Pattern) : MetaM (Array LocalDecl × 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 occurrences 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 constructor could be hidden inside of it.
• it is a variable. Here you we need to introduce a fresh variable of a different type.

partial def Lean.Meta.IndPredBelow.mkBelowMatcher.transformFields (belowMotive belowCtor : Expr) (indName : Name) (belowFieldOpts : Array (Option Match.Pattern)) : MetaM (Array LocalDecl × Array Match.Pattern)

partial def Lean.Meta.IndPredBelow.mkBelowMatcher.transformFields.loop (belowMotive : Expr) (indName : Name) (belowCtor : Expr) (belowFieldOpts : Array (Option Match.Pattern)) (belowFields : Array Match.Pattern) (additionalFVars : Array LocalDecl) : MetaM (Array LocalDecl × Array Match.Pattern)

def Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible : Match.Pattern → MetaM Match.Pattern

Equations

• Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible (Lean.Meta.Match.Pattern.inaccessible p) = pure (Lean.Meta.Match.Pattern.inaccessible p)
• Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible (Lean.Meta.Match.Pattern.var v) = pure (Lean.Meta.Match.Pattern.var v)
• Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible x✝ = do let __do_lift ← x✝.toExpr pure (Lean.Meta.Match.Pattern.inaccessible __do_lift)

def Lean.Meta.IndPredBelow.mkBelowMatcher.newMotive (matcherApp : MatcherApp) (belowType : Expr) (ys : Array Expr) : MetaM Expr

Equations

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

def Lean.Meta.IndPredBelow.findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM (Option (Expr × Nat))

Equations

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

def Lean.Meta.IndPredBelow.mkBelow (declName : Name) : MetaM Unit

Generates the auxiliary lemmas below and brecOn for a recursive inductive predicate. The current generator doesn't support nested predicates, but pattern-matching on them still works thanks to well-founded recursion.

Equations

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