From 97e46d64a5594251afa8b1f6c06a8922ecc996bb Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 15 May 2025 18:58:55 -0700 Subject: [PATCH 1/7] feat: Meta.letToHave This PR adds a module for transforming `let`s to `have`s when we can detect that they are not dependent. The transformation is applied to all declarations defined using `def`/`theorem`/`instance`/`opaque`. The compiler does not seem to recognize join points that use `have` instead of `let`, so there's a hack where `let`s named `__do_jp` are preserved. We'll revisit this when the new compiler is in place. fix bugs, fix tests fix tests move letToFun to equation lemma generation, got funind to behave about the same as before make sure to run letToHave *after* abstracting proofs, add optimization to not do the transformation if there are no lets add tests file more tests better app caching, added profiling, added better error messages improve zeta tracking combinators work fix spelling in function name, use some Expr' api first step of getting `nonDep` flag to encode `have`/`let` restore letToHave on types, fix bug in mkBinder, fix tests make `have` use non-dep `letE`. implement `have` telescope `simp`. add `zetaHave` simp config. simp of `have` telescopes gets comparable performance to `letFun` version delete old code, correct the fixed handling (only the body type matters) avoid computing types in letToHave if not necessary reverting as cdecls, WF have->let for in proofs, small letToHave speedup, fix conceptual errors in simpLet, tests fix tests (was d78ba84063665ed916f2f712d88cd9cc6a843038) --- src/Lean/Elab/MutualDef.lean | 7 + src/Lean/Elab/PreDefinition/Basic.lean | 43 ++- src/Lean/Elab/PreDefinition/Main.lean | 4 +- .../PreDefinition/PartialFixpoint/Eqns.lean | 1 + .../Elab/PreDefinition/Structural/BRecOn.lean | 2 + .../Elab/PreDefinition/Structural/Eqns.lean | 2 + .../Structural/SmartUnfolding.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Fix.lean | 3 + src/Lean/Elab/PreDefinition/WF/Unfold.lean | 2 + src/Lean/Meta/Eqns.lean | 2 + src/Lean/Meta/Tactic/ElimInfo.lean | 8 +- src/Lean/Meta/Tactic/FunInd.lean | 5 + tests/lean/445.lean.expected.out | 2 +- tests/lean/funind_errors.lean.expected.out | 4 +- tests/lean/run/1026.lean | 14 +- tests/lean/run/2058.lean | 2 +- tests/lean/run/delabConst.lean | 6 +- tests/lean/run/funind_tests.lean | 4 +- tests/lean/run/funind_unfolding.lean | 8 +- tests/lean/run/issue5767.lean | 6 +- tests/lean/run/letToHave.lean | 327 ++++++++++++++++++ tests/lean/run/prefixTableStep.lean | 2 +- tests/lean/run/rflTacticErrors.lean | 2 + tests/lean/run/structInst3.lean | 4 +- tests/lean/run/structInstExtraEta.lean | 6 +- tests/lean/run/wf_preprocess.lean | 12 +- tests/lean/simp_trace.lean.expected.out | 2 +- tests/lean/unusedLet.lean.expected.out | 2 +- 28 files changed, 443 insertions(+), 41 deletions(-) diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 796d1de9b805..60abd4e74632 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1156,6 +1156,7 @@ where finishElab headers processDeriving headers elabAsync header view declId := do + assert! view.kind.isTheorem let env ← getEnv let async ← env.addConstAsync declId.declName .thm (exportedKind? := guard (!isPrivateName declId.declName) *> some .axiom) @@ -1178,6 +1179,12 @@ where s := collectLevelParams s type let scopeLevelNames ← getLevelNames let levelParams ← IO.ofExcept <| sortDeclLevelParams scopeLevelNames allUserLevelNames s.params + + let type ← if cleanup.letToHave.get (← getOptions) then + withRef header.declId <| Meta.letToHave type + else + pure type + async.commitSignature { name := header.declName, levelParams, type } -- attributes should be applied on the main thread; see below diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 9ae6132c9a72..31fd4ad2f79b 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -13,6 +13,7 @@ import Lean.Util.NumApps import Lean.Meta.AbstractNestedProofs import Lean.Meta.ForEachExpr import Lean.Meta.Eqns +import Lean.Meta.LetToHave import Lean.Elab.RecAppSyntax import Lean.Elab.DefView import Lean.Elab.PreDefinition.TerminationHint @@ -21,6 +22,11 @@ namespace Lean.Elab open Meta open Term +register_builtin_option cleanup.letToHave : Bool := { + defValue := true + descr := "Enables transforming `let`s to `have`s when elaborating a declaration." +} + /-- A (potentially recursive) definition. The elaborator converts it into Kernel definitions using many different strategies. @@ -88,6 +94,31 @@ def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : Attribu for preDef in preDefs do applyAttributesAt preDef.declName preDef.modifiers.attrs applicationTime +/-- +Applies `Meta.letToHave` to the values of defs, instances, and abbrevs. +Does not apply the transformation to values that are proofs, or to unsafe definitions. +-/ +def letToHaveValue (preDef : PreDefinition) : MetaM PreDefinition := withRef preDef.ref do + if !cleanup.letToHave.get (← getOptions) + || preDef.modifiers.isUnsafe + || preDef.kind matches .theorem | .example | .opaque then + return preDef + else if ← Meta.isProp preDef.type then + return preDef + else + let value ← Meta.letToHave preDef.value + return { preDef with value } + +/-- +Applies `Meta.letToHave` to the type of the predef. +-/ +def letToHaveType (preDef : PreDefinition) : MetaM PreDefinition := withRef preDef.ref do + if !cleanup.letToHave.get (← getOptions) || preDef.kind matches .example then + return preDef + else + let type ← Meta.letToHave preDef.type + return { preDef with type } + def abstractNestedProofs (preDef : PreDefinition) (cache := true) : MetaM PreDefinition := withRef preDef.ref do if preDef.kind.isTheorem || preDef.kind.isExample then pure preDef @@ -138,9 +169,11 @@ private def checkMeta (preDef : PreDefinition) : TermElabM Unit := do | _, _ => pure () return true -private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) : TermElabM Unit := +private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit := withRef preDef.ref do let preDef ← abstractNestedProofs (cache := cacheProofs) preDef + let preDef ← letToHaveType preDef + let preDef ← if cleanupValue then letToHaveValue preDef else pure preDef let mkDefDecl : TermElabM Declaration := return Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value @@ -185,11 +218,11 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N generateEagerEqns preDef.declName applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation -def addAndCompileNonRec (preDef : PreDefinition) (all : List Name := [preDef.declName]) : TermElabM Unit := do - addNonRecAux preDef (compile := true) (all := all) +def addAndCompileNonRec (preDef : PreDefinition) (all : List Name := [preDef.declName]) (cleanupValue := false) : TermElabM Unit := do + addNonRecAux preDef (compile := true) (all := all) (cleanupValue := cleanupValue) -def addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true) : TermElabM Unit := do - addNonRecAux preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation) (all := all) (cacheProofs := cacheProofs) +def addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation := true) (all : List Name := [preDef.declName]) (cacheProofs := true) (cleanupValue := false) : TermElabM Unit := do + addNonRecAux preDef (compile := false) (applyAttrAfterCompilation := applyAttrAfterCompilation) (all := all) (cacheProofs := cacheProofs) (cleanupValue := cleanupValue) /-- Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 7b6506cc03ba..c55ae3c05552 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -319,9 +319,9 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC let preDef ← eraseRecAppSyntax preDefs[0]! ensureEqnReservedNamesAvailable preDef.declName if preDef.modifiers.isNoncomputable then - addNonRec preDef + addNonRec preDef (cleanupValue := true) else - addAndCompileNonRec preDef + addAndCompileNonRec preDef (cleanupValue := true) preDef.termination.ensureNone "not recursive" else if preDefs.any (·.modifiers.isUnsafe) then addAndCompileUnsafe preDefs diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean index d02f8e0cecf6..dea65694ef54 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean @@ -97,6 +97,7 @@ where catch e => throwError "failed to generate unfold theorem for '{declName}':\n{e.toMessageData}" let type ← mkForallFVars xs type + let type ← letToHave type let value ← mkLambdaFVars xs goal addDecl <| Declaration.thmDecl { name, type, value diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 7831031879d3..b6961590b7dd 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -134,6 +134,8 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : withLocalDecl n c (← loop below d) fun x => do mkForallFVars #[x] (← loop below (b.instantiate1 x)) | Expr.letE n type val body nondep => + -- Turn `have`s into `let`s if they are not propositions. + let nondep ← pure nondep <&&> not <$> Meta.isProp type mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do loop below (body.instantiate1 x) | Expr.mdata d b => diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index 890cc07902b0..8f71a848021a 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -93,6 +93,7 @@ where doRealize name type := withOptions (tactic.hygienic.set · false) do let value ← mkProof info.declName type let (type, value) ← removeUnusedEqnHypotheses type value + let type ← letToHave type addDecl <| Declaration.thmDecl { name, type, value levelParams := info.levelParams @@ -126,6 +127,7 @@ where let goal ← mkFreshExprSyntheticOpaqueMVar type mkUnfoldProof declName goal.mvarId! let type ← mkForallFVars xs type + let type ← letToHave type let value ← mkLambdaFVars xs (← instantiateMVars goal) addDecl <| Declaration.thmDecl { name, type, value diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean index 215a770b6093..62a5f277adfe 100644 --- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean +++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean @@ -66,6 +66,6 @@ partial def addSmartUnfoldingDef (preDef : PreDefinition) (recArgPos : Nat) : Te else withEnableInfoTree false do let preDefSUnfold ← addSmartUnfoldingDefAux preDef recArgPos - addNonRec preDefSUnfold + addNonRec preDefSUnfold (cleanupValue := true) end Lean.Elab.Structural diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index d7ad8d3a2186..472775ce8b97 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -85,6 +85,9 @@ where withLocalDecl n c (← loop F d) fun x => do mkForallFVars #[x] (← loop F (b.instantiate1 x)) | Expr.letE n type val body nondep => + -- Convert `have`s to `let`s if they aren't propositions so that the values + -- of local declarations can be used within decreasing-by proofs. + let nondep ← pure nondep <&&> Meta.isProp type mapLetDecl n (← loop F type) (← loop F val) (nondep := nondep) (usedLetOnly := false) fun x => do loop F (body.instantiate1 x) | Expr.mdata d b => diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean index 01373ec6493c..58ae0838d233 100644 --- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean +++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean @@ -91,6 +91,7 @@ def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessPr let value ← instantiateMVars main let type ← mkForallFVars xs type + let type ← letToHave type let value ← mkLambdaFVars xs value addDecl <| Declaration.thmDecl { name, type, value @@ -123,6 +124,7 @@ def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM U let value ← instantiateMVars main let type ← mkForallFVars xs type + let type ← letToHave type let value ← mkLambdaFVars xs value addDecl <| Declaration.thmDecl { name, type, value diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index acce8162dde2..baf7d4102a10 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -10,6 +10,7 @@ import Lean.Meta.Basic import Lean.Meta.AppBuilder import Lean.Meta.Match.MatcherInfo import Lean.DefEqAttrib +import Lean.Meta.LetToHave namespace Lean.Meta @@ -178,6 +179,7 @@ where doRealize name info := do lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs let type ← mkForallFVars xs (← mkEq lhs body) + -- let type ← letToHave type let value ← mkLambdaFVars xs (← mkEqRefl lhs) addDecl <| Declaration.thmDecl { name, type, value diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index 01eedf52d9ec..bf58484b5188 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/src/Lean/Meta/Tactic/ElimInfo.lean @@ -45,10 +45,14 @@ structure ElimInfo where /-- Given the type `t` of an alternative, determines the number of parameters (.forall and .let)-bound, and whether the conclusion is a `motive`-application. -/ -def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool +partial def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool | .forallE _ _ b _ => altArity motive (n+1) b | .letE _ _ _ b _ => altArity motive (n+1) b - | conclusion => (n, conclusion.getAppFn == motive) + | conclusion => + if let some (_, _, _, b) := conclusion.letFun? then + altArity motive (n+1) b + else + (n, conclusion.getAppFn == motive) def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index 2530ef121a5a..e5ca3d0172ae 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -1057,6 +1057,7 @@ where doRealize (inductName : Name) := do let eTyp ← inferType e' let eTyp ← elimTypeAnnotations eTyp + let eTyp ← letToHave eTyp -- logInfo m!"eTyp: {eTyp}" let levelParams := (collectLevelParams {} eTyp).params -- Prune unused level parameters, preserving the original order @@ -1090,6 +1091,7 @@ def projectMutualInduct (unfolding : Bool) (names : Array Name) (mutualInduct : let value ← PProdN.projM names.size idx value mkLambdaFVars xs value let type ← inferType value + let type ← letToHave type addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value } if idx == 0 then finalizeFirstInd @@ -1248,6 +1250,7 @@ where doRealize inductName := do check value let type ← inferType value let type ← elimOptParam type + let type ← letToHave type addDecl <| Declaration.thmDecl { name := inductName, levelParams := ci.levelParams, type, value } @@ -1480,6 +1483,7 @@ where doRealize inductName := do let eTyp ← inferType e' let eTyp ← elimTypeAnnotations eTyp + let eTyp ← letToHave eTyp -- logInfo m!"eTyp: {eTyp}" let levelParams := (collectLevelParams {} eTyp).params -- Prune unused level parameters, preserving the original order @@ -1623,6 +1627,7 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do let eTyp ← inferType e' let eTyp ← elimTypeAnnotations eTyp + let eTyp ← letToHave eTyp -- logInfo m!"eTyp: {eTyp}" let levelParams := (collectLevelParams {} eTyp).params -- Prune unused level parameters, preserving the original order diff --git a/tests/lean/445.lean.expected.out b/tests/lean/445.lean.expected.out index 816015d5d61d..512da23bf880 100644 --- a/tests/lean/445.lean.expected.out +++ b/tests/lean/445.lean.expected.out @@ -11,5 +11,5 @@ i + 1 i + i * 2 i + i * r i j i + i * r i j -let z := s i j; +have z := s i j; z + z diff --git a/tests/lean/funind_errors.lean.expected.out b/tests/lean/funind_errors.lean.expected.out index d6b20de5fcc7..6e9d9f21b774 100644 --- a/tests/lean/funind_errors.lean.expected.out +++ b/tests/lean/funind_errors.lean.expected.out @@ -3,11 +3,11 @@ funind_errors.lean:22:7-22:23: error: unknown constant 'takeWhile.induct' takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop) (case1 : ∀ (i : Nat) (r : Array α) (h : i < as.size), - let a := as.get i h; + have a := as.get i h; p a = true → motive (i + 1) (r.push a) → motive i r) (case2 : ∀ (i : Nat) (r : Array α) (h : i < as.size), - let a := as.get i h; + have a := as.get i h; ¬p a = true → motive i r) (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r funind_errors.lean:38:7-38:20: error: unknown constant 'idEven.induct' diff --git a/tests/lean/run/1026.lean b/tests/lean/run/1026.lean index 995c9114c403..fd649b794fca 100644 --- a/tests/lean/run/1026.lean +++ b/tests/lean/run/1026.lean @@ -15,9 +15,21 @@ info: foo.eq_def (n : Nat) : foo n = if n = 0 then 0 else - let x := n - 1; + have x := n - 1; have this := foo._proof_4; foo x -/ #guard_msgs in #check foo.eq_def + +/-- +info: foo.eq_unfold : + foo = fun n => + if n = 0 then 0 + else + have x := n - 1; + have this := foo._proof_4; + foo x +-/ +#guard_msgs in +#check foo.eq_unfold diff --git a/tests/lean/run/2058.lean b/tests/lean/run/2058.lean index c86998069138..dc645cf234d8 100644 --- a/tests/lean/run/2058.lean +++ b/tests/lean/run/2058.lean @@ -39,7 +39,7 @@ def foo : IO Unit := do -- specializes to 0 on error /-- info: def foo : IO Unit := -let x := PUnit.unit.{0}; +have x := PUnit.unit.{0}; pure.{0, 0} Unit.unit -/ #guard_msgs in set_option pp.universes true in #print foo diff --git a/tests/lean/run/delabConst.lean b/tests/lean/run/delabConst.lean index 868a33e400f0..c6fb2bd9d361 100644 --- a/tests/lean/run/delabConst.lean +++ b/tests/lean/run/delabConst.lean @@ -141,7 +141,7 @@ def f (true : Bool) : Nat := /-- info: def MatchTest2.f : Bool → Nat := fun true => - let Bool.true := 1; + have Bool.true := 1; match true with | _root_.Bool.true => 0 | false => 1 @@ -169,8 +169,8 @@ def f (true : Bool) := /-- info: def MatchTest3.f : Bool → Bool := fun true => - let Bool.true := true; - let false := true; + have Bool.true := true; + have false := true; match true with | _root_.Bool.true => false | Bool.false => diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 59a8f0f33fbf..a8fe7d604c36 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -733,11 +733,11 @@ def foo (n : Nat) : Nat := info: Dite.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), - let j := x - 1; + have j := x - 1; j < x → motive j → motive x) (case2 : ∀ (x : Nat), - let j := x - 1; + have j := x - 1; ¬j < x → motive x) (n : Nat) : motive n -/ diff --git a/tests/lean/run/funind_unfolding.lean b/tests/lean/run/funind_unfolding.lean index c149c1c74ae3..d66d6f9294b5 100644 --- a/tests/lean/run/funind_unfolding.lean +++ b/tests/lean/run/funind_unfolding.lean @@ -57,11 +57,11 @@ def fib'' (n : Nat) : Nat := info: fib''.fun_cases_unfolding (n : Nat) (motive : Nat → Prop) (case1 : n < 2 → motive n) (case2 : ¬n < 2 → - let foo := n - 2; + have foo := n - 2; foo < 100 → motive (fib'' (n - 1) + fib'' foo)) (case3 : ¬n < 2 → - let foo := n - 2; + have foo := n - 2; ¬foo < 100 → motive 0) : motive (fib'' n) -/ @@ -381,7 +381,7 @@ info: siftDown.induct_unfolding (e : Nat) (motive : (a : Array Int) → Nat → ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), leftChild root < e → let child := leftChild root; - let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child; + have child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child; ¬a[root]! < a[child]! → motive a root h a) (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h a) (a : Array Int) (root : Nat) (h : e ≤ a.size) : motive a root h (siftDown a root e h) @@ -403,7 +403,7 @@ info: siftDown.induct (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.si ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), leftChild root < e → let child := leftChild root; - let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child; + have child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child; ¬a[root]! < a[child]! → motive a root h) (case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h) (a : Array Int) (root : Nat) (h : e ≤ a.size) : motive a root h diff --git a/tests/lean/run/issue5767.lean b/tests/lean/run/issue5767.lean index c7ced93d71f5..920b197c1741 100644 --- a/tests/lean/run/issue5767.lean +++ b/tests/lean/run/issue5767.lean @@ -24,11 +24,11 @@ def go1 (ss : Int) (st0 : St) : Bool := info: go1.induct (ss : Int) (motive : St → Prop) (case1 : ∀ (x : St), - let st1 := { m := x.m, map := x.map.insert }; + have st1 := { m := x.m, map := x.map.insert }; ∀ (val : Unit), st1.map.get? ss = some val → P st1 → P st1 → motive st1 → motive x) (case2 : ∀ (x : St), - let st1 := { m := x.m, map := x.map.insert }; + have st1 := { m := x.m, map := x.map.insert }; st1.map.get? ss = none → motive x) (st0 : St) : motive st0 -/ @@ -55,7 +55,7 @@ def go2 (ss : Int) (st0 : St) : Bool := /-- info: go2.induct : ∀ (motive : St → Prop), (∀ (x : St), - let st1 := { m := x.m, map := x.map.insert }; + have st1 := { m := x.m, map := x.map.insert }; motive st1 → motive x) → ∀ (st0 : St), motive st0 -/ diff --git a/tests/lean/run/letToHave.lean b/tests/lean/run/letToHave.lean index 9c622d3d5ac6..fc1821b13d44 100644 --- a/tests/lean/run/letToHave.lean +++ b/tests/lean/run/letToHave.lean @@ -323,3 +323,330 @@ example (h : let x := 1; x = x) : let y := 1; y = y := by let_to_have at h trace_state rfl + +/-! +## Checking the transformation applied to definitions and equation lemmas +-/ + +/-! +Non-recursive definitions have the transformation applied on the declaration itself. +-/ + +def fnNonRec (n : Nat) : let α := Nat; α := + let m := n + 1 + m +/-- +info: def fnNonRec : Nat → + have α : Type := Nat; + α := +fun n => + have m : Nat := n + 1; + m +-/ +#guard_msgs in #print fnNonRec +/-- +info: fnNonRec.eq_def (n : Nat) : + fnNonRec n = + have m : Nat := n + 1; + m +-/ +#guard_msgs in #check fnNonRec.eq_def + + +/-! +For theorems, the proof doesn't get transformed, but the type does. +-/ +theorem thm : let n := 1; n = 1 := by + let m := 1 + intro + exact Eq.refl m +/-- +info: theorem thm : have n : Nat := 1; +n = 1 := +let m : Nat := 1; +let n : Nat := 1; +Eq.refl m +-/ +#guard_msgs in #print thm + + +/-! +Structural recursion doesn't apply the transformation to the declaration value itself, +but it's done to the type and to the equation lemmas. + +The smart unfolding definition has the transformation applied to the value. +-/ + +def fnStructRec (n : Nat) : let α := Nat; α := + match n with + | 0 => 0 + | n + 1 => id (let m := n + 1; m * fnStructRec n) +/-- +info: def fnStructRec : Nat → + have α : Type := Nat; + α := +fun n => + Nat.brecOn n fun n f => + (match (motive := + (n : Nat) → + Nat.below n → + let α : Type := Nat; + α) + n with + | 0 => fun x => 0 + | n.succ => fun x => + id + (let m : Nat := n + 1; + m * x.1)) + f +-/ +#guard_msgs in #print fnStructRec +/-- +info: fnStructRec.eq_def (n : Nat) : + fnStructRec n = + match n with + | 0 => 0 + | n.succ => + id + (have m : Nat := n + 1; + m * fnStructRec n) +-/ +#guard_msgs in #check fnStructRec.eq_def +/-- info: fnStructRec.eq_1 : fnStructRec 0 = 0 -/ +#guard_msgs in #check fnStructRec.eq_1 +/-- +info: fnStructRec.eq_2 (n_2 : Nat) : + fnStructRec n_2.succ = + id + (have m : Nat := n_2 + 1; + m * fnStructRec n_2) +-/ +#guard_msgs in #check fnStructRec.eq_2 +/-- +info: def fnStructRec._sunfold : Nat → + have α : Type := Nat; + α := +fun n => + match n with + | 0 => 0 + | n.succ => + id + (have m : Nat := n + 1; + m * fnStructRec n) +-/ +#guard_msgs in #print fnStructRec._sunfold + +/-! +Smart unfolding check +-/ +open Lean Elab Command in +elab "#unfold1 " t:term : command => do + runTermElabM fun _ => do + let e ← Term.withSynthesize <| Term.elabTerm t none + let e? ← Meta.unfoldDefinition? e + logInfo m!"{e?}" +/-- info: 0 -/ +#guard_msgs in #unfold1 fnStructRec 0 +/-- +info: id + (have m : Nat := 0 + 1; + m * fnStructRec 0) +-/ +#guard_msgs in #unfold1 fnStructRec 1 +/-- +info: Nat.brecOn 1 fun n f => + (match (motive := + (n : Nat) → + Nat.below n → + let α : Type := Nat; + α) + n with + | 0 => fun x => 0 + | n.succ => fun x => + id + (let m : Nat := n + 1; + m * x.1)) + f +-/ +#guard_msgs in +set_option smartUnfolding false in +#unfold1 fnStructRec 1 + + +/-! +Well-founded recursion doesn't apply the transformation to the declaration value itself, +but it's done to the type and to the equation lemmas. +-/ + +def fnWFRec (n : Nat) : let α := Nat; α := + match n with + | 0 => 0 + | n + 1 => id (let m := n + 1; m * fnWFRec (n / 2)) +/-- +info: @[irreducible] def fnWFRec : Nat → + have α : Type := Nat; + α := +fnWFRec._proof_1.fix fun n a => + (match (motive := + (n : Nat) → + ((y : Nat) → + (invImage (fun x => x) sizeOfWFRel).1 y n → + let α : Type := Nat; + α) → + let α : Type := Nat; + α) + n with + | 0 => fun x => 0 + | n.succ => fun x => + id + (let m : Nat := n + 1; + m * x (n / 2) ⋯)) + a +-/ +#guard_msgs in #print fnWFRec +/-- +info: fnWFRec.eq_def (n : Nat) : + fnWFRec n = + match n with + | 0 => 0 + | n.succ => + id + (have m : Nat := n + 1; + m * fnWFRec (n / 2)) +-/ +#guard_msgs in #check fnWFRec.eq_def +/-- info: fnWFRec.eq_1 : fnWFRec 0 = 0 -/ +#guard_msgs in #check fnWFRec.eq_1 +/-- +info: fnWFRec.eq_2 (n_2 : Nat) : + fnWFRec n_2.succ = + id + (have m : Nat := n_2 + 1; + m * fnWFRec (n_2 / 2)) +-/ +#guard_msgs in #check fnWFRec.eq_2 + + +/-! +Partial fixedpoint doesn't apply the transformation to the declaration value itself, +but it's done to the type and to the equation lemmas. +-/ + +def fnPartialFixpoint (n : Nat) : let α := Nat; α := + fnPartialFixpoint (let m := n + 1; m) +partial_fixpoint +/-- +info: @[irreducible] def fnPartialFixpoint : Nat → + have α : Type := Nat; + α := +Lean.Order.fix + (fun f n => + f + (let m : Nat := n + 1; + m)) + fnPartialFixpoint._proof_2 +-/ +#guard_msgs in #print fnPartialFixpoint +/-- +info: fnPartialFixpoint.eq_def (n : Nat) : + fnPartialFixpoint n = + fnPartialFixpoint + (have m : Nat := n + 1; + m) +-/ +#guard_msgs in #check fnPartialFixpoint.eq_def +/-- +info: fnPartialFixpoint.eq_1 (n : Nat) : + fnPartialFixpoint n = + fnPartialFixpoint + (have m : Nat := n + 1; + m) +-/ +#guard_msgs in #check fnPartialFixpoint.eq_1 + + +/-! +Do notation, non-recursive. +Note that the pretty printed `let __do_lift`s in the following are from the `do` notation itself; +these are not `let` expressions. +-/ +open Lean in +def fnDo (x : MetaM Bool) (y : Nat → MetaM α) : MetaM (Array α) := do + let a := (← x) + if a then + let mut arr := #[] + for i in [0:10] do + let b := (← y i) + arr := arr.push b + return arr + else + return #[] +/-- +info: def fnDo : {α : Type} → Lean.MetaM Bool → (Nat → Lean.MetaM α) → Lean.MetaM (Array α) := +fun {α} x y => do + let __do_lift ← x + have a : Bool := __do_lift + if a = true then + have arr : Array α := #[]; + do + let r ← + forIn { stop := 10, step_pos := Nat.zero_lt_one } arr fun i r => + have arr : Array α := r; + do + let __do_lift ← y i + have b : α := __do_lift + have arr : Array α := arr.push b + pure PUnit.unit + pure (ForInStep.yield arr) + have arr : Array α := r + pure arr + else pure #[] +-/ +#guard_msgs in #print fnDo + + +section +/-! +Tests of cases when `letToHave` is run. +These are verifying that either it's not run, or when there are no `let`s the transformation is skipped. +-/ +set_option trace.Meta.letToHave true + +/-- +trace: [Meta.letToHave] ✅️ no `let` expressions +[Meta.letToHave] ✅️ no `let` expressions +-/ +#guard_msgs in +def fnNoLet (n : Nat) := n + +-- Not run for `example` at all. +#guard_msgs in +example (n : Nat) := n + +/-! Two times, once for `async.commitSignature`, another for `addDecl`. -/ +/-- +trace: [Meta.letToHave] ✅️ no `let` expressions +--- +trace: [Meta.letToHave] ✅️ no `let` expressions +-/ +#guard_msgs in +theorem thmNoLet : True := let x := trivial; x + +structure A where + +/-- +trace: [Meta.letToHave] ✅️ no `let` expressions +[Meta.letToHave] ✅️ transformed 1 `let` expressions into `have` expressions + [Meta.letToHave] result: + have x : Inhabited A := { default := { } }; + x +-/ +#guard_msgs in +instance : Inhabited A := let x := ⟨{}⟩; x + +/-! It's a theorem instance. Only applied to the type. -/ +/-- trace: [Meta.letToHave] ✅️ no `let` expressions -/ +#guard_msgs in +instance : Nonempty A := let x := ⟨{}⟩; x + +end diff --git a/tests/lean/run/prefixTableStep.lean b/tests/lean/run/prefixTableStep.lean index 28c16afb93a5..8959ad202dc8 100644 --- a/tests/lean/run/prefixTableStep.lean +++ b/tests/lean/run/prefixTableStep.lean @@ -27,7 +27,7 @@ info: PrefixTable.step.eq_def.{u_1} {α : Type u_1} [BEq α] (t : PrefixTable α t.step x kf = match kf with | ⟨k, hk⟩ => - let cont := fun x_1 => + have cont := fun x_1 => match k, hk with | 0, hk => ⟨0, ⋯⟩ | k.succ, hk => diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean index 750b23ca014d..b5e3c2d2d265 100644 --- a/tests/lean/run/rflTacticErrors.lean +++ b/tests/lean/run/rflTacticErrors.lean @@ -8,6 +8,8 @@ This file tests the `rfl` tactic: * Effect of `with_reducible` -/ +set_option pp.mvars.levels false + -- First, let's see what `rfl` does: /-- diff --git a/tests/lean/run/structInst3.lean b/tests/lean/run/structInst3.lean index 91d4c62f136a..966266b52b38 100644 --- a/tests/lean/run/structInst3.lean +++ b/tests/lean/run/structInst3.lean @@ -31,7 +31,7 @@ rfl /-- info: ex1 : - (let __src := c1; + (have __src := c1; { toB := __src.toB, z := 2 : C Nat }).z = 2 -/ @@ -42,7 +42,7 @@ rfl /-- info: ex2 : - (let __src := c1; + (have __src := c1; { toB := __src.toB, z := 2 : C Nat }).x = c1.x -/ diff --git a/tests/lean/run/structInstExtraEta.lean b/tests/lean/run/structInstExtraEta.lean index 4bdfc01fd2c2..d9377deda0a6 100644 --- a/tests/lean/run/structInstExtraEta.lean +++ b/tests/lean/run/structInstExtraEta.lean @@ -20,7 +20,7 @@ def a : A := ⟨ 0 ⟩ def b : B := { a with } /-- info: def b : B := -let __src := a; +have __src := a; { toA := __src } -/ #guard_msgs in #print b @@ -28,7 +28,7 @@ let __src := a; def c : C := { a with } /-- info: def c : C := -let __src := a; +have __src := a; { toB := { toA := __src } } -/ #guard_msgs in #print c @@ -36,7 +36,7 @@ let __src := a; def d : D := { c with } /-- info: def d : D := -let __src := c; +have __src := c; { toB := __src.toB } -/ #guard_msgs in #print d diff --git a/tests/lean/run/wf_preprocess.lean b/tests/lean/run/wf_preprocess.lean index 22a771d5a43a..c1d07426d484 100644 --- a/tests/lean/run/wf_preprocess.lean +++ b/tests/lean/run/wf_preprocess.lean @@ -206,23 +206,23 @@ decreasing_by info: equations: theorem MTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (t : MTree α), t.size = - (let s := 1; + (have s := 1; do let r ← forIn t.cs s fun css r => - let s := r; + have s := r; do let r ← forIn css s fun c r => - let s := r; - let s := s + c.size; + have s := r; + have s := s + c.size; do pure PUnit.unit pure (ForInStep.yield s) - let s : Nat := r + have s : Nat := r pure PUnit.unit pure (ForInStep.yield s) - let s : Nat := r + have s : Nat := r pure s).run -/ #guard_msgs in diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out index 8070fab5c776..21cc51e4d748 100644 --- a/tests/lean/simp_trace.lean.expected.out +++ b/tests/lean/simp_trace.lean.expected.out @@ -40,7 +40,7 @@ Try this: simp only [foo] ==> True Try this: simp only [g, pure] -[Meta.Tactic.simp.rewrite] unfold g, g x ==> (let x := x; +[Meta.Tactic.simp.rewrite] unfold g, g x ==> (have x := x; pure x).run Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, pure, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, set, StateT.set] diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out index 8966ef27fc23..5a54516e81f0 100644 --- a/tests/lean/unusedLet.lean.expected.out +++ b/tests/lean/unusedLet.lean.expected.out @@ -1,5 +1,5 @@ def pro : Bool := -let x := 42; +have x := 42; false def f : Nat → Nat := fun x => From bd503318e21eb2cafc9bf36ef7f13ec55d84b71f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 27 Jun 2025 09:47:30 -0700 Subject: [PATCH 2/7] re-add magical.lean --- tests/lean/run/magical.lean | 111 ++++++++++++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 tests/lean/run/magical.lean diff --git a/tests/lean/run/magical.lean b/tests/lean/run/magical.lean new file mode 100644 index 000000000000..d586e4602c73 --- /dev/null +++ b/tests/lean/run/magical.lean @@ -0,0 +1,111 @@ +import Lean +/-! +# The kernel does not allow primitive projections on propositions + +This test is adapted from the test introduced in commits +7920db952116e838b31c6f59f17bde0af01df545 and 3746005f5fc35d030d26ced2f7bcaabc295224c2, +and which was removed in #8986 because the elaborator is better at rejecting them. +In this version, we do direct tests of the kernel. +-/ + +open Lean Meta + +set_option pp.proofs true + +/-! +Projection to the witness should be rejected. + +This test is creating the declaration +``` +def test.witness : Nat := (Exists.intro 0 True.intro : ∃ x : Nat, True).1 +``` +-/ +/-- +error: (kernel) invalid projection + (Exists.intro Nat.zero True.intro).1 +-/ +#guard_msgs in +#eval do + addDecl <| .defnDecl { + name := `test.witness + levelParams := [] + type := mkConst `Nat + hints := .abbrev + safety := .safe + value := + mkProj ``Exists 0 <| + mkApp4 (mkConst ``Exists.intro [levelOne]) + (mkConst ``Nat) + (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)) + (mkConst ``Nat.zero) + (mkConst ``True.intro) + } + +/-! +`Subtype` version is accepted. (This is to check that the expression above was constructed correctly.) +-/ +#guard_msgs in +#eval do + addDecl <| .defnDecl { + name := `test.witness' + levelParams := [] + type := mkConst `Nat + hints := .abbrev + safety := .safe + value := + mkProj ``Subtype 0 <| + mkApp4 (mkConst ``Subtype.mk [levelOne]) + (mkConst ``Nat) + (mkLambda `x .default (mkConst ``Nat) (mkConst ``True)) + (mkConst ``Nat.zero) + (mkConst ``True.intro) + } + +/-! +Projection to the property should be rejected as well (it could contain the witness projection). + +This test is creating the declaration +``` +theorem test.witness_eq (h : ∃ x : Nat, True) : h.2 = h.2 := rfl +``` +-/ +/-- +error: (kernel) invalid projection + h.2 +-/ +#guard_msgs in +#eval do + addDecl <| .thmDecl { + name := `test.witness_eq + levelParams := [] + type := + mkForall `h .default + (mkApp2 (mkConst ``Exists [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True))) + (mkApp3 (mkConst ``Eq [levelZero]) + (mkConst ``True) + (mkProj ``Exists 1 (mkBVar 0)) + (mkProj ``Exists 1 (mkBVar 0))) + value := mkLambda `h .default + (mkApp2 (mkConst ``Exists [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True))) + (mkApp2 (mkConst ``Eq.refl [levelZero]) (mkConst ``True) (mkProj ``Exists 1 (mkBVar 0))) + } + +/-! +`Subtype` version is accepted. (This is to check that the expression above was constructed correctly.) +-/ +#guard_msgs in +#eval do + addDecl <| .thmDecl { + name := `test.witness_eq' + levelParams := [] + type := + mkForall `h .default + (mkApp2 (mkConst ``Subtype [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True))) + (mkApp3 (mkConst ``Eq [levelZero]) + (mkConst ``True) + (mkProj ``Subtype 1 (mkBVar 0)) + (mkProj ``Subtype 1 (mkBVar 0))) + value := mkLambda `h .default + (mkApp2 (mkConst ``Subtype [levelOne]) (mkConst ``Nat) (mkLambda `x .default (mkConst ``Nat) (mkConst ``True))) + (mkApp2 (mkConst ``Eq.refl [levelZero]) (mkConst ``True) (mkProj ``Subtype 1 (mkBVar 0))) + } From 465151e70fe2aa9515b1b75f6f85898cdf409efe Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 28 Jun 2025 14:35:20 -0700 Subject: [PATCH 3/7] self review --- src/Lean/Elab/PreDefinition/WF/Fix.lean | 3 - src/Lean/Meta/Eqns.lean | 3 +- src/Lean/Meta/Tactic/ElimInfo.lean | 8 +- tests/lean/run/letToHave.lean | 327 ---------------------- tests/lean/run/letToHaveCleanup.lean | 342 ++++++++++++++++++++++++ 5 files changed, 346 insertions(+), 337 deletions(-) create mode 100644 tests/lean/run/letToHaveCleanup.lean diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index 472775ce8b97..d7ad8d3a2186 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -85,9 +85,6 @@ where withLocalDecl n c (← loop F d) fun x => do mkForallFVars #[x] (← loop F (b.instantiate1 x)) | Expr.letE n type val body nondep => - -- Convert `have`s to `let`s if they aren't propositions so that the values - -- of local declarations can be used within decreasing-by proofs. - let nondep ← pure nondep <&&> Meta.isProp type mapLetDecl n (← loop F type) (← loop F val) (nondep := nondep) (usedLetOnly := false) fun x => do loop F (body.instantiate1 x) | Expr.mdata d b => diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index baf7d4102a10..1d296a8813b6 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -179,7 +179,8 @@ where doRealize name info := do lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs let type ← mkForallFVars xs (← mkEq lhs body) - -- let type ← letToHave type + -- Note: if this definition was added using `def`, then `letToHave` has already been applied to the body. + let type ← letToHave type let value ← mkLambdaFVars xs (← mkEqRefl lhs) addDecl <| Declaration.thmDecl { name, type, value diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index bf58484b5188..01eedf52d9ec 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/src/Lean/Meta/Tactic/ElimInfo.lean @@ -45,14 +45,10 @@ structure ElimInfo where /-- Given the type `t` of an alternative, determines the number of parameters (.forall and .let)-bound, and whether the conclusion is a `motive`-application. -/ -partial def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool +def altArity (motive : Expr) (n : Nat) : Expr → Nat × Bool | .forallE _ _ b _ => altArity motive (n+1) b | .letE _ _ _ b _ => altArity motive (n+1) b - | conclusion => - if let some (_, _, _, b) := conclusion.letFun? then - altArity motive (n+1) b - else - (n, conclusion.getAppFn == motive) + | conclusion => (n, conclusion.getAppFn == motive) def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : MetaM ElimInfo := do diff --git a/tests/lean/run/letToHave.lean b/tests/lean/run/letToHave.lean index fc1821b13d44..9c622d3d5ac6 100644 --- a/tests/lean/run/letToHave.lean +++ b/tests/lean/run/letToHave.lean @@ -323,330 +323,3 @@ example (h : let x := 1; x = x) : let y := 1; y = y := by let_to_have at h trace_state rfl - -/-! -## Checking the transformation applied to definitions and equation lemmas --/ - -/-! -Non-recursive definitions have the transformation applied on the declaration itself. --/ - -def fnNonRec (n : Nat) : let α := Nat; α := - let m := n + 1 - m -/-- -info: def fnNonRec : Nat → - have α : Type := Nat; - α := -fun n => - have m : Nat := n + 1; - m --/ -#guard_msgs in #print fnNonRec -/-- -info: fnNonRec.eq_def (n : Nat) : - fnNonRec n = - have m : Nat := n + 1; - m --/ -#guard_msgs in #check fnNonRec.eq_def - - -/-! -For theorems, the proof doesn't get transformed, but the type does. --/ -theorem thm : let n := 1; n = 1 := by - let m := 1 - intro - exact Eq.refl m -/-- -info: theorem thm : have n : Nat := 1; -n = 1 := -let m : Nat := 1; -let n : Nat := 1; -Eq.refl m --/ -#guard_msgs in #print thm - - -/-! -Structural recursion doesn't apply the transformation to the declaration value itself, -but it's done to the type and to the equation lemmas. - -The smart unfolding definition has the transformation applied to the value. --/ - -def fnStructRec (n : Nat) : let α := Nat; α := - match n with - | 0 => 0 - | n + 1 => id (let m := n + 1; m * fnStructRec n) -/-- -info: def fnStructRec : Nat → - have α : Type := Nat; - α := -fun n => - Nat.brecOn n fun n f => - (match (motive := - (n : Nat) → - Nat.below n → - let α : Type := Nat; - α) - n with - | 0 => fun x => 0 - | n.succ => fun x => - id - (let m : Nat := n + 1; - m * x.1)) - f --/ -#guard_msgs in #print fnStructRec -/-- -info: fnStructRec.eq_def (n : Nat) : - fnStructRec n = - match n with - | 0 => 0 - | n.succ => - id - (have m : Nat := n + 1; - m * fnStructRec n) --/ -#guard_msgs in #check fnStructRec.eq_def -/-- info: fnStructRec.eq_1 : fnStructRec 0 = 0 -/ -#guard_msgs in #check fnStructRec.eq_1 -/-- -info: fnStructRec.eq_2 (n_2 : Nat) : - fnStructRec n_2.succ = - id - (have m : Nat := n_2 + 1; - m * fnStructRec n_2) --/ -#guard_msgs in #check fnStructRec.eq_2 -/-- -info: def fnStructRec._sunfold : Nat → - have α : Type := Nat; - α := -fun n => - match n with - | 0 => 0 - | n.succ => - id - (have m : Nat := n + 1; - m * fnStructRec n) --/ -#guard_msgs in #print fnStructRec._sunfold - -/-! -Smart unfolding check --/ -open Lean Elab Command in -elab "#unfold1 " t:term : command => do - runTermElabM fun _ => do - let e ← Term.withSynthesize <| Term.elabTerm t none - let e? ← Meta.unfoldDefinition? e - logInfo m!"{e?}" -/-- info: 0 -/ -#guard_msgs in #unfold1 fnStructRec 0 -/-- -info: id - (have m : Nat := 0 + 1; - m * fnStructRec 0) --/ -#guard_msgs in #unfold1 fnStructRec 1 -/-- -info: Nat.brecOn 1 fun n f => - (match (motive := - (n : Nat) → - Nat.below n → - let α : Type := Nat; - α) - n with - | 0 => fun x => 0 - | n.succ => fun x => - id - (let m : Nat := n + 1; - m * x.1)) - f --/ -#guard_msgs in -set_option smartUnfolding false in -#unfold1 fnStructRec 1 - - -/-! -Well-founded recursion doesn't apply the transformation to the declaration value itself, -but it's done to the type and to the equation lemmas. --/ - -def fnWFRec (n : Nat) : let α := Nat; α := - match n with - | 0 => 0 - | n + 1 => id (let m := n + 1; m * fnWFRec (n / 2)) -/-- -info: @[irreducible] def fnWFRec : Nat → - have α : Type := Nat; - α := -fnWFRec._proof_1.fix fun n a => - (match (motive := - (n : Nat) → - ((y : Nat) → - (invImage (fun x => x) sizeOfWFRel).1 y n → - let α : Type := Nat; - α) → - let α : Type := Nat; - α) - n with - | 0 => fun x => 0 - | n.succ => fun x => - id - (let m : Nat := n + 1; - m * x (n / 2) ⋯)) - a --/ -#guard_msgs in #print fnWFRec -/-- -info: fnWFRec.eq_def (n : Nat) : - fnWFRec n = - match n with - | 0 => 0 - | n.succ => - id - (have m : Nat := n + 1; - m * fnWFRec (n / 2)) --/ -#guard_msgs in #check fnWFRec.eq_def -/-- info: fnWFRec.eq_1 : fnWFRec 0 = 0 -/ -#guard_msgs in #check fnWFRec.eq_1 -/-- -info: fnWFRec.eq_2 (n_2 : Nat) : - fnWFRec n_2.succ = - id - (have m : Nat := n_2 + 1; - m * fnWFRec (n_2 / 2)) --/ -#guard_msgs in #check fnWFRec.eq_2 - - -/-! -Partial fixedpoint doesn't apply the transformation to the declaration value itself, -but it's done to the type and to the equation lemmas. --/ - -def fnPartialFixpoint (n : Nat) : let α := Nat; α := - fnPartialFixpoint (let m := n + 1; m) -partial_fixpoint -/-- -info: @[irreducible] def fnPartialFixpoint : Nat → - have α : Type := Nat; - α := -Lean.Order.fix - (fun f n => - f - (let m : Nat := n + 1; - m)) - fnPartialFixpoint._proof_2 --/ -#guard_msgs in #print fnPartialFixpoint -/-- -info: fnPartialFixpoint.eq_def (n : Nat) : - fnPartialFixpoint n = - fnPartialFixpoint - (have m : Nat := n + 1; - m) --/ -#guard_msgs in #check fnPartialFixpoint.eq_def -/-- -info: fnPartialFixpoint.eq_1 (n : Nat) : - fnPartialFixpoint n = - fnPartialFixpoint - (have m : Nat := n + 1; - m) --/ -#guard_msgs in #check fnPartialFixpoint.eq_1 - - -/-! -Do notation, non-recursive. -Note that the pretty printed `let __do_lift`s in the following are from the `do` notation itself; -these are not `let` expressions. --/ -open Lean in -def fnDo (x : MetaM Bool) (y : Nat → MetaM α) : MetaM (Array α) := do - let a := (← x) - if a then - let mut arr := #[] - for i in [0:10] do - let b := (← y i) - arr := arr.push b - return arr - else - return #[] -/-- -info: def fnDo : {α : Type} → Lean.MetaM Bool → (Nat → Lean.MetaM α) → Lean.MetaM (Array α) := -fun {α} x y => do - let __do_lift ← x - have a : Bool := __do_lift - if a = true then - have arr : Array α := #[]; - do - let r ← - forIn { stop := 10, step_pos := Nat.zero_lt_one } arr fun i r => - have arr : Array α := r; - do - let __do_lift ← y i - have b : α := __do_lift - have arr : Array α := arr.push b - pure PUnit.unit - pure (ForInStep.yield arr) - have arr : Array α := r - pure arr - else pure #[] --/ -#guard_msgs in #print fnDo - - -section -/-! -Tests of cases when `letToHave` is run. -These are verifying that either it's not run, or when there are no `let`s the transformation is skipped. --/ -set_option trace.Meta.letToHave true - -/-- -trace: [Meta.letToHave] ✅️ no `let` expressions -[Meta.letToHave] ✅️ no `let` expressions --/ -#guard_msgs in -def fnNoLet (n : Nat) := n - --- Not run for `example` at all. -#guard_msgs in -example (n : Nat) := n - -/-! Two times, once for `async.commitSignature`, another for `addDecl`. -/ -/-- -trace: [Meta.letToHave] ✅️ no `let` expressions ---- -trace: [Meta.letToHave] ✅️ no `let` expressions --/ -#guard_msgs in -theorem thmNoLet : True := let x := trivial; x - -structure A where - -/-- -trace: [Meta.letToHave] ✅️ no `let` expressions -[Meta.letToHave] ✅️ transformed 1 `let` expressions into `have` expressions - [Meta.letToHave] result: - have x : Inhabited A := { default := { } }; - x --/ -#guard_msgs in -instance : Inhabited A := let x := ⟨{}⟩; x - -/-! It's a theorem instance. Only applied to the type. -/ -/-- trace: [Meta.letToHave] ✅️ no `let` expressions -/ -#guard_msgs in -instance : Nonempty A := let x := ⟨{}⟩; x - -end diff --git a/tests/lean/run/letToHaveCleanup.lean b/tests/lean/run/letToHaveCleanup.lean new file mode 100644 index 000000000000..dd13cf1d67c1 --- /dev/null +++ b/tests/lean/run/letToHaveCleanup.lean @@ -0,0 +1,342 @@ +import Lean +/-! +## Checking that let-to-have is applied to definitions and equation lemmas +-/ + +set_option pp.letVarTypes true +set_option pp.mvars.anonymous false + +/-! +Non-recursive definitions have the transformation applied on the declaration itself. +-/ + +def fnNonRec (n : Nat) : let α := Nat; α := + let m := n + 1 + m +/-- +info: def fnNonRec : Nat → + have α : Type := Nat; + α := +fun n => + have m : Nat := n + 1; + m +-/ +#guard_msgs in #print fnNonRec +/-- +info: fnNonRec.eq_def (n : Nat) : + fnNonRec n = + have m : Nat := n + 1; + m +-/ +#guard_msgs in #check fnNonRec.eq_def +/-- +info: fnNonRec.eq_unfold : + fnNonRec = fun n => + have m : Nat := n + 1; + m +-/ +#guard_msgs in #check fnNonRec.eq_unfold + + +/-! +For theorems, the proof doesn't get transformed, but the type does. +-/ +theorem thm : let n := 1; n = 1 := by + let m := 1 + intro + exact Eq.refl m +/-- +info: theorem thm : have n : Nat := 1; +n = 1 := +let m : Nat := 1; +let n : Nat := 1; +Eq.refl m +-/ +#guard_msgs in #print thm + + +/-! +Structural recursion doesn't apply the transformation to the declaration value itself, +but it's done to the type and to the equation lemmas. + +The smart unfolding definition has the transformation applied to the value. +-/ + +def fnStructRec (n : Nat) : let α := Nat; α := + match n with + | 0 => 0 + | n + 1 => id (let m := n + 1; m * fnStructRec n) +/-- +info: def fnStructRec : Nat → + have α : Type := Nat; + α := +fun n => + Nat.brecOn n fun n f => + (match (motive := + (n : Nat) → + Nat.below n → + let α : Type := Nat; + α) + n with + | 0 => fun x => 0 + | n.succ => fun x => + id + (let m : Nat := n + 1; + m * x.1)) + f +-/ +#guard_msgs in #print fnStructRec +/-- +info: fnStructRec.eq_def (n : Nat) : + fnStructRec n = + match n with + | 0 => 0 + | n.succ => + id + (have m : Nat := n + 1; + m * fnStructRec n) +-/ +#guard_msgs in #check fnStructRec.eq_def +/-- info: fnStructRec.eq_1 : fnStructRec 0 = 0 -/ +#guard_msgs in #check fnStructRec.eq_1 +/-- +info: fnStructRec.eq_2 (n_2 : Nat) : + fnStructRec n_2.succ = + id + (have m : Nat := n_2 + 1; + m * fnStructRec n_2) +-/ +#guard_msgs in #check fnStructRec.eq_2 +/-- +info: def fnStructRec._sunfold : Nat → + have α : Type := Nat; + α := +fun n => + match n with + | 0 => 0 + | n.succ => + id + (have m : Nat := n + 1; + m * fnStructRec n) +-/ +#guard_msgs in #print fnStructRec._sunfold + +/-! +Smart unfolding check +-/ +open Lean Elab Command in +elab "#unfold1 " t:term : command => do + runTermElabM fun _ => do + let e ← Term.withSynthesize <| Term.elabTerm t none + let e? ← Meta.unfoldDefinition? e + logInfo m!"{e?}" +/-- info: 0 -/ +#guard_msgs in #unfold1 fnStructRec 0 +/-- +info: id + (have m : Nat := 0 + 1; + m * fnStructRec 0) +-/ +#guard_msgs in #unfold1 fnStructRec 1 +/-- +info: Nat.brecOn 1 fun n f => + (match (motive := + (n : Nat) → + Nat.below n → + let α : Type := Nat; + α) + n with + | 0 => fun x => 0 + | n.succ => fun x => + id + (let m : Nat := n + 1; + m * x.1)) + f +-/ +#guard_msgs in +set_option smartUnfolding false in +#unfold1 fnStructRec 1 + + +/-! +Well-founded recursion doesn't apply the transformation to the declaration value itself, +but it's done to the type and to the equation lemmas. +-/ + +def fnWFRec (n : Nat) : let α := Nat; α := + match n with + | 0 => 0 + | n + 1 => id (let m := n + 1; m * fnWFRec (n / 2)) +/-- +info: @[irreducible] def fnWFRec : Nat → + have α : Type := Nat; + α := +fnWFRec._proof_1.fix fun n a => + (match (motive := + (n : Nat) → + ((y : Nat) → + (invImage (fun x => x) sizeOfWFRel).1 y n → + let α : Type := Nat; + α) → + let α : Type := Nat; + α) + n with + | 0 => fun x => 0 + | n.succ => fun x => + id + (let m : Nat := n + 1; + m * x (n / 2) ⋯)) + a +-/ +#guard_msgs in #print fnWFRec +/-- +info: fnWFRec.eq_def (n : Nat) : + fnWFRec n = + match n with + | 0 => 0 + | n.succ => + id + (have m : Nat := n + 1; + m * fnWFRec (n / 2)) +-/ +#guard_msgs in #check fnWFRec.eq_def +/-- info: fnWFRec.eq_1 : fnWFRec 0 = 0 -/ +#guard_msgs in #check fnWFRec.eq_1 +/-- +info: fnWFRec.eq_2 (n_2 : Nat) : + fnWFRec n_2.succ = + id + (have m : Nat := n_2 + 1; + m * fnWFRec (n_2 / 2)) +-/ +#guard_msgs in #check fnWFRec.eq_2 + + +/-! +Partial fixedpoint doesn't apply the transformation to the declaration value itself, +but it's done to the type and to the equation lemmas. +-/ + +def fnPartialFixpoint (n : Nat) : let α := Nat; α := + fnPartialFixpoint (let m := n + 1; m) +partial_fixpoint +/-- +info: @[irreducible] def fnPartialFixpoint : Nat → + have α : Type := Nat; + α := +Lean.Order.fix + (fun f n => + f + (let m : Nat := n + 1; + m)) + fnPartialFixpoint._proof_2 +-/ +#guard_msgs in #print fnPartialFixpoint +/-- +info: fnPartialFixpoint.eq_def (n : Nat) : + fnPartialFixpoint n = + fnPartialFixpoint + (have m : Nat := n + 1; + m) +-/ +#guard_msgs in #check fnPartialFixpoint.eq_def +/-- +info: fnPartialFixpoint.eq_1 (n : Nat) : + fnPartialFixpoint n = + fnPartialFixpoint + (have m : Nat := n + 1; + m) +-/ +#guard_msgs in #check fnPartialFixpoint.eq_1 + + +/-! +Do notation, non-recursive. +Note that the pretty printed `let __do_lift`s in the following are from the `do` notation itself; +these are not `let` expressions. +-/ +open Lean in +def fnDo (x : MetaM Bool) (y : Nat → MetaM α) : MetaM (Array α) := do + let a := (← x) + if a then + let mut arr := #[] + for i in [0:10] do + let b := (← y i) + arr := arr.push b + return arr + else + return #[] +/-- +info: def fnDo : {α : Type} → Lean.MetaM Bool → (Nat → Lean.MetaM α) → Lean.MetaM (Array α) := +fun {α} x y => do + let __do_lift ← x + have a : Bool := __do_lift + if a = true then + have arr : Array α := #[]; + do + let r ← + forIn { stop := 10, step_pos := Nat.zero_lt_one } arr fun i r => + have arr : Array α := r; + do + let __do_lift ← y i + have b : α := __do_lift + have arr : Array α := arr.push b + pure PUnit.unit + pure (ForInStep.yield arr) + have arr : Array α := r + pure arr + else pure #[] +-/ +#guard_msgs in #print fnDo + + +section +/-! +Tests of cases when `letToHave` is run. +These are verifying that either it's not run, or when there are no `let`s the transformation is skipped. +-/ +set_option trace.Meta.letToHave true + +/-- +trace: [Meta.letToHave] ✅️ no `let` expressions +[Meta.letToHave] ✅️ no `let` expressions +-/ +#guard_msgs in +def fnNoLet (n : Nat) := n + +-- Not run for `example` at all. +#guard_msgs in +example (n : Nat) := n + +/-! Two times, once for `async.commitSignature`, another for `addDecl`, and only on the type. -/ +/-- +trace: [Meta.letToHave] ✅️ no `let` expressions +--- +trace: [Meta.letToHave] ✅️ no `let` expressions +-/ +#guard_msgs in +theorem thmNoLet : True := let x := trivial; x +/-! With async disabled, only applied once. -/ +/-- trace: [Meta.letToHave] ✅️ no `let` expressions -/ +#guard_msgs in +set_option Elab.async false in +theorem thmNoLet' : True := let x := trivial; x + +structure A where + +/-- +trace: [Meta.letToHave] ✅️ no `let` expressions +[Meta.letToHave] ✅️ transformed 1 `let` expressions into `have` expressions + [Meta.letToHave] result: + have x : Inhabited A := { default := { } }; + x +-/ +#guard_msgs in +instance : Inhabited A := let x := ⟨{}⟩; x + +/-! It's a theorem instance. Only applied to the type. -/ +/-- trace: [Meta.letToHave] ✅️ no `let` expressions -/ +#guard_msgs in +instance : Nonempty A := let x := ⟨{}⟩; x + +end From b9efd4c9b7e6bc92f4beba94662c0f46beb17324 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 28 Jun 2025 14:36:49 -0700 Subject: [PATCH 4/7] change wording --- src/Lean/Elab/PreDefinition/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 31fd4ad2f79b..e4b131c6b24b 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -24,7 +24,7 @@ open Term register_builtin_option cleanup.letToHave : Bool := { defValue := true - descr := "Enables transforming `let`s to `have`s when elaborating a declaration." + descr := "Enables transforming `let`s to `have`s after elaborating declarations." } /-- From e9c340d9bc1ef79f5af281d822901122330fd107 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 28 Jun 2025 17:43:36 -0700 Subject: [PATCH 5/7] add withoutExporting --- src/Lean/Meta/LetToHave.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/LetToHave.lean b/src/Lean/Meta/LetToHave.lean index 2a392a56b97e..677852c5ba7d 100644 --- a/src/Lean/Meta/LetToHave.lean +++ b/src/Lean/Meta/LetToHave.lean @@ -434,7 +434,7 @@ The `Meta.letToHave` trace class logs errors and messages. def letToHave (e : Expr) : MetaM Expr := do profileitM Exception "let-to-have transformation" (← getOptions) do let e ← instantiateMVars e - LetToHave.main e + withoutExporting <| LetToHave.main e builtin_initialize registerTraceClass `Meta.letToHave From 7bb9ef9f05ecf5be6a6b8d8c71ced00a607e8ddb Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 28 Jun 2025 19:45:40 -0700 Subject: [PATCH 6/7] fix compileParserExpr --- src/Lean/ParserCompiler.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 182bc2660dda..5330b8741d45 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -37,8 +37,8 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do let reduceEval? e : MetaM (Option Name) := do try pure <| some (← reduceEval e) catch _ => pure none let e ← whnfCore e - if e matches Expr.lam .. then - lambdaLetTelescope e fun _ e => parserNodeKind? e + if e matches Expr.lam .. | Expr.letE .. then + lambdaLetTelescope (preserveNondepLet := false) e fun _ e => parserNodeKind? e else if e.isAppOfArity ``leadingNode 3 || e.isAppOfArity ``trailingNode 4 || e.isAppOfArity ``node 2 then reduceEval? (e.getArg! 0) else if e.isAppOfArity ``withAntiquot 2 then @@ -61,7 +61,7 @@ variable {α} (ctx : Context α) (builtin : Bool) (force : Bool) in partial def compileParserExpr (e : Expr) : MetaM Expr := do let e ← whnfCore e match e with - | .lam .. => mapLambdaLetTelescope e fun _ b => compileParserExpr b + | .lam .. | .letE .. => mapLambdaLetTelescope (preserveNondepLet := false) e fun _ b => compileParserExpr b | .fvar .. => return e | _ => do let fn := e.getAppFn From d9233e49d9530cf5da43c76637a43a9011b5be50 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 29 Jun 2025 10:58:21 -0700 Subject: [PATCH 7/7] remove brecon nondep reset --- src/Lean/Elab/PreDefinition/Structural/BRecOn.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index b6961590b7dd..7831031879d3 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -134,8 +134,6 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : withLocalDecl n c (← loop below d) fun x => do mkForallFVars #[x] (← loop below (b.instantiate1 x)) | Expr.letE n type val body nondep => - -- Turn `have`s into `let`s if they are not propositions. - let nondep ← pure nondep <&&> not <$> Meta.isProp type mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do loop below (body.instantiate1 x) | Expr.mdata d b =>