diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index ee9e40c811..4c938f9559 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -21,7 +21,7 @@ import Lean.Data.Array /-! This module finds lexicographic termination arguments for well-founded recursion. -Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), it tries all combinations +Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`) it tries all combinations until it finds one where all proof obligations go through with the given tactic (`decerasing_by`), if given, or the default `decreasing_tactic`. @@ -114,6 +114,77 @@ def naryVarNames (xs : Array Name) : MetaM (Array Name) := do else freshen ns (n.appendAfter "'") +/-- A termination measure with extra fields for use within GuessLex -/ +structure Measure extends TerminationArgument where + /-- + Like `.fn`, but unconditionally with `sizeOf` at the right type. + We use this one when in `evalRecCall` + -/ + natFn : Expr +deriving Inhabited + +/-- String desription of this measure -/ +def Measure.toString (measure : Measure) : MetaM String := do + lambdaTelescope measure.fn fun xs e => do + let e ← mkLambdaFVars xs[measure.arity:] e -- undo overshooting + return (← ppExpr e).pretty + +/-- +Determine if the measure for parameter `x` should be `sizeOf x` or just `x`. + +For non-mutual definitions, we omit `sizeOf` when the argument does not depend on +the other varying parameters, and its `WellFoundedRelation` instance goes via `SizeOf`. + +For mutual definitions, we omit `sizeOf` only when the argument is (at reducible transparency!) of +type `Nat` (else we'd have to worry about differently-typed measures from different functions to +line up). +-/ +def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool := do + let t ← inferType x + if is_mutual + then + withReducible (isDefEq t (.const `Nat [])) + else + try + if t.hasAnyFVar (fun fvar => args.contains (.fvar fvar)) then + pure false + else + let u ← getLevel t + let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t) + let soi ← synthInstance (.app (.const ``SizeOf [u]) t) + isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi) + catch _ => + pure false + +/-- Sets the user names for the given freevars in `xs`. -/ +def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do + let mut lctx ← getLCtx + for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n + withTheReader Meta.Context (fun ctx => { ctx with lctx }) k + +/-- Create one measure for each (eligible) parameter of the given predefintion. -/ +def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) + (userVarNamess : Array (Array Name)) : MetaM (Array (Array Measure)) := 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 + let mut ret : Array Measure := #[] + for x in xs[fixedPrefixSize:] 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]) + -- 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 + else pure natFn + let extraParams := preDef.termination.extraParams + ret := ret.push { ref := .missing, fn, natFn, arity := xs.size, extraParams } + return ret /-- Internal monad used by `withRecApps` -/ abbrev M (recFnName : Name) (α β : Type) : Type := @@ -224,11 +295,11 @@ structure RecCallWithContext where ref : Syntax /-- Function index of caller -/ caller : Nat - /-- Parameters of caller -/ + /-- Parameters of caller (including fixed prefix) -/ params : Array Expr /-- Function index of callee -/ callee : Nat - /-- Arguments to callee -/ + /-- Arguments to callee (including fixed prefix) -/ args : Array Expr ctxt : SavedLocalContext @@ -260,7 +331,8 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext return (false, true) return (true, true) -/-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive +/-- +Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive call site. -/ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) @@ -270,6 +342,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) unless xs.size == fixedPrefixSize + 1 do -- Maybe cleaner to have lambdaBoundedTelescope? 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 @@ -278,7 +351,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})" let (caller, params) ← argsPacker.unpack param let (callee, args) ← argsPacker.unpack arg - RecCallWithContext.create (← getRef) caller params callee args + RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args) /-- A `GuessLexRel` described how a recursive call affects a measure; whether it decreases strictly, non-strictly, is equal, or else. -/ @@ -301,31 +374,18 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat] | no_idea => unreachable! -/-- -Given an expression `e`, produce `sizeOf e` with a suitable instance. -NB: We must use the instance of the type of the function parameter! -The concrete argument at hand may have a different (still def-eq) typ. --/ -def mkSizeOf (e : Expr) : MetaM Expr := do - let ty ← inferType e - let lvl ← getLevel ty - let inst ← synthInstance (mkAppN (mkConst ``SizeOf [lvl]) #[ty]) - let res := mkAppN (mkConst ``sizeOf [lvl]) #[ty, inst, e] - check res - return res - /-- For a given recursive call, and a choice of parameter and argument index, try to prove equality, < or ≤. -/ -def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) - (paramIdx argIdx : Nat) : MetaM GuessLexRel := do +def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array Measure) + (rcc : RecCallWithContext) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do rcc.ctxt.run do - let param := rcc.params[paramIdx]! - let arg := rcc.args[argIdx]! + let callerMeasure := callerMeasures[callerMeasureIdx]! + let calleeMeasure := calleeMeasures[calleeMeasureIdx]! + let param := callerMeasure.natFn.beta rcc.params + let arg := calleeMeasure.natFn.beta rcc.args trace[Elab.definition.wf] "inspectRecCall: {rcc.caller} ({param}) → {rcc.callee} ({arg})" - let arg ← mkSizeOf rcc.args[argIdx]! - let param ← mkSizeOf rcc.params[paramIdx]! for rel in [GuessLexRel.eq, .lt, .le] do let goalExpr := mkAppN rel.toNatRel #[arg, param] trace[Elab.definition.wf] "Goal for {rel}: {goalExpr}" @@ -358,32 +418,35 @@ def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) /- A cache for `evalRecCall` -/ structure RecCallCache where mk'' :: decrTactic? : Option DecreasingBy + callerMeasures : Array Measure + calleeMeasures : Array Measure rcc : RecCallWithContext cache : IO.Ref (Array (Array (Option GuessLexRel))) /-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/ -def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) +def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) (measuress : Array (Array Measure)) (rcc : RecCallWithContext) : BaseIO RecCallCache := do let decrTactic? := decrTactics[rcc.caller]! - let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none) - return { decrTactic?, rcc, cache } + let callerMeasures := measuress[rcc.caller]! + let calleeMeasures := measuress[rcc.callee]! + let cache ← IO.mkRef <| Array.mkArray callerMeasures.size (Array.mkArray calleeMeasures.size Option.none) + return { decrTactic?, callerMeasures, calleeMeasures, rcc, cache } /-- Run `evalRecCall` and cache there result -/ -def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do +def RecCallCache.eval (rc: RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do -- Check the cache first - if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then + if let Option.some res := (← rc.cache.get)[callerMeasureIdx]![calleeMeasureIdx]! then return res else - let res ← evalRecCall rc.decrTactic? rc.rcc paramIdx argIdx - rc.cache.modify (·.modify paramIdx (·.set! argIdx res)) + let res ← evalRecCall rc.decrTactic? rc.callerMeasures rc.calleeMeasures rc.rcc callerMeasureIdx calleeMeasureIdx + rc.cache.modify (·.modify callerMeasureIdx (·.set! calleeMeasureIdx res)) return res - /-- Print a single cache entry as a string, without forcing it -/ -def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do +def RecCallCache.prettyEntry (rcc : RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM String := do let cachedEntries ← rcc.cache.get - return match cachedEntries[paramIdx]![argIdx]! with + return match cachedEntries[callerMeasureIdx]![calleeMeasureIdx]! with | .some rel => toString rel | .none => "_" @@ -397,10 +460,10 @@ inductive MutualMeasure where /-- Evaluate a recursive call at a given `MutualMeasure` -/ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel - | .args argIdxs => do - let paramIdx := argIdxs[rc.rcc.caller]! - let argIdx := argIdxs[rc.rcc.callee]! - rc.eval paramIdx argIdx + | .args taIdxs => do + let callerMeasureIdx := taIdxs[rc.rcc.caller]! + let calleeMeasureIdx := taIdxs[rc.rcc.callee]! + rc.eval callerMeasureIdx calleeMeasureIdx | .func funIdx => do if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then return .lt @@ -409,97 +472,29 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel else return .eq -/-- -Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`, -where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal. -This is the case for types such as `Prop`, `Type u`, etc. -These arguments should not be considered when guessing a well-founded relation. -See `generateCombinations?` --/ -def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) := - lambdaTelescope preDef.value fun xs _ => do - let mut result := #[] - for x in xs[fixedPrefixSize:], i in [:xs.size] do - try - let sizeOf ← whnfD (← mkAppM ``sizeOf #[x]) - if sizeOf.isLit then - result := result.push i - catch _ => - result := result.push i - return result /-- -Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`, -where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff the -`WellFoundedRelation` of `aᵢ` goes via `SizeOf`, and `aᵢ` does not depend on `y₁`…. +Generate all combination of measures. Assumes we have numbered the measures of each function, +and their counts is in `numMeasures`. -These are the parameters for which we omit an explicit call to `sizeOf` in the termination argument. - -We only use this in the non-mutual case; in the mutual case we would have to additional check -if the parameters that line up in the actual `TerminationWF` have the same type. --/ -def getSizeOfParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) := - lambdaTelescope preDef.value fun xs _ => do - let xs : Array Expr := xs[fixedPrefixSize:] - let mut result := #[] - for x in xs, i in [:xs.size] do - try - let t ← inferType x - if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then continue - let u ← getLevel t - let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t) - let soi ← synthInstance (.app (.const ``SizeOf [u]) t) - if ← isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi) then - result := result.push i - catch _ => - pure () - return result - -/-- -Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`, -where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `aᵢ` is `Nat`. -These are parameters where we can definitely omit the call to `sizeOf`. --/ -def getNatParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) := - lambdaTelescope preDef.value fun xs _ => do - let xs : Array Expr := xs[fixedPrefixSize:] - let mut result := #[] - for x in xs, i in [:xs.size] do - let t ← inferType x - if ← withReducible (isDefEq t (.const `Nat [])) then - result := result.push i - return result - -/-- -Generate all combination of arguments, skipping those that are forbidden. - -Sorts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to +This puts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to try first, when the mutually recursive functions have similar argument structures -/ -partial def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) - (threshold : Nat := 32) : Option (Array (Array Nat)) := +partial def generateCombinations? (numMeasures : Array Nat) (threshold : Nat := 32) : + Option (Array (Array Nat)) := (do goUniform 0; go 0 #[]) |>.run #[] |>.2 where - isForbidden (fidx : Nat) (argIdx : Nat) : Bool := - if h : fidx < forbiddenArgs.size then - forbiddenArgs[fidx] |>.contains argIdx - else - false - -- Enumerate all permissible uniform combinations - goUniform (argIdx : Nat) : OptionT (StateM (Array (Array Nat))) Unit := do - if numArgs.all (argIdx < ·) then - unless forbiddenArgs.any (·.contains argIdx) do - modify (·.push (Array.mkArray numArgs.size argIdx)) - goUniform (argIdx + 1) + goUniform (idx : Nat) : OptionT (StateM (Array (Array Nat))) Unit := do + if numMeasures.all (idx < ·) then + modify (·.push (Array.mkArray numMeasures.size idx)) + goUniform (idx + 1) -- Enumerate all other permissible combinations go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do - if h : fidx < numArgs.size then - let n := numArgs[fidx] - for argIdx in [:n] do - unless isForbidden fidx argIdx do - withReader (·.push argIdx) (go (fidx + 1)) + if h : fidx < numMeasures.size then + let n := numMeasures[fidx] + for idx in [:n] do withReader (·.push idx) (go (fidx + 1)) else let comb ← read unless comb.all (· == comb[0]!) do @@ -507,19 +502,19 @@ where if (← get).size > threshold then failure - /-- -Enumerate all meausures we want to try: All arguments (resp. combinations thereof) and +Enumerate all meausures we want to try. + +All arguments (resp. combinations thereof) and possible orderings of functions (if more than one) -/ -def generateMeasures (forbiddenArgs : Array (Array Nat)) (arities : Array Nat) : - MetaM (Array MutualMeasure) := do - let some arg_measures := generateCombinations? forbiddenArgs arities +def generateMeasures (numTermArgs : Array Nat) : MetaM (Array MutualMeasure) := do + let some arg_measures := generateCombinations? numTermArgs | throwError "Too many combinations" let func_measures := - if arities.size > 1 then - (List.range arities.size).toArray + if numTermArgs.size > 1 then + (List.range numTermArgs.size).toArray else #[] @@ -609,19 +604,19 @@ def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do /-- Explain what we found out about the recursive calls (non-mutual case) -/ -def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do - let header := varNames.map (·.eraseMacroScopes.toString) +def explainNonMutualFailure (measures : Array Measure) (rcs : Array RecCallCache) : MetaM Format := do + let header ← measures.mapM Measure.toString let mut table : Array (Array String) := #[#[""] ++ header] for i in [:rcs.size], rc in rcs do let mut row := #[s!"{i+1}) {← rc.rcc.posString}"] - for argIdx in [:varNames.size] do + for argIdx in [:measures.size] do row := row.push (← rc.prettyEntry argIdx argIdx) table := table.push row return formatTable table /-- Explain what we found out about the recursive calls (mutual case) -/ -def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name)) +def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Measure)) (rcs : Array RecCallCache) : MetaM Format := do let mut r := Format.nil @@ -631,33 +626,33 @@ def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++ f!"at {← rc.rcc.posString}:\n" - let header := varNamess[caller]!.map (·.eraseMacroScopes.toString) + let header ← measuress[caller]!.mapM Measure.toString let mut table : Array (Array String) := #[#[""] ++ header] if caller = callee then -- For self-calls, only the diagonal is interesting, so put it into one row let mut row := #[""] - for argIdx in [:varNamess[caller]!.size] do + for argIdx in [:measuress[caller]!.size] do row := row.push (← rc.prettyEntry argIdx argIdx) table := table.push row else - for argIdx in [:varNamess[callee]!.size] do + for argIdx in [:measuress[callee]!.size] do let mut row := #[] - row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString - for paramIdx in [:varNamess[caller]!.size] do + row := row.push (← measuress[callee]![argIdx]!.toString) + for paramIdx in [:measuress[caller]!.size] do row := row.push (← rc.prettyEntry paramIdx argIdx) table := table.push row r := r ++ formatTable table ++ "\n" return r -def explainFailure (declNames : Array Name) (varNamess : Array (Array Name)) +def explainFailure (declNames : Array Name) (measuress : Array (Array Measure)) (rcs : Array RecCallCache) : MetaM Format := do let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++ "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n" if declNames.size = 1 then - r := r ++ (← explainNonMutualFailure varNamess[0]! rcs) + r := r ++ (← explainNonMutualFailure measuress[0]! rcs) else - r := r ++ (← explainMutualFailure declNames varNamess rcs) + r := r ++ (← explainMutualFailure declNames measuress rcs) return r /-- @@ -671,25 +666,16 @@ 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 withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do - let mut lctx ← getLCtx - for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n - withTheReader Meta.Context (fun ctx => { ctx with lctx }) k - def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) - (userVarNamess : Array (Array Name)) (needsNoSizeOf : Array (Array Nat)) + (userVarNamess : Array (Array Name)) (measuress : Array (Array Measure)) (solution : Array MutualMeasure) : MetaM TerminationArguments := do preDefs.mapIdxM fun funIdx preDef => do + let measures := measuress[funIdx]! lambdaTelescope preDef.value fun xs _ => do withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do - let args ← solution.mapM fun - | .args varIdxs => - let arg := varIdxs[funIdx]! - if needsNoSizeOf[funIdx]!.contains arg then - pure xs[fixedPrefixSize + arg]! - else - mkAppM ``sizeOf #[xs[fixedPrefixSize + arg]!] - | .func funIdx' => pure <| mkNatLit <| if funIdx' == funIdx then 1 else 0 + let args := solution.map fun + | .args taIdxs => measures[taIdxs[funIdx]!]!.fn.beta xs + | .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0 let fn ← mkLambdaFVars xs (← mkProdElem args) let extraParams := preDef.termination.extraParams return { ref := .missing, arity := xs.size, extraParams, fn} @@ -716,40 +702,36 @@ terminates. See the module doc string for a high-level overview. def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) : MetaM TerminationArguments := do - let arities := argsPacker.varNamess.map (·.size) let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·) trace[Elab.definition.wf] "varNames is: {userVarNamess}" - let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize ·) - let needsNoSizeOf ← - if preDefs.size = 1 then - preDefs.mapM (getSizeOfParams fixedPrefixSize ·) - else - preDefs.mapM (getNatParams fixedPrefixSize ·) + -- For every function, the meaures we want to use + -- (One for each non-forbiddend arg) + let measuress ← simpleMeasures preDefs fixedPrefixSize userVarNamess -- The list of measures, including the measures that order functions. -- The function ordering measures come last - let measures ← generateMeasures forbiddenArgs arities + let measures ← generateMeasures (measuress.map (·.size)) -- If there is only one plausible measure, use that if let #[solution] := measures then - let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess needsNoSizeOf #[solution] + let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress #[solution] reportTermArgs preDefs termArgs return termArgs -- Collect all recursive calls and extract their context let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker let recCalls := filterSubsumed recCalls - let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·) + let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) measuress ·) let callMatrix := rcs.map (inspectCall ·) match ← liftMetaM <| solve measures callMatrix with | .some solution => do - let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess needsNoSizeOf solution + let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress solution reportTermArgs preDefs termArgs return termArgs | .none => - let explanation ← explainFailure (preDefs.map (·.declName)) userVarNamess rcs + let explanation ← explainFailure (preDefs.map (·.declName)) measuress rcs Lean.throwError <| "Could not find a decreasing measure.\n" ++ explanation ++ "\n" ++ "Please use `termination_by` to specify a decreasing measure." diff --git a/tests/lean/guessLex.lean b/tests/lean/guessLex.lean index 006cb2b696..9a8c6418e6 100644 --- a/tests/lean/guessLex.lean +++ b/tests/lean/guessLex.lean @@ -213,9 +213,9 @@ end MutualNotNat2 namespace MutualNotNat3 -- A varant of the above, but where the type of the parameter refined to `Nat`. --- This tests if `GuessLex` is inferring the `SizeOf` instance based on the type of the --- concrete parameter/argument (wrong, but status quo), or based on the types in the function --- signature (correct, todo) +-- Previously `GuessLex` was inferring the `SizeOf` instance based on the type of the +-- *concrete* parameter or argument, which was wrong. +-- The inference needs to be based on the parameter type in the function's signature. def OddNat3 := Nat instance : SizeOf OddNat3 := ⟨fun n => 42 - @id Nat n⟩ @[simp] theorem OddNat3.sizeOf_eq (n : OddNat3) : sizeOf n = 42 - @id Nat n := rfl diff --git a/tests/lean/guessLex.lean.expected.out b/tests/lean/guessLex.lean.expected.out index da0c771e09..3cedc21391 100644 --- a/tests/lean/guessLex.lean.expected.out +++ b/tests/lean/guessLex.lean.expected.out @@ -54,14 +54,7 @@ Inferred termination argument: termination_by x1 => x1 Inferred termination argument: termination_by sizeOf o -guessLex.lean:222:0-234:3: error: Could not find a decreasing measure. -The arguments relate at each recursive call as follows: -(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) -Call from MutualNotNat3.foo to MutualNotNat3.bar at 226:23-35: - x1 -x1 < -Call from MutualNotNat3.bar to MutualNotNat3.foo at 231:30-42: - x1 -x1 ? - -Please use `termination_by` to specify a decreasing measure. +Inferred termination argument: +termination_by x1 => x1 +Inferred termination argument: +termination_by x1 => sizeOf x1 diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out index 274909f64d..8aa7ad0dd4 100644 --- a/tests/lean/guessLexFailures.lean.expected.out +++ b/tests/lean/guessLexFailures.lean.expected.out @@ -46,10 +46,10 @@ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) - n m h x4 -1) 39:6-27 = = _ = -2) 40:6-25 = < _ _ -3) 41:6-25 < _ _ _ + n m x4 +1) 39:6-27 = = = +2) 40:6-25 = < _ +3) 41:6-25 < _ _ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: @@ -79,18 +79,17 @@ Call from Mutual.f to Mutual.g at 63:8-39: n m l n < ? ? m ? = ? -H _ _ _ l ? ? < Call from Mutual.g to Mutual.g at 68:8-35: - n m H l - ? ? _ = + n m l + ? ? = Call from Mutual.g to Mutual.g at 69:8-33: - n m H l - _ _ _ < + n m l + _ _ < Call from Mutual.g to Mutual.h at 70:8-27: - n m H l -n _ _ _ ? -m _ _ _ ? + n m l +n _ _ ? +m _ _ ? Call from Mutual.h to Mutual.f at 75:8-33: n m n _ _