From a2d5d94dc6ecf3983b08ba86dc0013667c93edc2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 14 Nov 2023 11:42:50 +0100 Subject: [PATCH 01/27] feat: Guess lexicographic order for well-founded recursion --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 613 +++++++++++++++++++ src/Lean/Elab/PreDefinition/WF/Main.lean | 10 +- 2 files changed, 622 insertions(+), 1 deletion(-) create mode 100644 src/Lean/Elab/PreDefinition/WF/GuessLex.lean diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean new file mode 100644 index 000000000000..484b19e5774c --- /dev/null +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -0,0 +1,613 @@ +/- +Copyright (c) 2023 Joachim Breitner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +import Lean.Util.HasConstCache +import Lean.Meta.CasesOn +import Lean.Meta.Match.Match +import Lean.Meta.Tactic.Cleanup +import Lean.Meta.Tactic.Refl +import Lean.Elab.Quotation +import Lean.Elab.RecAppSyntax +import Lean.Elab.PreDefinition.Basic +import Lean.Elab.PreDefinition.Structural.Basic +import Lean.Elab.PreDefinition.WF.TerminationHint + + +/-! +This module implements heuristics to finding lexicographic termination measures +for well-founded recursion. The goal is to try all lexicographic measures and +find one for which all proof obligations go through with the given or default +`decreasing_by` tatic. + +The crucial optimiziation is to look at each argument of each recursive call _once_, +try to prove `<` and (if that fails `≤`), and then look at that table to pick a suitable +measure. The next-crucial optimization is to fill that table lazily. + +This way, we run the (likely expensive) tactics as few times as possible, while still being +able to consider a possibly large number of combinations. + + +In the case of mutual recursion, a single measure is not just one argument position, but +one argument from each recursive function. Enumerating these can lead to a combinatoric explosion, +so we bound the nubmer of measures tried. + +In addition to measures derived from `sizeOf x` where `x` is an argument, it also considers +measures that order the functions. This way we can support mutual function definitions where +no arguments decrease from one function to another. + +The result of this module is a `TerminationWF`, which is then passed on to `wfRecursion`; this +design is crucial so that whatever we infer in this module could also be written manually by the +user. It would be bad if there are function definitions that can only be processed with the +guessed lexicographic order. + +The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL” +by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 10.1007/978-3-540-74591-4_5 +. + +-/ + +set_option autoImplicit false + +open Lean Meta Elab + +namespace Lean.Elab.WF.GuessLex + +/-- +Given a predefinition, find good variable names for its parameters. +Use user-given parameter names if present; use x1...xn otherwise. +The length of the returned array is also used to determine the arity +of the function, so it should match what `packDomain` does. +-/ +def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : TermElabM (Array Name):= do + lambdaTelescope preDef.value fun xs _ => do + let xs := xs.extract fixedPrefixSize xs.size + let mut ns := #[] + for i in List.range xs.size do + let n ← xs[i]!.fvarId!.getUserName + if n.hasMacroScopes then + -- TODO: Prettier code to generate x1...xn + ns := ns.push (← mkFreshUserName (.mkSimple ("x" ++ (repr (i+1)).pretty))) + else + ns := ns.push n + return ns + +/-- Given + - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and + - expression `e : B[discrs]`, + returns the expressions `B[C_1[ys_1]]) ... B[C_n[ys_n]]`. + (with `ys_i` as loose bound variable, ready to be `.instantiate`d) + Cf. `MatcherApp.addArg`. +-/ +def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := + lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do + unless motiveArgs.size == matcherApp.discrs.size do + -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. + throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" + + let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i eAbst => do + let motiveArg := motiveArgs[i]! + let discr := matcherApp.discrs[i]! + let eTypeAbst ← kabstract eAbst discr + return eTypeAbst.instantiate1 motiveArg + let eEq ← mkEq eAbst eAbst + + let matcherLevels ← match matcherApp.uElimPos? with + | none => pure matcherApp.matcherLevels + | some pos => + pure <| matcherApp.matcherLevels.set! pos levelZero + let motive ← mkLambdaFVars motiveArgs eEq + let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params + let aux := mkApp aux motive + let aux := mkAppN aux matcherApp.discrs + unless (← isTypeCorrect aux) do + throwError "failed to add argument to matcher application, type error when constructing the new motive" + let auxType ← inferType aux + let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let altAuxTys ← altAuxs.mapM inferType + let res ← altAuxTys.mapM fun altAux => do + let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAux + let body := body.getArg! 2 + -- and abstract over the parameters of the alternative again + Expr.abstractM body fvs + return res + +/-- + Given a `casesOn` application `c` of the form + ``` + casesOn As (fun is x => motive[i, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining + ``` + and a type `e : B[is, major]`, for every alternative `i`, construct the type + ``` + B[C_i[ys_i]] + ``` + (with `ys_i` as loose bound variable, ready to be `.instantiate`d) +-/ +def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := + lambdaTelescope c.motive fun motiveArgs _motiveBody => do + unless motiveArgs.size == c.indices.size + 1 do + throwError "failed to add argument to `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders" + let discrs := c.indices ++ #[c.major] + let mut eAbst := e + for motiveArg in motiveArgs.reverse, discr in discrs.reverse do + eAbst := (← kabstract eAbst discr).instantiate1 motiveArg + -- Up to this point, this is cargo-culted from `CasesOn.App.addArg` + -- Let's create something Prop-typed that mentions `e`, by writing `e = e`. + let eEq ← mkEq eAbst eAbst + let motive ← mkLambdaFVars motiveArgs eEq + let us := if c.propOnly then c.us else levelZero :: c.us.tail! + -- Now instantiate the casesOn wth this synthetic motive + let aux := mkAppN (mkConst c.declName us) c.params + let aux := mkApp aux motive + let aux := mkAppN aux discrs + check aux + let auxType ← inferType aux + -- The type of the remaining arguments will mention `e` instantiated for each arg + -- so extract them + let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let altAuxTys ← altAuxs.mapM inferType + let res ← altAuxTys.mapM fun altAux => do + let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAux + let body := body.getArg! 2 + -- and abstract over the parameters of the alternative again + Expr.abstractM body fvs + return res + +@[reducible] +def M (recFnName : Name) (α β : Type) : Type := + StateRefT (Array α) (StateRefT (HasConstCache recFnName) TermElabM) β + +partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (e : Expr) (scrut : Expr) + (k : Expr → Array Expr → TermElabM α) : TermElabM (Array α) := do + trace[Elab.definition.wf] "withRecApps: {indentExpr e}" + let (_, as) ← loop scrut e |>.run #[] |>.run' {} + return as +where + processRec (scrut : Expr) (e : Expr) : M recFnName α Unit := do + if e.getAppNumArgs < fixedPrefixSize + 1 then + loop scrut (← etaExpand e) + else + let a ← k scrut e.getAppArgs + modifyThe (Array α) (·.push a) + + processApp (scrut : Expr) (e : Expr) : M recFnName α Unit := do + e.withApp fun f args => do + args.forM (loop scrut) + if f.isConstOf recFnName then + processRec scrut e + else + loop scrut f + + containsRecFn (e : Expr) : M recFnName α Bool := do + modifyGetThe (HasConstCache recFnName) (·.contains e) + + loop (scrut : Expr) (e : Expr) : M recFnName α Unit := do + if !(← containsRecFn e) then + return + -- trace[Elab.definition.wf] "loop: {indentExpr scrut}{indentExpr e}" + match e with + | Expr.lam n d b c => + loop scrut d + withLocalDecl n c d fun x => do + loop scrut (b.instantiate1 x) + | Expr.forallE n d b c => + loop scrut d + withLocalDecl n c d fun x => do + loop scrut (b.instantiate1 x) + | Expr.letE n type val body _ => + loop scrut type + loop scrut val + withLetDecl n type val fun x => do + loop scrut (body.instantiate1 x) + | Expr.mdata _d b => + if let some stx := getRecAppSyntax? e then + withRef stx <| loop scrut b + else + loop scrut b + | Expr.proj _n _i e => loop scrut e + | Expr.const .. => if e.isConstOf recFnName then processRec scrut e + | Expr.app .. => + match (← matchMatcherApp? e) with + | some matcherApp => + if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then + processApp scrut e + else + let altScruts ← matcherApp.transform scrut + (Array.zip matcherApp.alts altScruts).forM fun (alt, altScrut) => + lambdaTelescope alt fun xs altBody => do + loop (altScrut.instantiateRev xs) altBody + | none => + match (← toCasesOnApp? e) with + | some casesOnApp => + if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then + processApp scrut e + else + let altScruts ← casesOnApp.transform scrut + (Array.zip casesOnApp.alts altScruts).forM fun (alt, altScrut) => + lambdaTelescope alt fun xs altBody => do + loop (altScrut.instantiateRev xs) altBody + | none => processApp scrut e + | e => do + let _ ← ensureNoRecFn recFnName e + +/-- A `SavedLocalCtxt` captures the local context (e.g. of a recursive call), +so that it can be resumed later. +-/ +structure SavedLocalCtxt where + savedState : Term.SavedState + savedLocalContext : LocalContext + savedLocalInstances : LocalInstances + savedTermContext : Term.Context + +def SavedLocalCtxt.create : TermElabM SavedLocalCtxt := do + let savedState ← saveState + let savedLocalContext ← getLCtx + let savedLocalInstances ← getLocalInstances + let savedTermContext ← readThe Term.Context + return { savedState, savedLocalContext, savedLocalInstances, savedTermContext } + + +def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : TermElabM α) : + TermElabM α := withoutModifyingState $ do + restoreState slc.savedState + withLCtx slc.savedLocalContext slc.savedLocalInstances do + withTheReader Term.Context (fun _ => slc.savedTermContext) do + k + +def SavedLocalCtxt.within {α} (slc : SavedLocalCtxt) (k : TermElabM α) : + TermElabM (SavedLocalCtxt × α) := + slc.run do + let x ← k + let slc' ← SavedLocalCtxt.create + pure (slc', x) + + +/-- A `RecCallContext` focuses on a single recursive call in a unary predefinition, +and runs the given action in the context of that call. +-/ +structure RecCallContext where + --- Function index of caller + caller : Nat + --- Parameters of caller + params : Array Expr + --- Function index of callee + callee : Nat + --- Arguments to callee + args : Array Expr + ctxt : SavedLocalCtxt + +/-- Given the packed argument of a (possibly) mutual and (possibly) nary call, +return the function index that is called and the arguments individually. +Cf. `packMutual` +-/ +def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) : + m (Nat × Array Expr) := do + -- count PSum injections to find out which function is doing the call + let mut funidx := 0 + let mut e := e + while funidx + 1 < arities.size do + if e.isAppOfArity ``PSum.inr 3 then + e := e.getArg! 2 + funidx := funidx + 1 + else if e.isAppOfArity ``PSum.inl 3 then + e := e.getArg! 2 + break + else + throwError "Unexpected expression while unpacking mutual argument" + + -- now unpack PSigmas + let arity := arities[funidx]! + let mut args := #[] + while args.size + 1 < arity do + if e.isAppOfArity ``PSigma.mk 4 then + args := args.push (e.getArg! 2) + e := e.getArg! 3 + else + throwError "Unexpected expression while unpacking n-ary argument" + args := args.push e + return (funidx, args) + +def RecCallContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) : + TermElabM RecCallContext := do + return { caller, params, callee, args, ctxt := (← SavedLocalCtxt.create) } + +/-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive +call site. +-/ +def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat) + : TermElabM (Array RecCallContext) := withoutModifyingState do + addAsAxiom unaryPreDef + lambdaTelescope unaryPreDef.value fun xs body => do + unless xs.size == fixedPrefixSize + 1 do + -- Maybe cleaner to have lambdaBoundedTelescope? + throwError "Unexpected number of lambdas in unary pre-definition" + -- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}" + let param := xs[fixedPrefixSize]! + withRecApps unaryPreDef.declName fixedPrefixSize body param fun param args => do + unless args.size ≥ fixedPrefixSize + 1 do + throwError "Insufficient arguments in recursive call" + let arg := args[fixedPrefixSize]! + let (caller, params) ← unpackArg arities param + let (callee, args) ← unpackArg arities arg + RecCallContext.create caller params callee args + +inductive GuessLexRel | lt | eq | le | no_idea +deriving Repr, DecidableEq + +instance : ToFormat GuessLexRel where + format | .lt => "<" + | .eq => "=" + | .le => "≤" + | .no_idea => "?" + +def GuessLexRel.toNatRel : GuessLexRel → Expr + | lt => mkAppN (mkConst ``LT.lt [levelZero]) #[mkConst ``Nat, mkConst ``instLTNat] + | eq => mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat] + | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat] + | no_idea => unreachable! -- TODO: keep it partial or refactor? + +def mkSizeOf (e : Expr) : TermElabM 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 choice of paramter index, +-- try to prove requality, < or ≤ +def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx argIdx : Nat) : + TermElabM GuessLexRel := do + rcc.ctxt.run do + let param := rcc.params[paramIdx]! + let arg := rcc.args[argIdx]! + 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 (unchecked): {goalExpr}" + check goalExpr + + let mvar ← mkFreshExprSyntheticOpaqueMVar goalExpr + let mvarId := mvar.mvarId! + let mvarId ← mvarId.cleanup + -- logInfo m!"Remaining goals: {goalsToMessageData [mvarId]}" + try + if rel = .eq then + MVarId.refl mvarId + else do + match decrTactic? with + | none => + let remainingGoals ← Tactic.run mvarId do + Tactic.evalTactic (← `(tactic| decreasing_tactic)) + remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId] + let _expr ← instantiateMVars mvar + -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" + pure () + | some decrTactic => Term.withoutErrToSorry do + -- make info from `runTactic` available + pushInfoTree (.hole mvarId) + Term.runTactic mvarId decrTactic + let _expr ← instantiateMVars mvar + -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" + pure () + return rel + catch _e => + -- trace[Elab.definition.wf] "Did not find {repr rel} proof of {goalsToMessageData [mvarId]}" + continue + return .no_idea + +-- A cache for `evalRecCall` +structure RecCallCache where mk'' :: + decrTactic? : Option Syntax + rcc : RecCallContext + cache : IO.Ref (Array (Array (Option GuessLexRel))) + +def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallContext) : + BaseIO RecCallCache := do + let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none) + return { decrTactic?, rcc, cache } + +def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : + TermElabM GuessLexRel := do + -- Check the cache first + if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then + return res + else + let res ← evalRecCall rc.decrTactic? rc.rcc paramIdx argIdx + rc.cache.modify (·.modify paramIdx (·.set! argIdx res)) + return res + +def RecCallCache.pretty (rc : RecCallCache) : IO Format := do + let mut r := Format.nil + let d ← rc.cache.get + for paramIdx in [:d.size] do + for argIdx in [:d[paramIdx]!.size] do + if let .some entry := d[paramIdx]![argIdx]! then + r := r ++ + f!"(Param {paramIdx}, arg {argIdx}): {entry}" ++ Format.line + return r + +/-- The measures that we order lexicographically can be comparing arguments, +or numbering the functions -/ +inductive MutualMeasure where + | args : Array Nat → MutualMeasure + --- The given function index is assigned 1, the rest 0 + | func : Nat → MutualMeasure + +-- Evaluate a call at a given measure +def inspectCall (rc : RecCallCache) : MutualMeasure → TermElabM GuessLexRel + | .args argIdxs => do + let paramIdx := argIdxs[rc.rcc.caller]! + let argIdx := argIdxs[rc.rcc.callee]! + rc.eval paramIdx argIdx + | .func funIdx => do + if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then + return .lt + if rc.rcc.caller != funIdx && rc.rcc.callee == funIdx then + return .no_idea + 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. + This 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 + + +-- 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 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)) := + (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) + + -- 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)) + else + let comb ← read + unless comb.all (· == comb[0]!) do + modify (·.push comb) + if (← get).size > threshold then + failure + + +/-- The core logic of guessing the lexicographic order +Given a matrix that for each call and measure indicates whether that measure is +decreasing, equal, less-or-equal or unknown, It finds a sequence of measures +that is lexicographically decreasing. + +The matrix is implemented here as an array of monadic query methods only so that +we can fill is lazily. Morally, this is a pure function +-/ +partial def solve {m} {α} [Monad m] (measures : Array α) + (calls : Array (α → m GuessLexRel)) : m (Option (Array α)) := do + go measures calls #[] + where + go (measures : Array α) (calls : Array (α → m GuessLexRel)) (acc : Array α) := do + if calls.isEmpty then return .some acc + + -- Find the first measure that has at least one < and otherwise only = or <= + for h : measureIdx in [:measures.size] do + let measure := measures[measureIdx]'h.2 + let mut has_lt := false + let mut all_le := true + let mut todo := #[] + for call in calls do + let entry ← call measure + if entry = .lt then + has_lt := true + else + todo := todo.push call + if entry != .le && entry != .eq then + all_le := false + break + -- No progress here? Try the next measure + if not (has_lt && all_le) then continue + -- We found a suitable measure, remove it from the list (mild optimization) + let measures' := measures.eraseIdx measureIdx + return ← go measures' todo (acc.push measure) + -- None found, we have to give up + return .none + +def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name)) + (measures : Array MutualMeasure) : TermElabM TerminationWF := do + -- logInfo <| m!"Solution: {solution}" + let mut termByElements := #[] + for h : funIdx in [:varNamess.size] do + let vars := (varNamess[funIdx]'h.2).map mkIdent + let body := ← Lean.Elab.Term.Quotation.mkTuple (← measures.mapM fun + | .args varIdxs => + let v := vars.get! (varIdxs[funIdx]!) + `(sizeOf $v) + | .func funIdx' => if funIdx' == funIdx then `(1) else `(0) + ) + let declName := declNames[funIdx]! + + -- TODO: Can we turn it into user-facing syntax? Maybe for a “try-this” feature? + trace[Elab.definition.wf] "Using termination {declName}: {vars} => {body}" + termByElements := termByElements.push + { ref := .missing -- is this the right function + declName, vars, body, + implicit := true -- TODO, what is this? + } + return .ext termByElements + +end Lean.Elab.WF.GuessLex + +namespace Lean.Elab.WF + +open Lean.Elab.WF.GuessLex + +def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) + (fixedPrefixSize : Nat )(decrTactic? : Option Syntax) : + TermElabM TerminationWF := do + let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize) + let arities := varNamess.map (·.size) + trace[Elab.definition.wf] "varNames is: {varNamess}" + + -- Collect all recursive calls and extract their context + let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities + let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·) + let callMatrix := rcs.map (inspectCall ·) + + let forbiddenArgs ← preDefs.mapM fun preDef => + getForbiddenByTrivialSizeOf fixedPrefixSize preDef + + -- Enumerate all meausures. + -- (With many functions with multiple arguments, this can explode a bit. + -- We could interleave enumerating measure with early pruning based on the recCalls, + -- once that becomes a problem. Until then, a use can always use an explicit + -- `terminating_by` annotatin.) + let some arg_measures := generateCombinations? forbiddenArgs arities + | throwError "Too many combinations" + + -- The list of measures, including the measures that order functions. + -- The function ordering measures should come last + let measures : Array MutualMeasure := + arg_measures.map .args ++ (List.range varNamess.size).toArray.map .func + + match ← solve measures callMatrix with + | .some solution => + buildTermWF (preDefs.map (·.declName)) varNamess solution + | .none => + logWarning ("Could not find a lexicographic ordering for which the function definition" ++ + " terminates.") + -- Continue with the first allowed measure, so that the user sees some failing goals. + buildTermWF (preDefs.map (·.declName)) varNamess (measures.extract 0 1) diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean index 3b490a250da0..d5b0ae2674ac 100644 --- a/src/Lean/Elab/PreDefinition/WF/Main.lean +++ b/src/Lean/Elab/PreDefinition/WF/Main.lean @@ -11,6 +11,7 @@ import Lean.Elab.PreDefinition.WF.Rel import Lean.Elab.PreDefinition.WF.Fix import Lean.Elab.PreDefinition.WF.Eqns import Lean.Elab.PreDefinition.WF.Ite +import Lean.Elab.PreDefinition.WF.GuessLex namespace Lean.Elab open WF @@ -87,10 +88,17 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) } let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize) + + let wf ← + if let .some wf := wf? then + pure wf + else + guessLex preDefs unaryPreDef fixedPrefixSize decrTactic? + let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do let type ← whnfForall type let packedArgType := type.bindingDomain! - elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf? fun wfRel => do + elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do trace[Elab.definition.wf] "wfRel: {wfRel}" let (value, envNew) ← withoutModifyingEnv' do addAsAxiom unaryPreDef From ea171dcb8f8d9ab6464fe8d53ab69f390237ca73 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 14 Nov 2023 11:49:22 +0100 Subject: [PATCH 02/27] Use same error message as before --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 484b19e5774c..ce6fa85dc767 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -607,7 +607,4 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) | .some solution => buildTermWF (preDefs.map (·.declName)) varNamess solution | .none => - logWarning ("Could not find a lexicographic ordering for which the function definition" ++ - " terminates.") - -- Continue with the first allowed measure, so that the user sees some failing goals. - buildTermWF (preDefs.map (·.declName)) varNamess (measures.extract 0 1) + throwError "failed to prove termination, use `termination_by` to specify a well-founded relation" From 0414156a65b80badbddae959789df9a1cba273f7 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 14 Nov 2023 21:52:35 +0100 Subject: [PATCH 03/27] Avoid overshooting in lambdaTelescope in matchers/casesOn --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 63 +++++++++++++------- 1 file changed, 40 insertions(+), 23 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index ce6fa85dc767..ff1e8b624484 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -81,7 +81,11 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : TermElabM (A (with `ys_i` as loose bound variable, ready to be `.instantiate`d) Cf. `MatcherApp.addArg`. -/ -def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := +def _root_.Lean.Meta.MatcherApp.transform {m} + -- TODO: Do we really need all these type classes? + [MonadControlT MetaM m] [MonadLiftT MetaM m] [Monad m] [MonadOptions m] [MonadTrace m] + [MonadLiftT IO m] [MonadError m] [AddMessageContext m] + (matcherApp : MatcherApp) (e : Expr) (k : Expr → Expr → m Unit) : m Unit := lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do unless motiveArgs.size == matcherApp.discrs.size do -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. @@ -106,13 +110,19 @@ def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : throwError "failed to add argument to matcher application, type error when constructing the new motive" let auxType ← inferType aux let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType - let altAuxTys ← altAuxs.mapM inferType - let res ← altAuxTys.mapM fun altAux => do - let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAux - let body := body.getArg! 2 - -- and abstract over the parameters of the alternative again - Expr.abstractM body fvs - return res + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip matcherApp.alts altAuxTys).forM fun (alt, altAuxTy) => do + let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy + trace[Elab.definition.wf] "alt fvs: {fvs}" + let body := body.getArg! 2 + -- and abstract over the parameters of the alternative again + let body ← Expr.abstractM body fvs + -- Go under the lambdas of the alt + -- (TODO: Use bounded lambdaTelescope) + lambdaTelescope alt fun xs altBody => do + let body := body.instantiateRev (xs.extract 0 fvs.size) + trace[Elab.definition.wf] "CasesOnApp.transform result {indentExpr body}" + k body altBody /-- Given a `casesOn` application `c` of the form @@ -125,14 +135,19 @@ def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : ``` (with `ys_i` as loose bound variable, ready to be `.instantiate`d) -/ -def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := +def _root_.Lean.Meta.CasesOnApp.transform {m} + -- TODO: Do we really need all these type classes? + [MonadControlT MetaM m] [MonadLiftT MetaM m] [Monad m] [MonadOptions m] [MonadTrace m] + [MonadLiftT IO m] [MonadError m] [AddMessageContext m] + (c : CasesOnApp) (e : Expr) (k : Expr → Expr → m Unit) : m Unit := lambdaTelescope c.motive fun motiveArgs _motiveBody => do unless motiveArgs.size == c.indices.size + 1 do throwError "failed to add argument to `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders" let discrs := c.indices ++ #[c.major] let mut eAbst := e for motiveArg in motiveArgs.reverse, discr in discrs.reverse do - eAbst := (← kabstract eAbst discr).instantiate1 motiveArg + eAbst ← kabstract eAbst discr + eAbst := eAbst.instantiate1 motiveArg -- Up to this point, this is cargo-culted from `CasesOn.App.addArg` -- Let's create something Prop-typed that mentions `e`, by writing `e = e`. let eEq ← mkEq eAbst eAbst @@ -147,13 +162,19 @@ def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (A -- The type of the remaining arguments will mention `e` instantiated for each arg -- so extract them let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType - let altAuxTys ← altAuxs.mapM inferType - let res ← altAuxTys.mapM fun altAux => do - let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAux + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip c.alts altAuxTys).forM fun (alt, altAuxTy) => do + let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy + trace[Elab.definition.wf] "alt fvs: {fvs}" let body := body.getArg! 2 -- and abstract over the parameters of the alternative again - Expr.abstractM body fvs - return res + let body ← Expr.abstractM body fvs + -- Go under the lambdas of the alt + -- (TODO: Use bounded lambdaTelescope) + lambdaTelescope alt fun xs altBody => do + let body := body.instantiateRev (xs.extract 0 fvs.size) + trace[Elab.definition.wf] "CasesOnApp.transform result {indentExpr body}" + k body altBody @[reducible] def M (recFnName : Name) (α β : Type) : Type := @@ -214,20 +235,16 @@ where if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then processApp scrut e else - let altScruts ← matcherApp.transform scrut - (Array.zip matcherApp.alts altScruts).forM fun (alt, altScrut) => - lambdaTelescope alt fun xs altBody => do - loop (altScrut.instantiateRev xs) altBody + matcherApp.transform scrut fun scrut' altBody => do + loop scrut' altBody | none => match (← toCasesOnApp? e) with | some casesOnApp => if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then processApp scrut e else - let altScruts ← casesOnApp.transform scrut - (Array.zip casesOnApp.alts altScruts).forM fun (alt, altScrut) => - lambdaTelescope alt fun xs altBody => do - loop (altScrut.instantiateRev xs) altBody + casesOnApp.transform scrut fun scrut' altBody => do + loop scrut' altBody | none => processApp scrut e | e => do let _ ← ensureNoRecFn recFnName e From 01f99687720dfe11b10c1d116a254e7fd78ef84f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 15 Nov 2023 13:59:28 +0100 Subject: [PATCH 04/27] feat: Add MatcherApp. and CasesOnApp.transform these are compagnions to `MatcherApp.addArg` and `CasesOnApp.addArg` when one only has a type to transform, but not a concrete values. Prerequisite for guessing lexicographic order (#2874) --- src/Lean/Meta/CasesOn.lean | 58 +++++++++++++++++++++++++++++++++- src/Lean/Meta/Match/Match.lean | 55 +++++++++++++++++++++++++++++++- 2 files changed, 111 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 7646455f9e2d..1b571b6a8199 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Meta.KAbstract import Lean.Meta.Check +import Lean.Meta.AppBuilder namespace Lean.Meta @@ -106,11 +107,66 @@ where throwError "failed to add argument to `casesOn` application, argument type was not refined by `casesOn`" return altsNew -/-- Similar `CasesOnApp.addArg`, but returns `none` on failure. -/ +/-- Similar to `CasesOnApp.addArg`, but returns `none` on failure. -/ def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM (Option CasesOnApp) := try return some (← c.addArg arg checkIfRefined) catch _ => return none +/-- + Given a `casesOn` application `c` of the form + ``` + casesOn As (fun is x => motive[i, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining + ``` + and a type `e : B[is, major]`, for every alternative `i`, construct the type + ``` + B[C_i[ys_i]] + ``` + with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`. + + This is similar to `CasesOnApp.addArg` when you only have a type to transform, not a concrete value. +-/ +def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := + lambdaTelescope c.motive fun motiveArgs _motiveBody => do + trace[Elab.definition.wf] "CasesOnApp.transform: {indentExpr e}" + unless motiveArgs.size == c.indices.size + 1 do + throwError "failed to transfer argument through `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders" + let discrs := c.indices ++ #[c.major] + let mut eAbst := e + for motiveArg in motiveArgs.reverse, discr in discrs.reverse do + eAbst ← kabstract eAbst discr + eAbst := eAbst.instantiate1 motiveArg + -- Up to this point, this is cargo-culted from `CasesOn.App.addArg` + -- Let's create something Prop-typed that mentions `e`, by writing `e = e`. + let eEq ← mkEq eAbst eAbst + let motive ← mkLambdaFVars motiveArgs eEq + let us := if c.propOnly then c.us else levelZero :: c.us.tail! + -- Now instantiate the casesOn wth this synthetic motive + let aux := mkAppN (mkConst c.declName us) c.params + let aux := mkApp aux motive + let aux := mkAppN aux discrs + check aux + let auxType ← inferType aux + -- The type of the remaining arguments will mention `e` instantiated for each arg + -- so extract them + let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs + +/-- A non-failing version of `transform` -/ +def CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : + MetaM (Option (Array Expr)) := + try + return some (← c.transform e) + catch _ => + return none + end Lean.Meta diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index b4ce22790431..cfcb1d0052b3 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -951,13 +951,66 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := remaining := #[e] ++ matcherApp.remaining } -/-- Similar `MatcherApp.addArg?`, but returns `none` on failure. -/ +/-- Similar to `MatcherApp.addArg`, but returns `none` on failure. -/ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp) := try return some (← matcherApp.addArg e) catch _ => return none + +/-- Given + - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and + - expression `e : B[discrs]`, + returns the expressions `B[C_1[ys_1]]) ... B[C_n[ys_n]]`, + with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`. + + This is similar to `MatcherApp.addArg` when you only have a type to transform, not a concrete value. +-/ +def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := + lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do + trace[Elab.definition.wf] "MatcherApp.transform {indentExpr e}" + unless motiveArgs.size == matcherApp.discrs.size do + -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. + throwError "failed to transfer argument through matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" + + let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i eAbst => do + let motiveArg := motiveArgs[i]! + let discr := matcherApp.discrs[i]! + let eTypeAbst ← kabstract eAbst discr + return eTypeAbst.instantiate1 motiveArg + let eEq ← mkEq eAbst eAbst + + let matcherLevels ← match matcherApp.uElimPos? with + | none => pure matcherApp.matcherLevels + | some pos => + pure <| matcherApp.matcherLevels.set! pos levelZero + let motive ← mkLambdaFVars motiveArgs eEq + let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params + let aux := mkApp aux motive + let aux := mkAppN aux matcherApp.discrs + unless (← isTypeCorrect aux) do + throwError "failed to transfer argument through matcher application, type error when constructing the new motive" + let auxType ← inferType aux + let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs + +/-- A non-failing version of `MatcherApp.transform` -/ +def MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) : + MetaM (Option (Array Expr)) := + try + return some (← matcherApp.transform e) + catch _ => + return none + builtin_initialize registerTraceClass `Meta.Match.match registerTraceClass `Meta.Match.debug From a117d02ec7654899d1957a7bc4c2b04fd5b1631b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Nov 2023 18:48:01 +0100 Subject: [PATCH 05/27] Use forallTelescope --- src/Lean/Meta/CasesOn.lean | 19 +++++++++---------- src/Lean/Meta/Match/Match.lean | 16 ++++++++-------- 2 files changed, 17 insertions(+), 18 deletions(-) diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 1b571b6a8199..4b5536223a73 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -137,7 +137,6 @@ def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := for motiveArg in motiveArgs.reverse, discr in discrs.reverse do eAbst ← kabstract eAbst discr eAbst := eAbst.instantiate1 motiveArg - -- Up to this point, this is cargo-culted from `CasesOn.App.addArg` -- Let's create something Prop-typed that mentions `e`, by writing `e = e`. let eEq ← mkEq eAbst eAbst let motive ← mkLambdaFVars motiveArgs eEq @@ -150,18 +149,18 @@ def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := let auxType ← inferType aux -- The type of the remaining arguments will mention `e` instantiated for each arg -- so extract them - let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let (altAuxs, _, _) ← forallMetaTelescope auxType let altAuxTys ← altAuxs.mapM (inferType ·) (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs -/-- A non-failing version of `transform` -/ +/-- A non-failing version of `CasesOnApp.transform` -/ def CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : MetaM (Option (Array Expr)) := try diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index cfcb1d0052b3..a057049f913f 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -992,16 +992,16 @@ def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Exp unless (← isTypeCorrect aux) do throwError "failed to transfer argument through matcher application, type error when constructing the new motive" let auxType ← inferType aux - let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let (altAuxs, _, _) ← forallMetaTelescope auxType let altAuxTys ← altAuxs.mapM (inferType ·) (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs /-- A non-failing version of `MatcherApp.transform` -/ def MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) : From 338a239e20990a00b65016e3cf4295aa4e49f193 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Nov 2023 18:55:09 +0100 Subject: [PATCH 06/27] Improve documentation, also for existing code --- src/Lean/Meta/CasesOn.lean | 24 +++++++++++++++++------- src/Lean/Meta/Match/Match.lean | 25 +++++++++++++++++++++---- 2 files changed, 38 insertions(+), 11 deletions(-) diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 4b5536223a73..7fc743c7a4bf 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -51,13 +51,17 @@ def CasesOnApp.toExpr (c : CasesOnApp) : Expr := /-- Given a `casesOn` application `c` of the form ``` - casesOn As (fun is x => motive[i, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining + casesOn As (fun is x => motive[is, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining ``` and an expression `e : B[is, major]`, construct the term ``` - casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining + casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[_, C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[_, C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining ``` We use `kabstract` to abstract the `is` and `major` from `B[is, major]`. + + This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to + the argument provided by `fix` to refine the termination argument, which may mention `major`. + See there for how to use this function. -/ def CasesOnApp.addArg (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM CasesOnApp := do lambdaTelescope c.motive fun motiveArgs motiveBody => do @@ -117,15 +121,20 @@ def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := f /-- Given a `casesOn` application `c` of the form ``` - casesOn As (fun is x => motive[i, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining + casesOn As (fun is x => motive[is, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining ``` - and a type `e : B[is, major]`, for every alternative `i`, construct the type + and an expression `B[is, major]`, for every alternative `i`, construct the type ``` - B[C_i[ys_i]] + B[_, C_i[ys_i]] ``` with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`. - This is similar to `CasesOnApp.addArg` when you only have a type to transform, not a concrete value. + This is similar to `CasesOnApp.addArg` when you only have an expression to + refined, and not a type with a value. + + This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive + calls to refine the functions' paramter, which may mention `major`. + See there for how to use this function. -/ def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := lambdaTelescope c.motive fun motiveArgs _motiveBody => do @@ -137,7 +146,8 @@ def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := for motiveArg in motiveArgs.reverse, discr in discrs.reverse do eAbst ← kabstract eAbst discr eAbst := eAbst.instantiate1 motiveArg - -- Let's create something Prop-typed that mentions `e`, by writing `e = e`. + -- Let's create something that’s a `Sort` and mentions `e`, by writing `e = e`, + -- so that we can use it as a motive let eEq ← mkEq eAbst eAbst let motive ← mkLambdaFVars motiveArgs eEq let us := if c.propOnly then c.us else levelZero :: c.us.tail! diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index a057049f913f..e37aaaecd73b 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -910,11 +910,17 @@ private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - expression `e : B[discrs]`, Construct the term - `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`, and + `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`. + We use `kabstract` to abstract the discriminants from `B[discrs]`. + This method assumes - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` + + This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to + the argument provided by `fix` to refine the termination argument, which may mention `major`. + See there for how to use this function. -/ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do @@ -961,11 +967,20 @@ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option Matc /-- Given - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - - expression `e : B[discrs]`, - returns the expressions `B[C_1[ys_1]]) ... B[C_n[ys_n]]`, + - a type `B[discrs]`, + returns the types `B[C_1[ys_1]] ... B[C_n[ys_n]]`, with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`. - This is similar to `MatcherApp.addArg` when you only have a type to transform, not a concrete value. + This method assumes + - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` + - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` + + This is similar to `MatcherApp.addArg` when you only have an expression to + refined, and not a type with a value. + + This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive + calls to refine the functions' paramter, which may mention `major`. + See there for how to use this function. -/ def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do @@ -979,6 +994,8 @@ def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Exp let discr := matcherApp.discrs[i]! let eTypeAbst ← kabstract eAbst discr return eTypeAbst.instantiate1 motiveArg + -- Let's create something that’s a `Sort` and mentions `e`, by writing `e = e`, + -- so that we can use it as a motive let eEq ← mkEq eAbst eAbst let matcherLevels ← match matcherApp.uElimPos? with From 9c1b76bb317bb40a7e43da09eed6528babb3b642 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 15 Nov 2023 11:06:53 +0100 Subject: [PATCH 07/27] Refactor stuff arount .transfer --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 173 +++++++++++-------- 1 file changed, 101 insertions(+), 72 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index ff1e8b624484..8b5516e89a96 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -17,6 +17,7 @@ import Lean.Elab.PreDefinition.WF.TerminationHint /-! + This module implements heuristics to finding lexicographic termination measures for well-founded recursion. The goal is to try all lexicographic measures and find one for which all proof obligations go through with the given or default @@ -77,19 +78,17 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : TermElabM (A /-- Given - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - expression `e : B[discrs]`, - returns the expressions `B[C_1[ys_1]]) ... B[C_n[ys_n]]`. - (with `ys_i` as loose bound variable, ready to be `.instantiate`d) + returns the expressions `B[C_1[ys_1]]) ... B[C_n[ys_n]]`, + with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`. Cf. `MatcherApp.addArg`. -/ -def _root_.Lean.Meta.MatcherApp.transform {m} - -- TODO: Do we really need all these type classes? - [MonadControlT MetaM m] [MonadLiftT MetaM m] [Monad m] [MonadOptions m] [MonadTrace m] - [MonadLiftT IO m] [MonadError m] [AddMessageContext m] - (matcherApp : MatcherApp) (e : Expr) (k : Expr → Expr → m Unit) : m Unit := +def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : + MetaM (Array Expr) := lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do + trace[Elab.definition.wf] "MatcherApp.transform {indentExpr e}" unless motiveArgs.size == matcherApp.discrs.size do -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. - throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" + throwError "failed to transfer argument through matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i eAbst => do let motiveArg := motiveArgs[i]! @@ -107,22 +106,27 @@ def _root_.Lean.Meta.MatcherApp.transform {m} let aux := mkApp aux motive let aux := mkAppN aux matcherApp.discrs unless (← isTypeCorrect aux) do - throwError "failed to add argument to matcher application, type error when constructing the new motive" + throwError "failed to transfer argument through matcher application, type error when constructing the new motive" let auxType ← inferType aux let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType let altAuxTys ← altAuxs.mapM (inferType ·) - (Array.zip matcherApp.alts altAuxTys).forM fun (alt, altAuxTy) => do - let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy - trace[Elab.definition.wf] "alt fvs: {fvs}" - let body := body.getArg! 2 - -- and abstract over the parameters of the alternative again - let body ← Expr.abstractM body fvs - -- Go under the lambdas of the alt - -- (TODO: Use bounded lambdaTelescope) - lambdaTelescope alt fun xs altBody => do - let body := body.instantiateRev (xs.extract 0 fvs.size) - trace[Elab.definition.wf] "CasesOnApp.transform result {indentExpr body}" - k body altBody + (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs + +/-- A non-failing version of `transform` -/ +def _root_.Lean.Meta.MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) : + MetaM (Option (Array Expr)) := + try + return some (← matcherApp.transform e) + catch _ => + return none + /-- Given a `casesOn` application `c` of the form @@ -133,16 +137,14 @@ def _root_.Lean.Meta.MatcherApp.transform {m} ``` B[C_i[ys_i]] ``` - (with `ys_i` as loose bound variable, ready to be `.instantiate`d) + with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`. -/ -def _root_.Lean.Meta.CasesOnApp.transform {m} - -- TODO: Do we really need all these type classes? - [MonadControlT MetaM m] [MonadLiftT MetaM m] [Monad m] [MonadOptions m] [MonadTrace m] - [MonadLiftT IO m] [MonadError m] [AddMessageContext m] - (c : CasesOnApp) (e : Expr) (k : Expr → Expr → m Unit) : m Unit := +def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : + MetaM (Array Expr) := lambdaTelescope c.motive fun motiveArgs _motiveBody => do + trace[Elab.definition.wf] "CasesOnApp.transform: {indentExpr e}" unless motiveArgs.size == c.indices.size + 1 do - throwError "failed to add argument to `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders" + throwError "failed to transfer argument through `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders" let discrs := c.indices ++ #[c.major] let mut eAbst := e for motiveArg in motiveArgs.reverse, discr in discrs.reverse do @@ -163,18 +165,22 @@ def _root_.Lean.Meta.CasesOnApp.transform {m} -- so extract them let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType let altAuxTys ← altAuxs.mapM (inferType ·) - (Array.zip c.alts altAuxTys).forM fun (alt, altAuxTy) => do + (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy - trace[Elab.definition.wf] "alt fvs: {fvs}" + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality let body := body.getArg! 2 - -- and abstract over the parameters of the alternative again - let body ← Expr.abstractM body fvs - -- Go under the lambdas of the alt - -- (TODO: Use bounded lambdaTelescope) - lambdaTelescope alt fun xs altBody => do - let body := body.instantiateRev (xs.extract 0 fvs.size) - trace[Elab.definition.wf] "CasesOnApp.transform result {indentExpr body}" - k body altBody + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs + +/-- A non-failing version of `transform` -/ +def _root_.Lean.Meta.CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : + MetaM (Option (Array Expr)) := + try + return some (← c.transform e) + catch _ => + return none @[reducible] def M (recFnName : Name) (α β : Type) : Type := @@ -235,16 +241,34 @@ where if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then processApp scrut e else - matcherApp.transform scrut fun scrut' altBody => do - loop scrut' altBody + if let some altScruts ← matcherApp.transform? scrut then + (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altScruts)).forM + fun (alt, altNumParam, altScrut) => + lambdaTelescope alt fun xs altBody => do + unless altNumParam ≤ xs.size do + throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}" + let altScrut := altScrut.instantiateRev xs[:altNumParam] + trace[Elab.definition.wf] "MatcherApp.transform result {indentExpr altScrut}" + loop altScrut altBody + else + processApp scrut e | none => match (← toCasesOnApp? e) with | some casesOnApp => if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then processApp scrut e else - casesOnApp.transform scrut fun scrut' altBody => do - loop scrut' altBody + if let some altScruts ← casesOnApp.transform? scrut then + (Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altScruts)).forM + fun (alt, altNumParam, altScrut) => + lambdaTelescope alt fun xs altBody => do + unless altNumParam ≤ xs.size do + throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" + let altScrut := altScrut.instantiateRev xs[:altNumParam] + trace[Elab.definition.wf] "CasesOnApp.transform result {indentExpr altScrut}" + loop altScrut altBody + else + processApp scrut e | none => processApp scrut e | e => do let _ ← ensureNoRecFn recFnName e @@ -593,35 +617,40 @@ namespace Lean.Elab.WF open Lean.Elab.WF.GuessLex def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) - (fixedPrefixSize : Nat )(decrTactic? : Option Syntax) : + (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) : TermElabM TerminationWF := do - let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize) - let arities := varNamess.map (·.size) - trace[Elab.definition.wf] "varNames is: {varNamess}" - - -- Collect all recursive calls and extract their context - let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities - let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·) - let callMatrix := rcs.map (inspectCall ·) - - let forbiddenArgs ← preDefs.mapM fun preDef => - getForbiddenByTrivialSizeOf fixedPrefixSize preDef - - -- Enumerate all meausures. - -- (With many functions with multiple arguments, this can explode a bit. - -- We could interleave enumerating measure with early pruning based on the recCalls, - -- once that becomes a problem. Until then, a use can always use an explicit - -- `terminating_by` annotatin.) - let some arg_measures := generateCombinations? forbiddenArgs arities - | throwError "Too many combinations" - - -- The list of measures, including the measures that order functions. - -- The function ordering measures should come last - let measures : Array MutualMeasure := - arg_measures.map .args ++ (List.range varNamess.size).toArray.map .func - - match ← solve measures callMatrix with - | .some solution => - buildTermWF (preDefs.map (·.declName)) varNamess solution - | .none => + try + let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize) + let arities := varNamess.map (·.size) + trace[Elab.definition.wf] "varNames is: {varNamess}" + + -- Collect all recursive calls and extract their context + let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities + let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·) + let callMatrix := rcs.map (inspectCall ·) + + let forbiddenArgs ← preDefs.mapM fun preDef => + getForbiddenByTrivialSizeOf fixedPrefixSize preDef + + -- Enumerate all meausures. + -- (With many functions with multiple arguments, this can explode a bit. + -- We could interleave enumerating measure with early pruning based on the recCalls, + -- once that becomes a problem. Until then, a use can always use an explicit + -- `terminating_by` annotatin.) + let some arg_measures := generateCombinations? forbiddenArgs arities + | throwError "Too many combinations" + + -- The list of measures, including the measures that order functions. + -- The function ordering measures should come last + let measures : Array MutualMeasure := + arg_measures.map .args ++ (List.range varNamess.size).toArray.map .func + + match ← solve measures callMatrix with + | .some solution => do + let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution + return wf + | .none => throwError "Cannot find a decreasing lexicographic order" + catch _ => + -- Hide all errors from guessing lexicographic orderings, as before + -- TODO: surface unexpected errors, maybe surface detailed explanation like Isabelle throwError "failed to prove termination, use `termination_by` to specify a well-founded relation" From dd26a050c9145a2f597620c66d2ae0d4b1df344f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 15 Nov 2023 14:35:56 +0100 Subject: [PATCH 08/27] Avoid TermElabM where MetaM suffices --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 84 ++++++++++---------- 1 file changed, 44 insertions(+), 40 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 8b5516e89a96..2a2a0143bd22 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -62,7 +62,7 @@ Use user-given parameter names if present; use x1...xn otherwise. The length of the returned array is also used to determine the arity of the function, so it should match what `packDomain` does. -/ -def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : TermElabM (Array Name):= do +def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name):= do lambdaTelescope preDef.value fun xs _ => do let xs := xs.extract fixedPrefixSize xs.size let mut ns := #[] @@ -281,28 +281,21 @@ structure SavedLocalCtxt where savedLocalContext : LocalContext savedLocalInstances : LocalInstances savedTermContext : Term.Context + savedTermState : Term.SavedState def SavedLocalCtxt.create : TermElabM SavedLocalCtxt := do let savedState ← saveState let savedLocalContext ← getLCtx let savedLocalInstances ← getLocalInstances let savedTermContext ← readThe Term.Context - return { savedState, savedLocalContext, savedLocalInstances, savedTermContext } - + let savedTermState ← saveState + return { savedLocalContext, savedLocalInstances, savedTermState, savedTermContext } def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : TermElabM α) : - TermElabM α := withoutModifyingState $ do - restoreState slc.savedState + MetaM α := withoutModifyingState $ do withLCtx slc.savedLocalContext slc.savedLocalInstances do - withTheReader Term.Context (fun _ => slc.savedTermContext) do - k - -def SavedLocalCtxt.within {α} (slc : SavedLocalCtxt) (k : TermElabM α) : - TermElabM (SavedLocalCtxt × α) := - slc.run do - let x ← k - let slc' ← SavedLocalCtxt.create - pure (slc', x) + slc.savedTermState.meta.restore + k slc.savedTermContext |>.run' slc.savedTermState.elab /-- A `RecCallContext` focuses on a single recursive call in a unary predefinition, @@ -358,21 +351,22 @@ def RecCallContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (a call site. -/ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat) - : TermElabM (Array RecCallContext) := withoutModifyingState do - addAsAxiom unaryPreDef - lambdaTelescope unaryPreDef.value fun xs body => do - unless xs.size == fixedPrefixSize + 1 do - -- Maybe cleaner to have lambdaBoundedTelescope? - throwError "Unexpected number of lambdas in unary pre-definition" - -- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}" - let param := xs[fixedPrefixSize]! - withRecApps unaryPreDef.declName fixedPrefixSize body param fun param args => do - unless args.size ≥ fixedPrefixSize + 1 do - throwError "Insufficient arguments in recursive call" - let arg := args[fixedPrefixSize]! - let (caller, params) ← unpackArg arities param - let (callee, args) ← unpackArg arities arg - RecCallContext.create caller params callee args + : MetaM (Array RecCallContext) := withoutModifyingState do + Lean.Elab.Term.TermElabM.run' do + addAsAxiom unaryPreDef + lambdaTelescope unaryPreDef.value fun xs body => do + unless xs.size == fixedPrefixSize + 1 do + -- Maybe cleaner to have lambdaBoundedTelescope? + throwError "Unexpected number of lambdas in unary pre-definition" + -- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}" + let param := xs[fixedPrefixSize]! + withRecApps unaryPreDef.declName fixedPrefixSize body param fun param args => do + unless args.size ≥ fixedPrefixSize + 1 do + throwError "Insufficient arguments in recursive call" + let arg := args[fixedPrefixSize]! + let (caller, params) ← unpackArg arities param + let (callee, args) ← unpackArg arities arg + RecCallContext.create caller params callee args inductive GuessLexRel | lt | eq | le | no_idea deriving Repr, DecidableEq @@ -389,7 +383,7 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat] | no_idea => unreachable! -- TODO: keep it partial or refactor? -def mkSizeOf (e : Expr) : TermElabM Expr := do +def mkSizeOf (e : Expr) : MetaM Expr := do let ty ← inferType e let lvl ← getLevel ty let inst ← synthInstance (mkAppN (mkConst ``SizeOf [lvl]) #[ty]) @@ -400,7 +394,7 @@ def mkSizeOf (e : Expr) : TermElabM Expr := do -- For a given recursive call and choice of paramter index, -- try to prove requality, < or ≤ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx argIdx : Nat) : - TermElabM GuessLexRel := do + MetaM GuessLexRel := do rcc.ctxt.run do let param := rcc.params[paramIdx]! let arg := rcc.args[argIdx]! @@ -452,8 +446,7 @@ def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallContext) : let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none) return { decrTactic?, rcc, cache } -def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : - TermElabM GuessLexRel := do +def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do -- Check the cache first if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then return res @@ -480,7 +473,7 @@ inductive MutualMeasure where | func : Nat → MutualMeasure -- Evaluate a call at a given measure -def inspectCall (rc : RecCallCache) : MutualMeasure → TermElabM GuessLexRel +def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel | .args argIdxs => do let paramIdx := argIdxs[rc.rcc.caller]! let argIdx := argIdxs[rc.rcc.callee]! @@ -587,13 +580,24 @@ partial def solve {m} {α} [Monad m] (measures : Array α) -- None found, we have to give up return .none + +-- Does this really not yet exist? Should it? +partial def mkTupleSyntax : Array Syntax → MetaM Syntax + | #[] => `(()) + | #[e] => return e + | es => do + let e : TSyntax `term := ⟨es[0]!⟩ + let es : Syntax.TSepArray `term "," := + ⟨(Syntax.SepArray.ofElems (sep := ",") es[1:]).1⟩ + `(term|($e, $es,*)) + def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name)) - (measures : Array MutualMeasure) : TermElabM TerminationWF := do + (measures : Array MutualMeasure) : MetaM TerminationWF := do -- logInfo <| m!"Solution: {solution}" let mut termByElements := #[] for h : funIdx in [:varNamess.size] do let vars := (varNamess[funIdx]'h.2).map mkIdent - let body := ← Lean.Elab.Term.Quotation.mkTuple (← measures.mapM fun + let body ← mkTupleSyntax (← measures.mapM fun | .args varIdxs => let v := vars.get! (varIdxs[funIdx]!) `(sizeOf $v) @@ -618,14 +622,14 @@ open Lean.Elab.WF.GuessLex def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) : - TermElabM TerminationWF := do + MetaM TerminationWF := do try - let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize) + let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·) let arities := varNamess.map (·.size) trace[Elab.definition.wf] "varNames is: {varNamess}" -- Collect all recursive calls and extract their context - let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities + let recCalls ←collectRecCalls unaryPreDef fixedPrefixSize arities let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·) let callMatrix := rcs.map (inspectCall ·) @@ -645,7 +649,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) let measures : Array MutualMeasure := arg_measures.map .args ++ (List.range varNamess.size).toArray.map .func - match ← solve measures callMatrix with + match ← liftMetaM <| solve measures callMatrix with | .some solution => do let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution return wf From b741f14dc6ee49e18eea12e0054fe8bc96354304 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 15 Nov 2023 14:55:14 +0100 Subject: [PATCH 09/27] More comments --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 89 +++++++++++++------- 1 file changed, 57 insertions(+), 32 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 2a2a0143bd22..4e023b3909c1 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -17,37 +17,47 @@ import Lean.Elab.PreDefinition.WF.TerminationHint /-! +This module finds lexicographic termination arguments for well-founded recursion. -This module implements heuristics to finding lexicographic termination measures -for well-founded recursion. The goal is to try all lexicographic measures and -find one for which all proof obligations go through with the given or default -`decreasing_by` tatic. +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`. -The crucial optimiziation is to look at each argument of each recursive call _once_, -try to prove `<` and (if that fails `≤`), and then look at that table to pick a suitable -measure. The next-crucial optimization is to fill that table lazily. +For mutual recursion, a single measure is not just one parameter, but one from each recursive +function. Enumerating these can lead to a combinatoric explosion, so we bound +the nubmer of measures tried. -This way, we run the (likely expensive) tactics as few times as possible, while still being -able to consider a possibly large number of combinations. +In addition to measures derived from `sizeOf xᵢ`, it also considers measures +that assign an order to the functions themselves. This way we can support mutual +function definitions where no arguments decrease from one function to another. -In the case of mutual recursion, a single measure is not just one argument position, but -one argument from each recursive function. Enumerating these can lead to a combinatoric explosion, -so we bound the nubmer of measures tried. - -In addition to measures derived from `sizeOf x` where `x` is an argument, it also considers -measures that order the functions. This way we can support mutual function definitions where -no arguments decrease from one function to another. - The result of this module is a `TerminationWF`, which is then passed on to `wfRecursion`; this design is crucial so that whatever we infer in this module could also be written manually by the user. It would be bad if there are function definitions that can only be processed with the guessed lexicographic order. +The following optimizations are applied to make this feasible: + +1. The crucial optimiziation is to look at each argument of each recursive call + _once_, try to prove `<` and (if that fails `≤`), and then look at that table to + pick a suitable measure. + +2. The next-crucial optimization is to fill that table lazily. This way, we run the (likely + expensive) tactics as few times as possible, while still being able to consider a possibly + large number of combinations. + +3. Before we even try to prove `<`, we check if the arguments are equal (`=`). No well-founded + measure will relate equal terms, likely this check is faster than firing up the tactic engine, + and it adds more signal to the output. + +4. Instead of traversing the whole function body over and over, we traverse it once and store + the arguments (in unpacked form) and the local `TermElabM` state at each recursive call + (see `collectRecCalls`), which we then re-use for the possibly many proof attempts. + The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 10.1007/978-3-540-74591-4_5 . - -/ set_option autoImplicit false @@ -62,6 +72,8 @@ Use user-given parameter names if present; use x1...xn otherwise. The length of the returned array is also used to determine the arity of the function, so it should match what `packDomain` does. -/ +-- TODO: Maybe the eta-expansion handling `fun foo : … | n -> ` should try to use +-- a nicer name than simply `x`? def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name):= do lambdaTelescope preDef.value fun xs _ => do let xs := xs.extract fixedPrefixSize xs.size @@ -75,6 +87,7 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array ns := ns.push n return ns + /-- Given - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - expression `e : B[discrs]`, @@ -82,6 +95,7 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`. Cf. `MatcherApp.addArg`. -/ +-- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do @@ -120,6 +134,7 @@ def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : Expr.abstractM body fvs /-- A non-failing version of `transform` -/ +-- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option (Array Expr)) := try @@ -139,6 +154,7 @@ def _root_.Lean.Meta.MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) ``` with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`. -/ +-- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := lambdaTelescope c.motive fun motiveArgs _motiveBody => do @@ -175,6 +191,7 @@ def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : Expr.abstractM body fvs /-- A non-failing version of `transform` -/ +-- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : MetaM (Option (Array Expr)) := try @@ -182,11 +199,19 @@ def _root_.Lean.Meta.CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : catch _ => return none +-- Q: Is it really not possible to add this to the `where` clause? @[reducible] def M (recFnName : Name) (α β : Type) : Type := StateRefT (Array α) (StateRefT (HasConstCache recFnName) TermElabM) β -partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (e : Expr) (scrut : Expr) +/-- +Traverses the given expression `e`, and invokes the continuation `k` +at every saturated call to `recFnName`. + +The expression `scrut` is passed along, and refined when going under a matcher +or `casesOn` application. +-/ +partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (scrut : Expr) (e : Expr) (k : Expr → Array Expr → TermElabM α) : TermElabM (Array α) := do trace[Elab.definition.wf] "withRecApps: {indentExpr e}" let (_, as) ← loop scrut e |>.run #[] |>.run' {} @@ -273,18 +298,17 @@ where | e => do let _ ← ensureNoRecFn recFnName e -/-- A `SavedLocalCtxt` captures the local context (e.g. of a recursive call), -so that it can be resumed later. +/-- +A `SavedLocalCtxt` captures the state and local context of a `TermElabM`, to be continued later. -/ +-- Q: Sensible? If so, can be moved near `TermElabM.saveState`? structure SavedLocalCtxt where - savedState : Term.SavedState savedLocalContext : LocalContext savedLocalInstances : LocalInstances savedTermContext : Term.Context savedTermState : Term.SavedState def SavedLocalCtxt.create : TermElabM SavedLocalCtxt := do - let savedState ← saveState let savedLocalContext ← getLCtx let savedLocalInstances ← getLocalInstances let savedTermContext ← readThe Term.Context @@ -299,8 +323,7 @@ def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : TermElabM α) : /-- A `RecCallContext` focuses on a single recursive call in a unary predefinition, -and runs the given action in the context of that call. --/ +and runs the given action in the context of that call. -/ structure RecCallContext where --- Function index of caller caller : Nat @@ -312,10 +335,16 @@ structure RecCallContext where args : Array Expr ctxt : SavedLocalCtxt +def RecCallContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) : + TermElabM RecCallContext := do + return { caller, params, callee, args, ctxt := (← SavedLocalCtxt.create) } + /-- Given the packed argument of a (possibly) mutual and (possibly) nary call, return the function index that is called and the arguments individually. -Cf. `packMutual` --/ + +We expect precisely the expressions produced by `packMutual`, with manifest +`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart +rather than using projectinos. -/ def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) : m (Nat × Array Expr) := do -- count PSum injections to find out which function is doing the call @@ -343,10 +372,6 @@ def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) : args := args.push e return (funidx, args) -def RecCallContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) : - TermElabM RecCallContext := do - return { caller, params, callee, args, ctxt := (← SavedLocalCtxt.create) } - /-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive call site. -/ @@ -360,7 +385,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti throwError "Unexpected number of lambdas in unary pre-definition" -- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}" let param := xs[fixedPrefixSize]! - withRecApps unaryPreDef.declName fixedPrefixSize body param fun param args => do + withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do unless args.size ≥ fixedPrefixSize + 1 do throwError "Insufficient arguments in recursive call" let arg := args[fixedPrefixSize]! From 925215189743b70b62f778923788c886bdab76d6 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 15 Nov 2023 14:59:06 +0100 Subject: [PATCH 10/27] Less TermElabM --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 90 ++++++++++---------- 1 file changed, 44 insertions(+), 46 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 4e023b3909c1..1b96c4cf84eb 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -52,7 +52,7 @@ The following optimizations are applied to make this feasible: and it adds more signal to the output. 4. Instead of traversing the whole function body over and over, we traverse it once and store - the arguments (in unpacked form) and the local `TermElabM` state at each recursive call + the arguments (in unpacked form) and the local `MetaM` state at each recursive call (see `collectRecCalls`), which we then re-use for the possibly many proof attempts. The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL” @@ -202,7 +202,7 @@ def _root_.Lean.Meta.CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : -- Q: Is it really not possible to add this to the `where` clause? @[reducible] def M (recFnName : Name) (α β : Type) : Type := - StateRefT (Array α) (StateRefT (HasConstCache recFnName) TermElabM) β + StateRefT (Array α) (StateRefT (HasConstCache recFnName) MetaM) β /-- Traverses the given expression `e`, and invokes the continuation `k` @@ -212,7 +212,7 @@ The expression `scrut` is passed along, and refined when going under a matcher or `casesOn` application. -/ partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (scrut : Expr) (e : Expr) - (k : Expr → Array Expr → TermElabM α) : TermElabM (Array α) := do + (k : Expr → Array Expr → MetaM α) : MetaM (Array α) := do trace[Elab.definition.wf] "withRecApps: {indentExpr e}" let (_, as) ← loop scrut e |>.run #[] |>.run' {} return as @@ -299,28 +299,25 @@ where let _ ← ensureNoRecFn recFnName e /-- -A `SavedLocalCtxt` captures the state and local context of a `TermElabM`, to be continued later. +A `SavedLocalCtxt` captures the state and local context of a `MetaM`, to be continued later. -/ --- Q: Sensible? If so, can be moved near `TermElabM.saveState`? +-- Q: Sensible? structure SavedLocalCtxt where savedLocalContext : LocalContext savedLocalInstances : LocalInstances - savedTermContext : Term.Context - savedTermState : Term.SavedState + savedState : Meta.SavedState -def SavedLocalCtxt.create : TermElabM SavedLocalCtxt := do +def SavedLocalCtxt.create : MetaM SavedLocalCtxt := do let savedLocalContext ← getLCtx let savedLocalInstances ← getLocalInstances - let savedTermContext ← readThe Term.Context - let savedTermState ← saveState - return { savedLocalContext, savedLocalInstances, savedTermState, savedTermContext } + let savedState ← saveState + return { savedLocalContext, savedLocalInstances, savedState } -def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : TermElabM α) : +def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : MetaM α) : MetaM α := withoutModifyingState $ do withLCtx slc.savedLocalContext slc.savedLocalInstances do - slc.savedTermState.meta.restore - k slc.savedTermContext |>.run' slc.savedTermState.elab - + slc.savedState.restore + k /-- A `RecCallContext` focuses on a single recursive call in a unary predefinition, and runs the given action in the context of that call. -/ @@ -336,7 +333,7 @@ structure RecCallContext where ctxt : SavedLocalCtxt def RecCallContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) : - TermElabM RecCallContext := do + MetaM RecCallContext := do return { caller, params, callee, args, ctxt := (← SavedLocalCtxt.create) } /-- Given the packed argument of a (possibly) mutual and (possibly) nary call, @@ -377,21 +374,20 @@ call site. -/ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat) : MetaM (Array RecCallContext) := withoutModifyingState do - Lean.Elab.Term.TermElabM.run' do - addAsAxiom unaryPreDef - lambdaTelescope unaryPreDef.value fun xs body => do - unless xs.size == fixedPrefixSize + 1 do - -- Maybe cleaner to have lambdaBoundedTelescope? - throwError "Unexpected number of lambdas in unary pre-definition" - -- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}" - let param := xs[fixedPrefixSize]! - withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do - unless args.size ≥ fixedPrefixSize + 1 do - throwError "Insufficient arguments in recursive call" - let arg := args[fixedPrefixSize]! - let (caller, params) ← unpackArg arities param - let (callee, args) ← unpackArg arities arg - RecCallContext.create caller params callee args + addAsAxiom unaryPreDef + lambdaTelescope unaryPreDef.value fun xs body => do + unless xs.size == fixedPrefixSize + 1 do + -- Maybe cleaner to have lambdaBoundedTelescope? + throwError "Unexpected number of lambdas in unary pre-definition" + -- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}" + let param := xs[fixedPrefixSize]! + withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do + unless args.size ≥ fixedPrefixSize + 1 do + throwError "Insufficient arguments in recursive call" + let arg := args[fixedPrefixSize]! + let (caller, params) ← unpackArg arities param + let (callee, args) ← unpackArg arities arg + RecCallContext.create caller params callee args inductive GuessLexRel | lt | eq | le | no_idea deriving Repr, DecidableEq @@ -439,21 +435,23 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx a if rel = .eq then MVarId.refl mvarId else do - match decrTactic? with - | none => - let remainingGoals ← Tactic.run mvarId do - Tactic.evalTactic (← `(tactic| decreasing_tactic)) - remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId] - let _expr ← instantiateMVars mvar - -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" - pure () - | some decrTactic => Term.withoutErrToSorry do - -- make info from `runTactic` available - pushInfoTree (.hole mvarId) - Term.runTactic mvarId decrTactic - let _expr ← instantiateMVars mvar - -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" - pure () + -- Q: Can I enter TermElabM like this? Is this even needed? + Lean.Elab.Term.TermElabM.run' do + match decrTactic? with + | none => + let remainingGoals ← Tactic.run mvarId do + Tactic.evalTactic (← `(tactic| decreasing_tactic)) + remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId] + let _expr ← instantiateMVars mvar + -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" + pure () + | some decrTactic => Term.withoutErrToSorry do + -- make info from `runTactic` available + pushInfoTree (.hole mvarId) + Term.runTactic mvarId decrTactic + let _expr ← instantiateMVars mvar + -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" + pure () return rel catch _e => -- trace[Elab.definition.wf] "Did not find {repr rel} proof of {goalsToMessageData [mvarId]}" From c514fa3d78d67af48f8be2271cf89e6391dcf31b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 15 Nov 2023 16:52:46 +0100 Subject: [PATCH 11/27] Code walkthrough with Sebastian --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 1b96c4cf84eb..609892df099f 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -82,7 +82,7 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array let n ← xs[i]!.fvarId!.getUserName if n.hasMacroScopes then -- TODO: Prettier code to generate x1...xn - ns := ns.push (← mkFreshUserName (.mkSimple ("x" ++ (repr (i+1)).pretty))) + ns := ns.push (← mkFreshUserName (.mkSimple s!"x{i+1}")) else ns := ns.push n return ns @@ -199,9 +199,7 @@ def _root_.Lean.Meta.CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : catch _ => return none --- Q: Is it really not possible to add this to the `where` clause? -@[reducible] -def M (recFnName : Name) (α β : Type) : Type := +abbrev M (recFnName : Name) (α β : Type) : Type := StateRefT (Array α) (StateRefT (HasConstCache recFnName) MetaM) β /-- @@ -302,6 +300,7 @@ where A `SavedLocalCtxt` captures the state and local context of a `MetaM`, to be continued later. -/ -- Q: Sensible? +-- See InfoTrees, similar stuff structure SavedLocalCtxt where savedLocalContext : LocalContext savedLocalInstances : LocalInstances @@ -322,13 +321,13 @@ def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : MetaM α) : /-- A `RecCallContext` focuses on a single recursive call in a unary predefinition, and runs the given action in the context of that call. -/ structure RecCallContext where - --- Function index of caller + /-- Function index of caller -/ caller : Nat - --- Parameters of caller + /-- Parameters of caller -/ params : Array Expr - --- Function index of callee + /-- Function index of callee -/ callee : Nat - --- Arguments to callee + /-- Arguments to callee -/ args : Array Expr ctxt : SavedLocalCtxt @@ -605,6 +604,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α) -- Does this really not yet exist? Should it? +-- Yes! partial def mkTupleSyntax : Array Syntax → MetaM Syntax | #[] => `(()) | #[e] => return e @@ -623,7 +623,8 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name)) let body ← mkTupleSyntax (← measures.mapM fun | .args varIdxs => let v := vars.get! (varIdxs[funIdx]!) - `(sizeOf $v) + let sizeOfIdent := mkIdent ``sizeOf + `($sizeOfIdent $v) | .func funIdx' => if funIdx' == funIdx then `(1) else `(0) ) let declName := declNames[funIdx]! From e8b6cb330547201ecb049bc9bb91d0ee50fada53 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 16 Nov 2023 18:44:56 +0100 Subject: [PATCH 12/27] Use forallTelescope --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 34 +++++++++----------- 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 609892df099f..e80bca282f84 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -122,16 +122,16 @@ def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : unless (← isTypeCorrect aux) do throwError "failed to transfer argument through matcher application, type error when constructing the new motive" let auxType ← inferType aux - let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let (altAuxs, _, _) ← forallMetaTelescope auxType let altAuxTys ← altAuxs.mapM (inferType ·) (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs /-- A non-failing version of `transform` -/ -- PR'ed at https://github.com/leanprover/lean4/pull/2882 @@ -166,7 +166,6 @@ def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : for motiveArg in motiveArgs.reverse, discr in discrs.reverse do eAbst ← kabstract eAbst discr eAbst := eAbst.instantiate1 motiveArg - -- Up to this point, this is cargo-culted from `CasesOn.App.addArg` -- Let's create something Prop-typed that mentions `e`, by writing `e = e`. let eEq ← mkEq eAbst eAbst let motive ← mkLambdaFVars motiveArgs eEq @@ -179,16 +178,16 @@ def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : let auxType ← inferType aux -- The type of the remaining arguments will mention `e` instantiated for each arg -- so extract them - let (altAuxs, _, _) ← Lean.Meta.forallMetaTelescope auxType + let (altAuxs, _, _) ← forallMetaTelescope auxType let altAuxTys ← altAuxs.mapM (inferType ·) (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - let (fvs, _, body) ← Lean.Meta.forallMetaTelescope altAuxTy - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs /-- A non-failing version of `transform` -/ -- PR'ed at https://github.com/leanprover/lean4/pull/2882 @@ -434,7 +433,6 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx a if rel = .eq then MVarId.refl mvarId else do - -- Q: Can I enter TermElabM like this? Is this even needed? Lean.Elab.Term.TermElabM.run' do match decrTactic? with | none => From 9e3db470a8abb0a976c0a62a4e16c53a58e5e117 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 18 Nov 2023 12:50:02 +0100 Subject: [PATCH 13/27] Use forallTelescope --- src/Lean/Meta/CasesOn.lean | 20 ++++++++++---------- src/Lean/Meta/Match/Match.lean | 20 ++++++++++---------- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 7fc743c7a4bf..636302f37162 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -159,16 +159,16 @@ def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := let auxType ← inferType aux -- The type of the remaining arguments will mention `e` instantiated for each arg -- so extract them - let (altAuxs, _, _) ← forallMetaTelescope auxType - let altAuxTys ← altAuxs.mapM (inferType ·) - (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - forallTelescope altAuxTy fun fvs body => do - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs + forallTelescope auxType fun altAuxs _ => do + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs /-- A non-failing version of `CasesOnApp.transform` -/ def CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index e37aaaecd73b..a28673c004bc 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -1009,16 +1009,16 @@ def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Exp unless (← isTypeCorrect aux) do throwError "failed to transfer argument through matcher application, type error when constructing the new motive" let auxType ← inferType aux - let (altAuxs, _, _) ← forallMetaTelescope auxType - let altAuxTys ← altAuxs.mapM (inferType ·) - (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - forallTelescope altAuxTy fun fvs body => do - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs + forallTelescope auxType fun altAuxs _ => do + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs /-- A non-failing version of `MatcherApp.transform` -/ def MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) : From d0b5a26f0ebaa952ee4cd7dae8d15d8abb3c81a0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 18 Nov 2023 12:51:01 +0100 Subject: [PATCH 14/27] Tuple syntax, forallTelescope --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 65 ++++++++++---------- 1 file changed, 31 insertions(+), 34 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index e80bca282f84..3078f0d2ab08 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -93,7 +93,8 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array - expression `e : B[discrs]`, returns the expressions `B[C_1[ys_1]]) ... B[C_n[ys_n]]`, with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`. - Cf. `MatcherApp.addArg`. + + This is similar to `MatcherApp.addArg` when you only have a type to transform, not a concrete value. -/ -- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : @@ -122,18 +123,18 @@ def _root_.Lean.Meta.MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : unless (← isTypeCorrect aux) do throwError "failed to transfer argument through matcher application, type error when constructing the new motive" let auxType ← inferType aux - let (altAuxs, _, _) ← forallMetaTelescope auxType - let altAuxTys ← altAuxs.mapM (inferType ·) - (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - forallTelescope altAuxTy fun fvs body => do - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs - -/-- A non-failing version of `transform` -/ + forallTelescope auxType fun altAuxs _ => do + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs + +/-- A non-failing version of `MatcherApp.transform` -/ -- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option (Array Expr)) := @@ -153,6 +154,8 @@ def _root_.Lean.Meta.MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) B[C_i[ys_i]] ``` with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`. + + This is similar to `CasesOnApp.addArg` when you only have a type to transform, not a concrete value. -/ -- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : @@ -178,18 +181,18 @@ def _root_.Lean.Meta.CasesOnApp.transform (c : CasesOnApp) (e : Expr) : let auxType ← inferType aux -- The type of the remaining arguments will mention `e` instantiated for each arg -- so extract them - let (altAuxs, _, _) ← forallMetaTelescope auxType - let altAuxTys ← altAuxs.mapM (inferType ·) - (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - forallTelescope altAuxTy fun fvs body => do - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - Expr.abstractM body fvs - -/-- A non-failing version of `transform` -/ + forallTelescope auxType fun altAuxs _ => do + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + forallTelescope altAuxTy fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + Expr.abstractM body fvs + +/-- A non-failing version of `CasesOnApp.transform` -/ -- PR'ed at https://github.com/leanprover/lean4/pull/2882 def _root_.Lean.Meta.CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : MetaM (Option (Array Expr)) := @@ -600,17 +603,11 @@ partial def solve {m} {α} [Monad m] (measures : Array α) -- None found, we have to give up return .none - --- Does this really not yet exist? Should it? --- Yes! -partial def mkTupleSyntax : Array Syntax → MetaM Syntax +-- TODO: Move to appropriate place +def mkTupleSyntax : Array Term → MetaM Term | #[] => `(()) | #[e] => return e - | es => do - let e : TSyntax `term := ⟨es[0]!⟩ - let es : Syntax.TSepArray `term "," := - ⟨(Syntax.SepArray.ofElems (sep := ",") es[1:]).1⟩ - `(term|($e, $es,*)) + | es => `(($(es[0]!), $(es[1:]),*)) def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name)) (measures : Array MutualMeasure) : MetaM TerminationWF := do From 6d17de52fee0b7224d83482a955dfadd476a9beb Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 20 Nov 2023 11:47:09 +0100 Subject: [PATCH 15/27] Docstring all the functions --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 60 +++++++++++++++----- 1 file changed, 45 insertions(+), 15 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 3078f0d2ab08..17455ec2ff5e 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -201,6 +201,7 @@ def _root_.Lean.Meta.CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : catch _ => return none +/-- Internal monad used by `withRecApps` -/ abbrev M (recFnName : Name) (α β : Type) : Type := StateRefT (Array α) (StateRefT (HasConstCache recFnName) MetaM) β @@ -308,12 +309,14 @@ structure SavedLocalCtxt where savedLocalInstances : LocalInstances savedState : Meta.SavedState +/-- Capture the `MetaM` state including local context. -/ def SavedLocalCtxt.create : MetaM SavedLocalCtxt := do let savedLocalContext ← getLCtx let savedLocalInstances ← getLocalInstances let savedState ← saveState return { savedLocalContext, savedLocalInstances, savedState } +/-- Run a `MetaM` action in the saved state. -/ def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : MetaM α) : MetaM α := withoutModifyingState $ do withLCtx slc.savedLocalContext slc.savedLocalInstances do @@ -333,6 +336,7 @@ structure RecCallContext where args : Array Expr ctxt : SavedLocalCtxt +/-- Store the current recursive call and its context. -/ def RecCallContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) : MetaM RecCallContext := do return { caller, params, callee, args, ctxt := (← SavedLocalCtxt.create) } @@ -390,6 +394,8 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti let (callee, args) ← unpackArg arities arg RecCallContext.create caller params callee args +/-- A `GuessLexRel` described how a recursive call affects a measure; whether it +decreases strictly, non-strictly, is equal, or else. -/ inductive GuessLexRel | lt | eq | le | no_idea deriving Repr, DecidableEq @@ -399,12 +405,14 @@ instance : ToFormat GuessLexRel where | .le => "≤" | .no_idea => "?" +/-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/ def GuessLexRel.toNatRel : GuessLexRel → Expr | lt => mkAppN (mkConst ``LT.lt [levelZero]) #[mkConst ``Nat, mkConst ``instLTNat] | eq => mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat] | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat] | no_idea => unreachable! -- TODO: keep it partial or refactor? +/-- Given an expression `e`, produce `sizeOf e` with a suitable instance -/ def mkSizeOf (e : Expr) : MetaM Expr := do let ty ← inferType e let lvl ← getLevel ty @@ -413,8 +421,10 @@ def mkSizeOf (e : Expr) : MetaM Expr := do check res return res --- For a given recursive call and choice of paramter index, --- try to prove requality, < or ≤ +/-- +For a given recursive call, and a choice of parameter and argument index, +try to prove requality, < or ≤. +-/ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do rcc.ctxt.run do @@ -458,17 +468,19 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx a continue return .no_idea --- A cache for `evalRecCall` +/- A cache for `evalRecCall` -/ structure RecCallCache where mk'' :: decrTactic? : Option Syntax rcc : RecCallContext cache : IO.Ref (Array (Array (Option GuessLexRel))) +/-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/ def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallContext) : BaseIO RecCallCache := do let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none) return { decrTactic?, rcc, cache } +/-- Run `evalRecCall` and cache there result -/ def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do -- Check the cache first if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then @@ -478,6 +490,7 @@ def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLe rc.cache.modify (·.modify paramIdx (·.set! argIdx res)) return res +/-- Pretty-print the cache entries -/ def RecCallCache.pretty (rc : RecCallCache) : IO Format := do let mut r := Format.nil let d ← rc.cache.get @@ -491,11 +504,12 @@ def RecCallCache.pretty (rc : RecCallCache) : IO Format := do /-- The measures that we order lexicographically can be comparing arguments, or numbering the functions -/ inductive MutualMeasure where + /-- For every function, the given argument index -/ | args : Array Nat → MutualMeasure - --- The given function index is assigned 1, the rest 0 + /-- The given function index is assigned 1, the rest 0 -/ | func : Nat → MutualMeasure --- Evaluate a call at a given measure +/-- Evaluate a recursive call at a given `MutualMeasure` -/ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel | .args argIdxs => do let paramIdx := argIdxs[rc.rcc.caller]! @@ -510,11 +524,11 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel 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. - This arguments should not be considered when guessing a well-founded relation. - See `generateCombinations?` +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 @@ -529,10 +543,12 @@ def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) 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 try first, when the mutually recursive functions have similar --- argument structures +/-- +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 +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)) := (do goUniform 0; go 0 #[]) |>.run #[] |>.2 @@ -565,7 +581,8 @@ where failure -/-- The core logic of guessing the lexicographic order +/-- +The core logic of guessing the lexicographic order Given a matrix that for each call and measure indicates whether that measure is decreasing, equal, less-or-equal or unknown, It finds a sequence of measures that is lexicographically decreasing. @@ -604,11 +621,18 @@ partial def solve {m} {α} [Monad m] (measures : Array α) return .none -- TODO: Move to appropriate place +/-- +Create Tuple syntax. +-/ def mkTupleSyntax : Array Term → MetaM Term | #[] => `(()) | #[e] => return e | es => `(($(es[0]!), $(es[1:]),*)) +/-- +Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic +combination of these measures. +-/ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name)) (measures : Array MutualMeasure) : MetaM TerminationWF := do -- logInfo <| m!"Solution: {solution}" @@ -639,6 +663,12 @@ namespace Lean.Elab.WF open Lean.Elab.WF.GuessLex +/-- +Main entry point of this module: + +Try to find a lexicographic ordering of the arguments for which the recursive definition +terminates. See the module doc string for a high-level overview. +-/ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) : MetaM TerminationWF := do From 2f04011f91b779a35f875898621b9d9451c04d82 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 21 Nov 2023 17:14:40 +0100 Subject: [PATCH 16/27] Change copyright --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 17455ec2ff5e..d1678d7bb8fd 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2023 Joachim Breitner. All rights reserved. +Copyright (c) 2023 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ From 6f7165a34606b019f5ab89a044b4f766b09d6f47 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 18:36:07 +0100 Subject: [PATCH 17/27] Clean-up pass --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 43 ++++++++------------ 1 file changed, 18 insertions(+), 25 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index eb176eae2d2e..218fa83af05f 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -72,16 +72,13 @@ Use user-given parameter names if present; use x1...xn otherwise. The length of the returned array is also used to determine the arity of the function, so it should match what `packDomain` does. -/ --- TODO: Maybe the eta-expansion handling `fun foo : … | n -> ` should try to use --- a nicer name than simply `x`? def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name):= do lambdaTelescope preDef.value fun xs _ => do let xs := xs.extract fixedPrefixSize xs.size let mut ns := #[] - for i in List.range xs.size do - let n ← xs[i]!.fvarId!.getUserName + for h : i in [:xs.size] do + let n ← (xs[i]'h.2).fvarId!.getUserName if n.hasMacroScopes then - -- TODO: Prettier code to generate x1...xn ns := ns.push (← mkFreshUserName (.mkSimple s!"x{i+1}")) else ns := ns.push n @@ -125,7 +122,6 @@ where loop (scrut : Expr) (e : Expr) : M recFnName α Unit := do if !(← containsRecFn e) then return - -- trace[Elab.definition.wf] "loop: {indentExpr scrut}{indentExpr e}" match e with | Expr.lam n d b c => loop scrut d @@ -291,14 +287,14 @@ instance : ToFormat GuessLexRel where | .le => "≤" | .no_idea => "?" -/-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/ +/-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/ def GuessLexRel.toNatRel : GuessLexRel → Expr | lt => mkAppN (mkConst ``LT.lt [levelZero]) #[mkConst ``Nat, mkConst ``instLTNat] | eq => mkAppN (mkConst ``Eq [levelOne]) #[mkConst ``Nat] | le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat] - | no_idea => unreachable! -- TODO: keep it partial or refactor? + | no_idea => unreachable! -/-- Given an expression `e`, produce `sizeOf e` with a suitable instance -/ +/-- Given an expression `e`, produce `sizeOf e` with a suitable instance. -/ def mkSizeOf (e : Expr) : MetaM Expr := do let ty ← inferType e let lvl ← getLevel ty @@ -309,7 +305,7 @@ def mkSizeOf (e : Expr) : MetaM Expr := do /-- For a given recursive call, and a choice of parameter and argument index, -try to prove requality, < or ≤. +try to prove equality, < or ≤. -/ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do @@ -321,7 +317,7 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx a 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 (unchecked): {goalExpr}" + trace[Elab.definition.wf] "Goal for {rel}: {goalExpr}" check goalExpr let mvar ← mkFreshExprSyntheticOpaqueMVar goalExpr @@ -338,19 +334,18 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx a let remainingGoals ← Tactic.run mvarId do Tactic.evalTactic (← `(tactic| decreasing_tactic)) remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId] - let _expr ← instantiateMVars mvar - -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" + -- trace[Elab.definition.wf] "Found {rel} proof: {← instantiateMVars mvar}" pure () | some decrTactic => Term.withoutErrToSorry do -- make info from `runTactic` available pushInfoTree (.hole mvarId) Term.runTactic mvarId decrTactic - let _expr ← instantiateMVars mvar - -- trace[Elab.definition.wf] "Found {repr rel} proof: {expr}" + -- trace[Elab.definition.wf] "Found {rel} proof: {← instantiateMVars mvar}" pure () + trace[Elab.definition.wf] "inspectRecCall: success!" return rel catch _e => - -- trace[Elab.definition.wf] "Did not find {repr rel} proof of {goalsToMessageData [mvarId]}" + trace[Elab.definition.wf] "Did not find {rel} proof: {goalsToMessageData [mvarId]}" continue return .no_idea @@ -380,9 +375,9 @@ def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLe def RecCallCache.pretty (rc : RecCallCache) : IO Format := do let mut r := Format.nil let d ← rc.cache.get - for paramIdx in [:d.size] do - for argIdx in [:d[paramIdx]!.size] do - if let .some entry := d[paramIdx]![argIdx]! then + for h₁ : paramIdx in [:d.size] do + for h₂ : argIdx in [:(d[paramIdx]'h₁.2).size] do + if let .some entry := (d[paramIdx]'h₁.2)[argIdx]'h₂.2 then r := r ++ f!"(Param {paramIdx}, arg {argIdx}): {entry}" ++ Format.line return r @@ -506,7 +501,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α) -- None found, we have to give up return .none --- TODO: Move to appropriate place +-- Question: Which module should have this? /-- Create Tuple syntax. -/ @@ -521,7 +516,6 @@ combination of these measures. -/ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name)) (measures : Array MutualMeasure) : MetaM TerminationWF := do - -- logInfo <| m!"Solution: {solution}" let mut termByElements := #[] for h : funIdx in [:varNamess.size] do let vars := (varNamess[funIdx]'h.2).map mkIdent @@ -534,12 +528,11 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name)) ) let declName := declNames[funIdx]! - -- TODO: Can we turn it into user-facing syntax? Maybe for a “try-this” feature? trace[Elab.definition.wf] "Using termination {declName}: {vars} => {body}" termByElements := termByElements.push - { ref := .missing -- is this the right function + { ref := .missing declName, vars, body, - implicit := true -- TODO, what is this? + implicit := true } return .ext termByElements @@ -591,5 +584,5 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) | .none => throwError "Cannot find a decreasing lexicographic order" catch _ => -- Hide all errors from guessing lexicographic orderings, as before - -- TODO: surface unexpected errors, maybe surface detailed explanation like Isabelle + -- Future work: explain the failure to the user, like Isabelle does throwError "failed to prove termination, use `termination_by` to specify a well-founded relation" From 5611e580b9279576b9197b870a4068b0540e4f60 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 18:41:55 +0100 Subject: [PATCH 18/27] Apply review comments --- src/Lean/Meta/CasesOn.lean | 21 +++++++++++---------- src/Lean/Meta/Match/Match.lean | 17 ++++++++++------- 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 636302f37162..152e5a0e467a 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -123,10 +123,8 @@ def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := f ``` casesOn As (fun is x => motive[is, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining ``` - and an expression `B[is, major]`, for every alternative `i`, construct the type - ``` - B[_, C_i[ys_i]] - ``` + and an expression `B[is, major]` (which may not be a type, e.g. `n : Nat`) + for every alternative `i`, construct the type `B[_, C_i[ys_i]]` with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`. This is similar to `CasesOnApp.addArg` when you only have an expression to @@ -135,10 +133,12 @@ def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := f This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive calls to refine the functions' paramter, which may mention `major`. See there for how to use this function. + + It returns an open term, rather than following the idiom of applying a continuation, + so that `CasesOn.refineThrough?` can reliably recognize failure from within this function. -/ -def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := +def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := lambdaTelescope c.motive fun motiveArgs _motiveBody => do - trace[Elab.definition.wf] "CasesOnApp.transform: {indentExpr e}" unless motiveArgs.size == c.indices.size + 1 do throwError "failed to transfer argument through `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders" let discrs := c.indices ++ #[c.major] @@ -146,8 +146,9 @@ def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := for motiveArg in motiveArgs.reverse, discr in discrs.reverse do eAbst ← kabstract eAbst discr eAbst := eAbst.instantiate1 motiveArg - -- Let's create something that’s a `Sort` and mentions `e`, by writing `e = e`, - -- so that we can use it as a motive + -- Let's create something that’s a `Sort` and mentions `e` + -- (recall that `e` itself possibly isn't a type), + -- by writing `e = e`, so that we can use it as a motive let eEq ← mkEq eAbst eAbst let motive ← mkLambdaFVars motiveArgs eEq let us := if c.propOnly then c.us else levelZero :: c.us.tail! @@ -171,10 +172,10 @@ def CasesOnApp.transform (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := Expr.abstractM body fvs /-- A non-failing version of `CasesOnApp.transform` -/ -def CasesOnApp.transform? (c : CasesOnApp) (e : Expr) : +def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) : MetaM (Option (Array Expr)) := try - return some (← c.transform e) + return some (← c.refineThrough e) catch _ => return none diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index a28673c004bc..2e0bd8eee3f5 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -967,7 +967,7 @@ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option Matc /-- Given - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - - a type `B[discrs]`, + - a type `B[discrs]` (which may not be a type, e.g. `n : Nat`), returns the types `B[C_1[ys_1]] ... B[C_n[ys_n]]`, with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`. @@ -981,10 +981,12 @@ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option Matc This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive calls to refine the functions' paramter, which may mention `major`. See there for how to use this function. + + It returns an open term, rather than following the idiom of applying a continuation, + so that `MatcherApp.refineThrough?` can reliably recognize failure from within this function -/ -def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := +def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do - trace[Elab.definition.wf] "MatcherApp.transform {indentExpr e}" unless motiveArgs.size == matcherApp.discrs.size do -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. throwError "failed to transfer argument through matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" @@ -994,8 +996,9 @@ def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Exp let discr := matcherApp.discrs[i]! let eTypeAbst ← kabstract eAbst discr return eTypeAbst.instantiate1 motiveArg - -- Let's create something that’s a `Sort` and mentions `e`, by writing `e = e`, - -- so that we can use it as a motive + -- Let's create something that’s a `Sort` and mentions `e` + -- (recall that `e` itself possibly isn't a type), + -- by writing `e = e`, so that we can use it as a motive let eEq ← mkEq eAbst eAbst let matcherLevels ← match matcherApp.uElimPos? with @@ -1021,10 +1024,10 @@ def MatcherApp.transform (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Exp Expr.abstractM body fvs /-- A non-failing version of `MatcherApp.transform` -/ -def MatcherApp.transform? (matcherApp : MatcherApp) (e : Expr) : +def MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option (Array Expr)) := try - return some (← matcherApp.transform e) + return some (← matcherApp.refineThrough e) catch _ => return none From cd7fbd4aa08a8f92a79eec77a8e841fbc070c509 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 18:43:31 +0100 Subject: [PATCH 19/27] Forgot one --- src/Lean/Meta/CasesOn.lean | 2 +- src/Lean/Meta/Match/Match.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 152e5a0e467a..86371632a4cc 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -171,7 +171,7 @@ def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) := -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out Expr.abstractM body fvs -/-- A non-failing version of `CasesOnApp.transform` -/ +/-- A non-failing version of `CasesOnApp.refineThrough` -/ def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) : MetaM (Option (Array Expr)) := try diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 2e0bd8eee3f5..00295e4cc1dc 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -1023,7 +1023,7 @@ def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out Expr.abstractM body fvs -/-- A non-failing version of `MatcherApp.transform` -/ +/-- A non-failing version of `MatcherApp.refineThrough` -/ def MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option (Array Expr)) := try From 069da842e7935d07b3ee0e41c1e5216a9f518185 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 18:44:10 +0100 Subject: [PATCH 20/27] .transform got renamed --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 218fa83af05f..1d071844f876 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -149,14 +149,13 @@ where if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then processApp scrut e else - if let some altScruts ← matcherApp.transform? scrut then + if let some altScruts ← matcherApp.refineThrough? scrut then (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altScruts)).forM fun (alt, altNumParam, altScrut) => lambdaTelescope alt fun xs altBody => do unless altNumParam ≤ xs.size do throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}" let altScrut := altScrut.instantiateRev xs[:altNumParam] - trace[Elab.definition.wf] "MatcherApp.transform result {indentExpr altScrut}" loop altScrut altBody else processApp scrut e @@ -166,14 +165,13 @@ where if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then processApp scrut e else - if let some altScruts ← casesOnApp.transform? scrut then + if let some altScruts ← casesOnApp.refineThrough? scrut then (Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altScruts)).forM fun (alt, altNumParam, altScrut) => lambdaTelescope alt fun xs altBody => do unless altNumParam ≤ xs.size do throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" let altScrut := altScrut.instantiateRev xs[:altNumParam] - trace[Elab.definition.wf] "CasesOnApp.transform result {indentExpr altScrut}" loop altScrut altBody else processApp scrut e From 429996716fe51023dff64b4c468dc0301ee9f12b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 18:48:16 +0100 Subject: [PATCH 21/27] Docstring --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 1d071844f876..f66d40eff73b 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -501,7 +501,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α) -- Question: Which module should have this? /-- -Create Tuple syntax. +Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton) -/ def mkTupleSyntax : Array Term → MetaM Term | #[] => `(()) From 768c53238be8326722c342e3d1d2e1b1a5f745b2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 18:52:54 +0100 Subject: [PATCH 22/27] Apply review comments --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 43 ++++++++++---------- 1 file changed, 21 insertions(+), 22 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index f66d40eff73b..e38699f259d6 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -180,32 +180,31 @@ where let _ ← ensureNoRecFn recFnName e /-- -A `SavedLocalCtxt` captures the state and local context of a `MetaM`, to be continued later. +A `SavedLocalContext` captures the state and local context of a `MetaM`, to be continued later. -/ --- Q: Sensible? --- See InfoTrees, similar stuff -structure SavedLocalCtxt where +structure SavedLocalContext where savedLocalContext : LocalContext savedLocalInstances : LocalInstances savedState : Meta.SavedState /-- Capture the `MetaM` state including local context. -/ -def SavedLocalCtxt.create : MetaM SavedLocalCtxt := do +def SavedLocalContext.create : MetaM SavedLocalContext := do let savedLocalContext ← getLCtx let savedLocalInstances ← getLocalInstances let savedState ← saveState return { savedLocalContext, savedLocalInstances, savedState } /-- Run a `MetaM` action in the saved state. -/ -def SavedLocalCtxt.run {α} (slc : SavedLocalCtxt) (k : MetaM α) : - MetaM α := withoutModifyingState $ do - withLCtx slc.savedLocalContext slc.savedLocalInstances do - slc.savedState.restore - k - -/-- A `RecCallContext` focuses on a single recursive call in a unary predefinition, +def SavedLocalContext.run {α} (slc : SavedLocalContext) (k : MetaM α) : + MetaM α := + withoutModifyingState $ do + withLCtx slc.savedLocalContext slc.savedLocalInstances do + slc.savedState.restore + k + +/-- A `RecCallWithContext` focuses on a single recursive call in a unary predefinition, and runs the given action in the context of that call. -/ -structure RecCallContext where +structure RecCallWithContext where /-- Function index of caller -/ caller : Nat /-- Parameters of caller -/ @@ -214,12 +213,12 @@ structure RecCallContext where callee : Nat /-- Arguments to callee -/ args : Array Expr - ctxt : SavedLocalCtxt + ctxt : SavedLocalContext /-- Store the current recursive call and its context. -/ -def RecCallContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) : - MetaM RecCallContext := do - return { caller, params, callee, args, ctxt := (← SavedLocalCtxt.create) } +def RecCallWithContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) : + MetaM RecCallWithContext := do + return { caller, params, callee, args, ctxt := (← SavedLocalContext.create) } /-- Given the packed argument of a (possibly) mutual and (possibly) nary call, return the function index that is called and the arguments individually. @@ -258,7 +257,7 @@ def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) : call site. -/ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat) - : MetaM (Array RecCallContext) := withoutModifyingState do + : MetaM (Array RecCallWithContext) := withoutModifyingState do addAsAxiom unaryPreDef lambdaTelescope unaryPreDef.value fun xs body => do unless xs.size == fixedPrefixSize + 1 do @@ -272,7 +271,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti let arg := args[fixedPrefixSize]! let (caller, params) ← unpackArg arities param let (callee, args) ← unpackArg arities arg - RecCallContext.create caller params callee args + RecCallWithContext.create caller params callee args /-- A `GuessLexRel` described how a recursive call affects a measure; whether it decreases strictly, non-strictly, is equal, or else. -/ @@ -305,7 +304,7 @@ def mkSizeOf (e : Expr) : MetaM Expr := do For a given recursive call, and a choice of parameter and argument index, try to prove equality, < or ≤. -/ -def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx argIdx : Nat) : +def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do rcc.ctxt.run do let param := rcc.params[paramIdx]! @@ -350,11 +349,11 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallContext) (paramIdx a /- A cache for `evalRecCall` -/ structure RecCallCache where mk'' :: decrTactic? : Option Syntax - rcc : RecCallContext + rcc : RecCallWithContext cache : IO.Ref (Array (Array (Option GuessLexRel))) /-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/ -def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallContext) : +def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallWithContext) : BaseIO RecCallCache := do let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none) return { decrTactic?, rcc, cache } From f4f64e52dab9b7789c47535909d6dd2519526788 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 18:56:41 +0100 Subject: [PATCH 23/27] Remove old guessing code --- src/Lean/Elab/PreDefinition/WF/Rel.lean | 94 ++----------------------- 1 file changed, 7 insertions(+), 87 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean index 9b872e659206..6ca0bd16ea51 100644 --- a/src/Lean/Elab/PreDefinition/WF/Rel.lean +++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean @@ -53,67 +53,21 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva mvarId.rename fvarId varNames.back go 0 mvarId fvarId -def getNumCandidateArgs (fixedPrefixSize : Nat) (preDefs : Array PreDefinition) : MetaM (Array Nat) := do - preDefs.mapM fun preDef => - lambdaTelescope preDef.value fun xs _ => - return xs.size - fixedPrefixSize - -/-- - 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. - This 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 - -def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (threshold : Nat := 32) : Option (Array (Array Nat)) := - go 0 #[] |>.run #[] |>.2 -where - isForbidden (fidx : Nat) (argIdx : Nat) : Bool := - if h : fidx < forbiddenArgs.size then - forbiddenArgs.get ⟨fidx, h⟩ |>.contains argIdx - else - false - - go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do - if h : fidx < numArgs.size then - let n := numArgs.get ⟨fidx, h⟩ - for argIdx in [:n] do - unless isForbidden fidx argIdx do - withReader (·.push argIdx) (go (fidx + 1)) - else - modify (·.push (← read)) - if (← get).size > threshold then - failure -termination_by _ fidx => numArgs.size - fidx - -def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat) (argType : Expr) (wf? : Option TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do +def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat) + (argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do let α := argType let u ← getLevel α let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}" - match wf? with - | some (TerminationWF.core wfStx) => withDeclName unaryPreDefName do + withDeclName unaryPreDefName do + match wf with + | TerminationWF.core wfStx => let wfRel ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType) let pendingMVarIds ← getMVars wfRel discard <| logUnassignedUsingErrorInfos pendingMVarIds k wfRel - | some (TerminationWF.ext elements) => go expectedType elements - | none => guess expectedType -where - go (expectedType : Expr) (elements : Array TerminationByElement) : TermElabM α := - withDeclName unaryPreDefName <| withRef (getRefFromElems elements) do + | TerminationWF.ext elements => + withRef (getRefFromElems elements) do let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId! let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'" let (d, fMVarId) ← fMVarId.intro1 @@ -127,38 +81,4 @@ where wfRelMVarId.assign wfRelVal k (← instantiateMVars (mkMVar mainMVarId)) - generateElements (numArgs : Array Nat) (argCombination : Array Nat) : TermElabM (Array TerminationByElement) := do - let mut result := #[] - let var ← `(x) - let hole ← `(_) - for preDef in preDefs, numArg in numArgs, argIdx in argCombination, i in [:preDefs.size] do - let mut vars := #[var] - for _ in [:numArg - argIdx - 1] do - vars := vars.push hole - -- TODO: improve this. - -- The following trick allows a function `f` in a mutual block to invoke `g` appearing before it with the input argument. - -- We should compute the "right" order (if there is one) in the future. - let body ← if preDefs.size > 1 then `((sizeOf x, $(quote i))) else `(sizeOf x) - result := result.push { - ref := preDef.ref - declName := preDef.declName - vars := vars - body := body - implicit := false - } - return result - - guess (expectedType : Expr) : TermElabM α := do - -- TODO: add support for lex - let numArgs ← getNumCandidateArgs fixedPrefixSize preDefs - -- TODO: include in `forbiddenArgs` arguments that are fixed but are not in the fixed prefix - let forbiddenArgs ← preDefs.mapM fun preDef => getForbiddenByTrivialSizeOf fixedPrefixSize preDef - -- TODO: add option to control the maximum number of cases to try - if let some combs := generateCombinations? forbiddenArgs numArgs then - for comb in combs do - let elements ← generateElements numArgs comb - if let some r ← observing? (go expectedType elements) then - return r - throwError "failed to prove termination, use `termination_by` to specify a well-founded relation" - end Lean.Elab.WF From 64a8074894203366a17866850741381e946b8609 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 19:16:51 +0100 Subject: [PATCH 24/27] Add test cases --- tests/lean/guessLexFailures.lean | 34 ++++++ tests/lean/guessLexFailures.lean.expected.out | 13 +++ tests/lean/run/guessLex.lean | 109 ++++++++++++++++++ tests/lean/run/guessLexTricky.lean | 51 ++++++++ tests/lean/run/guessLexTricky2.lean | 23 ++++ 5 files changed, 230 insertions(+) create mode 100644 tests/lean/guessLexFailures.lean create mode 100644 tests/lean/guessLexFailures.lean.expected.out create mode 100644 tests/lean/run/guessLex.lean create mode 100644 tests/lean/run/guessLexTricky.lean create mode 100644 tests/lean/run/guessLexTricky2.lean diff --git a/tests/lean/guessLexFailures.lean b/tests/lean/guessLexFailures.lean new file mode 100644 index 000000000000..28e7bff8d5cd --- /dev/null +++ b/tests/lean/guessLexFailures.lean @@ -0,0 +1,34 @@ +/-! +A few cases where guessing the lexicographic order fails, and +where we want to keep tabs on the output. +-/ + +def nonTerminating : Nat → Nat + | 0 => 0 + | n => nonTerminating (.succ n) + +-- Saying decreasing_by forces Lean to use structural recursion, which gives a different +-- error message +def nonTerminating2 : Nat → Nat + | 0 => 0 + | n => nonTerminating2 (.succ n) +decreasing_by decreasing_tactic + + +-- The GuessLex code does not like eta-contracted motives in `casesOn`. +-- At the time of writing, the error message is swallowed +-- When guessing the lexicographic order becomes more verbose this will improve. +def FinPlus1 n := Fin (n + 1) +def badCasesOn (n : Nat) : Fin (n + 1) := + Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n)) +decreasing_by decreasing_tactic +-- termination_by badCasesOn n => n + + +-- Like above, but now with a `casesOn` alternative with insufficient lambdas +def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) := fun n => Fin.succ (f n) +def badCasesOn2 (n : Nat) : Fin (n + 1) := + Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩) + (Fin_succ_comp (fun n => badCasesOn2 n)) +decreasing_by decreasing_tactic +-- termination_by badCasesOn2 n => n diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out new file mode 100644 index 000000000000..d170019599cb --- /dev/null +++ b/tests/lean/guessLexFailures.lean.expected.out @@ -0,0 +1,13 @@ +guessLexFailures.lean:8:9-8:33: error: fail to show termination for + nonTerminating +with errors +argument #1 was not used for structural recursion + failed to eliminate recursive application + nonTerminating (Nat.succ n) + +structural recursion cannot be used + +failed to prove termination, use `termination_by` to specify a well-founded relation +guessLexFailures.lean:12:0-15:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation +guessLexFailures.lean:22:0-24:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation +guessLexFailures.lean:30:0-33:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation diff --git a/tests/lean/run/guessLex.lean b/tests/lean/run/guessLex.lean new file mode 100644 index 000000000000..993ccddc1b33 --- /dev/null +++ b/tests/lean/run/guessLex.lean @@ -0,0 +1,109 @@ +/-! +This files tests Lean's ability to guess the right lexicographic order. + +TODO: Once lean spits out the guessed order (probably guarded by an +option), turn this on and check the output. +-/ + +def ackermann (n m : Nat) := match n, m with + | 0, m => m + 1 + | .succ n, 0 => ackermann n 1 + | .succ n, .succ m => ackermann n (ackermann (n + 1) m) + +def ackermann2 (n m : Nat) := match n, m with + | m, 0 => m + 1 + | 0, .succ n => ackermann2 1 n + | .succ m, .succ n => ackermann2 (ackermann2 m (n + 1)) n + +def ackermannList (n m : List Unit) := match n, m with + | [], m => () :: m + | ()::n, [] => ackermannList n [()] + | ()::n, ()::m => ackermannList n (ackermannList (()::n) m) + +def foo2 : Nat → Nat → Nat + | .succ n, 1 => foo2 n 1 + | .succ n, 2 => foo2 (.succ n) 1 + | n, 3 => foo2 (.succ n) 2 + | .succ n, 4 => foo2 (if n > 10 then n else .succ n) 3 + | n, 5 => foo2 (n - 1) 4 + | n, .succ m => foo2 n m + | _, _ => 0 + +mutual +def even : Nat → Bool + | 0 => true + | .succ n => not (odd n) +def odd : Nat → Bool + | 0 => false + | .succ n => not (even n) +end + +mutual +def evenWithFixed (m : String) : Nat → Bool + | 0 => true + | .succ n => not (oddWithFixed m n) +def oddWithFixed (m : String) : Nat → Bool + | 0 => false + | .succ n => not (evenWithFixed m n) +end + +def ping (n : Nat) := pong n + where pong : Nat → Nat + | 0 => 0 + | .succ n => ping n + +def hasForbiddenArg (n : Nat) (_h : n = n) (m : Nat) : Nat := + match n, m with + | 0, 0 => 0 + | .succ m, n => hasForbiddenArg m rfl n + | m, .succ n => hasForbiddenArg (.succ m) rfl n + +/-! +Example from “Finding Lexicographic Orders for Termination Proofs in +Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, +10.1007/978-3-540-74591-4_5 +-/ +def blowup : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat + | 0, 0, 0, 0, 0, 0, 0, 0 => 0 + | 0, 0, 0, 0, 0, 0, 0, .succ i => .succ (blowup i i i i i i i i) + | 0, 0, 0, 0, 0, 0, .succ h, i => .succ (blowup h h h h h h h i) + | 0, 0, 0, 0, 0, .succ g, h, i => .succ (blowup g g g g g g h i) + | 0, 0, 0, 0, .succ f, g, h, i => .succ (blowup f f f f f g h i) + | 0, 0, 0, .succ e, f, g, h, i => .succ (blowup e e e e f g h i) + | 0, 0, .succ d, e, f, g, h, i => .succ (blowup d d d e f g h i) + | 0, .succ c, d, e, f, g, h, i => .succ (blowup c c d e f g h i) + | .succ b, c, d, e, f, g, h, i => .succ (blowup b c d e f g h i) + +-- Let’s try to confuse the lexicographic guessing function's +-- unpacking of packed n-ary arguments +def confuseLex1 : Nat → @PSigma Nat (fun _ => Nat) → Nat + | 0, _p => 0 + | .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x,y⟩ + +def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat + | ⟨_y,0⟩ => 0 + | ⟨y,.succ n⟩ => confuseLex2 ⟨y,n⟩ + +def dependent : (n : Nat) → (m : Fin n) → Nat + | 0, i => Fin.elim0 i + | .succ 0, 0 => 0 + | .succ (.succ n), 0 => dependent (.succ n) ⟨n, n.lt_succ_self⟩ + | .succ (.succ n), ⟨.succ m, h⟩ => + dependent (.succ (.succ n)) ⟨m, Nat.lt_of_le_of_lt (Nat.le_succ _) h⟩ + + +-- An example based on a real world problem, condensed by Leo +inductive Expr where + | add (a b : Expr) + | val (n : Nat) + +mutual +def eval (a : Expr) : Nat := + match a with + | .add x y => eval_add (x, y) + | .val n => n + +def eval_add (a : Expr × Expr) : Nat := + match a with + | (x, y) => eval x + eval y +end diff --git a/tests/lean/run/guessLexTricky.lean b/tests/lean/run/guessLexTricky.lean new file mode 100644 index 000000000000..b4f4298d0a09 --- /dev/null +++ b/tests/lean/run/guessLexTricky.lean @@ -0,0 +1,51 @@ +/-! +A “tricky” example from “Finding Lexicographic Orders for Termination Proofs in +Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, +10.1007/978-3-540-74591-4_5 + +At the time of writing, Lean is able to find the lexicographic order +just fine, but only if the tactic is powerful enough. In partiuclar, +the default `decreasing_tactic` can only handle lexicographic descend when either +the left gets smaller, or the left stays equal and the right gets smaller. +But here we need to allow the general form, where the left is ≤ and the right +gets smaller. This needs a backtracking proof search, it seems, which we build here +(`search_lex`). +-/ + +macro_rules | `(tactic| decreasing_trivial) => + `(tactic| apply Nat.le_refl) +macro_rules | `(tactic| decreasing_trivial) => + `(tactic| apply Nat.succ_lt_succ; decreasing_trivial) +macro_rules | `(tactic| decreasing_trivial) => + `(tactic| apply Nat.sub_le) +macro_rules | `(tactic| decreasing_trivial) => + `(tactic| apply Nat.div_le_self) + +syntax "search_lex " tacticSeq : tactic + +macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| ( + solve + | apply Prod.Lex.right' + · $ts + · search_lex $ts + | apply Prod.Lex.left + · $ts + | $ts + )) + +-- set_option trace.Elab.definition.wf true in +mutual +def prod (x y z : Nat) : Nat := + if y % 2 = 0 then eprod x y z else oprod x y z +def oprod (x y z : Nat) := eprod x (y - 1) (z + x) +def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z +end +-- termination_by +-- prod x y z => (y, 2) +-- oprod x y z => (y, 1) +-- eprod x y z => (y, 0) +decreasing_by + simp_wf + search_lex solve + | decreasing_trivial + | apply Nat.bitwise_rec_lemma; assumption diff --git a/tests/lean/run/guessLexTricky2.lean b/tests/lean/run/guessLexTricky2.lean new file mode 100644 index 000000000000..54136a75ea4c --- /dev/null +++ b/tests/lean/run/guessLexTricky2.lean @@ -0,0 +1,23 @@ +/-! +Another “tricky” example from “Finding Lexicographic Orders for Termination Proofs in +Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, +10.1007/978-3-540-74591-4_5. + +Works out of the box! +-/ + +mutual +def pedal : Nat → Nat → Nat → Nat + | 0, _m, c => c + | _n, 0, c => c + | n+1, m+1, c => + if n < m + then coast n m (c + m + 1) + else pedal n (m + 1) (c + m + 1) + +def coast : Nat → Nat → Nat → Nat + | n, m , c => + if n < m + then coast n (m - 1) (c + n) + else pedal n m (c + n) +end From 40fcd73218463da494d6099ce7fe8b47609846db Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 23 Nov 2023 19:24:31 +0100 Subject: [PATCH 25/27] Factor out generateMeasures --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 30 +++++++++++++------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index e38699f259d6..db8db41c089b 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -459,6 +459,23 @@ where failure +/-- +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 + | throwError "Too many combinations" + + let func_measures := + if arities.size > 1 then + (List.range arities.size).toArray + else + #[] + + return arg_measures.map .args ++ func_measures.map .func + /-- The core logic of guessing the lexicographic order Given a matrix that for each call and measure indicates whether that measure is @@ -561,18 +578,9 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) let forbiddenArgs ← preDefs.mapM fun preDef => getForbiddenByTrivialSizeOf fixedPrefixSize preDef - -- Enumerate all meausures. - -- (With many functions with multiple arguments, this can explode a bit. - -- We could interleave enumerating measure with early pruning based on the recCalls, - -- once that becomes a problem. Until then, a use can always use an explicit - -- `terminating_by` annotatin.) - let some arg_measures := generateCombinations? forbiddenArgs arities - | throwError "Too many combinations" - -- The list of measures, including the measures that order functions. - -- The function ordering measures should come last - let measures : Array MutualMeasure := - arg_measures.map .args ++ (List.range varNamess.size).toArray.map .func + -- The function ordering measures come last + let measures ← generateMeasures forbiddenArgs arities match ← liftMetaM <| solve measures callMatrix with | .some solution => do From b33b52419d64edef2ef0bb05ca5ddf13d03a4124 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 24 Nov 2023 13:30:51 +0100 Subject: [PATCH 26/27] Empty commit to trigger mathlib CI From 99cb590b8a432a4622d9f286b6066cd5c3f75dab Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 24 Nov 2023 20:18:26 +0100 Subject: [PATCH 27/27] =?UTF-8?q?Let=E2=80=99s=20just=20leave=20this=20her?= =?UTF-8?q?e=20for=20now?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index db8db41c089b..f12a0bbadcfa 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -515,7 +515,6 @@ partial def solve {m} {α} [Monad m] (measures : Array α) -- None found, we have to give up return .none --- Question: Which module should have this? /-- Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton) -/