Lean 4.15.0 (2025-01-04)🔗

Language

#4595 implements Simp.Config.implicitDefEqsProofs. When true (default: true), simp will not create a proof term for a rewriting rule associated with an rfl-theorem. Rewriting rules are provided by users by annotating theorems with the attribute @[simp]. If the proof of the theorem is just rfl (reflexivity), and implicitDefEqProofs := true, simp will not create a proof term which is an application of the annotated theorem.
#5429 avoid negative environment lookup
#5501 ensure instantiateMVarsProfiling adds a trace node
#5856 adds a feature to the the mutual def elaborator where the instance command yields theorems instead of definitions when the class is a Prop.
#5907 unset trailing for simpa? "try this" suggestion
#5920 changes the rule for which projections become instances. Before, all parents along with all indirect ancestors that were represented as subobject fields would have their projections become instances. Now only projections for direct parents become instances.
#5934 make all_goals admit goals on failure
#5942 introduce synthetic atoms in bv_decide
#5945 adds a new definition Message.kind which returns the top-level tag of a message. This is serialized as the new field kind in SerialMessaege so that i can be used by external consumers (e.g., Lake) to identify messages via lean --json.
#5968 arg conv tactic misreported number of arguments on error
#5979 BitVec.twoPow in bv_decide
#5991 simplifies the implementation of omega.
#5992 fix style in bv_decide normalizer
#5999 adds configuration options for decide/decide!/native_decide and refactors the tactics to be frontends to the same backend. Adds a +revert option that cleans up the local context and reverts all local variables the goal depends on, along with indirect propositional hypotheses. Makes native_decide fail at elaboration time on failure without sacrificing performance (the decision procedure is still evaluated just once). Now native_decide supports universe polymorphism.
#6010 changes bv_decide's configuration from lots of set_option to an elaborated config like simp or omega. The notable exception is sat.solver which is still a set_option such that users can configure a custom SAT solver globally for an entire project or file. Additionally it introduces the ability to set maxSteps for the simp preprocessing run through the new config.
#6012 improves the validation of new syntactic tokens. Previously, the validation code had inconsistencies: some atoms would be accepted only if they had a leading space as a pretty printer hint. Additionally, atoms with internal whitespace are no longer allowed.
#6016 removes the decide! tactic in favor of decide +kernel (breaking change).
#6019 removes @[specilize] from MkBinding.mkBinding, which is a function that cannot be specialized (as none of its arguments are functions). As a result, the specializable function Nat.foldRevM.loop doesn't get specialized, which leads to worse performing code.
#6022 makes the change tactic and conv tactic use the same elaboration strategy. It works uniformly for both the target and local hypotheses. Now change can assign metavariables, for example:

example (x y z : Nat) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`

#6024 fixes a bug where the monad lift coercion elaborator would partially unify expressions even if they were not monads. This could be taken advantage of to propagate information that could help elaboration make progress, for example the first change worked because the monad lift coercion elaborator was unifying @Eq _ _ with @Eq (Nat × Nat) p:

example (p : Nat × Nat) : p = p := by
  change _ = ⟨_, _⟩ -- used to work (yielding `p = (p.fst, p.snd)`), now it doesn't
  change ⟨_, _⟩ = _ -- never worked

As such, this is a breaking change; you may need to adjust expressions to include additional implicit arguments.

#6029 adds a normalization rule to bv_normalize (which is used by bv_decide) that converts x / 2^k into x >>> k under suitable conditions. This allows us to simplify the expensive division circuits that are used for bitblasting into much cheaper shifting circuits. Concretely, it allows for the following canonicalization:
#6030 fixes simp only [· ∈ ·] after #5020.
#6035 introduces the and flattening pre processing pass from Bitwuzla to bv_decide. It splits hypotheses of the form (a && b) = true into a = true and b = true which has synergy potential with the already existing embedded constraint substitution pass.
#6037 fixes bv_decide's embedded constraint substitution to generate correct counter examples in the corner case where duplicate theorems are in the local context.
#6045 add LEAN_ALWAYS_INLINE to some functions
#6048 fixes simp? suggesting output with invalid indentation
#6051 mark Meta.Context.config as private
#6053 fixes the caching infrastructure for whnf and isDefEq, ensuring the cache accounts for all relevant configuration flags. It also cleans up the WHNF.lean module and improves the configuration of whnf.
#6061 adds a simp_arith benchmark.
#6062 optimize Nat.Linear.Expr.toPoly
#6064 optimize Nat.Linear.Poly.norm
#6068 improves the asymptotic performance of simp_arith when there are many variables to consider.
#6077 adds options to bv_decide's configuration structure such that all non mandatory preprocessing passes can be disabled.
#6082 changes how the canonicalizer handles forall and lambda, replacing bvars with temporary fvars. Fixes a bug reported by @hrmacbeth on zulip.
#6093 use mkFreshUserName in ArgsPacker
#6096 improves the #print command for structures to show all fields and which parents the fields were inherited from, hiding internal details such as which parents are represented as subobjects. This information is still present in the constructor if needed. The pretty printer for private constants is also improved, and it now handles private names from the current module like any other name; private names from other modules are made hygienic.
#6098 modifies Lean.MVarId.replaceTargetDefEq and Lean.MVarId.replaceLocalDeclDefEq to use Expr.equal instead of Expr.eqv when determining whether the expression has changed. This is justified on the grounds that binder names and binder infos are user-visible and affect elaboration.
#6105 fixes a stack overflow caused by a cyclic assignment in the metavariable context. The cycle is unintentionally introduced by the structure instance elaborator.
#6108 turn off pp.mvars in apply? results
#6109 fixes an issue in the injection tactic. This tactic may execute multiple sub-tactics. If any of them fail, we must backtrack the partial assignment. This issue was causing the error: "mvarId is already assigned" in issue #6066. The issue is not yet resolved, as the equation generator for the match expressions is failing in the example provided in this issue.
#6112 makes stricter requirements for the @[deprecated] attribute, requiring either a replacement identifier as @[deprecated bar] or suggestion text @[deprecated "Past its use by date"], and also requires a since := "..." field.
#6114 liberalizes atom rules by allowing '' to be a prefix of an atom, after #6012 only added an exception for '' alone, and also adds some unit tests for atom validation.
#6116 fixes a bug where structural recursion did not work when indices of the recursive argument appeared as function parameters in a different order than in the argument's type's definition.
#6125 adds support for structure in mutual blocks, allowing inductive types defined by inductive and structure to be mutually recursive. The limitations are (1) that the parents in the extends clause must be defined before the mutual block and (2) mutually recursive classes are not allowed (a limitation shared by class inductive). There are also improvements to universe level inference for inductive types and structures. Breaking change: structure parents now elaborate with the structure in scope (fix: use qualified names or rename the structure to avoid shadowing), and structure parents no longer elaborate with autoimplicits enabled.
#6128 does the same fix as #6104, but such that it doesn't break the test/the file in Plausible. This is done by not creating unused let binders in metavariable types that are made by elimMVar. (This is also a positive thing for users looking at metavariable types, for example in error messages)
#6129 fixes a bug at isDefEq when zetaDelta := false. See new test for a small example that exposes the issue.
#6131 fixes a bug at the definitional equality test (isDefEq). At unification constraints of the form c.{u} =?= c.{v}, it was not trying to unfold c. This bug did not affect the kernel.
#6141 make use of recursive structures in snapshot types
#6145 fixes the revert tactic so that it creates a syntheticOpaque metavariable as the new goal, instead of a natural metavariable
#6146 fixes a non-termination bug that occurred when generating the match-expression splitter theorem. The bug was triggered when the proof automation for the splitter theorem repeatedly applied injection to the same local declaration, as it could not be removed due to forward dependencies. See issue #6065 for an example that reproduces this issue.
#6165 modifies structure instance notation and where notation to use the same notation for fields. Structure instance notation now admits binders, type ascriptions, and equations, and where notation admits full structure lvals. Examples of these for structure instance notation:

structure PosFun where
  f : Nat → Nat
  pos : ∀ n, 0 < f n

#6168 extends the "motive is not type correct" error message for the rewrite tactic to explain what it means. It also pretty prints the type-incorrect motive and reports the type error.
#6170 adds core metaprogramming functions for forking off background tasks from elaboration such that their results are visible to reporting and the language server
#6175 fixes a bug with the structure/class command where if there are parents that are not represented as subobjects but which used other parents as instances, then there would be a kernel error. Closes #2611.
#6180 fixes a non-termination bug that occurred when generating the match-expression equation theorems. The bug was triggered when the proof automation for the equation theorem repeatedly applied injection( to the same local declaration, as it could not be removed due to forward dependencies. See issue #6067 for an example that reproduces this issue.
#6189 changes how generalized field notation ("dot notation") resolves the function. The new resolution rule is that if x : S, then x.f resolves the name S.f relative to the root namespace (hence it now affected by export and open). Breaking change: aliases now resolve differently. Before, if x : S, and if S.f is an alias for S'.f, then x.f would use S'.f and look for an argument of type S'. Now, it looks for an argument of type S, which is more generally useful behavior. Code making use of the old behavior should consider defining S or S' in terms of the other, since dot notation can unfold definitions during resolution.
#6206 makes it possible to write rw (occs := [1,2]) ... instead of rw (occs := .pos [1,2]) ... by adding a coercion from List.Nat to Lean.Meta.Occurrences.
#6220 adds proper support for let_fun in simp.
#6236 fixes an issue where edits to a command containing a nested docstring fail to reparse the entire command.

Library

#4904 introduces date and time functionality to the Lean 4 Std.
#5616 is a follow-up to https://github.com/leanprover/lean4/pull/5609, where we add lemmas characterizing smtUDiv and smtSDiv's behavior when the denominator is zero.
#5866 verifies the keys function on Std.HashMap.
#5885 add Int16/Int32/Int64
#5926 add Option.or_some'
#5927 List.pmap_eq_self
#5937 upstream lemmas about Fin.foldX
#5938 upstream List.ofFn and relate to Array.ofFn
#5941 List.mapFinIdx, lemmas, relate to Array version
#5949 consolidate decide_True and decide_true_eq_true
#5950 relate Array.takeWhile with List.takeWhile
#5951 remove @[simp] from BitVec.ofFin_sub and sub_ofFin
#5952 relate Array.eraseIdx with List.eraseIdx
#5961 define ISize and basic operations on it
#5969 upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas
#5970 deprecate Array.split in favour of identical Array.partition
#5971 relate Array.isPrefixOf with List.isPrefixOf
#5972 relate Array.zipWith/zip/unzip with List versions
#5974 add another List.find?_eq_some lemma
#5981 names the default SizeOf instance instSizeOfDefault
#5982 minor lemmas about List.ofFn
#5984 adds lemmas for List for the interactions between {foldl, foldr, foldlM, foldlrM} and {filter, filterMap}.
#5985 relates the operations findSomeM?, findM?, findSome?, and find? on Array with the corresponding operations on List, and also provides simp lemmas for the Array operations findSomeRevM?, findRevM?, findSomeRev?, findRev? (in terms of reverse and the usual forward find operations).
#5987 BitVec.getMsbD in bv_decide
#5988 changes the signature of Array.set to take a Nat, and a tactic-provided bound, rather than a Fin.
#5995 BitVec.sshiftRight' in bv_decide
#6007 List.modifyTailIdx naming fix
#6008 missing @[ext] attribute on monad transformer ext lemmas
#6023 variants of List.forIn_eq_foldlM
#6025 deprecate duplicated Fin.size_pos
#6032 changes the signature of Array.get to take a Nat and a proof, rather than a Fin, for consistency with the rest of the (planned) Array API. Note that because of bootstrapping issues we can't provide get_elem_tactic as an autoparameter for the proof. As users will mostly use the xs[i] notation provided by GetElem, this hopefully isn't a problem.
#6041 modifies the order of arguments for higher-order Array functions, preferring to put the Array last (besides positional arguments with defaults). This is more consistent with the List API, and is more flexible, as dot notation allows two different partially applied versions.
#6049 adds a primitive for accessing the current thread ID
#6052 adds Array.pmap, as well as a @[csimp] lemma in terms of the no-copy Array.attachWith.
#6055 adds lemmas about for loops over Array, following the existing lemmas for List.
#6056 upstream some NameMap functions
#6060 implements conversion functions from Bool to all UIntX and IntX types.
#6070 adds the Lean.RArray data structure.
#6074 allow Sort u in Squash
#6094 adds raw transmutation of floating-point numbers to and from UInt64. Floats and UInts share the same endianness across all supported platforms. The IEEE 754 standard precisely specifies the bit layout of floats. Note that Float.toBits is distinct from Float.toUInt64, which attempts to preserve the numeric value rather than the bitwise value.
#6095 generalize List.get_mem
#6097 naming convention and NaN normalization
#6102 moves IO.rand and IO.setRandSeed to be in the BaseIO monad.
#6106 fix naming of left/right injectivity lemmas
#6111 fills in the API for Array.findSome? and Array.find?, transferring proofs from the corresponding List statements.
#6120 adds theorems BitVec.(getMsbD, msb)_(rotateLeft, rotateRight).
#6126 adds lemmas for extracting a given bit of a BitVec obtained via sub/neg/sshiftRight'/abs.
#6130 adds Lean.loadPlugin which exposes functionality similar to the lean executable's --plugin option to Lean code.
#6132 duplicates the verification API for List.attach/attachWith/pmap over to Array.
#6133 replaces Array.feraseIdx and Array.insertAt with Array.eraseIdx and Array.insertIdx, both of which take a Nat argument and a tactic-provided proof that it is in bounds. We also have eraseIdxIfInBounds and insertIdxIfInBounds which are noops if the index is out of bounds. We also provide a Fin valued version of Array.findIdx?. Together, these quite ergonomically improve the array indexing safety at a number of places in the compiler/elaborator.
#6136 fixes the run-time evaluation of (default : Float).
#6139 modifies the signature of the functions Nat.fold, Nat.foldRev, Nat.any, Nat.all, so that the function is passed the upper bound. This allows us to change runtime array bounds checks to compile time checks in many places.
#6148 adds a primitive for creating temporary directories, akin to the existing functionality for creating temporary files.
#6149 completes the elementwise accessors for ofNatLt, allOnes, and not by adding their implementations of getMsbD.
#6151 completes the toInt interface for BitVec bitwise operations.
#6154 implements BitVec.toInt_abs.
#6155 adds toNat theorems for BitVec.signExtend.
#6157 adds toInt theorems for BitVec.signExtend.
#6160 adds theorem mod_eq_sub, makes theorem sub_mul_eq_mod_of_lt_of_le not private anymore and moves its location within the rotate* section to use it in other proofs.
#6184 uses Array.findFinIdx? in preference to Array.findIdx? where it allows converting a runtime bounds check to a compile time bounds check.
#6188 completes the toNat theorems for the bitwise operations (and, or, xor, shiftLeft, shiftRight) of the UInt types and adds toBitVec theorems as well. It also renames and_toNat to toNat_and to fit with the current naming convention.
#6190 adds the builtin simproc USize.reduceToNat which reduces the USize.toNat operation on literals less than UInt32.size (i.e., 4294967296).
#6191 adds Array.zipWithAll, and the basic lemmas relating it to List.zipWithAll.
#6192 adds deprecations for Lean.HashMap functions which did not receive deprecation attributes initially.
#6193 completes the TODO in Init.Data.Array.BinSearch, removing the partial keyword and converting runtime bounds checks to compile time bounds checks.
#6194 changes the signature of Array.swap, so it takes Nat arguments with tactic provided bounds checking. It also renames Array.swap! to Array.swapIfInBounds.
#6195 renames Array.setD to Array.setIfInBounds.
#6197 upstreams the definition of Vector from Batteries, along with the basic functions.
#6200 upstreams Nat.lt_pow_self and Nat.lt_two_pow from Mathlib and uses them to prove the simp theorem Nat.mod_two_pow.
#6202 makes USize.toUInt64 a regular non-opaque definition.
#6203 adds the theorems le_usize_size and usize_size_le, which make proving inequalities about USize.size easier.
#6205 upstreams some UInt theorems from Batteries and adds more toNat-related theorems. It also adds the missing UInt8 and UInt16 to/from USize conversions so that the the interface is uniform across the UInt types.
#6207 ensures the Fin.foldl and Fin.foldr are semireducible. Without this the defeq example (f : Fin 3 → ℕ) : List.ofFn f = [f 0, f 1, f 2] := rfl was failing.
#6208 fix Vector.indexOf?
#6217 adds simp lemmas about List's == operation.
#6221 fixes:
Problems in other linux distributions that the default tzdata directory is not the same as previously defined by ensuring it with a fallback behavior when directory is missing.
Trim unnecessary characters from local time identifier.
#6222 changes the definition of HashSet.insertMany and HashSet.Raw.insertMany so that it is equivalent to repeatedly calling HashSet.insert/HashSet.Raw.insert. It also clarifies the docstrings of all the insert and insertMany functions.
#6230 copies some lemmas about List.foldX to Array.
#6233 upstreams lemmas about Vector from Batteries.
#6234 upstreams the definition and basic lemmas about List.finRange from Batteries.
#6235 relates that operations Nat.fold/foldRev/any/all to the corresponding List operations over List.finRange.
#6241 refactors Array.qsort to remove runtime array bounds checks, and avoids the use of partial. We use the Vector API, along with auto_params, to avoid having to write any proofs. The new code benchmarks indistinguishably from the old.
#6242 deprecates Fin.ofNat in favour of Fin.ofNat' (which takes an [NeZero] instance, rather than returning an element of Fin (n+1)).
#6247 adds the theorems numBits_pos, le_numBits, numBits_le , which make proving inequalities about System.Platform.numBits easier.

Compiler

#5840 changes lean_sharecommon_{eq,hash} to only consider the salient bytes of an object, and not any bytes of any unspecified/uninitialized unused capacity.
#6087 fixes a bug in the constant folding for the Nat.ble and Nat.blt function in the old code generator, leading to a miscompilation.
#6143 should make lean better-behaved around sanitizers, per https://github.com/google/sanitizers/issues/1688. As far as I can tell, https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterReturn#algorithm replaces local variables with heap allocations, and so taking the address of a local is not effective at producing a monotonic measure of stack usage.
#6209 documents under which conditions Runtime.markPersistent is unsafe and adjusts the elaborator accordingly
#6257 harden markPersistent uses

Pretty Printing

#2934 adds the option pp.parens (default: false) that causes the pretty printer to eagerly insert parentheses, which can be useful for teaching and for understanding the structure of expressions. For example, it causes p → q → r to pretty print as p → (q → r).
#6014 prevents Nat.succ ?_ from pretty printing as ?_.succ, which should make apply? be more usable.
#6085 improves the term info for coercions marked with CoeFnType.coeFun (such as DFunLike.coe in Mathlib), making "go to definition" on the function name work. Hovering over such a coerced function will show the coercee rather than the coercion expression. The coercion expression can still be seen by hovering over the whitespace in the function application.
#6096 improves the #print command for structures to show all fields and which parents the fields were inherited from, hiding internal details such as which parents are represented as subobjects. This information is still present in the constructor if needed. The pretty printer for private constants is also improved, and it now handles private names from the current module like any other name; private names from other modules are made hygienic.
#6119 adds a new delab option pp.coercions.types which, when enabled, will display all coercions with an explicit type ascription.
#6161 ensures whitespace is printed before +opt and -opt configuration options when pretty printing, improving the experience of tactics such as simp?.
#6181 fixes a bug where the signature pretty printer would ignore the current setting of pp.raw. This fixes an issue where #check ident would not heed pp.raw. Closes #6090.
#6213 exposes the difference in "synthesized type class instance is not definitionally equal" errors.

Documentation

#6009 fixes a typo in the docstring for prec and makes the text slightly more precise.
#6040 join → flatten in docstring
#6110 does some mild refactoring of the Lean.Elab.StructInst module while adding documentation.
#6144 converts 3 doc-string to module docs since it seems that this is what they were intended to be!
#6150 refine kernel code comments
#6158 adjust file reference in Data.Sum
#6239 explains the order in which Expr.abstract introduces de Bruijn indices.

Server

#5835 adds auto-completion for the fields of structure instance notation. Specifically, querying the completions via Ctrl+Space in the whitespace of a structure instance notation will now bring up the full list of fields. Whitespace structure completion can be enabled for custom syntax by wrapping the parser for the list of fields in a structInstFields parser.
#5837 fixes an old auto-completion bug where x. would issue nonsensical completions when x. could not be elaborated as a dot completion.
#5996 avoid max heartbeat error in completion
#6031 fixes a regression with go-to-definition and document highlight misbehaving on tactic blocks.
#6246 fixes a performance issue where the Lean language server would walk the full project file tree every time a file was saved, blocking the processing of all other requests and notifications and significantly increasing overall language server latency after saving.

Lake

#5684 update toolchain on lake update
#6026 adds a newline at end of each Lean file generated by lake new templates.
#6218 makes Lake no longer automatically fetch GitHub cloud releases if the package build directory is already present (mirroring the behavior of the Reservoir cache). This prevents the cache from clobbering existing prebuilt artifacts. Users can still manually fetch the cache and clobber the build directory by running lake build <pkg>:release.
#6225 makes lake build also eagerly print package materialization log lines. Previously, only a lake update performed eager logging.
#6231 improves the errors Lake produces when it fails to fetch a dependency from Reservoir. If the package is not indexed, it will produce a suggestion about how to require it from GitHub.

Other

#6137 adds support for displaying multiple threads in the trace profiler output.
#6138 fixes trace.profiler.pp not using the term pretty printer.
#6259 ensures that nesting trace nodes are annotated with timing information iff trace.profiler is active.