Lean.Meta.IndPredBelow

Type

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

source

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

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

source

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

Lean.MetaM Lean.Meta.IndPredBelow.Context

Equations

Lean.Meta.IndPredBelow.mkContext declName = (fun motiveName mkHeader addMotives motiveType mkIndValConst => do let indVal ← Lean.getConstInfoInduct declName let typeInfos ← Array.mapM Lean.getConstInfoInduct (List.toArray indVal.all) let motiveTypes ← Array.mapM motiveType typeInfos let motives ← Array.mapIdxM motiveTypes fun j motive => do let a ← motiveName motiveTypes j.val pure (a, motive) let headers ← Array.mapM (mkHeader motives indVal.numParams) typeInfos let a ← pure (Array.map (fun a => a ++ `below) (List.toArray indVal.all)) pure { motives := motives, typeInfos := typeInfos, belowNames := a, headers := headers, numParams := indVal.numParams }) Lean.Meta.IndPredBelow.mkContext.motiveName Lean.Meta.IndPredBelow.mkContext.mkHeader Lean.Meta.IndPredBelow.mkContext.addMotives Lean.Meta.IndPredBelow.mkContext.motiveType Lean.Meta.IndPredBelow.mkContext.mkIndValConst

source

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

Lean.MetaM Lean.Name

Equations

Lean.Meta.IndPredBelow.mkContext.motiveName motiveTypes i = if Array.size motiveTypes > 1 then liftM (Lean.mkFreshUserName (Lean.Name.mkSimple (toString "motive_" ++ toString (Nat.succ i) ++ toString ""))) else liftM (Lean.mkFreshUserName (Lean.Name.mkSimple "motive"))

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.IndPredBelow.mkContext.mkHeader motives numParams indVal = do let header ← Lean.Meta.forallTelescopeReducing indVal.toConstantVal.type fun xs t => do let a ← Lean.Meta.mkArrow (Lean.mkAppN (Lean.Meta.IndPredBelow.mkContext.mkIndValConst indVal) xs) t Lean.Meta.withNewBinderInfos (Array.map (fun x => (Lean.Expr.fvarId! x, Lean.BinderInfo.implicit)) xs) (Lean.Meta.mkForallFVars xs a false true) Lean.Meta.IndPredBelow.mkContext.addMotives motives numParams header

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.IndPredBelow.mkContext.addMotives motives numParams init = Array.foldrM (fun x t => match x with | (motiveName, motive) => Lean.Meta.forallTelescopeReducing t fun xs s => do let motiveType ← Lean.Meta.instantiateForall motive (Array.ofSubarray (Array.toSubarray xs 0 numParams)) Lean.Meta.withLocalDecl motiveName Lean.BinderInfo.implicit motiveType fun motive => Lean.Meta.mkForallFVars (Array.insertAt xs numParams motive) s false true) init motives (Array.size motives)

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.IndPredBelow.mkContext.motiveType indVal = Lean.Meta.forallTelescopeReducing indVal.toConstantVal.type fun xs t => do let a ← Lean.Meta.mkArrow (Lean.mkAppN (Lean.Meta.IndPredBelow.mkContext.mkIndValConst indVal) xs) (Lean.mkSort Lean.levelZero) Lean.Meta.mkForallFVars xs a false true

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

Lean.Meta.IndPredBelow.mkCtorType ctx belowIdx originalCtor = (fun addMotives modifyBinders rebuild replaceTempVars checkCount mkBelowBinder mkMotiveBinder copyVarName => Lean.Meta.forallTelescopeReducing originalCtor.toConstantVal.type fun xs t => addHeaderVars { target := Array.ofSubarray (Array.toSubarray xs 0 ctx.numParams), indVal := #[], params := Array.ofSubarray (Array.toSubarray xs 0 ctx.numParams), args := let a := xs; Array.ofSubarray (Array.toSubarray a ctx.numParams (Array.size a)), motives := #[], innerType := t }) (Lean.Meta.IndPredBelow.mkCtorType.addHeaderVars ctx belowIdx originalCtor) (Lean.Meta.IndPredBelow.mkCtorType.addMotives ctx belowIdx originalCtor) (Lean.Meta.IndPredBelow.mkCtorType.modifyBinders ctx belowIdx originalCtor) (Lean.Meta.IndPredBelow.mkCtorType.rebuild ctx belowIdx originalCtor) (Lean.Meta.IndPredBelow.mkCtorType.replaceTempVars ctx) (Lean.Meta.IndPredBelow.mkCtorType.checkCount ctx) (Lean.Meta.IndPredBelow.mkCtorType.mkBelowBinder ctx) (Lean.Meta.IndPredBelow.mkCtorType.mkMotiveBinder ctx) Lean.Meta.IndPredBelow.mkCtorType.copyVarName

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

Lean.Meta.IndPredBelow.mkCtorType.addHeaderVars ctx belowIdx originalCtor vars = do let headersWithNames ← Array.mapIdxM ctx.headers fun idx header => pure (Array.getOp ctx.belowNames idx.val, fun x => pure header) Lean.Meta.withLocalDeclsD headersWithNames fun xs => Lean.Meta.IndPredBelow.mkCtorType.addMotives ctx belowIdx originalCtor { target := vars.target, indVal := xs, params := vars.params, args := vars.args, motives := vars.motives, innerType := vars.innerType }

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

Lean.Meta.IndPredBelow.mkCtorType.addMotives ctx belowIdx originalCtor vars = do let motiveBuilders ← Array.mapM (fun x => match x with | (motiveName, motiveType) => pure (motiveName, Lean.BinderInfo.implicit, fun x => Lean.Meta.instantiateForall motiveType vars.params)) ctx.motives Lean.Meta.withLocalDecls motiveBuilders fun xs => Lean.Meta.IndPredBelow.mkCtorType.modifyBinders ctx belowIdx originalCtor { target := vars.target ++ xs, indVal := vars.indVal, params := vars.params, args := vars.args, motives := xs, innerType := vars.innerType } 0

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

Lean.Meta.IndPredBelow.mkCtorType.rebuild ctx belowIdx originalCtor vars = Lean.Expr.withApp vars.innerType fun f args => let hApp := Lean.mkAppN (Lean.mkConst originalCtor.toConstantVal.name (List.map Lean.mkLevelParam (Array.getOp ctx.typeInfos 0).toConstantVal.levelParams)) (vars.params ++ vars.args); let innerType := Lean.mkAppN (Array.getOp vars.indVal belowIdx) (vars.params ++ vars.motives ++ Array.ofSubarray (let a := args; Array.toSubarray a ctx.numParams (Array.size a)) ++ #[hApp]); do let x ← Lean.Meta.mkForallFVars vars.target innerType false true pure (Lean.Meta.IndPredBelow.mkCtorType.replaceTempVars ctx vars x)

source

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

Lean.Expr

Equations

Lean.Meta.IndPredBelow.mkCtorType.replaceTempVars ctx vars ctor = let levelParams := List.map Lean.mkLevelParam (Array.getOp ctx.typeInfos 0).toConstantVal.levelParams; Lean.Expr.replaceFVars ctor vars.indVal (Array.map (fun indVal => Lean.mkConst indVal levelParams) ctx.belowNames)

source

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

Lean.MetaM Bool

Equations

Lean.Meta.IndPredBelow.mkCtorType.checkCount ctx domain = let run := fun x => StateRefT'.run x 0; do let discr ← run (Lean.Meta.transform domain (fun e => let _do_jp := fun y => pure (Lean.TransformStep.visit e); match Lean.Expr.constName? e with | some name => match Array.findIdx? ctx.typeInfos fun indVal => indVal.toConstantVal.name == name with | some idx => do let y ← modify fun a => a + 1 _do_jp y | x => do let y ← pure PUnit.unit _do_jp y | x => do let y ← pure PUnit.unit _do_jp y) fun e => pure (Lean.TransformStep.done e)) let x : Lean.Expr × Nat := discr match x with | (x, cnt) => let _do_jp := fun y => pure (cnt == 1); if cnt > 1 then do let y ← Lean.throwError (Lean.toMessageData "only arrows are allowed as premises. Multiple recursive occurrences detected:" ++ Lean.toMessageData (Lean.indentExpr domain) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

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

Lean.Meta.IndPredBelow.mkCtorType.mkBelowBinder ctx vars binder domain k = Lean.Meta.forallTelescopeReducing domain fun xs t => let fail := fun x => Lean.throwError (Lean.toMessageData "only trivial inductive applications supported in premises:" ++ Lean.toMessageData (Lean.indentExpr t) ++ Lean.toMessageData ""); Lean.Expr.withApp t fun f args => match Lean.Expr.constName? f with | some name => match Array.findIdx? ctx.typeInfos fun indVal => indVal.toConstantVal.name == name with | some idx => let indVal := Array.getOp ctx.typeInfos idx; let hApp := Lean.mkAppN binder xs; let t := Lean.mkAppN (Array.getOp vars.indVal idx) (vars.params ++ vars.motives ++ Array.ofSubarray (let a := args; Array.toSubarray a ctx.numParams (Array.size a)) ++ #[hApp]); do let newDomain ← Lean.Meta.mkForallFVars xs t false true let a ← Lean.Meta.IndPredBelow.mkCtorType.copyVarName (Lean.Expr.fvarId! binder) Lean.Meta.withLocalDecl a (Lean.Expr.binderInfo binder) newDomain (k idx) | x => fail () | x => fail ()

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

Lean.Meta.IndPredBelow.mkCtorType.mkMotiveBinder ctx vars indValIdx binder domain k = Lean.Meta.forallTelescopeReducing domain fun xs t => Lean.Expr.withApp t fun f args => let hApp := Lean.mkAppN binder xs; let t := Lean.mkAppN (Array.getOp vars.motives indValIdx) (Array.ofSubarray (let a := args; Array.toSubarray a ctx.numParams (Array.size a)) ++ #[hApp]); do let newDomain ← Lean.Meta.mkForallFVars xs t false true let a ← Lean.Meta.IndPredBelow.mkCtorType.copyVarName (Lean.Expr.fvarId! binder) Lean.Meta.withLocalDecl a (Lean.Expr.binderInfo binder) newDomain k

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

Lean.Meta.IndPredBelow.mkConstructor ctx i ctor = do let ctorInfo ← Lean.getConstInfoCtor ctor let name : Lean.Name := Lean.Name.updatePrefix ctor (Array.getOp ctx.belowNames i) let type ← Lean.Meta.IndPredBelow.mkCtorType ctx i ctorInfo pure { name := name, type := type }

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

Lean.Meta.IndPredBelow.mkInductiveType ctx i indVal = do let a ← List.mapM (Lean.Meta.IndPredBelow.mkConstructor ctx i.val) indVal.ctors pure { name := Array.getOp ctx.belowNames i.val, type := Array.getOp ctx.headers i.val, ctors := a }

source

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

Lean.MetaM Lean.Declaration

Equations

Lean.Meta.IndPredBelow.mkBelowDecl ctx = let lparams := (Array.getOp ctx.typeInfos 0).toConstantVal.levelParams; do let a ← Array.mapIdxM ctx.typeInfos (Lean.Meta.IndPredBelow.mkInductiveType ctx) pure (Lean.Declaration.inductDecl lparams (ctx.numParams + Array.size ctx.motives) (Array.toList a) (Array.getOp ctx.typeInfos 0).isUnsafe)

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

Lean.Meta.IndPredBelow.proveBrecOn ctx indVal type = (fun intros induction applyCtors introNPRec closeGoal => do let main ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar type Lean.Name.anonymous let discr ← intros (Lean.Expr.mvarId! main) let x : Lean.MVarId × Lean.Meta.IndPredBelow.BrecOnVariables := discr match x with | (m, vars) => do let discr ← applyIH m vars match discr with | [m] => do let ms ← induction m vars let ms ← applyCtors ms let a ← Lean.getOptions let maxDepth : Nat := Lean.Option.get a Lean.Meta.IndPredBelow.maxBackwardChainingDepth List.forM ms (closeGoal vars maxDepth) Lean.Meta.instantiateMVars main | x => Lean.throwError (Lean.toMessageData "applying the induction hypothesis should only return one goal")) (Lean.Meta.IndPredBelow.proveBrecOn.intros ctx indVal) Lean.Meta.IndPredBelow.proveBrecOn.applyIH (Lean.Meta.IndPredBelow.proveBrecOn.induction ctx indVal) Lean.Meta.IndPredBelow.proveBrecOn.applyCtors Lean.Meta.IndPredBelow.proveBrecOn.introNPRec Lean.Meta.IndPredBelow.proveBrecOn.closeGoal

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

Lean.Meta.IndPredBelow.proveBrecOn.intros ctx indVal m = do let discr ← Lean.Meta.introNP m indVal.numParams let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (params, m) => do let discr ← Lean.Meta.introNP m (Array.size ctx.motives) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (motives, m) => do let discr ← Lean.Meta.introNP m indVal.numIndices let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (indices, m) => do let discr ← Lean.Meta.intro1P m let x : Lean.FVarId × Lean.MVarId := discr match x with | (witness, m) => do let discr ← Lean.Meta.introNP m (Array.size ctx.motives) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (indHyps, m) => pure (m, { params := params, motives := motives, indices := indices, witness := witness, indHyps := indHyps })

source

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

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.IndPredBelow.proveBrecOn.applyIH m vars = do let a ← Array.findSomeM? vars.indHyps fun ih => tryCatch (do let a ← Lean.Meta.apply m (Lean.mkFVar ih) pure (some a)) fun ex => pure none match a with | some goals => pure goals | none => Lean.throwError (Lean.toMessageData "cannot apply induction hypothesis: " ++ Lean.toMessageData (Lean.MessageData.ofGoal m) ++ Lean.toMessageData "")

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

Lean.Meta.IndPredBelow.proveBrecOn.induction ctx indVal m vars = let params := Array.map Lean.mkFVar vars.params; let motives := Array.map Lean.mkFVar vars.motives; let levelParams := List.map Lean.mkLevelParam indVal.toConstantVal.levelParams; do let motives ← Array.mapIdxM ctx.motives fun idx x => match x with | (x, motive) => do let motive ← Lean.Meta.instantiateForall motive params Lean.Meta.forallTelescopeReducing motive fun xs x => Lean.Meta.mkLambdaFVars xs (Lean.mkAppN (Lean.mkConst (Array.getOp ctx.belowNames idx.val) levelParams) (params ++ motives ++ xs)) false true let recursorInfo ← Lean.getConstInfo (Lean.mkRecName indVal.toConstantVal.name) let recLevels : List Lean.Level := if Lean.ConstantInfo.numLevelParams recursorInfo > List.length levelParams then Lean.levelZero :: levelParams else levelParams let recursor ← pure (Lean.mkAppN (Lean.mkConst (Lean.ConstantInfo.name recursorInfo) recLevels) (params ++ motives)) Lean.Meta.apply m recursor

source

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

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.IndPredBelow.proveBrecOn.applyCtors ms = do let mss ← Array.mapIdxM (List.toArray ms) fun idx m => do let m ← Lean.Meta.IndPredBelow.proveBrecOn.introNPRec m let a ← Lean.Meta.getMVarType m Lean.Expr.withApp a fun below args => Lean.Meta.withMVarContext m (Lean.Expr.withApp (Array.back args) fun ctor ctorArgs => let ctorName := Lean.Name.updatePrefix (Lean.Expr.constName! ctor) (Lean.Expr.constName! below); let ctor := Lean.mkConst ctorName (Lean.Expr.constLevels! below); do let ctorInfo ← Lean.getConstInfoCtor ctorName let discr ← Lean.Meta.forallMetaTelescope ctorInfo.toConstantVal.type Lean.MetavarKind.natural let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (mvars, x, t) => let ctor := Lean.mkAppN ctor mvars; Lean.Meta.apply m ctor) pure (Array.foldr List.append [] mss (Array.size mss))

source

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

Lean.MetaM Lean.MVarId

source

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

Lean.MetaM Unit

Equations

Lean.Meta.IndPredBelow.proveBrecOn.closeGoal vars maxDepth m = do let a ← Lean.Meta.isExprMVarAssigned m if a = true then pure PUnit.unit else do let m ← Lean.Meta.IndPredBelow.proveBrecOn.introNPRec m let a ← Lean.Meta.IndPredBelow.backwardsChaining m maxDepth if a = true then pure PUnit.unit else Lean.Meta.withMVarContext m (Lean.throwError (Lean.toMessageData "couldn't solve by backwards chaining (" ++ Lean.toMessageData `Lean.Meta.IndPredBelow.maxBackwardChainingDepth ++ Lean.toMessageData " = " ++ Lean.toMessageData maxDepth ++ Lean.toMessageData "): " ++ Lean.toMessageData (Lean.MessageData.ofGoal m) ++ Lean.toMessageData ""))

source

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

Lean.MetaM Lean.Declaration

Equations

Lean.Meta.IndPredBelow.mkBrecOnDecl ctx idx = (fun mkType mkIH => do let type ← mkType let indVal : Lean.InductiveVal := Array.getOp ctx.typeInfos idx let name : Lean.Name := indVal.toConstantVal.name ++ Lean.Name.mkSimple Lean.brecOnSuffix let a ← Lean.Meta.IndPredBelow.proveBrecOn ctx indVal type pure (Lean.Declaration.thmDecl { toConstantVal := { name := name, levelParams := indVal.toConstantVal.levelParams, type := type }, value := a })) (Lean.Meta.IndPredBelow.mkBrecOnDecl.mkType ctx idx) (Lean.Meta.IndPredBelow.mkBrecOnDecl.mkIH ctx)

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.IndPredBelow.mkBrecOnDecl.mkType ctx idx = Lean.Meta.forallTelescopeReducing (Array.getOp ctx.headers idx) fun xs t => let params := Array.toSubarray xs 0 ctx.numParams; let motives := Subarray.toArray (Array.toSubarray xs ctx.numParams (ctx.numParams + Array.size ctx.motives)); let indices := let a := xs; Array.toSubarray a (ctx.numParams + Array.size ctx.motives) (Array.size a); do let motiveBinders ← Array.mapIdxM ctx.motives (Lean.Meta.IndPredBelow.mkBrecOnDecl.mkIH ctx (Array.ofSubarray params) motives) Lean.Meta.withLocalDeclsD motiveBinders fun ys => Lean.Meta.mkForallFVars (xs ++ ys) (Lean.mkAppN (Array.getOp motives idx) (Array.ofSubarray indices)) false true

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

Lean.Meta.IndPredBelow.mkBrecOnDecl.mkIH ctx params motives idx motive = let name := if Array.size ctx.motives > 1 then Lean.mkFreshUserName (Lean.Name.mkSimple (toString "ih_" ++ toString (Nat.succ idx.val) ++ toString "")) else Lean.mkFreshUserName (Lean.Name.mkSimple "ih"); do let ih ← Lean.Meta.instantiateForall motive.snd params let mkDomain : Array Lean.Expr → Lean.MetaM Lean.Expr := fun x => Lean.Meta.forallTelescopeReducing ih fun ys t => let levels := List.map Lean.mkLevelParam (Array.getOp ctx.typeInfos idx.val).toConstantVal.levelParams; let args := params ++ motives ++ ys; let premise := Lean.mkAppN (Lean.mkConst (Array.getOp ctx.belowNames idx.val) levels) args; let conclusion := Lean.mkAppN (Array.getOp motives idx.val) ys; do let a ← Lean.Meta.mkArrow premise conclusion Lean.Meta.mkForallFVars ys a false true let a ← liftM name pure (a, mkDomain)

source

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

Lean.MetaM (Array Nat)

Equations

Lean.Meta.IndPredBelow.getBelowIndices ctorName = (fun loop => do let ctorInfo ← Lean.getConstInfoCtor ctorName let belowCtorInfo ← Lean.getConstInfoCtor (Lean.Name.updatePrefix ctorName (ctorInfo.induct ++ `below)) let _ ← Lean.getConstInfoInduct belowCtorInfo.induct Lean.Meta.forallTelescopeReducing ctorInfo.toConstantVal.type fun xs t => loop xs belowCtorInfo.toConstantVal.type #[] 0 0) Lean.Meta.IndPredBelow.getBelowIndices.loop

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)

Equations

Lean.Meta.IndPredBelow.mkBelowMatcher matcherApp belowMotive below idx = (fun addBelowPattern convertToBelow transformFields toInaccessible newMotive => do let mkMatcherInput ← Lean.Meta.Match.getMkMatcherInputInContext matcherApp let discr ← Lean.Meta.forallBoundedTelescope mkMatcherInput.matchType (some mkMatcherInput.numDiscrs) fun xs t => do let discr ← Lean.Meta.IndPredBelow.belowType belowMotive xs idx let x : Lean.Name × Lean.Expr := discr match x with | (indName, belowType) => do let a ← liftM (Lean.mkFreshUserName `h_below) let matchType ← Lean.Meta.withLocalDeclD a belowType fun h_below => Lean.Meta.mkForallFVars (Array.push xs h_below) t false true let motive ← newMotive belowType xs pure (indName, Lean.Expr.replaceFVars belowType xs matcherApp.discrs, motive, matchType) let x : Lean.Name × Lean.Expr × Lean.Expr × Lean.Expr := discr match x with | (indName, belowType, motive, matchType) => do let lhss ← List.mapM (addBelowPattern indName) mkMatcherInput.lhss let alts ← Array.mapIdxM (Array.zip (List.toArray (List.zip mkMatcherInput.lhss lhss)) matcherApp.alts) fun idx x => match x with | ((oldLhs, lhs), alt) => Lean.Meta.withExistingLocalDecls (oldLhs.fvarDecls ++ lhs.fvarDecls) (Lean.Meta.lambdaTelescope alt fun xs t => let oldFVars := List.toArray oldLhs.fvarDecls; let fvars := Array.map (fun a => Lean.LocalDecl.toExpr a) (List.toArray lhs.fvarDecls); let xs := let _discr := Array.size fvars; match Array.size oldFVars, Array.size fvars with | 0, Nat.succ n => let a := xs; Array.ofSubarray (Array.toSubarray a 1 (Array.size a)) | x, x_1 => xs; let t := Lean.Expr.replaceFVars t (Array.ofSubarray (Array.toSubarray xs 0 (Array.size oldFVars))) (Array.ofSubarray (Array.toSubarray fvars 0 (Array.size oldFVars))); let cls := `Meta.IndPredBelow.match; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => do let newAlt ← Lean.Meta.mkLambdaFVars (Array.ofSubarray (Array.toSubarray fvars 0 (Array.size oldFVars)) ++ Array.ofSubarray (let a := xs; Array.toSubarray a (Array.size oldFVars) (Array.size a)) ++ Array.ofSubarray (let a := fvars; Array.toSubarray a (Array.size oldFVars) (Array.size a))) t false true let cls : Lean.Name := `Meta.IndPredBelow.match let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => pure newAlt if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "alt " ++ Lean.toMessageData idx ++ Lean.toMessageData ":\n" ++ Lean.toMessageData alt ++ Lean.toMessageData " ↦ " ++ Lean.toMessageData newAlt ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "xs = " ++ Lean.toMessageData xs ++ Lean.toMessageData "; oldFVars = " ++ Lean.toMessageData (Array.map (fun a => Lean.LocalDecl.toExpr a) oldFVars) ++ Lean.toMessageData "; fvars = " ++ Lean.toMessageData fvars ++ Lean.toMessageData "; new = " ++ Lean.toMessageData ((Array.toSubarray fvars 0 (Array.size oldFVars) ++ let a := xs; Array.toSubarray a (Array.size oldFVars) (Array.size a)) ++ let a := fvars; Array.toSubarray a (Array.size oldFVars) (Array.size a)) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y) let matcherName ← liftM (Lean.mkFreshUserName mkMatcherInput.matcherName) Lean.Meta.withExistingLocalDecls (List.foldl (fun s v => s ++ v.fvarDecls) [] lhss) do let r ← forIn lhss PUnit.unit fun lhs r => let cls := `Meta.IndPredBelow.match; do let a ← Lean.isTracingEnabledFor cls if a = true then do let a ← List.mapM (fun a => pure (Lean.Meta.Match.Pattern.toMessageData a)) lhs.patterns Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData a ++ Lean.toMessageData "") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit let res ← Lean.Meta.Match.mkMatcher { matcherName := matcherName, matchType := matchType, numDiscrs := mkMatcherInput.numDiscrs + 1, lhss := lhss } res.addMatcher Lean.Meta.check res.matcher let args : Array Lean.Expr := #[motive] ++ Array.push matcherApp.discrs below ++ alts let newApp : Lean.Expr := Lean.mkApp res.matcher motive let newApp : Lean.Expr := Lean.mkAppN newApp (Array.push matcherApp.discrs below) let newApp : Lean.Expr := Lean.mkAppN newApp alts pure (newApp, res.addMatcher)) (Lean.Meta.IndPredBelow.mkBelowMatcher.addBelowPattern belowMotive idx) (Lean.Meta.IndPredBelow.mkBelowMatcher.convertToBelow belowMotive) (Lean.Meta.IndPredBelow.mkBelowMatcher.transformFields belowMotive) Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible (Lean.Meta.IndPredBelow.mkBelowMatcher.newMotive matcherApp)

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

Lean.Meta.IndPredBelow.mkBelowMatcher.addBelowPattern belowMotive idx indName lhs = Lean.Meta.withExistingLocalDecls lhs.fvarDecls (let patterns := List.toArray lhs.patterns; let originalPattern := Array.getOp patterns idx; do let discr ← Lean.Meta.IndPredBelow.mkBelowMatcher.convertToBelow belowMotive indName (Array.getOp patterns idx) let x : Array Lean.LocalDecl × Lean.Meta.Match.Pattern := discr match x with | (fVars, belowPattern) => Lean.Meta.withExistingLocalDecls (Array.toList fVars) (let patterns := Array.push patterns belowPattern; do let a ← Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible originalPattern let patterns : Array Lean.Meta.Match.Pattern := Array.set! patterns idx a pure { ref := lhs.ref, fvarDecls := lhs.fvarDecls ++ Array.toList fVars, patterns := Array.toList patterns }))

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)

source

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

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

source

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

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

source

def Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible :

Lean.Meta.Match.Pattern → Lean.MetaM Lean.Meta.Match.Pattern

Equations

Lean.Meta.IndPredBelow.mkBelowMatcher.toInaccessible x = match x with | Lean.Meta.Match.Pattern.inaccessible p => pure (Lean.Meta.Match.Pattern.inaccessible p) | Lean.Meta.Match.Pattern.var v => pure (Lean.Meta.Match.Pattern.var v) | p => do let a ← Lean.Meta.Match.Pattern.toExpr p false pure (Lean.Meta.Match.Pattern.inaccessible a)

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.IndPredBelow.mkBelowMatcher.newMotive matcherApp belowType ys = Lean.Meta.lambdaTelescope matcherApp.motive fun xs t => let numDiscrs := Array.size matcherApp.discrs; do let a ← liftM (Lean.mkFreshUserName `h_below) let a_1 ← pure (Lean.Expr.replaceFVars belowType ys xs) Lean.Meta.withLocalDeclD a a_1 fun h_below => do let motive ← Lean.Meta.mkLambdaFVars (Array.ofSubarray (Array.toSubarray xs 0 numDiscrs) ++ #[h_below] ++ Array.ofSubarray (let a := xs; Array.toSubarray a numDiscrs (Array.size a))) t false true let cls : Lean.Name := `Meta.IndPredBelow.match let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => pure motive if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "motive := " ++ Lean.toMessageData motive ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Meta.IndPredBelow.findBelowIdx (xs : Array Lean.Expr) (motive : Lean.Expr) :

Lean.MetaM (Option (Lean.Expr × Nat))

Equations

Lean.Meta.IndPredBelow.findBelowIdx xs motive = Array.findSomeM? xs fun x => do let xTy ← Lean.Meta.inferType x Lean.Expr.withApp xTy fun f args => let _discr := Array.indexOf? xs x; match Lean.Expr.constName? f, Array.indexOf? xs x with | some name, some idx => do let a ← Lean.Meta.isInductivePredicate name if a = true then do let discr ← Lean.Meta.IndPredBelow.belowType motive xs idx.val let x : Lean.Name × Lean.Expr := discr match x with | (x, belowTy) => do let below ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar belowTy Lean.Name.anonymous tryCatch (let cls := `Meta.IndPredBelow.match; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.Expr × Nat)) := fun y => do let a ← Lean.Meta.IndPredBelow.backwardsChaining (Lean.Expr.mvarId! below) 10 if a = true then let cls := `Meta.IndPredBelow.match; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.Expr × Nat)) := fun y => do let a ← Array.anyM (Lean.Meta.isDefEq below) xs 0 (Array.size xs) if a = true then pure none else pure (some (below, idx.val)) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "Found below term in the local context: " ++ Lean.toMessageData below ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y else let cls := `Meta.IndPredBelow.match; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Option (Lean.Expr × Nat)) := fun y => pure none if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "could not find below term in the local context") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let a ← Lean.Meta.ppGoal (Lean.Expr.mvarId! below) let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData a ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y) fun x => pure none else pure none | x, x_1 => pure none

source

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

Lean.MetaM Unit

Equations

Lean.Meta.IndPredBelow.mkBelow declName = do let a ← Lean.Meta.isInductivePredicate declName if a = true then do let x ← Lean.getConstInfoInduct declName if x.isRec = true then do let ctx ← Lean.Meta.IndPredBelow.mkContext declName let decl ← Lean.Meta.IndPredBelow.mkBelowDecl ctx Lean.addDecl decl let cls : Lean.Name := `Meta.IndPredBelow let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Unit := fun y => do Array.forM Lean.mkCasesOn ctx.belowNames 0 (Array.size ctx.belowNames) let r ← let col := { start := 0, stop := Array.size ctx.typeInfos, step := 1 }; forIn col PUnit.unit fun i r => do tryCatch (do let decl ← Lean.Meta.IndPredBelow.mkBrecOnDecl ctx i Lean.addDecl decl) fun e => let cls := `Meta.IndPredBelow; do let a ← Lean.isTracingEnabledFor cls if a = true then Lean.addTrace cls (Lean.toMessageData "failed to prove brecOn for " ++ Lean.toMessageData (Array.getOp ctx.belowNames i) ++ Lean.toMessageData "\n" ++ Lean.toMessageData (Lean.Exception.toMessageData e) ++ Lean.toMessageData "") else pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "added " ++ Lean.toMessageData ctx.belowNames ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y else let cls := `Meta.IndPredBelow; do let a ← Lean.isTracingEnabledFor cls if a = true then Lean.addTrace cls (Lean.toMessageData "Not recursive") else pure PUnit.unit else let cls := `Meta.IndPredBelow; do let a ← Lean.isTracingEnabledFor cls if a = true then Lean.addTrace cls (Lean.toMessageData "Not inductive predicate") else pure PUnit.unit