From 53af5ead5359eeb47e1c7a62381000337b5d04c0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 13 Jan 2024 19:02:41 +0100 Subject: [PATCH] fix: Fix/GuessLex: refine through more casesOnApp/matcherApp (#3176) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit there was a check if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then that would avoid going through `.refineThrough`/`.addArg` for matcher/casesOn applications. It seems it tries to detect when refining the motive/param is pointless, but it was too eager, and cause confusion with, for example, this reasonably reasonable function: def foo : (n : Nat) → (i : Fin n) → Bool | 0, _ => false | 1, _ => false | _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩ decreasing_by simp_wf; simp_arith In particular, the `GuessLex` code later expects that the (implict) `PProd.casesOn` in the implementation of `foo._unary` will refine the paramter, because else the (rather picky) `unpackArg` fails. But it also prevents this from being provable. So let's try without this shortcut. Fixing this also revealed that `withRecApps` wasn’t looking in all corners of a matcherApp/casesOnApp. Fixes #3175 --- src/Lean/Elab/PreDefinition/WF/Fix.lean | 8 +--- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 40 ++++++++++---------- tests/lean/run/issue3175.lean | 12 ++++++ tests/lean/treeMap.lean.expected.out | 6 ++- 4 files changed, 38 insertions(+), 28 deletions(-) create mode 100644 tests/lean/run/issue3175.lean diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index e52adb048ff9..c42f40dd16d4 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -79,9 +79,7 @@ where | Expr.app .. => match (← matchMatcherApp? e) with | some matcherApp => - if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then - processApp F e - else if let some matcherApp ← matcherApp.addArg? F then + if let some matcherApp ← matcherApp.addArg? F then if !(← Structural.refinedArgType matcherApp F) then processApp F e else @@ -97,9 +95,7 @@ where | none => match (← toCasesOnApp? e) with | some casesOnApp => - if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then - processApp F e - else if let some casesOnApp ← casesOnApp.addArg? F (checkIfRefined := true) then + if let some casesOnApp ← casesOnApp.addArg? F (checkIfRefined := true) then let altsNew ← (Array.zip casesOnApp.alts casesOnApp.altNumParams).mapM fun (alt, numParams) => lambdaTelescope alt fun xs altBody => do unless xs.size >= numParams do diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 4034f4519325..026aef3ee983 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -129,7 +129,7 @@ or `casesOn` application. -/ partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (param : Expr) (e : Expr) (k : Expr → Array Expr → MetaM α) : MetaM (Array α) := do - trace[Elab.definition.wf] "withRecApps: {indentExpr e}" + trace[Elab.definition.wf] "withRecApps (param {param}): {indentExpr e}" let (_, as) ← loop param e |>.run #[] |>.run' {} return as where @@ -178,27 +178,24 @@ where | Expr.app .. => match (← matchMatcherApp? e) with | some matcherApp => - if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then - processApp param e + if let some altParams ← matcherApp.refineThrough? param then + matcherApp.discrs.forM (loop param) + (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altParams)).forM + fun (alt, altNumParam, altParam) => + lambdaTelescope altParam fun xs altParam => do + -- TODO: Use boundedLambdaTelescope + unless altNumParam = xs.size do + throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" + let altBody := alt.beta xs + loop altParam altBody + matcherApp.remaining.forM (loop param) else - if let some altParams ← matcherApp.refineThrough? param then - (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altParams)).forM - fun (alt, altNumParam, altParam) => - lambdaTelescope altParam fun xs altParam => do - -- TODO: Use boundedLambdaTelescope - unless altNumParam = xs.size do - throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" - let altBody := alt.beta xs - loop altParam altBody - else - processApp param e + processApp param e | none => match (← toCasesOnApp? e) with | some casesOnApp => - if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then - processApp param e - else - if let some altParams ← casesOnApp.refineThrough? param then + if let some altParams ← casesOnApp.refineThrough? param then + loop param casesOnApp.major (Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altParams)).forM fun (alt, altNumParam, altParam) => lambdaTelescope altParam fun xs altParam => do @@ -207,8 +204,10 @@ where throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" let altBody := alt.beta xs loop altParam altBody - else - processApp param e + casesOnApp.remaining.forM (loop param) + else + trace[Elab.definition.wf] "withRecApps: casesOnApp.refineThrough? failed" + processApp param e | none => processApp param e | e => do let _ ← ensureNoRecFn recFnName e @@ -294,6 +293,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti unless args.size ≥ fixedPrefixSize + 1 do throwError "Insufficient arguments in recursive call" let arg := args[fixedPrefixSize]! + trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})" let (caller, params) ← unpackArg arities param let (callee, args) ← unpackArg arities arg RecCallWithContext.create (← getRef) caller params callee args diff --git a/tests/lean/run/issue3175.lean b/tests/lean/run/issue3175.lean new file mode 100644 index 000000000000..831aac668e59 --- /dev/null +++ b/tests/lean/run/issue3175.lean @@ -0,0 +1,12 @@ +def foo : (n : Nat) → (i : Fin n) → Bool + | 0, _ => false + | 1, _ => false + | _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩ +decreasing_by simp_wf; simp_arith + +def bar : (n : Nat) → (i : Fin n) → Bool + | 0, _ => false + | 1, _ => false + | _+2, _ => bar 1 ⟨0, Nat.zero_lt_one⟩ +termination_by n i => n +decreasing_by simp_wf; simp_arith diff --git a/tests/lean/treeMap.lean.expected.out b/tests/lean/treeMap.lean.expected.out index 793de618245f..58a4d88893e7 100644 --- a/tests/lean/treeMap.lean.expected.out +++ b/tests/lean/treeMap.lean.expected.out @@ -2,5 +2,7 @@ treeMap.lean:8:59-8:69: error: failed to prove termination, possible solutions: - Use `have`-expressions to prove the remaining goals - Use `termination_by` to specify a different well-founded relation - Use `decreasing_by` to specify your own tactic for discharging this kind of goal -t✝ t : TreeNode -⊢ sizeOf t < sizeOf t✝ +name : String +children : List TreeNode +t : TreeNode +⊢ sizeOf t < 1 + sizeOf name + sizeOf children