From dede354e775c28fa9272cf145295207e550be9d1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 22 Nov 2023 15:25:09 +0100 Subject: [PATCH] fix: Float RecApp out of applications (#2818) This didn't work before ``` def f (n : Nat) : Nat := match n with | 0 => 0 | n + 1 => (f) n ``` because the `RecApp` metadata marker gets in the way. More practically relevant, such code is to be produced when using `rw` or `simp` in recursive theorems (see included test case). We can fix this by preprocessing the definitions and floating the `.mdata` marker out of applications. For structural recursion, there already exists a `preprocess` function; this now also floats out `.mdata` markers. For well-founded recursion, this introduces an analogous `preprocess` function. Fixes #2810. One test case output changes: With the `.mdata` out of the way, we get a different error message. Seems fine. Alternative approaches are: * Leaving the `.mdata` marker where it is, and looking around it. Tried in #2813, but not nice (many many places where `withApp` etc. need to be adjusted). * Moving the `.mdata` _inside_ the application, so that `withApp` still works. Tried in #2814. Also not nice, the invariant that the `.mdata` is around the `.const` is tedious to maintain. --- .../PreDefinition/Structural/Preprocess.lean | 33 +++++++++++---- src/Lean/Elab/PreDefinition/WF/Main.lean | 2 + .../Elab/PreDefinition/WF/Preprocess.lean | 37 +++++++++++++++++ src/Lean/Elab/RecAppSyntax.lean | 6 +++ tests/lean/1673.lean.expected.out | 2 +- tests/lean/run/2810.lean | 41 +++++++++++++++++++ 6 files changed, 113 insertions(+), 8 deletions(-) create mode 100644 src/Lean/Elab/PreDefinition/WF/Preprocess.lean create mode 100644 tests/lean/run/2810.lean diff --git a/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean b/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean index 1b67a1c62b..7354102412 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Preprocess.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Meta.Transform +import Lean.Elab.RecAppSyntax namespace Lean.Elab.Structural open Meta @@ -15,21 +16,39 @@ private def shouldBetaReduce (e : Expr) (recFnName : Name) : Bool := false /-- - Beta reduce terms where the recursive function occurs in the lambda term. - This is useful to improve the effectiveness of `elimRecursion`. +Preprocesses the expessions to improve the effectiveness of `elimRecursion`. + +* Beta reduce terms where the recursive function occurs in the lambda term. Example: ``` def f : Nat → Nat | 0 => 1 | i+1 => (fun x => f x) i ``` + +* Floats out the RecApp markers. + Example: + ``` + def f : Nat → Nat + | 0 => 1 + | i+1 => (f x) i + ``` -/ def preprocess (e : Expr) (recFnName : Name) : CoreM Expr := Core.transform e - fun e => - if shouldBetaReduce e recFnName then - return .visit e.headBeta - else - return .continue + (pre := fun e => + if shouldBetaReduce e recFnName then + return .visit e.headBeta + else + return .continue) + (post := fun e => + match e with + | .app (.mdata m f) a => + if m.isRecApp then + return .done (.mdata m (.app f a)) + else + return .done e + | _ => return .done e) + end Lean.Elab.Structural diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean index 3b490a250d..7067c1b439 100644 --- a/src/Lean/Elab/PreDefinition/WF/Main.lean +++ b/src/Lean/Elab/PreDefinition/WF/Main.lean @@ -7,6 +7,7 @@ import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.WF.TerminationHint import Lean.Elab.PreDefinition.WF.PackDomain import Lean.Elab.PreDefinition.WF.PackMutual +import Lean.Elab.PreDefinition.WF.Preprocess import Lean.Elab.PreDefinition.WF.Rel import Lean.Elab.PreDefinition.WF.Fix import Lean.Elab.PreDefinition.WF.Eqns @@ -79,6 +80,7 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize : return false def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (decrTactic? : Option Syntax) : TermElabM Unit := do + let preDefs ← preDefs.mapM fun preDef => return { preDef with value := (← preprocess preDef.value) } let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do for preDef in preDefs do addAsAxiom preDef diff --git a/src/Lean/Elab/PreDefinition/WF/Preprocess.lean b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean new file mode 100644 index 0000000000..afcd6f7623 --- /dev/null +++ b/src/Lean/Elab/PreDefinition/WF/Preprocess.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Meta.Transform +import Lean.Elab.RecAppSyntax + +namespace Lean.Elab.WF +open Meta + +/-- +Preprocesses the expessions to improve the effectiveness of `wfRecursion`. + +* Floats out the RecApp markers. + Example: + ``` + def f : Nat → Nat + | 0 => 1 + | i+1 => (f x) i + ``` + +Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could +remove `let_fun`-lambdas that contain explicit termination proofs. +-/ +def preprocess (e : Expr) : CoreM Expr := + Core.transform e + (post := fun e => + match e with + | .app (.mdata m f) a => + if m.isRecApp then + return .done (.mdata m (.app f a)) + else + return .done e + | _ => return .done e) + +end Lean.Elab.WF diff --git a/src/Lean/Elab/RecAppSyntax.lean b/src/Lean/Elab/RecAppSyntax.lean index f482029aad..1a2ad6dda7 100644 --- a/src/Lean/Elab/RecAppSyntax.lean +++ b/src/Lean/Elab/RecAppSyntax.lean @@ -27,4 +27,10 @@ def getRecAppSyntax? (e : Expr) : Option Syntax := | _ => none | _ => none +/-- + Checks if the `MData` is for a recursive applciation. +-/ +def MData.isRecApp (d : MData) : Bool := + d.contains recAppKey + end Lean diff --git a/tests/lean/1673.lean.expected.out b/tests/lean/1673.lean.expected.out index d3cb50446e..123de0fba7 100644 --- a/tests/lean/1673.lean.expected.out +++ b/tests/lean/1673.lean.expected.out @@ -3,4 +3,4 @@ with errors structural recursion cannot be used -failed to prove termination, use `termination_by` to specify a well-founded relation +well-founded recursion cannot be used, 'foo.a' does not take any (non-fixed) arguments diff --git a/tests/lean/run/2810.lean b/tests/lean/run/2810.lean new file mode 100644 index 0000000000..59037eddc7 --- /dev/null +++ b/tests/lean/run/2810.lean @@ -0,0 +1,41 @@ +/-! +Test that parentheses don't get in the way of structural recursion. +https://github.com/leanprover/lean4/issues/2810 +-/ + +def f (n : Nat) : Nat := + match n with + | 0 => 0 + | n + 1 => (f) n + +-- with beta-reduction +def f2 (n : Nat) : Nat := + match n with + | 0 => 0 + | n + 1 => (fun n' => (f2) n') n + +-- structural recursion +def f3 (n : Nat) : Nat := + match n with + | 0 => 0 + | n + 1 => (f3) n +termination_by f3 n => n + +-- Same with rewrite + +theorem f_zero (n : Nat) : f n = 0 := by + match n with + | .zero => rfl + | .succ n => + unfold f + rewrite [f_zero] + rfl + +-- Same with simp + +theorem f_zero' (n : Nat) : f n = 0 := by + match n with + | .zero => rfl + | .succ n => + unfold f + simp only [f_zero']