diff --git a/src/Lean/Elab/PreDefinition/FixedParams.lean b/src/Lean/Elab/PreDefinition/FixedParams.lean new file mode 100644 index 0000000000..556223d7c1 --- /dev/null +++ b/src/Lean/Elab/PreDefinition/FixedParams.lean @@ -0,0 +1,496 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +prelude +import Lean.Elab.PreDefinition.Basic + +/-! +This module contains the logic for figuring out, given mutually recursive predefinitions, +which parameters are “fixed”. This used to be a simple task when we only considered a fixed prefix, +but becomes a quite involved task if we allow fixed parameters also later in the parameter list, +and possibly in a different order in different modules. + +The main components of this module are + + * The pure `Info` data type for the bookkeeping during analysis + * The `FixedParamPerm` type, with the analysis result for one function + (effectively a mask and a permutation) + * The `FixedParamPerms` data type, with the data for a whole recursive group. + * The `getFixedParamPerms` function that calculates the fixed parameters + * Various `MetaM` functions for bringing into scope fixed and varying paramters, assembling + argument lists etc. + +-/ + +namespace Lean.Elab.FixedParams + + +/-- +To determine which parameters in mutually recursive predefinitions are fixed, and how they +correspond to each other, we run an analysis that aggregates information in the `Info` data type. + +Abstractly, this represents +* a set `varying` of `(funIdx × paramIdx)` pairs known to be varying, initially empty +* a directed graph whose nodes are `(funIdx × paramIdx)` pairs, initially empty + +We find the largest set and graph that satisfies these rules: +* Every parameter has to be related to itself: `(funIdx, paramIdx) → (funIdx, paramIdx)`. +* whenever the function with index `caller` calls `callee` and the `argIdx`'s argument is reducibly + defeq to `paramIdx`, then we have an edge `(caller, paramIdx) → (callee, argIdx)`. +* whenever the function with index `caller` calls `callee` and the `argIdx`'s argument is not reducibly + defeq to any of the `caller`'s parameters, then `(callee, argIdx) ∈ varying`. +* If we have `(caller, paramIdx₁) → (callee, argIdx)` and `(caller, paramIdx₂) → (callee, argIdx)` + with `paramIdx₁ ≠ paramIdx₂`, then `(callee, argIdx) ∈ varying`. +* The graph is transitive +* If we have `(caller, paramIdx) → (callee, argIdx)` and `(caller, paramIdx) ∈ varying`, then + `(callee, argIdx) ∈ varying` +* If the type of `funIdx`’s parameter `paramIdx₂ depends on the `paramIdx₁` and + `(funIdx, paramIdx₁) ∈ varying`, then `(funIdx, paramIdx₁) ∈ varying` +* For structural recursion: The target and all its indices are `varying`. + (This is taking into account post-hoc, using `FixedParamPerms.erase`) + +Under the assumption that the predefintions indeed are mutually recursive, then the resulting graph, +restricted to the non-`varying` nodes, should partition into cliques that have one member from each +function. Every such clique becomes a fixed parameter. + +-/ +structure Info where + /- + The concrete data structure for set and graph exploits some of the invariants: + * Once we know a parameter is varying, it's incoming edges are irrelevant. + * There can be at most one incoming edge + + So we have + + * `graph[callee][argIdx] = none`: `(callee, argIdx) ∈ varying` + * `graph[callee][argIdx] = some a`: + * `(callee, argIdx) ∉ varying` (yet) and + * `a[callerIdx] = none`: we have no edge to `(callee, argIdx)` + * `a[callerIdx] = some paramIdx`: we have edge `(callerIdx, paramIdx) → (callee, argIdx)` + -/ + graph : Array (Array (Option (Array (Option Nat)))) + /-- + The dependency structure of the function parameter. + If `paramIdx₂ ∈ revDeps[funIdx][paraIdx₁]`, then the type of `paramIdx₂` depends on `parmaIdx₁` + -/ + revDeps : Array (Array (Array Nat)) + + +def Info.init (revDeps : Array (Array (Array Nat))) : Info where + graph := revDeps.map fun deps => + mkArray deps.size (some (mkArray revDeps.size none)) + revDeps + +def Info.addSelfCalls (info : Info) : Info := + { info with graph := info.graph.mapIdx fun funIdx paramInfos => + paramInfos.mapIdx fun paramIdx paramInfo? => + paramInfo?.map fun callers => + callers.set! funIdx (some paramIdx) } + +/-- +Is this parameter still plausibly a fixed parameter? +-/ +def Info.mayBeFixed (callerIdx paramIdx : Nat) (info : Info) : Bool := + info.graph[callerIdx]![paramIdx]!.isSome + +/-- +This parameter is varying. Set and propagate that information. +-/ +partial def Info.setVarying (funIdx paramIdx : Nat) (info : Info) : Info := Id.run do + let mut info : Info := info + if info.mayBeFixed funIdx paramIdx then + -- Set this as varying + info := { info with graph := info.graph.modify funIdx (·.set! paramIdx none) } + -- Propagate along edges for already observed calls + for otherFunIdx in [:info.graph.size] do + for otherParamIdx in [:info.graph[otherFunIdx]!.size] do + if let some otherParamInfo := info.graph[otherFunIdx]![otherParamIdx]! then + if otherParamInfo[funIdx]! = some paramIdx then + info := Info.setVarying otherFunIdx otherParamIdx info + -- Propagate along type dependencies edges + for dependingParam in info.revDeps[funIdx]![paramIdx]! do + info := Info.setVarying funIdx dependingParam info + info + +def Info.getCallerParam? (calleeIdx argIdx callerIdx : Nat) (info : Info) : Option Nat := + info.graph[calleeIdx]![argIdx]!.bind (·[callerIdx]!) + +/-- +We observe a possibly valid edge. +-/ +partial def Info.setCallerParam (calleeIdx argIdx callerIdx paramIdx : Nat) (info : Info) : Info := + if info.mayBeFixed calleeIdx argIdx then + if info.mayBeFixed callerIdx paramIdx then + if let some paramIdx' := info.getCallerParam? calleeIdx argIdx callerIdx then + -- We already have an etry + if paramIdx = paramIdx' then + -- all good + info + else + -- Inconsistent information + info.setVarying calleeIdx argIdx + else + -- Set the new entry + let info := { info with graph := info.graph.modify calleeIdx (·.modify argIdx (·.map (·.set! callerIdx (some paramIdx)))) } + Id.run do + -- Propagate information about the caller + let mut info : Info := info + if let some callerParamInfo := info.graph[callerIdx]![paramIdx]! then + for h : otherFunIdx in [:callerParamInfo.size] do + if let some otherParamIdx := callerParamInfo[otherFunIdx] then + info := info.setCallerParam calleeIdx argIdx otherFunIdx otherParamIdx + -- Propagate information about the callee + for otherFunIdx in [:info.graph.size] do + for otherArgIdx in [:info.graph[otherFunIdx]!.size] do + if let some otherArgsInfo := info.graph[otherFunIdx]![otherArgIdx]! then + if let some paramIdx' := otherArgsInfo[calleeIdx]! then + if paramIdx' = argIdx then + info := info.setCallerParam otherFunIdx otherArgIdx callerIdx paramIdx + + return info + else + -- Param not fixed, so argument isn't either + info.setVarying calleeIdx argIdx + else + info + +def Info.format (info : Info) : Format := Format.line.joinSep <| + info.graph.toList.map fun paramInfos => + (f!"• " ++ ·) <| f!" ".joinSep <| paramInfos.toList.map fun + | .none => f!"❌" + | .some callerInfos => .sbracket <| f!" ".joinSep <| callerInfos.toList.map fun + | Option.none => f!"?" + | .some idx => f!"#{idx+1}" + + +instance : ToFormat Info := ⟨Info.format⟩ + +end FixedParams + +open Lean Meta FixedParams + +def getParamRevDeps (preDefs : Array PreDefinition) : MetaM (Array (Array (Array Nat))) := do + preDefs.mapM fun preDef => + lambdaTelescope preDef.value (cleanupAnnotations := true) fun xs _ => do + let mut revDeps := #[] + for h : i in [:xs.size] do + let mut deps := #[] + for h : j in [i+1:xs.size] do + if (← dependsOn (← inferType xs[j]) xs[i].fvarId!) then + deps := deps.push j + revDeps := revDeps.push deps + pure revDeps + +def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info := do + let revDeps ← getParamRevDeps preDefs + let arities := revDeps.map (·.size) + let ref ← IO.mkRef (Info.init revDeps) + + ref.modify .addSelfCalls + + for h : callerIdx in [:preDefs.size] do + let preDef := preDefs[callerIdx] + lambdaTelescope preDef.value fun params body => do + assert! params.size = arities[callerIdx]! + + -- TODO: transform is overkill, a simple visit-all-subexpression that takes applications + -- as whole suffices + discard <| Meta.transform (skipConstInApp := true) body fun e => e.withApp fun f args => do + unless f.isConst do + return .continue + let n := f.constName! + let some calleeIdx := preDefs.findIdx? (·.declName = n) | return .continue + for argIdx in [:arities[calleeIdx]!] do + if (← ref.get).mayBeFixed calleeIdx argIdx then + if h : argIdx < args.size then + let arg := args[argIdx] + -- We have seen this before (or it is a self-call), so only check that one param + if let some paramIdx := (← ref.get).getCallerParam? calleeIdx argIdx callerIdx then + let param := params[paramIdx]! + unless (← withoutProofIrrelevance <| withReducible <| isDefEq param arg) do + trace[Elab.definition.fixedParams] "getFixedParams: notFixed {calleeIdx} {argIdx}:\nIn {e}\n{param} =/= {arg}" + ref.modify (Info.setVarying calleeIdx argIdx) + else + -- Try all parameters + let mut any := false + for h : paramIdx in [:params.size] do + if (← ref.get).mayBeFixed callerIdx paramIdx then + let param := params[paramIdx] + if (← withoutProofIrrelevance <| withReducible <| isDefEq param arg) then + ref.modify (Info.setCallerParam calleeIdx argIdx callerIdx paramIdx) + any := true + unless any do + trace[Elab.definition.fixedParams] "getFixedParams: notFixed {calleeIdx} {argIdx}:\nIn {e}\n{arg} not matched" + -- Argument is none of the plausible parameters, so it cannot be a fixed argument + ref.modify (Info.setVarying calleeIdx argIdx) + else + -- Underapplication + trace[Elab.definition.fixedParams] "getFixedParams: notFixed {calleeIdx} {argIdx}:\nIn {e}\ntoo few arguments for {argIdx}" + ref.modify (Info.setVarying calleeIdx argIdx) + return .continue + + let info ← ref.get + trace[Elab.definition.fixedParams] "getFixedParams:{info.format.indentD}" + return info + +/-- +For a given function, a mapping from its parameters to the (indices of the) fixed parameters of the +recursive group. +The length of the array is the arity of the function, as determined from its body, consistent +with the arity used by well-founded recursion. +For the first function, they appear in order; for other functions they may be reordered. +-/ +abbrev FixedParamPerm := Array (Option Nat) + +/-- +This data structure stores the result of the fixed parameter analysis. See `FixedParams.Info` for +details on the analysis. +-/ +structure FixedParamPerms where + /-- Number of fixed parameters -/ + numFixed : Nat + /-- + For each function in the clique, a mapping from its parameters to the fixed parameters. + For the first function, they appear in order; for other functions they may be reordered. + -/ + perms : Array FixedParamPerm + /-- + The dependencies among the parameters. See `FixedParams.Info.revDeps`. + We need this for the `FixedParamsPerm.erase` operation. + -/ + revDeps : Array (Array (Array Nat)) +deriving Inhabited, Repr + +def getFixedParamPerms (preDefs : Array PreDefinition) : MetaM FixedParamPerms := do + let info ← getFixedParamsInfo preDefs + lambdaTelescope preDefs[0]!.value fun xs _ => do + let paramInfos := info.graph[0]! + assert! xs.size = paramInfos.size + + let mut firstPerm := #[] + let mut numFixed := 0 + for paramIdx in [:xs.size], x in xs, paramInfo? in paramInfos do + if let some paramInfo := paramInfo? then + assert! paramInfo[0]! = some paramIdx + firstPerm := firstPerm.push (some numFixed) + numFixed := numFixed + 1 + else + firstPerm := firstPerm.push none + + let mut perms := #[firstPerm] + for h : funIdx in [1:info.graph.size] do + let paramInfos := info.graph[funIdx] + let mut perm := #[] + for paramInfo? in paramInfos do + if let some paramInfo := paramInfo? then + if let some firstParamIdx := paramInfo[0]! then + assert! firstPerm[firstParamIdx]!.isSome + perm := perm.push firstPerm[firstParamIdx]! + else + panic! "Incomplete paramInfo" + else + perm := perm.push none + perms := perms.push perm + + return { numFixed, perms, revDeps := info.revDeps } + +def FixedParamPerm.numFixed (perm : FixedParamPerm) : Nat := + perm.countP Option.isSome + +def FixedParamPerm.isFixed (perm : FixedParamPerm) (i : Nat) : Bool := + perm[i]?.join.isSome + +/-- +Brings the fixed parameters from `type`, which should the the type of the `funIdx`'s function, into +scope. +-/ +private partial def FixedParamPerm.forallTelescopeImpl (perm : FixedParamPerm) + (type : Expr) (k : Array Expr → MetaM α) : MetaM α := do + go 0 type (mkArray perm.numFixed (mkSort 0)) +where + go i type xs := do + match perm[i]? with + | .some (Option.some fixedParamIdx) => + forallBoundedTelescope type (some 1) (cleanupAnnotations := true) fun xs' type => do + assert! xs'.size = 1 + let x := xs'[0]! + assert! !(← inferType x).hasLooseBVars + assert! fixedParamIdx < xs.size + go (i + 1) type (xs.set! fixedParamIdx x) + | .some .none => + let type ← whnf type + assert! type.isForall + go (i + 1) type.bindingBody! xs + | .none => + k xs + +def FixedParamPerm.forallTelescope [MonadControlT MetaM n] [Monad n] + (perm : FixedParamPerm) (type : Expr) (k : Array Expr → n α) : n α := do + map1MetaM (fun k => perm.forallTelescopeImpl type k) k + + +/-- +If `type` is the type of the `funIdx`'s function, instantiate the fixed paramters. +-/ +def FixedParamPerm.instantiateForall (perm: FixedParamPerm) (type₀ : Expr) (xs : Array Expr) : MetaM Expr := do + assert! xs.size = perm.numFixed + let mask := perm.toList + go mask type₀ +where + go | [], type => pure type + | (.some fixedParamIdx)::mask, type => do + assert! fixedParamIdx < xs.size + go mask (← Meta.instantiateForall type #[xs[fixedParamIdx]!]) + | .none::mask, type => + forallBoundedTelescope type (some 1) fun ys type => do + assert! ys.size = 1 + mkForallFVars ys (← go mask type) + +/-- +If `value` is the body of the `funIdx`'s function, instantiate the fixed paramters. +Expects enough manifest lambdas to instantiate all fixed parameters, but can handle +eta-contracted definitions beyond that. +-/ +def FixedParamPerm.instantiateLambda (perm : FixedParamPerm) (value₀ : Expr) (xs : Array Expr) : MetaM Expr := do + assert! xs.size = perm.numFixed + let mask := perm.toList + go mask value₀ +where + go | [], value => pure value + | (.some fixedParamIdx)::mask, value => do + assert! fixedParamIdx < xs.size + go mask (← Meta.instantiateLambda value #[xs[fixedParamIdx]!]) + | .none::mask, value => + if mask.all Option.isNone then + -- Nothing left to do. Also helpful if we may encounter an eta-contracted value + return value + else + lambdaBoundedTelescope value 1 fun ys value => do + assert! ys.size = 1 + mkLambdaFVars ys (← go mask value) + +/-- +If `xs` are arguments to the `funIdx`'s function, pick only the fixed ones, and reorder appropriately. +Expects `xs` to match the arity of the function. +-/ +def FixedParamPerm.pickFixed (perm : FixedParamPerm) (xs : Array α) : Array α := Id.run do + assert! xs.size = perm.size + if h : xs.size = 0 then + pure #[] + else + let dummy := xs[0] + let ys := mkArray perm.numFixed dummy + go (perm.zip xs).toList ys +where + go | [], ys => return ys + | (.some fixedParamIdx, x)::xs, ys => do + assert! fixedParamIdx < ys.size + go xs (ys.set! fixedParamIdx x) + | (.none, _) :: perm, ys => + go perm ys + +/-- +If `xs` are arguments to the `funIdx`'s function, pick only the varying ones. +Unlike `pickFixed`, this function can handle over- or under-application. +-/ +def FixedParamPerm.pickVarying (perm : FixedParamPerm) (xs : Array α) : Array α := Id.run do + let mut ys := #[] + for h : i in [:xs.size] do + if perm[i]?.join.isNone then ys := ys.push xs[i] + pure ys + +/-- +Intersperses the fixed and varying parameters to be in the original parameter order. +Can handle over- or und-application (extra or missing varying args), as long +as there are all varying parameters that go before fixed parameters. +(We expect to always find all fixed parameters, else they woudn't be fixed parameters.) +-/ +partial def FixedParamPerm.buildArgs (perm : FixedParamPerm) (fixedArgs varyingArgs : Array α) : Array α := + assert! fixedArgs.size = perm.numFixed + go 0 0 #[] +where + go i j (xs : Array α) := + if _ : i < perm.size then + if let some fixedParamIdx := perm[i] then + if _ : fixedParamIdx < fixedArgs.size then + go (i + 1) j (xs.push fixedArgs[fixedParamIdx]) + else + panic! "FixedParams.buildArgs: too few fixed args" + else + if _ : j < varyingArgs.size then + go (i + 1) (j + 1) (xs.push varyingArgs[j]) + else + if perm[i:].all Option.isNone then + xs -- Under-application + else + panic! "FixedParams.buildArgs: too few varying args" + else + xs ++ varyingArgs[j:] -- (Possibly) over-application + +/-- +Are all fixed parameters a non-reordered prefix? +-/ +def FixedParamPerms.fixedArePrefix (fixedParamPerms : FixedParamPerms) : Bool := + fixedParamPerms.perms.all fun paramInfos => + paramInfos == + (Array.range fixedParamPerms.numFixed).map Option.some ++ + mkArray (paramInfos.size - fixedParamPerms.numFixed) .none + +/-- +If `xs` are the fixed parameters that are in scope, and `toErase` are, for each function, the +positions of arguments that must no longer be fixed parameters, then this function splits partitions +`xs` into those to keep and those to erase, and updates `FixedParams` accordingly. + +This is used in structural recursion, where we may discover that some fixed parameters are actually +indices and need to be treated as varying, including all parameters that depend on them. +-/ +def FixedParamPerms.erase (fixedParamPerms : FixedParamPerms) (xs : Array Expr) + (toErase : Array (Array Nat)) : (FixedParamPerms × Array Expr × Array FVarId) := Id.run do + assert! xs.all (·.isFVar) + assert! fixedParamPerms.numFixed = xs.size + assert! toErase.size = fixedParamPerms.perms.size + -- Calculate a mask on the fixed parameters of variables to erase + let mut mask := mkArray fixedParamPerms.numFixed false + for funIdx in [:toErase.size], paramIdxs in toErase, mapping in fixedParamPerms.perms do + for paramIdx in paramIdxs do + assert! paramIdx < mapping.size + if let some fixedParamIdx := mapping[paramIdx]! then + mask := mask.set! fixedParamIdx true + -- Take the transitive closure under under `fixedParamPerms.revDeps`. + let mut changed := true + while changed do + changed := false + for h : funIdx in [:fixedParamPerms.perms.size] do + for h : paramIdx₁ in [:fixedParamPerms.perms[funIdx].size] do + if let some fixedParamIdx₁ := fixedParamPerms.perms[funIdx][paramIdx₁] then + if mask[fixedParamIdx₁]! then + for paramIdx₂ in fixedParamPerms.revDeps[funIdx]![paramIdx₁]! do + if let some fixedParamIdx₂ := fixedParamPerms.perms[funIdx][paramIdx₂]! then + if !mask[fixedParamIdx₂]! then + mask := mask.set! fixedParamIdx₂ true + changed := true + -- Calculate reindexing map, variables to keep, variables to erase + let mut reindex := #[] + let mut fvarsToErase :=#[] + let mut toKeep :=#[] + for i in [:mask.size], erase in mask, x in xs do + if erase then + reindex := reindex.push none + fvarsToErase := fvarsToErase.push x.fvarId! + else + reindex := reindex.push (Option.some toKeep.size) + toKeep := toKeep.push x + let fixedParamPerms' : FixedParamPerms := { + numFixed := toKeep.size + perms := fixedParamPerms.perms.map (·.map (·.bind (reindex[·]!))) + revDeps := fixedParamPerms.revDeps + } + return (fixedParamPerms', toKeep, fvarsToErase) + +end Lean.Elab + +builtin_initialize + Lean.registerTraceClass `Elab.definition.fixedParams diff --git a/src/Lean/Elab/PreDefinition/Mutual.lean b/src/Lean/Elab/PreDefinition/Mutual.lean index a0266f2b54..38b4a7d4c4 100644 --- a/src/Lean/Elab/PreDefinition/Mutual.lean +++ b/src/Lean/Elab/PreDefinition/Mutual.lean @@ -26,24 +26,6 @@ where withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x => go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x) -def getFixedPrefix (preDefs : Array PreDefinition) : MetaM Nat := - withCommonTelescope preDefs fun xs vals => do - let resultRef ← IO.mkRef xs.size - for val in vals do - if (← resultRef.get) == 0 then return 0 - forEachExpr' val fun e => do - if preDefs.any fun preDef => e.isAppOf preDef.declName then - let args := e.getAppArgs - resultRef.modify (min args.size ·) - for arg in args, x in xs do - if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then - -- We continue searching if e's arguments are not a prefix of `xs` - return true - return false - else - return true - resultRef.get - def addPreDefsFromUnary (preDefs : Array PreDefinition) (preDefsNonrec : Array PreDefinition) (unaryPreDefNonRec : PreDefinition) : TermElabM Unit := do /- diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean index 367aad31ed..824ff0ddc3 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean @@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Rewrite import Lean.Meta.Tactic.Split import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Eqns +import Lean.Elab.PreDefinition.FixedParams import Lean.Meta.ArgsPacker.Basic import Init.Data.Array.Basic import Init.Internal.Order.Basic @@ -20,12 +21,13 @@ open Eqns structure EqnInfo extends EqnInfoCore where declNames : Array Name declNameNonRec : Name - fixedPrefixSize : Nat + fixedParamPerms : FixedParamPerms deriving Inhabited builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension -def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do +def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) + (fixedParamPerms : FixedParamPerms) : MetaM Unit := do preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName unless preDefs.all fun p => p.kind.isTheorem do unless (← preDefs.allM fun p => isProp p.type) do @@ -33,7 +35,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi modifyEnv fun env => preDefs.foldl (init := env) fun env preDef => eqnInfoExt.insert env preDef.declName { preDef with - declNames, declNameNonRec, fixedPrefixSize } + declNames, declNameNonRec, fixedParamPerms } private def deltaLHSUntilFix (declName declNameNonRec : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do let target ← mvarId.getType' diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean index a4cd82a705..eb8b5a289e 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean @@ -70,21 +70,21 @@ def deriveInduction (name : Name) : MetaM Unit := do let infos ← eqnInfo.declNames.mapM getConstInfoDefn -- First open up the fixed parameters everywhere - let e' ← lambdaBoundedTelescope infos[0]!.value eqnInfo.fixedPrefixSize fun xs _ => do + let e' ← eqnInfo.fixedParamPerms.perms[0]!.forallTelescope infos[0]!.type fun xs => do -- Now look at the body of an arbitrary of the functions (they are essentially the same -- up to the final projections) - let body ← instantiateLambda infos[0]!.value xs + let body ← eqnInfo.fixedParamPerms.perms[0]!.instantiateLambda infos[0]!.value xs -- The body should now be of the form of the form (fix … ).2.2.1 -- We strip the projections (if present) - let body' := PProdN.stripProjs body + let body' := PProdN.stripProjs body.eta -- TODO: Eta more carefully? let some fixApp ← whnfUntil body' ``fix - | throwError "Unexpected function body {body}" + | throwError "Unexpected function body {body}, could not whnfUntil fix" let_expr fix α instCCPOα F hmono := fixApp - | throwError "Unexpected function body {body'}" + | throwError "Unexpected function body {body'}, not an application of fix" let instCCPOs := CCPOProdProjs infos.size instCCPOα - let types ← infos.mapM (instantiateForall ·.type xs) + let types ← infos.mapIdxM (eqnInfo.fixedParamPerms.perms[·]!.instantiateForall ·.type xs) let packedType ← PProdN.pack 0 types let motiveTypes ← types.mapM (mkArrow · (.sort 0)) let motiveNames := numberNames motiveTypes.size "motive" @@ -135,7 +135,11 @@ def deriveInduction (name : Name) : MetaM Unit := do let packedConclusion ← PProdN.pack 0 <| ← motives.mapIdxM fun i motive => do let f ← mkConstWithLevelParams infos[i]!.name - return mkApp motive (mkAppN f xs) + let fEtaExpanded ← lambdaTelescope infos[i]!.value fun ys _ => + mkLambdaFVars ys (mkAppN f ys) + let fInst ← eqnInfo.fixedParamPerms.perms[i]!.instantiateLambda fEtaExpanded xs + let fInst := fInst.eta + return mkApp motive fInst let e' ← mkExpectedTypeHint e' packedConclusion let e' ← mkLambdaFVars hs e' let e' ← mkLambdaFVars adms e' @@ -228,9 +232,10 @@ def derivePartialCorrectness (name : Name) : MetaM Unit := do throwError "{name} is not defined by partial_fixpoint" let infos ← eqnInfo.declNames.mapM getConstInfoDefn + let fixedParamPerm0 := eqnInfo.fixedParamPerms.perms[0]! -- First open up the fixed parameters everywhere - let e' ← lambdaBoundedTelescope infos[0]!.value eqnInfo.fixedPrefixSize fun xs _ => do - let types ← infos.mapM (instantiateForall ·.type xs) + let e' ← fixedParamPerm0.forallTelescope infos[0]!.type fun xs => do + let types ← infos.mapIdxM (eqnInfo.fixedParamPerms.perms[·]!.instantiateForall ·.type xs) -- for `f : α → β → Option γ`, we expect a `motive : α → β → γ → Prop` let motiveTypes ← types.mapM fun type => diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean index 72d0f44f7c..eb16116d3a 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean @@ -18,33 +18,44 @@ open Monotonicity open Lean.Order -private def replaceRecApps (recFnNames : Array Name) (fixedPrefixSize : Nat) (f : Expr) (e : Expr) : MetaM Expr := do +private def replaceRecApps (recFnNames : Array Name) (fixedParamPerms : FixedParamPerms) (f : Expr) (e : Expr) : MetaM Expr := do + assert! recFnNames.size = fixedParamPerms.perms.size let t ← inferType f - return e.replace fun e => - if let some idx := recFnNames.findIdx? (e.isAppOfArity · fixedPrefixSize) then - some <| PProdN.proj recFnNames.size idx t f - else - none + return e.replace fun e => do + let fn := e.getAppFn + guard fn.isConst + let idx ← recFnNames.idxOf? fn.constName! + let args := e.getAppArgs + let varying := fixedParamPerms.perms[idx]!.pickVarying args + return mkAppN (PProdN.proj recFnNames.size idx t f) varying /-- For pretty error messages: Takes `F : (fun f => e)`, where `f` is the packed function, and replaces `f` in `e` with the user-visible constants, which are added to the environment temporarily. -/ -private def unReplaceRecApps {α} (preDefs : Array PreDefinition) (fixedArgs : Array Expr) +private def unReplaceRecApps {α} (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr) (F : Expr) (k : Expr → MetaM α) : MetaM α := do unless F.isLambda do throwError "Expected lambda:{indentExpr F}" withoutModifyingEnv do preDefs.forM addAsAxiom - let fns := preDefs.map fun d => - mkAppN (.const d.declName (d.levelParams.map mkLevelParam)) fixedArgs + let fns ← preDefs.mapIdxM fun funIdx preDef => do + let value ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs + lambdaTelescope value fun xs _ => + let args := fixedParamPerms.perms[funIdx]!.buildArgs fixedArgs xs + let call := mkAppN (.const preDef.declName (preDef.levelParams.map mkLevelParam)) args + mkLambdaFVars (etaReduce := true) xs call let packedFn ← PProdN.mk 0 fns let e ← lambdaBoundedTelescope F 1 fun f e => do let f := f[0]! -- Replace f with calls to the constants - let e := e.replace fun e => do if e == f then return packedFn else none - -- And reduce projection redexes + let e := e.replace fun e => do + if e == f then return packedFn else none + -- And reduce projection and beta redexes + -- (This is a bit blunt; we could try harder to only replace the projection and beta-redexes + -- introduced above) let e ← PProdN.reduceProjs e + let e ← Core.betaReduce e pure e k e @@ -81,15 +92,12 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do mkAppOptM ``FlatOrder.instCCPO #[none, classicalWitness] mkLambdaFVars xs inst - let fixedPrefixSize ← Mutual.getFixedPrefix preDefs - trace[Elab.definition.partialFixpoint] "fixed prefix size: {fixedPrefixSize}" - let declNames := preDefs.map (·.declName) - - forallBoundedTelescope preDefs[0]!.type fixedPrefixSize fun fixedArgs _ => do + let fixedParamPerms ← getFixedParamPerms preDefs + fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun fixedArgs => do -- ∀ x y, CCPO (rᵢ x y) - let ccpoInsts := ccpoInsts.map (·.beta fixedArgs) - let types ← preDefs.mapM (instantiateForall ·.type fixedArgs) + let ccpoInsts ← ccpoInsts.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda · fixedArgs) + let types ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateForall ·.type fixedArgs) -- (∀ x y, r₁ x y) ×' (∀ x y, r₂ x y) let packedType ← PProdN.pack 0 types @@ -108,7 +116,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do -- Error reporting hook, presenting monotonicity errors in terms of recursive functions let failK {α} f (monoThms : Array Name) : MetaM α := do - unReplaceRecApps preDefs fixedArgs f fun t => do + unReplaceRecApps preDefs fixedParamPerms fixedArgs f fun t => do let extraMsg := if monoThms.isEmpty then m!"" else m!"Tried to apply {.andList (monoThms.toList.map (m!"'{.ofConstName ·}'"))}, but failed.\n\ Possible cause: A missing `{.ofConstName ``MonoBind}` instance.\n\ @@ -122,13 +130,13 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do -- Adjust the body of each function to take the other functions as a -- (packed) parameter - let Fs ← preDefs.mapM fun preDef => do - let body ← instantiateLambda preDef.value fixedArgs + let Fs ← preDefs.mapIdxM fun funIdx preDef => do + let body ← fixedParamPerms.perms[funIdx]!.instantiateLambda preDef.value fixedArgs withLocalDeclD (← mkFreshUserName `f) packedType fun f => do let body' ← withoutModifyingEnv do -- replaceRecApps needs the constants in the env to typecheck things preDefs.forM (addAsAxiom ·) - replaceRecApps declNames fixedPrefixSize f body + replaceRecApps declNames fixedParamPerms f body mkLambdaFVars #[f] body' -- Construct and solve monotonicity goals for each function separately @@ -160,7 +168,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do trace[Elab.definition.partialFixpoint] "packedValue: {packedValue}" let declName := - if preDefs.size = 1 then + if preDefs.size = 1 && fixedParamPerms.fixedArePrefix then preDefs[0]!.declName else preDefs[0]!.declName ++ `mutual @@ -170,17 +178,22 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do declName := declName type := packedType' value := packedValue'} + let preDefsNonrec ← preDefs.mapIdxM fun fidx preDef => do - let us := preDefNonRec.levelParams.map mkLevelParam - let value := mkConst preDefNonRec.declName us - let value := mkAppN value fixedArgs - let value := PProdN.proj preDefs.size fidx packedType value - let value ← mkLambdaFVars fixedArgs value - pure { preDef with value } + forallBoundedTelescope preDef.type fixedParamPerms.perms[fidx]!.size fun params _ => do + let fixed := fixedParamPerms.perms[fidx]!.pickFixed params + let varying := fixedParamPerms.perms[fidx]!.pickVarying params + let us := preDefNonRec.levelParams.map mkLevelParam + let value := mkConst preDefNonRec.declName us + let value := mkAppN value fixed + let value := PProdN.proj preDefs.size fidx packedType value + let value := mkAppN value varying + let value ← mkLambdaFVars (etaReduce := true) params value + pure { preDef with value } Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec let preDefs ← Mutual.cleanPreDefs preDefs - PartialFixpoint.registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize + PartialFixpoint.registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms Mutual.addPreDefAttributes preDefs end Lean.Elab diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 91ad989c0c..53a6a37e76 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -155,7 +155,8 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : try toBelow below recArgInfo.indGroupInst.params.size positions fnIdx recArg catch _ => throwError "failed to eliminate recursive application{indentExpr e}" -- We don't pass the fixed parameters, the indices and the major arg to `f`, only the rest - let (_, fArgs) := recArgInfo.pickIndicesMajor args[recArgInfo.numFixed:] + let ys := recArgInfo.fixedParamPerm.pickVarying args + let (_, fArgs) := recArgInfo.pickIndicesMajor ys let fArgs ← fArgs.mapM (replaceRecApps recArgInfos positions below ·) return mkAppN f fArgs else diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index b3e039ae9f..82f2ea471b 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Simp.Main import Lean.Meta.Tactic.Apply import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Eqns +import Lean.Elab.PreDefinition.FixedParams import Lean.Elab.PreDefinition.Structural.Basic namespace Lean.Elab @@ -21,7 +22,7 @@ namespace Structural structure EqnInfo extends EqnInfoCore where recArgPos : Nat declNames : Array Name - numFixed : Nat + fixedParamPerms : FixedParamPerms deriving Inhabited private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do @@ -85,10 +86,10 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) := builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat) - (numFixed : Nat) : CoreM Unit := do + (fixedParamPerms : FixedParamPerms) : CoreM Unit := do ensureEqnReservedNamesAvailable preDef.declName modifyEnv fun env => eqnInfoExt.insert env preDef.declName - { preDef with recArgPos, declNames, numFixed } + { preDef with recArgPos, declNames, fixedParamPerms } def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do if let some info := eqnInfoExt.find? (← getEnv) declName then diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index 786af4b14a..754016a5d6 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Joachim Breitner -/ prelude import Lean.Elab.PreDefinition.TerminationMeasure +import Lean.Elab.PreDefinition.FixedParams import Lean.Elab.PreDefinition.Structural.Basic import Lean.Elab.PreDefinition.Structural.RecArgInfo @@ -58,9 +59,10 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM ( Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs various sanity checks on the parameter (is it even of inductive type etc). -/ -def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do +def getRecArgInfo (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) (i : Nat) : MetaM RecArgInfo := do + assert! fixedParamPerm.size = xs.size if h : i < xs.size then - if i < numFixed then + if fixedParamPerm.isFixed i then throwError "it is unchanged in the recursive calls" let x := xs[i] let localDecl ← getFVarLocalDecl x @@ -79,16 +81,14 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : else if !indIndices.allDiff then throwError "its type {indInfo.name} is an inductive family and indices are not pairwise distinct{indentExpr xType}" else - let indexMinPos := getIndexMinPos xs indIndices - let numFixed := if indexMinPos < numFixed then indexMinPos else numFixed - let ys := xs[numFixed:] + let ys := fixedParamPerm.pickVarying xs match (← hasBadIndexDep? ys indIndices) with | some (index, y) => throwError "its type {indInfo.name} is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}" | none => match (← hasBadParamDep? ys indParams) with | some (indParam, y) => - throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich does not come before the varying parameters and before the indices of the recursion parameter." + throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich is not fixed." | none => let indAll := indInfo.all.toArray let .some indIdx := indAll.idxOf? indInfo.name | panic! "{indInfo.name} not in {indInfo.all}" @@ -98,7 +98,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) : levels := us params := indParams } return { fnName := fnName - numFixed := numFixed + fixedParamPerm := fixedParamPerm recArgPos := i indicesPos := indicesPos indGroupInst := indGroupInst @@ -115,25 +115,27 @@ The `xs` are the fixed parameters, `value` the body with the fixed prefix instan Takes the optional user annotation into account (`termMeasure?`). If this is given and the measure is unsuitable, throw an error. -/ -def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr) - (termMeasure? : Option TerminationMeasure) : MetaM (Array RecArgInfo × MessageData) := do +def getRecArgInfos (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) + (value : Expr) (termMeasure? : Option TerminationMeasure) : MetaM (Array RecArgInfo × MessageData) := do lambdaTelescope value fun ys _ => do if let .some termMeasure := termMeasure? then -- User explicitly asked to use a certain measure, so throw errors eagerly let recArgInfo ← withRef termMeasure.ref do mapError (f := (m!"cannot use specified measure for structural recursion:{indentD ·}")) do - getRecArgInfo fnName xs.size (xs ++ ys) (← termMeasure.structuralArg) + let args := fixedParamPerm.buildArgs xs ys + getRecArgInfo fnName fixedParamPerm args (← termMeasure.structuralArg) return (#[recArgInfo], m!"") else + let args := fixedParamPerm.buildArgs xs ys let mut recArgInfos := #[] let mut report : MessageData := m!"" -- No `termination_by`, so try all, and remember the errors - for idx in [:xs.size + ys.size] do + for idx in [:args.size] do try - let recArgInfo ← getRecArgInfo fnName xs.size (xs ++ ys) idx + let recArgInfo ← getRecArgInfo fnName fixedParamPerm args idx recArgInfos := recArgInfos.push recArgInfo catch e => - report := report ++ (m!"Not considering parameter {← prettyParam (xs ++ ys) idx} of {fnName}:" ++ + report := report ++ (m!"Not considering parameter {← prettyParam args idx} of {fnName}:" ++ indentD e.toMessageData) ++ "\n" trace[Elab.definition.structural] "getRecArgInfos report: {report}" return (recArgInfos, report) @@ -211,7 +213,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr) let indicesPos := indIndices.map fun index => match (xs++ys).idxOf? index with | some i => i | none => unreachable! return .some { fnName := recArgInfo.fnName - numFixed := recArgInfo.numFixed + fixedParamPerm := recArgInfo.fixedParamPerm recArgPos := recArgInfo.recArgPos indicesPos := indicesPos indGroupInst := group @@ -232,13 +234,13 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) := some (go 0 #[]) -def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr) - (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do +def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs : Array Expr) + (values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do let mut report := m!"" -- Gather information on all possible recursive arguments let mut recArgInfoss := #[] - for fnName in fnNames, value in values, termMeasure? in termMeasure?s do - let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termMeasure? + for fnName in fnNames, value in values, termMeasure? in termMeasure?s, fixedParamPerm in fixedParamPerms.perms do + let (recArgInfos, thisReport) ← getRecArgInfos fnName fixedParamPerm xs value termMeasure? report := report ++ thisReport recArgInfoss := recArgInfoss.push recArgInfos -- Put non-indices first @@ -266,8 +268,6 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr) -- are ok in a nested group. This logic can maybe simplified) unless (← hasConst (group.brecOnName false 0)) do throwError "the type {group} does not have a `.brecOn` recursor" - -- TODO: Here we used to save and restore the state. But should the `try`-`catch` - -- not suffice? let r ← k comb trace[Elab.definition.structural] "tryAllArgs report:\n{report}" return r diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean index 395978fc25..5bfa77812e 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean @@ -12,23 +12,24 @@ import Lean.Elab.PreDefinition.Structural.RecArgInfo namespace Lean.Elab.Structural open Meta -private def replaceIndPredRecApp (numFixed : Nat) (funType : Expr) (e : Expr) : M Expr := do +private def replaceIndPredRecApp (fixedParamPerm : FixedParamPerm) (funType : Expr) (e : Expr) : M Expr := do withoutProofIrrelevance do withTraceNode `Elab.definition.structural (fun _ => pure m!"eliminating recursive call {e}") do -- We want to replace `e` with an expression of the same type let main ← mkFreshExprSyntheticOpaqueMVar (← inferType e) - let args : Array Expr := e.getAppArgs[numFixed:] + let args : Array Expr := e.getAppArgs + let ys := fixedParamPerm.pickVarying args let lctx ← getLCtx let r ← lctx.anyM fun localDecl => do if localDecl.isAuxDecl then return false let (mvars, _, t) ← forallMetaTelescope localDecl.type -- NB: do not reduce, we want to see the `funType` unless t.getAppFn == funType do return false withTraceNodeBefore `Elab.definition.structural (do pure m!"trying {mkFVar localDecl.fvarId} : {localDecl.type}") do - if args.size < t.getAppNumArgs then - trace[Elab.definition.structural] "too few arguments. Underapplied recursive call?" + if ys.size < t.getAppNumArgs then + trace[Elab.definition.structural] "too few arguments, expected {t.getAppNumArgs}, found {ys.size}. Underapplied recursive call?" return false - if (← (t.getAppArgs.zip args).allM (fun (t,s) => isDefEq t s)) then - main.mvarId!.assign (mkAppN (mkAppN localDecl.toExpr mvars) args[t.getAppNumArgs:]) + if (← (t.getAppArgs.zip ys).allM (fun (t,s) => isDefEq t s)) then + main.mvarId!.assign (mkAppN (mkAppN localDecl.toExpr mvars) ys[t.getAppNumArgs:]) return ← mvars.allM fun v => do unless (← v.mvarId!.isAssigned) do trace[Elab.definition.structural] "Cannot use {mkFVar localDecl.fvarId}: parameter {v} remains unassigned" @@ -62,7 +63,7 @@ private partial def replaceIndPredRecApps (recArgInfo : RecArgInfo) (funType : E let processApp (e : Expr) : M Expr := do e.withApp fun f args => do if f.isConstOf recArgInfo.fnName then - replaceIndPredRecApp recArgInfo.numFixed funType e + replaceIndPredRecApp recArgInfo.fixedParamPerm funType e else return mkAppN (← loop f) (← args.mapM loop) match (← matchMatcherApp? e) with @@ -100,7 +101,7 @@ def mkIndPredBRecOn (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do lambdaTelescope value fun ys value => do let type := (← inferType value).headBeta let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor ys - trace[Elab.definition.structural] "numFixed: {recArgInfo.numFixed}, indexMajorArgs: {indexMajorArgs}, otherArgs: {otherArgs}" + trace[Elab.definition.structural] "indexMajorArgs: {indexMajorArgs}, otherArgs: {otherArgs}" let funType ← mkLambdaFVars ys type withLetDecl `funType (← inferType funType) funType fun funType => do let motive ← mkForallFVars otherArgs (mkAppN funType ys) diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean index 454d573bf1..733864d2d2 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Main.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Main.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Joachim Breitner -/ prelude import Lean.Elab.PreDefinition.TerminationMeasure +import Lean.Elab.PreDefinition.Mutual import Lean.Elab.PreDefinition.Structural.Basic import Lean.Elab.PreDefinition.Structural.FindRecArg import Lean.Elab.PreDefinition.Structural.Preprocess @@ -71,27 +72,9 @@ where withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x => go (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x) -def getMutualFixedPrefix (preDefs : Array PreDefinition) : M Nat := - withCommonTelescope preDefs fun xs vals => do - let resultRef ← IO.mkRef xs.size - for val in vals do - if (← resultRef.get) == 0 then return 0 - forEachExpr' val fun e => do - if preDefs.any fun preDef => e.isAppOf preDef.declName then - let args := e.getAppArgs - resultRef.modify (min args.size ·) - for arg in args, x in xs do - if !(← withoutProofIrrelevance <| withReducible <| isDefEq arg x) then - -- We continue searching if e's arguments are not a prefix of `xs` - return true - return false - else - return true - resultRef.get - -private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr) - (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do - let values ← preDefs.mapM (instantiateLambda ·.value xs) +private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms) + (xs : Array Expr) (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do + let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs) let indInfo ← getConstInfoInduct recArgInfos[0]!.indGroupInst.all[0]! if ← isInductivePredicate indInfo.name then -- Here we branch off to the IndPred construction, but only for non-mutual functions @@ -102,7 +85,8 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr let recArgInfo := recArgInfos[0]! let value := values[0]! let valueNew ← mkIndPredBRecOn recArgInfo value - let valueNew ← mkLambdaFVars xs valueNew + let valueNew ← lambdaTelescope value fun ys _ => do + mkLambdaFVars (etaReduce := true) (fixedParamPerms.perms[0]!.buildArgs xs ys) (mkAppN valueNew ys) trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}" check valueNew return #[{ preDef with value := valueNew }] @@ -123,12 +107,16 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr -- Assemble the individual `.brecOn` applications let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) => mkBrecOnApp positions i brecOnConst FArgs r v - -- Abstract over the fixed prefixed - let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·) + -- Abstract over the fixed prefixed, preserving the original parameter order + let valuesNew ← (values.zip valuesNew).mapIdxM fun i ⟨value, valueNew⟩ => + lambdaTelescope value fun ys _ => do + -- NB: Do not eta-contract here, other code (e.g. FunInd) expects this to have the + -- same number of head lambdas as the original definition + mkLambdaFVars (fixedParamPerms.perms[i]!.buildArgs xs ys) (valueNew.beta ys) return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew } private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : - M (Array Nat × (Array PreDefinition) × Nat) := do + M (Array Nat × (Array PreDefinition) × FixedParamPerms) := do withoutModifyingEnv do preDefs.forM (addAsAxiom ·) let fnNames := preDefs.map (·.declName) @@ -136,25 +124,39 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Arra return { preDef with value := (← preprocess preDef.value fnNames) } -- The syntactically fixed arguments - let maxNumFixed ← getMutualFixedPrefix preDefs + let fixedParamPerms ← getFixedParamPerms preDefs - lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do - assert! xs.size = maxNumFixed - let values ← preDefs.mapM (instantiateLambda ·.value xs) + fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun xs => do + let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs) - tryAllArgs fnNames xs values termMeasure?s fun recArgInfos => do + tryAllArgs fnNames fixedParamPerms xs values termMeasure?s fun recArgInfos => do let recArgPoss := recArgInfos.map (·.recArgPos) trace[Elab.definition.structural] "Trying argument set {recArgPoss}" - let numFixed := recArgInfos.foldl (·.min ·.numFixed) maxNumFixed - if numFixed < maxNumFixed then - trace[Elab.definition.structural] "Reduced numFixed from {maxNumFixed} to {numFixed}" - -- We may have decreased the number of arguments we consider fixed, so update - -- the recArgInfos, remove the extra arguments from local environment, and recalculate value - let recArgInfos := recArgInfos.map ({· with numFixed := numFixed }) - withErasedFVars (xs.extract numFixed xs.size |>.map (·.fvarId!)) do - let xs := xs[:numFixed] - let preDefs' ← elimMutualRecursion preDefs xs recArgInfos - return (recArgPoss, preDefs', numFixed) + let (fixedParamPerms', xs', toErase) := fixedParamPerms.erase xs (recArgInfos.map (·.indicesAndRecArgPos)) + -- We may have to turn some fixed parameters into varying parameters + let recArgInfos := recArgInfos.mapIdx fun i recArgInfo => + {recArgInfo with fixedParamPerm := fixedParamPerms'.perms[i]!} + if xs'.size != xs.size then + trace[Elab.definition.structural] "Reduced fixed params from {xs} to {xs'}, erasing {toErase.map mkFVar}" + trace[Elab.definition.structural] "New recArgInfos {repr recArgInfos}" + -- Check that the parameters of the IndGroupInsts are still fine + for recArgInfo in recArgInfos do + for indParam in recArgInfo.indGroupInst.params do + for y in toErase do + if (← dependsOn indParam y) then + if indParam.isFVarOf y then + throwError "its type is an inductive datatype and the datatype parameter\ + {indentExpr indParam}\n\ + which cannot be fixed as it is an index or depends on an index, and indices \ + cannot be fixed parameters when using structural recursion." + else + throwError "its type is an inductive datatype and the datatype parameter\ + {indentExpr indParam}\ndepends on the function parameter{indentExpr (mkFVar y)}\n\ + which cannot be fixed as it is an index or depends on an index, and indices \ + cannot be fixed parameters when using structural recursion." + withErasedFVars toErase do + let preDefs' ← elimMutualRecursion preDefs fixedParamPerms' xs' recArgInfos + return (recArgPoss, preDefs', fixedParamPerms') def reporttermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do if let some ref := preDef.termination.terminationBy?? then @@ -167,7 +169,7 @@ def reporttermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) : TermElabM Unit := do let names := preDefs.map (·.declName) - let ((recArgPoss, preDefsNonRec, numFixed), state) ← run <| inferRecArgPos preDefs termMeasure?s + let ((recArgPoss, preDefsNonRec, fixedParamPerms), state) ← run <| inferRecArgPos preDefs termMeasure?s for recArgPos in recArgPoss, preDef in preDefs do reporttermMeasure preDef recArgPos state.addMatchers.forM liftM @@ -190,7 +192,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array ( for theorems and definitions that are propositions. See issue #2327 -/ - registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos numFixed + registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms addSmartUnfoldingDef preDef recArgPos markAsRecursive preDef.declName for preDef in preDefs do diff --git a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean index 874ecbc921..ada75b2f7c 100644 --- a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Joachim Breitner prelude import Lean.Meta.Basic import Lean.Meta.ForEachExpr +import Lean.Elab.PreDefinition.FixedParams import Lean.Elab.PreDefinition.Structural.IndGroupInfo namespace Lean.Elab.Structural @@ -14,18 +15,18 @@ namespace Lean.Elab.Structural /-- Information about the argument of interest of a structurally recursive function. -The `Expr`s in this data structure expect the `fixedParams` to be in scope, but not the other +The `Expr`s in this data structure expect the fixed parameters to be in scope, but not the other parameters of the function. This ensures that this data structure makes sense in the other functions of a mutually recursive group. -/ structure RecArgInfo where /-- the name of the recursive function -/ fnName : Name - /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/ - numFixed : Nat - /-- position (counted including fixed prefix) of the argument we are recursing on -/ + /-- Information which arguments are fixed -/ + fixedParamPerm : FixedParamPerm + /-- position of the argument we are recursing on, among all parameters -/ recArgPos : Nat - /-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/ + /-- position of the indices of the inductive datatype we are recursing on, among all parameters -/ indicesPos : Array Nat /-- The inductive group (with parameters) of the argument's type -/ indGroupInst : IndGroupInst @@ -36,23 +37,29 @@ structure RecArgInfo where indIdx : Nat deriving Inhabited, Repr + /-- position of the argument and its indices we are recursing on, among all parameters -/ +def RecArgInfo.indicesAndRecArgPos (info : RecArgInfo) : Array Nat := + info.indicesPos.push info.recArgPos + /-- -If `xs` are the parameters of the functions (excluding fixed prefix), partitions them -into indices and major arguments, and other parameters. +If `xs` are the varing parameters of the functions, partitions them into indices and major +arguments, and other parameters. -/ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do + -- To simplify the index calculation, pad xs with dummy values where fixed parameters are + let xs := info.fixedParamPerm.buildArgs (mkArray info.fixedParamPerm.numFixed (mkSort 0)) xs -- First indices and major arg, using the order they appear in `info.indicesPos` let mut indexMajorArgs := #[] let indexMajorPos := info.indicesPos.push info.recArgPos for j in indexMajorPos do - assert! info.numFixed ≤ j && j - info.numFixed < xs.size - indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]! + indexMajorArgs := indexMajorArgs.push xs[j]! -- Then the other arguments, in the order they appear in `xs` - let mut otherArgs := #[] + let mut otherVaryingArgs := #[] for h : i in [:xs.size] do - unless indexMajorPos.contains (i + info.numFixed) do - otherArgs := otherArgs.push xs[i] - return (indexMajorArgs, otherArgs) + unless indexMajorPos.contains i do + unless info.fixedParamPerm.isFixed i do + otherVaryingArgs := otherVaryingArgs.push xs[i] + return (indexMajorArgs, otherVaryingArgs) /-- Name of the recursive data type. Assumes that it is not one of the auxiliary ones. diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 5a712cc12c..5c374e9e91 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -10,6 +10,7 @@ import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Eqns import Lean.Meta.ArgsPacker.Basic import Lean.Elab.PreDefinition.WF.Unfold +import Lean.Elab.PreDefinition.FixedParams import Init.Data.Array.Basic namespace Lean.Elab.WF @@ -21,13 +22,15 @@ structure EqnInfo extends EqnInfoCore where declNameNonRec : Name fixedPrefixSize : Nat argsPacker : ArgsPacker + fixedParamPerms : FixedParamPerms deriving Inhabited builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension -def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) +def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) : MetaM Unit := do + let fixedPrefixSize := fixedParamPerms.numFixed preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName /- See issue #2327. @@ -40,7 +43,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi modifyEnv fun env => preDefs.foldl (init := env) fun env preDef => eqnInfoExt.insert env preDef.declName { preDef with - declNames, declNameNonRec, fixedPrefixSize, argsPacker } + declNames, declNameNonRec, fixedPrefixSize, argsPacker, fixedParamPerms } def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do if let some info := eqnInfoExt.find? (← getEnv) declName then diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 98a33ef8f7..38a4f79255 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -13,8 +13,10 @@ import Lean.Meta.ArgsPacker import Lean.Elab.Quotation import Lean.Elab.RecAppSyntax import Lean.Elab.PreDefinition.Basic +import Lean.Elab.PreDefinition.Mutual import Lean.Elab.PreDefinition.Structural.Basic import Lean.Elab.PreDefinition.TerminationMeasure +import Lean.Elab.PreDefinition.FixedParams import Lean.Elab.PreDefinition.WF.Basic import Lean.Data.Array @@ -169,24 +171,25 @@ def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : Meta withLCtx' lctx k /-- Create one measure for each (eligible) parameter of the given predefintion. -/ -def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) +def simpleMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms) (userVarNamess : Array (Array Name)) : MetaM (Array (Array BasicMeasure)) := do let is_mutual : Bool := preDefs.size > 1 preDefs.mapIdxM fun funIdx preDef => do - lambdaTelescope preDef.value fun xs _ => do - withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do + lambdaTelescope preDef.value fun params _ => do + let xs := fixedParamPerms.perms[funIdx]!.pickVarying params + withUserNames xs userVarNamess[funIdx]! do let mut ret : Array BasicMeasure := #[] - for x in xs[fixedPrefixSize:] do + for x in xs do -- If the `SizeOf` instance produces a constant (e.g. because it's type is a `Prop` or -- `Type`), then ignore this parameter let sizeOf ← whnfD (← mkAppM ``sizeOf #[x]) if sizeOf.isLit then continue - let natFn ← mkLambdaFVars xs (← mkAppM ``sizeOf #[x]) + let natFn ← mkLambdaFVars params (← mkAppM ``sizeOf #[x]) -- Determine if we need to exclude `sizeOf` in the measure we show/pass on. let fn ← - if ← mayOmitSizeOf is_mutual xs[fixedPrefixSize:] x - then mkLambdaFVars xs x + if ← mayOmitSizeOf is_mutual xs x + then mkLambdaFVars params x else pure natFn ret := ret.push { ref := .missing, structural := false, fn, natFn } return ret @@ -339,24 +342,26 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive call site. -/ -def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) +def collectRecCalls (unaryPreDef : PreDefinition) (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) : MetaM (Array RecCallWithContext) := withoutModifyingState do addAsAxiom unaryPreDef - lambdaBoundedTelescope unaryPreDef.value (fixedPrefixSize + 1) fun xs body => do - unless xs.size == fixedPrefixSize + 1 do + lambdaBoundedTelescope unaryPreDef.value (fixedParamPerms.numFixed + 1) fun xs body => do + unless xs.size == fixedParamPerms.numFixed + 1 do throwError "Unexpected number of lambdas in unary pre-definition" - let ys := xs[:fixedPrefixSize] - let param := xs[fixedPrefixSize]! - withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do - unless args.size ≥ fixedPrefixSize + 1 do + let ys := xs[:fixedParamPerms.numFixed] + let param := xs[fixedParamPerms.numFixed]! + withRecApps unaryPreDef.declName fixedParamPerms.numFixed param body fun param args => do + unless args.size ≥ fixedParamPerms.numFixed + 1 do throwError "Insufficient arguments in recursive call" - let arg := args[fixedPrefixSize]! + let arg := args[fixedParamPerms.numFixed]! trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})" let some (caller, params) := argsPacker.unpack param | throwError "Cannot unpack param, unexpected expression:{indentExpr param}" let some (callee, args) := argsPacker.unpack arg | throwError "Cannot unpack arg, unexpected expression:{indentExpr arg}" - RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args) + let callerParams := fixedParamPerms.perms[caller]!.buildArgs ys params + let calleeArgs := fixedParamPerms.perms[callee]!.buildArgs ys args + RecCallWithContext.create (← getRef) caller callerParams callee calleeArgs /-- Is the expression a `<`-like comparison of `Nat` expressions -/ def isNatCmp (e : Expr) : Option (Expr × Expr) := @@ -367,7 +372,7 @@ def isNatCmp (e : Expr) : Option (Expr × Expr) := | GE.ge α _ e₁ e₂ => if α.isConstOf ``Nat then some (e₂, e₁) else none | _ => none -def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) +def complexMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms) (userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) : MetaM (Array (Array BasicMeasure)) := do preDefs.mapIdxM fun funIdx _preDef => do @@ -377,20 +382,21 @@ def complexMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) unless rc.caller = funIdx do continue -- Only look at calls where the parameters have not been refined unless rc.params.all (·.isFVar) do continue - let xs := rc.params.map (·.fvarId!) - let varyingParams : Array FVarId := xs[fixedPrefixSize:] + let varyingParams := fixedParamPerms.perms[funIdx]!.pickVarying rc.params + let varyingFVars := varyingParams.map (·.fvarId!) + let params := rc.params.map (·.fvarId!) measures ← rc.ctxt.run do - withUserNames rc.params[fixedPrefixSize:] userVarNamess[funIdx]! do + withUserNames varyingParams userVarNamess[funIdx]! do trace[Elab.definition.wf] "rc: {rc.caller} ({rc.params}) → {rc.callee} ({rc.args})" let mut measures := measures for ldecl in ← getLCtx do if let some (e₁, e₂) := isNatCmp ldecl.type then -- We only want to consider these expressions if they depend only on the function's -- immediate arguments, so check that - if e₁.hasAnyFVar (! xs.contains ·) then continue - if e₂.hasAnyFVar (! xs.contains ·) then continue + if e₁.hasAnyFVar (! params.contains ·) then continue + if e₂.hasAnyFVar (! params.contains ·) then continue -- If e₁ does not depend on any varying parameters, simply ignore it - let e₁_is_const := ! e₁.hasAnyFVar (varyingParams.contains ·) + let e₁_is_const := ! e₁.hasAnyFVar (varyingFVars.contains ·) let body := if e₁_is_const then e₂ else mkNatSub e₂ e₁ -- Avoid adding simple measures unless body.isFVar do @@ -742,17 +748,18 @@ def mkProdElem (xs : Array Expr) : MetaM Expr := do let n := xs.size xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p] -def toTerminationMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) +def toTerminationMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms) (userVarNamess : Array (Array Name)) (measuress : Array (Array BasicMeasure)) (solution : Array MutualMeasure) : MetaM TerminationMeasures := do preDefs.mapIdxM fun funIdx preDef => do let measures := measuress[funIdx]! - lambdaTelescope preDef.value fun xs _ => do - withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do + lambdaTelescope preDef.value fun params _ => do + let xs := fixedParamPerms.perms[funIdx]!.pickVarying params + withUserNames xs userVarNamess[funIdx]! do let args := solution.map fun - | .args tmIdxs => measures[tmIdxs[funIdx]!]!.fn.beta xs + | .args tmIdxs => measures[tmIdxs[funIdx]!]!.fn.beta params | .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0 - let fn ← mkLambdaFVars xs (← mkProdElem args) + let fn ← mkLambdaFVars params (← mkProdElem args) return { ref := .missing, structural := false, fn} /-- @@ -780,19 +787,19 @@ terminates. See the module doc string for a high-level overview. The `preDefs` are used to determine arity and types of parameters; the bodies are ignored. -/ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) - (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) : + (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) : MetaM TerminationMeasures := do let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·) trace[Elab.definition.wf] "varNames is: {userVarNamess}" -- Collect all recursive calls and extract their context - let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker + let recCalls ← collectRecCalls unaryPreDef fixedParamPerms argsPacker let recCalls := filterSubsumed recCalls -- For every function, the measures we want to use -- (One for each non-forbiddend arg) - let basicMeassures₁ ← simpleMeasures preDefs fixedPrefixSize userVarNamess - let basicMeassures₂ ← complexMeasures preDefs fixedPrefixSize userVarNamess recCalls + let basicMeassures₁ ← simpleMeasures preDefs fixedParamPerms userVarNamess + let basicMeassures₂ ← complexMeasures preDefs fixedParamPerms userVarNamess recCalls let basicMeasures := Array.zipWith (· ++ ·) basicMeassures₁ basicMeassures₂ -- The list of measures, including the measures that order functions. @@ -801,7 +808,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) -- If there is only one plausible measure, use that if let #[solution] := mutualMeasures then - let termMeasures ← toTerminationMeasures preDefs fixedPrefixSize userVarNamess basicMeasures #[solution] + let termMeasures ← toTerminationMeasures preDefs fixedParamPerms userVarNamess basicMeasures #[solution] reportTerminationMeasures preDefs termMeasures return termMeasures @@ -810,7 +817,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) match ← liftMetaM <| solve mutualMeasures callMatrix with | .some solution => do - let termMeasures ← toTerminationMeasures preDefs fixedPrefixSize userVarNamess basicMeasures solution + let termMeasures ← toTerminationMeasures preDefs fixedParamPerms userVarNamess basicMeasures solution reportTerminationMeasures preDefs termMeasures return termMeasures | .none => diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean index 2d89fdafa7..48ae229134 100644 --- a/src/Lean/Elab/PreDefinition/WF/Main.lean +++ b/src/Lean/Elab/PreDefinition/WF/Main.lean @@ -23,12 +23,11 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T let termMeasures? := termMeasure?s.mapM id -- Either all or none, checked by `elabTerminationByHints` let preDefs ← preDefs.mapM fun preDef => return { preDef with value := (← floatRecApp preDef.value) } - let (fixedPrefixSize, argsPacker, unaryPreDef, wfPreprocessProofs) ← withoutModifyingEnv do + let (fixedParamPerms, argsPacker, unaryPreDef, wfPreprocessProofs) ← withoutModifyingEnv do for preDef in preDefs do addAsAxiom preDef - let fixedPrefixSize ← Mutual.getFixedPrefix preDefs - trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}" - let varNamess ← preDefs.mapM (varyingVarNames fixedPrefixSize ·) + let fixedParamPerms ← getFixedParamPerms preDefs + let varNamess ← preDefs.mapIdxM fun i preDef => varyingVarNames fixedParamPerms i preDef for varNames in varNamess, preDef in preDefs do if varNames.isEmpty then throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments" @@ -36,33 +35,35 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T let (preDefsAttached, wfPreprocessProofs) ← Array.unzip <$> preDefs.mapM fun preDef => do let result ← preprocess preDef.value return ({preDef with value := result.expr}, result) - return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsAttached, wfPreprocessProofs) + let unaryPreDef ← packMutual fixedParamPerms argsPacker preDefsAttached + return (fixedParamPerms, argsPacker, unaryPreDef, wfPreprocessProofs) + trace[Elab.definition.wf] "unaryPreDef:{indentD unaryPreDef.value}" let wf : TerminationMeasures ← do if let some tms := termMeasures? then pure tms else -- No termination_by here, so use GuessLex to infer one - guessLex preDefs unaryPreDef fixedPrefixSize argsPacker + guessLex preDefs unaryPreDef fixedParamPerms argsPacker - let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do + let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedParamPerms.numFixed fun fixedArgs type => do let type ← whnfForall type unless type.isForall do throwError "wfRecursion: expected unary function type: {type}" let packedArgType := type.bindingDomain! - elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do + elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName fixedParamPerms fixedArgs argsPacker packedArgType wf fun wfRel => do trace[Elab.definition.wf] "wfRel: {wfRel}" let (value, envNew) ← withoutModifyingEnv' do addAsAxiom unaryPreDef - let value ← mkFix unaryPreDef prefixArgs argsPacker wfRel (preDefs.map (·.declName)) (preDefs.map (·.termination.decreasingBy?)) + let value ← mkFix unaryPreDef fixedArgs argsPacker wfRel (preDefs.map (·.declName)) (preDefs.map (·.termination.decreasingBy?)) eraseRecAppSyntaxExpr value /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/ let value ← unfoldDeclsFrom envNew value return { unaryPreDef with value } trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}" - let preDefsNonrec ← preDefsFromUnaryNonRec fixedPrefixSize argsPacker preDefs preDefNonRec + let preDefsNonrec ← preDefsFromUnaryNonRec fixedParamPerms argsPacker preDefs preDefNonRec Mutual.addPreDefsFromUnary preDefs preDefsNonrec preDefNonRec let preDefs ← Mutual.cleanPreDefs preDefs - registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker + registerEqnsInfo preDefs preDefNonRec.declName fixedParamPerms argsPacker for preDef in preDefs, wfPreprocessProof in wfPreprocessProofs do unless preDef.kind.isTheorem do unless (← isProp preDef.type) do diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean index 59dd5149ed..93ae84c181 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Joachim Breitner prelude import Lean.Meta.ArgsPacker import Lean.Elab.PreDefinition.Basic +import Lean.Elab.PreDefinition.FixedParams import Lean.Elab.PreDefinition.WF.Eqns /-! @@ -38,7 +39,7 @@ def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr : /-- Processes the expression and replaces calls to the `preDefs` with calls to `f`. -/ -def packCalls (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Name) (newF : Expr) +def packCalls (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) (funNames : Array Name) (newF : Expr) (e : Expr) : MetaM Expr := do let fType ← inferType newF unless fType.isForall do @@ -49,16 +50,19 @@ def packCalls (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Na if !f.isConst then return TransformStep.done e if let some fidx := funNames.idxOf? f.constName! then - let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size + assert! fidx < fixedParamPerms.perms.size + let mask := fixedParamPerms.perms[fidx]!.map Option.isSome + let arity := mask.size let e' ← withAppN arity e fun args => do - let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:] + let varying := fixedParamPerms.perms[fidx]!.pickVarying args + let packedArg ← argsPacker.pack domain fidx varying return mkApp newF packedArg return TransformStep.done e' return TransformStep.done e ) -def mutualName (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : Name := - if argsPacker.onlyOneUnary then +def mutualName (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : Name := + if fixedParamPerms.fixedArePrefix && argsPacker.onlyOneUnary then preDefs[0]!.declName else if argsPacker.numFuncs > 1 then @@ -70,13 +74,16 @@ def mutualName (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : Name Creates a single unary function from the given `preDefs`, using the machinery in the `ArgPacker` module. -/ -def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do - if argsPacker.onlyOneUnary then return preDefs[0]! - let newFn := mutualName argsPacker preDefs +def packMutual (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do + let newFn := mutualName fixedParamPerms argsPacker preDefs + if newFn = preDefs[0]!.declName then + return preDefs[0]! -- Bring the fixed prefix into scope - forallBoundedTelescope preDefs[0]!.type (some fixedPrefix) fun ys _ => do - let types ← preDefs.mapM (instantiateForall ·.type ys) - let vals ← preDefs.mapM (instantiateLambda ·.value ys) + fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun ys => do + let types ← preDefs.mapIdxM fun i preDef => + fixedParamPerms.perms[i]!.instantiateForall preDef.type ys + let vals ← preDefs.mapIdxM fun i preDef => + fixedParamPerms.perms[i]!.instantiateLambda preDef.value ys let type ← argsPacker.uncurryType types @@ -90,12 +97,12 @@ def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array Pr let f := mkAppN (mkConst newFn us) ys let value ← argsPacker.uncurry vals - let value ← packCalls fixedPrefix argsPacker (preDefs.map (·.declName)) f value + let value ← packCalls fixedParamPerms argsPacker (preDefs.map (·.declName)) f value let value ← mkLambdaFVars ys value return { preDefNew with value } /-- -Collect the names of the varying variables (after the fixed prefix); this also determines the +Collect the names of the varying variables (excluding the fixed parameters); this also determines the arity for the well-founded translations, and is turned into an `ArgsPacker`. We use the term to determine the arity, but take the name from the type, for better names in the ``` @@ -103,26 +110,33 @@ fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n ``` idiom. -/ -def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do +def varyingVarNames (fixedParamPerms : FixedParamPerms) (preDefIdx : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do -- We take the arity from the term, but the names from the types let arity ← lambdaTelescope preDef.value fun xs _ => return xs.size - assert! fixedPrefixSize ≤ arity forallBoundedTelescope preDef.type arity fun xs _ => do assert! xs.size = arity - let xs : Array Expr := xs[fixedPrefixSize:] - xs.mapM (·.fvarId!.getUserName) + assert! fixedParamPerms.perms[preDefIdx]!.size = arity + let mut ns := #[] + for x in xs, paramInfo in fixedParamPerms.perms[preDefIdx]! do + if paramInfo.isSome then continue -- skip fixed parameters + ns := ns.push (← x.fvarId!.getUserName) + return ns - -def preDefsFromUnaryNonRec (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) +def preDefsFromUnaryNonRec (fixedParamPerms : FixedParamPerms) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (unaryPreDefNonRec : PreDefinition) : MetaM (Array PreDefinition) := do withoutModifyingEnv do let us := unaryPreDefNonRec.levelParams.map mkLevelParam addAsAxiom unaryPreDefNonRec preDefs.mapIdxM fun fidx preDef => do - let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do + let arity := fixedParamPerms.perms[fidx]!.size + let value ← forallBoundedTelescope preDef.type (some arity) fun params _ => do + assert! arity = params.size + let xs := fixedParamPerms.perms[fidx]!.pickFixed params + let ys := fixedParamPerms.perms[fidx]!.pickVarying params let value := mkAppN (mkConst unaryPreDefNonRec.declName us) xs let value ← argsPacker.curryProj value fidx - mkLambdaFVars xs value + let value := value.beta ys + mkLambdaFVars params value trace[Elab.definition.wf] "{preDef.declName} := {value}" pure { preDef with value } diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean index 5b14e2ce02..3ce99c914b 100644 --- a/src/Lean/Elab/PreDefinition/WF/Rel.lean +++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean @@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Rename import Lean.Elab.SyntheticMVars import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.TerminationMeasure +import Lean.Elab.PreDefinition.FixedParams import Lean.Meta.ArgsPacker namespace Lean.Elab.WF @@ -22,16 +23,18 @@ a mutual clique, they must be the same for all functions. This ensures the preconditions for `ArgsPacker.uncurryND`. -/ -def checkCodomains (names : Array Name) (prefixArgs : Array Expr) (arities : Array Nat) +def checkCodomains (names : Array Name) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr) (arities : Array Nat) (termMeasures : TerminationMeasures) : TermElabM Expr := do let mut codomains := #[] - for name in names, arity in arities, termMeasure in termMeasures do - let type ← inferType (termMeasure.fn.beta prefixArgs) - let codomain ← forallBoundedTelescope type arity fun xs codomain => do + for name in names, funIdx in [:names.size], arity in arities, termMeasure in termMeasures do + let measureType ← inferType termMeasure.fn + let measureType ← fixedParamPerms.perms[funIdx]!.instantiateForall measureType fixedArgs + let codomain ← forallBoundedTelescope measureType arity fun xs codomain => do + assert! xs.size = arity let fvars := xs.map (·.fvarId!) if codomain.hasAnyFVar (fvars.contains ·) then throwErrorAt termMeasure.ref m!"The termination measure's type must not depend on the " ++ - m!"function's varying parameters, but {name}'s termination measure does:{indentExpr type}\n" ++ + m!"function's varying parameters, but {name}'s termination measure does:{indentExpr measureType}\n" ++ "Try using `sizeOf` explicitly" pure codomain codomains := codomains.push codomain @@ -51,14 +54,16 @@ If the `termMeasures` map the packed argument `argType` to `β`, then this funct continuation a value of type `WellFoundedRelation argType` that is derived from the instance for `WellFoundedRelation β` using `invImage`. -/ -def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (prefixArgs : Array Expr) - (argsPacker : ArgsPacker) (argType : Expr) (termMeasures : TerminationMeasures) +def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (fixedParamPerms : FixedParamPerms) + (fixedArgs : Array Expr) (argsPacker : ArgsPacker) (argType : Expr) (termMeasures : TerminationMeasures) (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do let α := argType let u ← getLevel α - let β ← checkCodomains declNames prefixArgs argsPacker.arities termMeasures + let β ← checkCodomains declNames fixedParamPerms fixedArgs argsPacker.arities termMeasures let v ← getLevel β - let packedF ← argsPacker.uncurryND (termMeasures.map (·.fn.beta prefixArgs)) + let fns ← termMeasures.mapIdxM fun i measure => + fixedParamPerms.perms[i]!.instantiateLambda measure.fn fixedArgs + let packedF ← argsPacker.uncurryND fns let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β) let rel ← instantiateMVars (mkApp4 (.const ``invImage [u,v]) α β packedF inst) k rel diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean index df83f46889..22c067cc79 100644 --- a/src/Lean/Meta/ArgsPacker.lean +++ b/src/Lean/Meta/ArgsPacker.lean @@ -328,6 +328,8 @@ if they are all the same. -/ def uncurryType (types : Array Expr) : MetaM Expr := do + if types.size = 1 then + return types[0]! let types ← types.mapM whnfForall types.forM fun type => do unless type.isForall do diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index e3207ccbbb..fa72a95312 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -695,10 +695,10 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do | fix@WellFounded.fix α _motive rel wf body target => unless params.back! == target do throwError "functional induction: expected the target as last parameter{indentExpr e}" - let fixedParams := params.pop + let fixedParamPerms := params.pop let motiveType ← mkForallFVars #[target] (.sort levelZero) withLocalDeclD `motive motiveType fun motive => do - let fn := mkAppN (← mkConstWithLevelParams name) fixedParams + let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms let isRecCall : Expr → Option Expr := fun e => if e.isApp && e.appFn!.isFVarOf motive.fvarId! then mkApp fn e.appArg! @@ -732,7 +732,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do -- induction principle match the type of the function better. -- But this leads to avoidable parameters that make functional induction strictly less -- useful (e.g. when the unsued parameter mentions bound variables in the users' goal) - let (paramMask, e') ← mkLambdaFVarsMasked fixedParams e' + let (paramMask, e') ← mkLambdaFVarsMasked fixedParamPerms e' let e' ← instantiateMVars e' return (e', paramMask) | _ => @@ -787,16 +787,25 @@ def projectMutualInduct (names : Array Name) (mutualInduct : Name) : MetaM Unit For a (non-mutual!) definition of `name`, uses the `FunIndInfo` associated with the `unaryInduct` and derives the one for the n-ary function. -/ -def setNaryFunIndInfo (name : Name) (arity : Nat) (unaryInduct : Name) : MetaM Unit := do - let inductName := getFunInductName name - unless inductName = unaryInduct do - let some unaryFunIndInfo ← getFunIndInfoForInduct? unaryInduct - | throwError "Expected {unaryInduct} to have FunIndInfo" - setFunIndInfo { - unaryFunIndInfo with - funIndName := inductName - params := unaryFunIndInfo.params.filter (· != .target) ++ mkArray arity .target - } +def setNaryFunIndInfo (fixedParamPerms : FixedParamPerms) (name : Name) (unaryInduct : Name) : MetaM Unit := do + assert! fixedParamPerms.perms.size = 1 -- only non-mutual for now + let funIndName := getFunInductName name + unless funIndName = unaryInduct do + let some unaryFunIndInfo ← getFunIndInfoForInduct? unaryInduct + | throwError "Expected {unaryInduct} to have FunIndInfo" + let fixedParamPerm := fixedParamPerms.perms[0]! + let mut params := #[] + let mut j := 0 + for h : i in [:fixedParamPerm.size] do + if fixedParamPerm[i].isSome then + assert! j + 1 < unaryFunIndInfo.params.size + params := params.push unaryFunIndInfo.params[j]! + j := j + 1 + else + params := params.push .target + assert! j + 1 = unaryFunIndInfo.params.size + + setFunIndInfo { unaryFunIndInfo with funIndName, params } /-- In the type of `value`, reduces @@ -920,13 +929,15 @@ Given a recursive definition `foo` defined via structural recursion, derive `foo if needed, and `foo.induct` for all functions in the group. See module doc for details. -/ -def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit := do +def deriveInductionStructural (names : Array Name) (fixedParamPerms : FixedParamPerms) : MetaM Unit := do let infos ← names.mapM getConstInfoDefn + assert! infos.size > 0 -- First open up the fixed parameters everywhere - let (e', paramMask, motiveArities) ← lambdaBoundedTelescope infos[0]!.value numFixed fun xs _ => do + let (e', paramMask, motiveArities) ← fixedParamPerms.perms[0]!.forallTelescope infos[0]!.type fun xs => do -- Now look at the body of an arbitrary of the functions (they are essentially the same -- up to the final projections) - let body ← instantiateLambda infos[0]!.value xs + let body ← fixedParamPerms.perms[0]!.instantiateLambda infos[0]!.value xs + let body := body.eta lambdaTelescope body fun ys body => do -- The body is of the form (brecOn … ).2.2.1 extra1 extra2 etc; ignore the @@ -938,7 +949,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit let body := PProdN.stripProjs body let .const brecOnName us := f | - throwError "{infos[0]!.name}: unexpected body:{indentExpr infos[0]!.value}" + throwError "{infos[0]!.name}: unexpected body:{indentExpr infos[0]!.value}\ninstantiated to{indentExpr body}" unless isBRecOnRecursor (← getEnv) brecOnName do throwError "{infos[0]!.name}: expected .brecOn application, found:{indentExpr body}" @@ -975,12 +986,13 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit motives.mapM fun motive => forallTelescopeReducing motive fun xs _ => pure xs.size - - let recArgInfos ← infos.mapM fun info => do + -- Recreate the recArgInfos. Maybe more robust and simpler to store relevant parts in the EqnInfos? + let recArgInfos ← infos.mapIdxM fun funIdx info => do let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) info.name | throwError "{info.name} missing eqnInfo" - let value ← instantiateLambda info.value xs + let value ← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs let recArgInfo' ← lambdaTelescope value fun ys _ => - Structural.getRecArgInfo info.name numFixed (xs ++ ys) eqnInfo.recArgPos + let args := fixedParamPerms.perms[funIdx]!.buildArgs xs ys + Structural.getRecArgInfo info.name fixedParamPerms.perms[funIdx]! args eqnInfo.recArgPos let #[recArgInfo] ← Structural.argsInGroup group xs value #[recArgInfo'] | throwError "Structural.argsInGroup did not return a recArgInfo" pure recArgInfo @@ -998,23 +1010,24 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit -- context, and are the parts relevant for every function in the mutual group -- Calculate the types of the induction motives (natural argument order) for each function - let motiveTypes ← infos.mapM fun info => do - lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => + let motiveTypes ← infos.mapIdxM fun funIdx info => do + lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ => mkForallFVars ys (.sort levelZero) - let motiveArities ← infos.mapM fun info => do - lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size + let motiveArities ← infos.mapIdxM fun funIdx info => do + lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ => + pure ys.size let motiveNames := Array.ofFn (n := infos.size) fun ⟨i, _⟩ => if infos.size = 1 then .mkSimple "motive" else .mkSimple s!"motive_{i+1}" withLocalDeclsDND (motiveNames.zip motiveTypes) fun motives => do -- Prepare the `isRecCall` that recognizes recursive calls - let fns := infos.map fun info => - mkAppN (.const info.name (info.levelParams.map mkLevelParam)) xs let isRecCall : Expr → Option Expr := fun e => do - if let .some i := motives.idxOf? e.getAppFn then - if e.getAppNumArgs = motiveArities[i]! then - return mkAppN fns[i]! e.getAppArgs + if let .some funIdx := motives.idxOf? e.getAppFn then + if e.getAppNumArgs = motiveArities[funIdx]! then + let info := infos[funIdx]! + let args := fixedParamPerms.perms[funIdx]!.buildArgs xs e.getAppArgs + return mkAppN (.const info.name (info.levelParams.map mkLevelParam)) args .none -- Motives with parameters reordered, to put indices and major first @@ -1062,8 +1075,8 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit for info in infos, recArgInfo in recArgInfos, idx in [:infos.size] do -- Take care to pick the `ys` from the type, to get the variable names expected -- by the user, but use the value arity - let arity ← lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size - let e ← forallBoundedTelescope (← instantiateForall info.type xs) arity fun ys _ => do + let arity ← lambdaTelescope (← fixedParamPerms.perms[idx]!.instantiateLambda info.value xs) fun ys _ => pure ys.size + let e ← forallBoundedTelescope (← fixedParamPerms.perms[idx]!.instantiateForall info.type xs) arity fun ys _ => do let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys -- Find where in the function packing we are (TODO: abstract out) let some indIdx := positions.findIdx? (·.contains idx) | panic! "invalid positions" @@ -1205,9 +1218,9 @@ def deriveInduction (name : Name) : MetaM Unit := do let unpackedInductName ← unpackMutualInduction eqnInfo unaryInductName projectMutualInduct eqnInfo.declNames unpackedInductName if eqnInfo.argsPacker.numFuncs = 1 then - setNaryFunIndInfo eqnInfo.declNames[0]! eqnInfo.argsPacker.arities[0]! unaryInductName + setNaryFunIndInfo eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then - deriveInductionStructural eqnInfo.declNames eqnInfo.numFixed + deriveInductionStructural eqnInfo.declNames eqnInfo.fixedParamPerms else throwError "constant '{name}' is not structurally or well-founded recursive" diff --git a/src/Lean/Meta/Tactic/FunIndInfo.lean b/src/Lean/Meta/Tactic/FunIndInfo.lean index 68b3f93fda..34f1dd8bad 100644 --- a/src/Lean/Meta/Tactic/FunIndInfo.lean +++ b/src/Lean/Meta/Tactic/FunIndInfo.lean @@ -21,7 +21,7 @@ inductive FunIndParamKind where | dropped | param | target -deriving BEq, Repr +deriving BEq, Repr, Inhabited /-- A `FunIndInfo` indicates how a function's arguments map to the arguments of the functional induction diff --git a/tests/lean/1673.lean.expected.out b/tests/lean/1673.lean.expected.out index 972889b428..c139bb7bbb 100644 --- a/tests/lean/1673.lean.expected.out +++ b/tests/lean/1673.lean.expected.out @@ -4,7 +4,7 @@ with errors failed to infer structural recursion: Not considering parameter n of foo.a: it is unchanged in the recursive calls -Not considering parameter nope of foo.a: +Not considering parameter #2 of foo.a: it is unchanged in the recursive calls no parameters suitable for structural recursion diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out index 8cd0d6ffd6..86a4f5907a 100644 --- a/tests/lean/guessLexFailures.lean.expected.out +++ b/tests/lean/guessLexFailures.lean.expected.out @@ -49,7 +49,7 @@ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure. The basic measures relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) - n m x4 + n m x3 1) 39:6-27 = = = 2) 40:6-25 = < _ 3) 41:6-25 < _ _ diff --git a/tests/lean/run/4928.lean b/tests/lean/run/4928.lean index 6e9c6d1ec0..3376aa6eec 100644 --- a/tests/lean/run/4928.lean +++ b/tests/lean/run/4928.lean @@ -1,17 +1,16 @@ /-- error: tactic 'fail' failed -x y : Nat -⊢ x - 1 < x +z : Nat +⊢ z - 1 < z -/ #guard_msgs in -def g (x : Nat) (y : Nat) : Nat := g (x - 1) y -termination_by x +def g (z : Nat) (y : Nat) : Nat := g (z - 1) y +termination_by z decreasing_by fail /-- error: tactic 'fail' failed x : List Nat -y : Nat ⊢ sizeOf x.tail < sizeOf x -/ #guard_msgs in @@ -22,7 +21,6 @@ decreasing_by fail /-- error: tactic 'fail' failed x : List Nat -y : Nat ⊢ x.tail.length < x.length -/ #guard_msgs in @@ -33,7 +31,6 @@ decreasing_by fail /-- error: tactic 'fail' failed x : List Nat -y : Nat ⊢ x.tail.length < x.length -/ #guard_msgs in @@ -49,13 +46,8 @@ end /-- error: tactic 'fail' failed x : List Nat -y : Nat -⊢ (invImage - (fun x => - PSum.casesOn x (fun _x => PSigma.casesOn _x fun x y => x.length) fun _x => - PSigma.casesOn _x fun x y => x.length) - instWellFoundedRelationOfSizeOf).1 - (PSum.inr ⟨x.tail, y⟩) (PSum.inl ⟨x, y⟩) +⊢ (invImage (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) instWellFoundedRelationOfSizeOf).1 + (PSum.inr x.tail) (PSum.inl x) -/ #guard_msgs in set_option debug.rawDecreasingByGoal true in diff --git a/tests/lean/run/fixedParams.lean b/tests/lean/run/fixedParams.lean new file mode 100644 index 0000000000..04317f95a2 --- /dev/null +++ b/tests/lean/run/fixedParams.lean @@ -0,0 +1,101 @@ +private axiom test_sorry : ∀ {α}, α + +set_option trace.Elab.definition.fixedParams true + +namespace Ex1 + +/-- +error: well-founded recursion cannot be used, 'Ex1.foo' does not take any (non-fixed) arguments +--- +info: [Elab.definition.fixedParams] getFixedParams: + • ⏎ + • +-/ +#guard_msgs in +mutual +def foo : Nat := bar +def bar : Nat := foo +decreasing_by exact test_sorry +end + +end Ex1 + + +namespace Ex2 +/-- +error: well-founded recursion cannot be used, 'Ex2.foo' does not take any (non-fixed) arguments +--- +info: [Elab.definition.fixedParams] getFixedParams: + • [#1 #1] + • [#1 #1] +-/ +#guard_msgs in +mutual +def foo (n : Nat) : Nat := bar n +def bar (n : Nat) : Nat := foo n +decreasing_by exact test_sorry +end +end Ex2 + +namespace Ex3 +/-- +error: well-founded recursion cannot be used, 'Ex3.foo' does not take any (non-fixed) arguments +--- +info: [Elab.definition.fixedParams] getFixedParams: + • [#1 #2] [#2 #1] + • [#2 #1] [#1 #2] +-/ +#guard_msgs in +mutual +def foo (n : Nat) (m : Nat) : Nat := bar m n +decreasing_by all_goals exact test_sorry +def bar (n : Nat) (m : Nat) : Nat := foo m n +decreasing_by all_goals exact test_sorry +end +end Ex3 + +namespace Ex4 +/-- +info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3: + In foo c n b m + m not matched +[Elab.definition.fixedParams] getFixedParams: • [#1 #3] ❌ [#3 #1] ❌ • [#3 #1] ❌ [#1 #3] ❌ +-/ +#guard_msgs in +mutual +def foo (a : Nat) (n : Nat) (d : Nat) (m : Nat) : Nat := bar d m a n +decreasing_by exact test_sorry +def bar (b : Nat) (n : Nat) (c : Nat) (m : Nat) : Nat := foo c n b m +decreasing_by exact test_sorry +end +end Ex4 + +namespace Append1 + +/-- +info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1: + In app as bs + x✝¹ =/= as +[Elab.definition.fixedParams] getFixedParams: notFixed 0 2: + In app as bs + x✝ =/= bs +[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ ❌ +-/ +#guard_msgs(info) in +def app : List α → List α → List α + | [], bs => bs + | a::as, bs => a :: app as bs + +/-- +info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1: + In app' as bs + as✝ =/= as +[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ [#3] +-/ +#guard_msgs(info) in +def app' (as : List α) (bs : List α) : List α := + match as with + | [] => bs + | a::as => a :: app' as bs + +end Append1 diff --git a/tests/lean/run/fixedParamsAnnot.lean b/tests/lean/run/fixedParamsAnnot.lean new file mode 100644 index 0000000000..09b80a9018 --- /dev/null +++ b/tests/lean/run/fixedParamsAnnot.lean @@ -0,0 +1,75 @@ +/-! +This test contains functions with fixed parameter that have dependencies on varying parameter, +but only in annotations (optional parameters). +-/ + +private axiom test_sorry : ∀ {α}, α + +namespace Ex1 + +mutual +def foo (varying : Nat) (fixed := varying) : Nat := bar fixed (varying + fixed) +decreasing_by exact test_sorry +def bar (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed +decreasing_by exact test_sorry +end + +/-- +info: equations: +theorem Ex1.foo.eq_1 : ∀ (varying fixed : Nat), foo varying fixed = bar fixed (varying + fixed) +-/ +#guard_msgs in +#print equations foo + +/-- +info: equations: +theorem Ex1.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed +-/ +#guard_msgs in +#print equations bar + + +/-- +info: Ex1.foo.induct (fixed : Nat) (motive1 motive2 : Nat → Prop) + (case1 : ∀ (varying : Nat), motive2 (varying + fixed) → motive1 varying) + (case2 : ∀ (varying : Nat), motive1 (varying + fixed) → motive2 varying) (varying : Nat) : motive1 varying +-/ +#guard_msgs in +#check foo.induct + + +end Ex1 + +namespace Ex2 + +mutual +def bar (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed +decreasing_by exact test_sorry +def foo (varying : Nat) (fixed := varying) : Nat := bar fixed (varying + fixed) +decreasing_by exact test_sorry +end + +/-- +info: equations: +theorem Ex2.foo.eq_1 : ∀ (varying fixed : Nat), foo varying fixed = bar fixed (varying + fixed) +-/ +#guard_msgs in +#print equations foo + +/-- +info: equations: +theorem Ex2.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed +-/ +#guard_msgs in +#print equations bar + +/-- +info: Ex2.foo.induct (fixed : Nat) (motive1 motive2 : Nat → Prop) + (case1 : ∀ (varying : Nat), motive2 (varying + fixed) → motive1 varying) + (case2 : ∀ (varying : Nat), motive1 (varying + fixed) → motive2 varying) (varying : Nat) : motive2 varying +-/ +#guard_msgs in +#check foo.induct + + +end Ex2 diff --git a/tests/lean/run/fixedParamsDep.lean b/tests/lean/run/fixedParamsDep.lean new file mode 100644 index 0000000000..96da1fdc86 --- /dev/null +++ b/tests/lean/run/fixedParamsDep.lean @@ -0,0 +1,79 @@ +/-! +This test contains functions with fixed parameter that have dependencies on varying parameter, +which can happen when those dependencies reduce away. +-/ + +def const (x : α) (_ : β) : α := x + +private axiom test_sorry : ∀ {α}, α + +namespace Ex1 + +mutual +def foo (varying : Nat) (fixed : const Nat varying) : Nat := bar fixed (Nat.add varying fixed) +decreasing_by exact test_sorry +def bar (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed +decreasing_by exact test_sorry +end + +/-- +info: equations: +theorem Ex1.foo.eq_1 : ∀ (varying : Nat) (fixed : const Nat varying), foo varying fixed = bar fixed (varying.add fixed) +-/ +#guard_msgs in +#print equations foo + +/-- +info: equations: +theorem Ex1.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed +-/ +#guard_msgs in +#print equations bar + + +/-- +info: Ex1.foo.induct (motive1 : (varying : Nat) → const Nat varying → Prop) (motive2 : Nat → Nat → Prop) + (case1 : ∀ (varying : Nat) (fixed : const Nat varying), motive2 fixed (varying.add fixed) → motive1 varying fixed) + (case2 : ∀ (fixed varying : Nat), motive1 (varying + fixed) fixed → motive2 fixed varying) (varying : Nat) + (fixed : const Nat varying) : motive1 varying fixed +-/ +#guard_msgs in +#check foo.induct + + +end Ex1 + +namespace Ex2 + +mutual +def bar (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed +decreasing_by exact test_sorry +def foo (varying : Nat) (fixed : const Nat varying) : Nat := bar fixed (Nat.add varying fixed) +decreasing_by exact test_sorry +end + +/-- +info: equations: +theorem Ex2.foo.eq_1 : ∀ (varying : Nat) (fixed : const Nat varying), foo varying fixed = bar fixed (varying.add fixed) +-/ +#guard_msgs in +#print equations foo + +/-- +info: equations: +theorem Ex2.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed +-/ +#guard_msgs in +#print equations bar + +/-- +info: Ex2.foo.induct (motive1 : Nat → Nat → Prop) (motive2 : (varying : Nat) → const Nat varying → Prop) + (case1 : ∀ (fixed varying : Nat), motive2 (varying + fixed) fixed → motive1 fixed varying) + (case2 : ∀ (varying : Nat) (fixed : const Nat varying), motive1 fixed (varying.add fixed) → motive2 varying fixed) + (varying : Nat) (fixed : const Nat varying) : motive2 varying fixed +-/ +#guard_msgs in +#check foo.induct + + +end Ex2 diff --git a/tests/lean/run/fixedParamsReorder.lean b/tests/lean/run/fixedParamsReorder.lean new file mode 100644 index 0000000000..c67bea671f --- /dev/null +++ b/tests/lean/run/fixedParamsReorder.lean @@ -0,0 +1,34 @@ +/-! +This test contains functions with fixed parameter that appear in different orders. +-/ + +private axiom test_sorry : ∀ {α}, α + +mutual +def foo (a : Nat) (n : Nat) (d : Nat) (m : Int) : Nat := bar d m (a + n + d + m.natAbs) n +decreasing_by exact test_sorry +def bar (b : Nat) (n : Int) (c : Nat) (m : Nat) : Nat := foo c m (b + n.natAbs + c + m) n +decreasing_by exact test_sorry +end + +/-- +info: equations: +theorem bar.eq_1 : ∀ (b : Nat) (n : Int) (c m : Nat), bar b n c m = foo c m (b + n.natAbs + c + m) n +-/ +#guard_msgs in +#print equations bar + +/-- +info: foo.induct (n : Nat) (m : Int) (motive1 motive2 : Nat → Nat → Prop) + (case1 : ∀ (a d : Nat), motive2 d (a + n + d + m.natAbs) → motive1 a d) + (case2 : ∀ (b c : Nat), motive1 c (b + m.natAbs + c + n) → motive2 b c) (a d : Nat) : motive1 a d +-/ +#guard_msgs in +#check foo.induct +/-- +info: bar.induct (n : Nat) (m : Int) (motive1 motive2 : Nat → Nat → Prop) + (case1 : ∀ (a d : Nat), motive2 d (a + n + d + m.natAbs) → motive1 a d) + (case2 : ∀ (b c : Nat), motive1 c (b + m.natAbs + c + n) → motive2 b c) (b c : Nat) : motive2 b c +-/ +#guard_msgs in +#check bar.induct diff --git a/tests/lean/run/fixedParamsStructDeps.lean b/tests/lean/run/fixedParamsStructDeps.lean new file mode 100644 index 0000000000..13f64c07d8 --- /dev/null +++ b/tests/lean/run/fixedParamsStructDeps.lean @@ -0,0 +1,33 @@ +/-! +Testing a few more corner cases related to structural mutual recursion, parameters, indices, +dependencies. +-/ + +def const (x : α) (_ : β) : α := x + +private axiom test_sorry : ∀ {α}, α + + +inductive T (p : Nat) : (i : Nat) → Type where + | zero : T p i + | succ : T p i → T p (i + p) → T p i + +/-- +error: failed to infer structural recursion: +Cannot use parameters #4 of foo and #4 of bar: + its type is an inductive datatype and the datatype parameter + p1 + which cannot be fixed as it is an index or depends on an index, and indices cannot be fixed parameters when using structural recursion. +-/ +#guard_msgs in +mutual +def foo (i : Nat) (p1 : Nat) (p2 : const Nat i) : T p1 i → Unit + | .zero => () + | .succ t1 _ => bar i p2 p1 t1 +termination_by structural t => t + +def bar (i : Nat) (p2 : Nat) (p1 : const Nat p2) : T p1 i → Unit + | .zero => () + | .succ t1 _ => foo i p1 p2 t1 +termination_by structural t => t +end diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean index 16b9597626..0c0f7ac157 100644 --- a/tests/lean/run/funind_structural.lean +++ b/tests/lean/run/funind_structural.lean @@ -72,9 +72,10 @@ theorem zip_length {α β} (xs : List α) (ys : List β) : simp [Nat.min_def] split <;> omega -theorem zip_get? {α β} (as : List α) (bs : List β) : - (List.zip as bs).get? i = match as.get? i, bs.get? i with - | some a, some b => some (a, b) | _, _ => none := by +theorem zip_get? {i : Nat} {α β} (as : List α) (bs : List β) : + (List.zip as bs)[i]? = match as[i]?, bs[i]? with + | some a, some b => some (a, b) + | _, _ => none := by induction as, bs using zip.induct generalizing i <;> cases i <;> simp_all @@ -118,18 +119,17 @@ def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β := termination_by structural t /-- -info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop) - (case1 : ∀ (k : Nat) (v : β), motive Tree.leaf k v) +info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (k : Nat) (motive : Tree β → Prop) (case1 : motive Tree.leaf) (case2 : - ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β), - k < key → motive left k v → motive (left.node key value right) k v) + ∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β), + k < key → motive left → motive (left.node key value right)) (case3 : - ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β), - ¬k < key → key < k → motive right k v → motive (left.node key value right) k v) + ∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β), + ¬k < key → key < k → motive right → motive (left.node key value right)) (case4 : - ∀ (k : Nat) (v : β) (left : Tree β) (key : Nat) (value : β) (right : Tree β), - ¬k < key → ¬key < k → motive (left.node key value right) k v) - (t : Tree β) (k : Nat) (v : β) : motive t k v + ∀ (left : Tree β) (key : Nat) (value : β) (right : Tree β), + ¬k < key → ¬key < k → motive (left.node key value right)) + (t : Tree β) : motive t -/ #guard_msgs in #check Tree.insert.induct diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 04ea2ebac6..346f7bf300 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -689,8 +689,8 @@ def foo (fixed : Bool := false) (n : Nat) (m : Nat := 0) : Nat := termination_by n /-- -info: DefaultArgument.foo.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) - (case2 : ∀ (m n : Nat), motive n m → motive n.succ m) (n m : Nat) : motive n m +info: DefaultArgument.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) + (n : Nat) : motive n -/ #guard_msgs in #check foo.induct diff --git a/tests/lean/run/funinduction_generalize.lean b/tests/lean/run/funinduction_generalize.lean index 9e88484a77..d34db2c470 100644 --- a/tests/lean/run/funinduction_generalize.lean +++ b/tests/lean/run/funinduction_generalize.lean @@ -7,6 +7,11 @@ In particular that it behaves the same as `induction … using ….induct`. variable (xs ys : List Nat) variable (P : ∀ {α}, List α → Prop) +-- We re-define this here to avoid stage0 complications +def zipWith (f : α → β → γ) : (xs : List α) → (ys : List β) → List γ + | x::xs, y::ys => f x y :: zipWith f xs ys + | _, _ => [] + /-- error: unsolved goals case case1 @@ -28,7 +33,7 @@ x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs -/ #guard_msgs in example : P (List.zip xs ys) := by - fun_induction List.zipWith _ xs ys + fun_induction zipWith _ xs ys /-- @@ -54,7 +59,7 @@ h : t✝.isEmpty = true -/ #guard_msgs in example (h : xs.isEmpty) : P (List.zip xs ys) := by - fun_induction List.zipWith _ xs ys + fun_induction zipWith _ xs ys /-- @@ -80,7 +85,7 @@ h : t✝.isEmpty = true -/ #guard_msgs in example (h : xs.isEmpty) : P (List.zip xs ys) := by - fun_induction List.zipWith _ xs (ys.take 2) + fun_induction zipWith _ xs (ys.take 2) /-- error: unsolved goals @@ -105,7 +110,7 @@ h : t✝.isEmpty = true -/ #guard_msgs in example (h : xs.isEmpty) : P (List.zip xs ys) := by - induction xs, ys.take 2 using List.zipWith.induct + induction xs, ys.take 2 using zipWith.induct /-- error: unsolved goals @@ -130,7 +135,7 @@ x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs -/ #guard_msgs in example (h : xs.isEmpty) : P (List.zip xs ys) := by - fun_induction List.zipWith _ (xs.take 2) ys + fun_induction zipWith _ (xs.take 2) ys /-- error: unsolved goals @@ -155,7 +160,7 @@ x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs -/ #guard_msgs in example (h : xs.isEmpty) : P (List.zip xs ys) := by - induction xs.take 2, ys using List.zipWith.induct + induction xs.take 2, ys using zipWith.induct /-- error: unsolved goals @@ -180,7 +185,7 @@ h : xs.isEmpty = true -/ #guard_msgs in example (h : xs.isEmpty) : P (List.zip xs ys) := by - fun_induction List.zipWith _ (xs.take 2) ys generalizing xs + fun_induction zipWith _ (xs.take 2) ys generalizing xs /-- error: unsolved goals @@ -205,4 +210,4 @@ h : xs.isEmpty = true -/ #guard_msgs in example (h : xs.isEmpty) : P (List.zip xs ys) := by - induction xs.take 2, ys using List.zipWith.induct generalizing xs + induction xs.take 2, ys using zipWith.induct generalizing xs diff --git a/tests/lean/run/funinduction_ident.lean b/tests/lean/run/funinduction_ident.lean index b3318a4fe8..4af0a168d1 100644 --- a/tests/lean/run/funinduction_ident.lean +++ b/tests/lean/run/funinduction_ident.lean @@ -1,23 +1,36 @@ +-- We re-define these here to avoid stage0 complications +def map (f : α → β) : List α → List β + | [] => [] + | a::as => f a :: map f as + +def zipWith (f : α → β → γ) : (xs : List α) → (ys : List β) → List γ + | x::xs, y::ys => f x y :: zipWith f xs ys + | _, _ => [] + +def append : (xs ys : List α) → List α + | [], bs => bs + | a::as, bs => a :: append as bs + namespace ListEx -theorem map_id (xs : List α) : List.map id xs = xs := by - fun_induction List.map <;> simp_all only [List.map, id] +theorem map_id (xs : List α) : map id xs = xs := by + fun_induction map <;> simp_all only [map, id] -- This works because collect ignores `.dropped` arguments theorem map_map (f : α → β) (g : β → γ) xs : - List.map g (List.map f xs) = List.map (g ∘ f) xs := by - fun_induction List.map <;> simp_all only [List.map, Function.comp] + map g (map f xs) = map (g ∘ f) xs := by + fun_induction map <;> simp_all only [map, Function.comp] -- This should genuinely not work, but have a good error message /-- -error: found more than one suitable call of 'List.append' in the goal. Please include the desired arguments. +error: found more than one suitable call of 'append' in the goal. Please include the desired arguments. -/ #guard_msgs in theorem append_assoc : - List.append xs (List.append ys zs) = List.append (List.append xs ys) zs := by - fun_induction List.append <;> simp_all only [List.append] + append xs (append ys zs) = append (append xs ys) zs := by + fun_induction append <;> simp_all only [append] end ListEx diff --git a/tests/lean/run/grind_constProp.lean b/tests/lean/run/grind_constProp.lean index b12191d1b4..b2cce03842 100644 --- a/tests/lean/run/grind_constProp.lean +++ b/tests/lean/run/grind_constProp.lean @@ -82,10 +82,10 @@ attribute [local grind] State.update State.find? State.get State.erase grind @[simp] theorem State.find?_update_self (σ : State) (x : Var) (v : Val) : (σ.update x v).find? x = some v := by - induction σ, x, v using State.update.induct <;> grind + induction σ using State.update.induct x <;> grind @[simp] theorem State.find?_update (σ : State) (v : Val) (h : x ≠ z) : (σ.update x v).find? z = σ.find? z := by - induction σ, x, v using State.update.induct <;> grind + induction σ using State.update.induct x <;> grind @[grind =] theorem State.find?_update_eq (σ : State) (v : Val) : (σ.update x v).find? z = if x = z then some v else σ.find? z := by @@ -95,17 +95,17 @@ attribute [local grind] State.update State.find? State.get State.erase grind @[simp] theorem State.find?_erase_self (σ : State) (x : Var) : (σ.erase x).find? x = none := by - induction σ, x using State.erase.induct <;> grind + induction σ using State.erase.induct x <;> grind @[simp] theorem State.find?_erase (σ : State) (h : x ≠ z) : (σ.erase x).find? z = σ.find? z := by - induction σ, x using State.erase.induct <;> grind + induction σ using State.erase.induct x <;> grind @[simp, grind =] theorem State.find?_erase_eq (σ : State) : (σ.erase x).find? z = if x = z then none else σ.find? z := by grind only [= find?_erase_self, = find?_erase, cases Or] @[grind] theorem State.length_erase_le (σ : State) (x : Var) : (σ.erase x).length ≤ σ.length := by - induction σ, x using erase.induct <;> grind + induction σ using erase.induct x <;> grind def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ := by grind @@ -299,7 +299,7 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : ( grind @[grind] theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ := by - induction σ₁, σ₂ using State.join.induct <;> grind + induction σ₁ using State.join.induct σ₂ <;> grind @[grind] theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ := by grind diff --git a/tests/lean/run/issue2102.lean b/tests/lean/run/issue2102.lean new file mode 100644 index 0000000000..cfe0675ad2 --- /dev/null +++ b/tests/lean/run/issue2102.lean @@ -0,0 +1,45 @@ +-- works +def g' (T : Type) (ls : List T) : (Option (List T)) := + match ls with + | _::tl => + let res := Option.attach (g' T tl) + res.bind fun x => x.val + | [] => .none + +-- doesn't + +/-- +error: fail to show termination for + g'' +with errors +failed to infer structural recursion: +Not considering parameter T of g'': + its type is not an inductive +Not considering parameter ls of g'': + its type is an inductive datatype + List T + and the datatype parameter + T + depends on the function parameter + T + which is not fixed. +no parameters suitable for structural recursion + +failed to prove termination, possible solutions: + - Use `have`-expressions to prove the remaining goals + - Use `termination_by` to specify a different well-founded relation + - Use `decreasing_by` to specify your own tactic for discharging this kind of goal +T✝ : Type +head✝ : T✝ +tl : List T✝ +T : Type +ls : List T +⊢ sizeOf ls < 1 + sizeOf tl +-/ +#guard_msgs in +def g'' (T : Type) (ls : List T) : (Option (List T)) := + match ls with + | _::tl => + let res := Option.attach (g'' T tl) + res.bind fun ⟨x,h⟩ => x + | [] => .none diff --git a/tests/lean/run/issue2108.lean b/tests/lean/run/issue2108.lean new file mode 100644 index 0000000000..6ca3c98791 --- /dev/null +++ b/tests/lean/run/issue2108.lean @@ -0,0 +1,40 @@ +inductive Foo : Nat → Type where +| foo: (Nat → Foo n) → Foo n + +-- structural recursion failed, produced type incorrect term + +/-- +error: fail to show termination for + Foo.bar +with errors +failed to infer structural recursion: +Not considering parameter #2 of Foo.bar: + its type is an inductive datatype + Foo x✝¹ + and the datatype parameter + x✝¹ + depends on the function parameter + x✝¹ + which is not fixed. +Cannot use parameter #1: + failed to eliminate recursive application + (f 0).bar + + +Could not find a decreasing measure. +The basic measures relate at each recursive call as follows: +(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) + n #1 +1) 36:14-23 = ? + +#1: sizeOf x2 + +Please use `termination_by` to specify a decreasing measure. +-/ +#guard_msgs in +def Foo.bar : {n: Nat} → Foo n → Foo n +| _, foo f => (f 0).bar + +-- it works +def Foo.bar' {n: Nat} : Foo n → Foo n +| foo f => (f 0).bar' diff --git a/tests/lean/run/issue2113.lean b/tests/lean/run/issue2113.lean new file mode 100644 index 0000000000..911b97a151 --- /dev/null +++ b/tests/lean/run/issue2113.lean @@ -0,0 +1,5 @@ +inductive Foo {f: Nat}: {d: Nat} → (h: d ≤ f) → Type where +| foo : Foo (Nat.zero_le _) → (Bool → Foo h) → Foo h + +def Foo.bar (h: d ≤ f): Foo h → Foo h +| foo _ f => (f true).bar h diff --git a/tests/lean/run/issue4671.lean b/tests/lean/run/issue4671.lean index 47dd047082..d6135ac49e 100644 --- a/tests/lean/run/issue4671.lean +++ b/tests/lean/run/issue4671.lean @@ -4,17 +4,6 @@ inductive A (n : Nat) : Type | a : A n | b : A n → A n -/-- -error: cannot use specified measure for structural recursion: - its type is an inductive datatype - A n - and the datatype parameter - n - depends on the function parameter - n - which does not come before the varying parameters and before the indices of the recursion parameter. --/ -#guard_msgs in def A.size (acc n : Nat) : A n → Nat | .a => acc | .b a' => 1 + A.size (acc + 1) n a' @@ -27,17 +16,6 @@ inductive Xn (e : Sigma.{0} (· → Type)) (α : Type) : Nat → Type where | mk1_S {n} (x : Xn e α n) : Xn e α (n+1) | mk2 {n} (s : e.1) (p : e.2 s → Xn e α n) : Xn e α n -/-- -error: cannot use specified measure for structural recursion: - its type is an inductive datatype - Xn e (Xn e α n) m - and the datatype parameter - Xn e α n - depends on the function parameter - n - which does not come before the varying parameters and before the indices of the recursion parameter. --/ -#guard_msgs in def Xn.zip {e α m n} : Xn e (Xn e α n) m → Xn e α (n+m+1) | .mk1_S x => .mk1_S x.zip | .mk2 s p => .mk2 s fun a => (p a).zip diff --git a/tests/lean/run/issue6281.lean b/tests/lean/run/issue6281.lean index 1717f16b6e..20301b5824 100644 --- a/tests/lean/run/issue6281.lean +++ b/tests/lean/run/issue6281.lean @@ -6,6 +6,8 @@ def f (n : Nat) (hn : n % 2 = 1) (m : Nat) (hm : (n + m) % 2 = 1) : Nat := | 0 => 1 | m' + 1 => f n' (by sorry) m' (by sorry) +set_option pp.proofs true + /-- info: f.induct (motive : (n : Nat) → n % 2 = 1 → (m : Nat) → (n + m) % 2 = 1 → Prop) (case1 : ∀ (m : Nat) (hn : 1 % 2 = 1) (hm : (1 + m) % 2 = 1), motive 1 hn m hm) @@ -14,7 +16,8 @@ info: f.induct (motive : (n : Nat) → n % 2 = 1 → (m : Nat) → (n + m) % 2 = (n' + 3 + 0) % 2 = 1 → motive n'.succ.succ.succ hn 0 hm) (case3 : ∀ (n' : Nat) (hn : (n' + 3) % 2 = 1) (m' : Nat) (hm : (n' + 3 + (m' + 1)) % 2 = 1), - (n' + 3 + m'.succ) % 2 = 1 → motive n' ⋯ m' ⋯ → motive n'.succ.succ.succ hn m'.succ hm) + (n' + 3 + m'.succ) % 2 = 1 → + motive n' (f.proof_1 n') m' (f.proof_2 n' m') → motive n'.succ.succ.succ hn m'.succ hm) (n : Nat) (hn : n % 2 = 1) (m : Nat) (hm : (n + m) % 2 = 1) : motive n hn m hm -/ #guard_msgs in diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean index 4d3a3da10e..25b3e90e69 100644 --- a/tests/lean/run/omega.lean +++ b/tests/lean/run/omega.lean @@ -520,54 +520,6 @@ example n = 65536 := by bv_omega --- From https://github.com/leanprover/lean4/issues/5315 --- This used to fail with an unexpected bound variable error. - -def simple_foldl (f: β → α → β) (a: Array α) (i: Nat) (b: β): β := - if h: i < a.size then - simple_foldl f a (i+1) (f b a[i]) - else - b - -/-- -error: omega could not prove the goal: -No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants. --/ -#guard_msgs in -theorem simple_fold_monotonic₁ (a: Array α) (f: β → α → β) (i: Nat) {P: α → β → Prop} {x: α} - (base: P x b) - (mono: ∀ x x' y, P x y → P x (f y x')): P x (simple_foldl f a i b) := by - unfold simple_foldl - split <;> try trivial - apply simple_fold_monotonic₁ - . apply mono; exact base - . exact mono - termination_by a.size - i - decreasing_by - exfalso - rename_i a b - clear a b mono base - rename_i a; clear a - clear base - clear x - rename_i a; clear a - clear x - clear P - rename_i a; clear a - clear P - clear i - rename_i a; clear a - clear i - clear f - rename_i a; clear a - clear f - clear a - rename_i a; clear a - clear a - clear b - rename_i a - omega - /-! ### Error messages -/ /-- diff --git a/tests/lean/run/partial_fixpoint_induct.lean b/tests/lean/run/partial_fixpoint_induct.lean index d0a5f4e6cc..1ed636e09e 100644 --- a/tests/lean/run/partial_fixpoint_induct.lean +++ b/tests/lean/run/partial_fixpoint_induct.lean @@ -72,29 +72,29 @@ partial_fixpoint end /-- -info: dependent2''a.fixpoint_induct (m : Nat) (motive_1 : (Nat → (b : Bool) → if b = true then Nat else Bool) → Prop) - (motive_2 : (Nat → Nat → (b : Bool) → if b = true then Nat else Bool) → Prop) - (motive_3 : (Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool) → Prop) - (adm_1 : Lean.Order.admissible motive_1) (adm_2 : Lean.Order.admissible motive_2) - (adm_3 : Lean.Order.admissible motive_3) +info: dependent2''a.fixpoint_induct (m : Nat) (b : Bool) (motive_1 : (Nat → if b = true then Nat else Bool) → Prop) + (motive_2 : (Nat → Nat → if b = true then Nat else Bool) → Prop) + (motive_3 : (Fin (m + 1) → Nat → if b = true then Nat else Bool) → Prop) (adm_1 : Lean.Order.admissible motive_1) + (adm_2 : Lean.Order.admissible motive_2) (adm_3 : Lean.Order.admissible motive_3) (h_1 : - ∀ (dependent2''a : Nat → (b : Bool) → if b = true then Nat else Bool) - (dependent2''b : Nat → Nat → (b : Bool) → if b = true then Nat else Bool), + ∀ (dependent2''a : Nat → if b = true then Nat else Bool) + (dependent2''b : Nat → Nat → if b = true then Nat else Bool), motive_1 dependent2''a → motive_2 dependent2''b → - motive_1 fun n b => if x : b = true then dependent2''a (n + 1) b else dependent2''b m (n + m) b) + motive_1 fun n => if x : b = true then dependent2''a (n + 1) else dependent2''b m (n + m)) (h_2 : - ∀ (dependent2''b : Nat → Nat → (b : Bool) → if b = true then Nat else Bool) - (dependent2''c : Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool), + ∀ (dependent2''b : Nat → Nat → if b = true then Nat else Bool) + (dependent2''c : Fin (m + 1) → Nat → if b = true then Nat else Bool), motive_2 dependent2''b → motive_3 dependent2''c → - motive_2 fun k n b => if b = true then dependent2''b k n b else dependent2''c (Fin.last m) (n + m) b) + motive_2 fun k n => if b = true then dependent2''b k n else dependent2''c (Fin.last m) (n + m)) (h_3 : - ∀ (dependent2''a : Nat → (b : Bool) → if b = true then Nat else Bool) - (dependent2''c : Fin (m + 1) → Nat → (b : Bool) → if b = true then Nat else Bool), + ∀ (dependent2''a : Nat → if b = true then Nat else Bool) + (dependent2''c : Fin (m + 1) → Nat → if b = true then Nat else Bool), motive_1 dependent2''a → - motive_3 dependent2''c → motive_3 fun i n b => if b = true then dependent2''c i n b else dependent2''a (↑i) b) : - motive_1 (dependent2''a m) ∧ motive_2 (dependent2''b m) ∧ motive_3 (dependent2''c m) + motive_3 dependent2''c → motive_3 fun i n => if b = true then dependent2''c i n else dependent2''a ↑i) : + (motive_1 fun n => dependent2''a m n b) ∧ + (motive_2 fun k n => dependent2''b m k n b) ∧ motive_3 fun i n => dependent2''c m i n b -/ #guard_msgs in #check dependent2''a.fixpoint_induct @@ -115,38 +115,36 @@ partial_fixpoint end /-- -info: dependent3''a.partial_correctness (m : Nat) (motive_1 : Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop) - (motive_2 : Nat → Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop) - (motive_3 : Fin (m + 1) → Nat → (b : Bool) → (if b = true then Nat else Bool) → Prop) +info: dependent3''a.partial_correctness (m : Nat) (b : Bool) (motive_1 : Nat → (if b = true then Nat else Bool) → Prop) + (motive_2 : Nat → Nat → (if b = true then Nat else Bool) → Prop) + (motive_3 : Fin (m + 1) → Nat → (if b = true then Nat else Bool) → Prop) (h_1 : - ∀ (dependent3''a : Nat → (b : Bool) → Option (if b = true then Nat else Bool)) - (dependent3''b : Nat → Nat → (b : Bool) → Option (if b = true then Nat else Bool)), - (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a n b = some r → motive_1 n b r) → - (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), - dependent3''b k n b = some r → motive_2 k n b r) → - ∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), - (if x : b = true then dependent3''a (n + 1) b else dependent3''b m (n + m) b) = some r → motive_1 n b r) + ∀ (dependent3''a : Nat → Option (if b = true then Nat else Bool)) + (dependent3''b : Nat → Nat → Option (if b = true then Nat else Bool)), + (∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a n = some r → motive_1 n r) → + (∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b k n = some r → motive_2 k n r) → + ∀ (n : Nat) (r : if b = true then Nat else Bool), + (if x : b = true then dependent3''a (n + 1) else dependent3''b m (n + m)) = some r → motive_1 n r) (h_2 : - ∀ (dependent3''b : Nat → Nat → (b : Bool) → Option (if b = true then Nat else Bool)) - (dependent3''c : Fin (m + 1) → Nat → (b : Bool) → Option (if b = true then Nat else Bool)), - (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''b k n b = some r → motive_2 k n b r) → - (∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), - dependent3''c i n b = some r → motive_3 i n b r) → - ∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), - (if b = true then dependent3''b k n b else dependent3''c (Fin.last m) (n + m) b) = some r → - motive_2 k n b r) + ∀ (dependent3''b : Nat → Nat → Option (if b = true then Nat else Bool)) + (dependent3''c : Fin (m + 1) → Nat → Option (if b = true then Nat else Bool)), + (∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b k n = some r → motive_2 k n r) → + (∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool), + dependent3''c i n = some r → motive_3 i n r) → + ∀ (k n : Nat) (r : if b = true then Nat else Bool), + (if b = true then dependent3''b k n else dependent3''c (Fin.last m) (n + m)) = some r → motive_2 k n r) (h_3 : - ∀ (dependent3''a : Nat → (b : Bool) → Option (if b = true then Nat else Bool)) - (dependent3''c : Fin (m + 1) → Nat → (b : Bool) → Option (if b = true then Nat else Bool)), - (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a n b = some r → motive_1 n b r) → - (∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), - dependent3''c i n b = some r → motive_3 i n b r) → - ∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), - (if b = true then dependent3''c i n b else dependent3''a (↑i) b) = some r → motive_3 i n b r) : - (∀ (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''a m n b = some r → motive_1 n b r) ∧ - (∀ (k n : Nat) (b : Bool) (r : if b = true then Nat else Bool), dependent3''b m k n b = some r → motive_2 k n b r) ∧ - ∀ (i : Fin (m + 1)) (n : Nat) (b : Bool) (r : if b = true then Nat else Bool), - dependent3''c m i n b = some r → motive_3 i n b r + ∀ (dependent3''a : Nat → Option (if b = true then Nat else Bool)) + (dependent3''c : Fin (m + 1) → Nat → Option (if b = true then Nat else Bool)), + (∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a n = some r → motive_1 n r) → + (∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool), + dependent3''c i n = some r → motive_3 i n r) → + ∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool), + (if b = true then dependent3''c i n else dependent3''a ↑i) = some r → motive_3 i n r) : + (∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a m n b = some r → motive_1 n r) ∧ + (∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b m k n b = some r → motive_2 k n r) ∧ + ∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool), + dependent3''c m i n b = some r → motive_3 i n r -/ #guard_msgs in #check dependent3''a.partial_correctness @@ -162,25 +160,25 @@ def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs wit partial_fixpoint /-- -info: List.findIndex.partial_correctness.{u_1} {α : Type u_1} (motive : List α → (α → Bool) → Nat → Prop) +info: List.findIndex.partial_correctness.{u_1} {α : Type u_1} (p : α → Bool) (motive : List α → Nat → Prop) (h : - ∀ (findIndex : List α → (α → Bool) → Option Nat), - (∀ (xs : List α) (p : α → Bool) (r : Nat), findIndex xs p = some r → motive xs p r) → - ∀ (xs : List α) (p : α → Bool) (r : Nat), + ∀ (findIndex : List α → Option Nat), + (∀ (xs : List α) (r : Nat), findIndex xs = some r → motive xs r) → + ∀ (xs : List α) (r : Nat), (match xs with | [] => none - | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys p) = + | x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys) = some r → - motive xs p r) - (xs : List α) (p : α → Bool) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs p r✝ + motive xs r) + (xs : List α) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs r✝ -/ #guard_msgs in #check List.findIndex.partial_correctness theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : xs.findIndex p = some i → xs[i]?.any p := by - apply List.findIndex.partial_correctness (motive := fun xs p i => xs[i]?.any p) - intro findIndex ih xs p r hsome + apply List.findIndex.partial_correctness (motive := fun xs i => xs[i]?.any p) + intro findIndex ih xs r hsome split at hsome next => contradiction next x ys => @@ -191,5 +189,5 @@ theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) : next => simp only [Option.map_eq_map, Option.map_eq_some'] at hsome obtain ⟨r', hr, rfl⟩ := hsome - specialize ih _ _ _ hr + specialize ih _ _ hr simpa diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index 24a44208d2..be2f6f530e 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -414,17 +414,6 @@ inductive B (n : Nat) : Type | a : A n → B n end -/-- -error: cannot use specified measure for structural recursion: - its type is an inductive datatype - A n - and the datatype parameter - n - depends on the function parameter - n - which does not come before the varying parameters and before the indices of the recursion parameter. --/ -#guard_msgs in set_option linter.constructorNameAsVariable false in mutual def A.size (n : Nat) (m : Nat) : A n → Nat @@ -460,14 +449,11 @@ inductive T (n : Nat) : Nat → Type where | n : T n n → T n n /-- -error: cannot use specified measure for structural recursion: - its type is an inductive datatype - T n n - and the datatype parameter +error: failed to infer structural recursion: +Cannot use parameter #2: + its type is an inductive datatype and the datatype parameter n - depends on the function parameter - n - which does not come before the varying parameters and before the indices of the recursion parameter. + which cannot be fixed as it is an index or depends on an index, and indices cannot be fixed parameters when using structural recursion. -/ #guard_msgs in def T.a {n : Nat} : T n n → Nat @@ -525,18 +511,18 @@ Too many possible combinations of parameters of type Nattish (or please indicate Could not find a decreasing measure. The basic measures relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) -Call from ManyCombinations.f to ManyCombinations.g at 557:15-29: +Call from ManyCombinations.f to ManyCombinations.g at 543:15-29: #1 #2 #3 #4 #5 ? ? ? ? -#6 ? = ? ? -#7 ? ? = ? -#8 ? ? ? = -Call from ManyCombinations.g to ManyCombinations.f at 560:15-29: +#6 ? ? = ? +#7 ? ? ? = +#8 ? = ? ? +Call from ManyCombinations.g to ManyCombinations.f at 546:15-29: #5 #6 #7 #8 #1 _ _ _ _ -#2 _ = _ _ -#3 _ _ = _ -#4 _ _ _ = +#2 _ _ _ ? +#3 _ ? _ _ +#4 _ _ ? _ #1: sizeOf a @@ -554,7 +540,7 @@ Please use `termination_by` to specify a decreasing measure. mutual def f (a b c d : Nattish) : Nat := match a with | .zero => 0 - | .cons n => g (n 23) b c d + | .cons n => g (n 23) c d b def g (a b c d : Nattish) : Nat := match a with | .zero => 0 | .cons n => f (n 42) b c d diff --git a/tests/lean/run/structuralRec2.lean b/tests/lean/run/structuralRec2.lean new file mode 100644 index 0000000000..60753dc559 --- /dev/null +++ b/tests/lean/run/structuralRec2.lean @@ -0,0 +1,37 @@ +/-! +More tests related to structural indices depending on fixed parameters +-/ + +inductive T (n : Nat) : Nat → Type where + | zero : T n 0 + | succ {i} : T n i → T n (i + n) → T n i + + +/-- +error: cannot use specified measure for structural recursion: + its type is an inductive datatype + T (↑f) i + and the datatype parameter + ↑f + depends on the function parameter + i + which is not fixed. +-/ +#guard_msgs in +def foo (i : Nat) (f : Fin i) : T f i → Unit + | .zero => () + | .succ t _ => foo i f t +termination_by structural t => t + +def bar (a : Nat) (i : Nat) (f : Fin a) : T f i → Unit + | .zero => () + | .succ t _ => bar a i f t +termination_by structural t => t + +/-- +info: bar.induct (a : Nat) (f : Fin a) (motive : (i : Nat) → T (↑f) i → Prop) (case1 : motive 0 T.zero) + (case2 : ∀ (i : Nat) (t : T (↑f) i) (a_1 : T (↑f) (i + ↑f)), motive i t → motive i (t.succ a_1)) (i : Nat) + (a✝ : T (↑f) i) : motive i a✝ +-/ +#guard_msgs in +#check bar.induct diff --git a/tests/lean/wf2.lean.expected.out b/tests/lean/wf2.lean.expected.out index 0dfbf6ab6c..95f424e634 100644 --- a/tests/lean/wf2.lean.expected.out +++ b/tests/lean/wf2.lean.expected.out @@ -2,6 +2,6 @@ wf2.lean:3:8-3:17: error: failed to prove termination, possible solutions: - Use `have`-expressions to prove the remaining goals - Use `termination_by` to specify a different well-founded relation - Use `decreasing_by` to specify your own tactic for discharging this kind of goal -x y : Nat +y x : Nat h✝ : x < y ⊢ x - 1 < x