Lean 4.13.0

Lean FRO
2024-11-07

We're thrilled to announce Lean 4.13.0, which brings an array of improvements and new features to both the language and its tooling.

Full Changelog

Language features, tactics, and metaprograms

  • structure command

    • #5511 allows structure parents to be type synonyms.

    • #5531 allows default values for structure fields to be noncomputable.

  • rfl and apply_rfl tactics

    • #3714, #3718 improve the rfl tactic and give better error messages.

    • #3772 makes rfl no longer use kernel defeq for ground terms.

    • #5329 tags Iff.refl with @[refl] (@Parcly-Taxel)

    • #5359 ensures that the rfl tactic tries Iff.rfl (@Parcly-Taxel)

  • unfold tactic

    • #4834 let unfold do zeta-delta reduction of local definitions, incorporating functionality of the Mathlib unfold_let tactic.

  • omega tactic

  • simp tactic

    • #5479 lets simp apply rules with higher-order patterns.

  • induction tactic

    • #5494 fixes induction’s "pre-tactic" block to always be indented, avoiding unintended uses of it.

  • ac_nf tactic

    • #5524 adds ac_nf, a counterpart to ac_rfl, for normalizing expressions with respect to associativity and commutativity. Tests it with BitVec expressions.

  • bv_decide

    • #5365 adds bv_decide diagnoses for potentially spurious counterexamples.

    • #5211 makes extractLsb' the primitive bv_decide understands, rather than extractLsb (@alexkeizer)

    • #5375 adds bv_decide normalization rules for ofBool (a.getLsbD i) and ofBool a[i] (@alexkeizer)

    • #5423 enhances the rewriting rules of bv_decide

    • #5433 presents the bv_decide counterexample at the API

    • #5484 handles BitVec.ofNat with Nat fvars in bv_decide

    • #5506, #5507 add bv_normalize rules.

    • #5568 generalize the bv_normalize pipeline to support more general preprocessing passes

    • #5573 gets bv_normalize up-to-date with the current BitVec rewrites

    • Cleanups: #5408, #5493, #5578

  • Elaboration improvements

    • #5266 preserve order of overapplied arguments in elab_as_elim procedure.

    • #5510 generalizes elab_as_elim to allow arbitrary motive applications.

    • #5283, #5512 refine how named arguments suppress explicit arguments. Breaking change: some previously omitted explicit arguments may need explicit _ arguments now.

    • #5376 modifies projection instance binder info for instances, making parameters that are instance implicit in the type be implicit.

    • #5402 localizes universe metavariable errors to let bindings and fun binders if possible. Makes "cannot synthesize metavariable" errors take precedence over unsolved universe level errors.

    • #5419 must not reduce ite in the discriminant of match-expression when reducibility setting is .reducible

    • #5474 have autoparams report parameter/field on failure

    • #5530 makes automatic instance names about types with hygienic names be hygienic.

  • Deriving handlers

    • #5432 makes Repr deriving instance handle explicit type parameters

  • Functional induction

    • #5364 adds more equalities in context, more careful cleanup.

  • Linters

    • #5335 fixes the unused variables linter complaining about match/tactic combinations

    • #5337 fixes the unused variables linter complaining about some wildcard patterns

  • Other fixes

    • #4768 fixes a parse error when .. appears with a . on the next line

  • Metaprogramming

    • #3090 handles level parameters in Meta.evalExpr (@eric-wieser)

    • #5401 instance for Inhabited (TacticM α) (@alexkeizer)

    • #5412 exposes Kernel.check for debugging purposes

    • #5556 improves the "invalid projection" type inference error in inferType.

    • #5587 allows MVarId.assertHypotheses to set BinderInfo and LocalDeclKind.

    • #5588 adds MVarId.tryClearMany', a variant of MVarId.tryClearMany.

Language server, widgets, and IDE extensions

  • #5205 decreases the latency of auto-completion in tactic blocks.

  • #5237 fixes symbol occurrence highlighting in VS Code not highlighting occurrences when moving the text cursor into the identifier from the right.

  • #5257 fixes several instances of incorrect auto-completions being reported.

  • #5299 allows auto-completion to report completions for global identifiers when the elaborator fails to provide context-specific auto-completions.

  • #5312 fixes the server breaking when changing whitespace after the module header.

  • #5322 fixes several instances of auto-completion reporting non-existent namespaces.

  • #5428 makes sure to always report some recent file range as progress when waiting for elaboration.

Pretty printing

  • #4979 make pretty printer escape identifiers that are tokens.

  • #5389 makes formatter use the current token table.

  • #5513 use breakable instead of unbreakable whitespace when formatting tokens.

Library

  • #5222 reduces allocations in Json.compress.

  • #5231 upstreams Zero and NeZero

  • #5292 refactors Lean.Elab.Deriving.FromToJson (@arthur-adjedj)

  • #5415 implements Repr Empty (@TomasPuverle)

  • #5421 implements To/FromJSON Empty (@TomasPuverle)

  • Logic

    • #5263 allows simplifying dite_not/decide_not with only Decidable (¬p).

    • #5268 fixes binders on ite_eq_left_iff

    • #5284 turns off Inhabited (Sum α β) instances

    • #5355 adds simp lemmas for LawfulBEq

    • #5374 add Nonempty instances for products, allowing more partial functions to elaborate successfully

    • #5447 updates Pi instance names

    • #5454 makes some instance arguments implicit

    • #5456 adds heq_comm

    • #5529 moves @[simp] from exists_prop' to exists_prop

  • Bool

    • #5228 fills gaps in Bool lemmas

    • #5332 adds notation ^^ for Bool.xor

    • #5351 removes _root_.and (and or/not/xor) and instead exports/uses Bool.and (etc.).

  • BitVec

    • #5240 removes BitVec simps with complicated RHS

    • #5247 BitVec.getElem_zeroExtend

    • #5248 simp lemmas for BitVec, improving confluence

    • #5249 removes @[simp] from some BitVec lemmas

    • #5252 changes BitVec.intMin/Max from abbrev to def

    • #5278 adds BitVec.getElem_truncate (@tobiasgrosser)

    • #5281 adds udiv/umod bitblasting for bv_decide (@bollu)

    • #5297 BitVec unsigned order theoretic results

    • #5313 adds more basic BitVec ordering theory for UInt

    • #5314 adds toNat_sub_of_le (@bollu)

    • #5357 adds BitVec.truncate lemmas

    • #5358 introduces BitVec.setWidth to unify zeroExtend and truncate (@tobiasgrosser)

    • #5361 some BitVec GetElem lemmas

    • #5385 adds BitVec.ofBool_[and|or|xor]_ofBool theorems (@tobiasgrosser)

    • #5404 more of BitVec.getElem_* (@tobiasgrosser)

    • #5410 BitVec analogues of Nat.{mul_two, two_mul, mul_succ, succ_mul} (@bollu)

    • #5411 BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning (@bollu)

    • #5413 adds _self, _zero, and _allOnes for BitVec.[and|or|xor] (@tobiasgrosser)

    • #5416 adds LawCommIdentity + IdempotentOp for BitVec.[and|or|xor] (@tobiasgrosser)

    • #5418 decidable quantifers for BitVec

    • #5450 adds BitVec.toInt_[intMin|neg|neg_of_ne_intMin] (@tobiasgrosser)

    • #5459 missing BitVec lemmas

    • #5469 adds BitVec.[not_not, allOnes_shiftLeft_or_shiftLeft, allOnes_shiftLeft_and_shiftLeft] (@luisacicolini)

    • #5478 adds BitVec.(shiftLeft_add_distrib, shiftLeft_ushiftRight) (@luisacicolini)

    • #5487 adds sdiv_eq, smod_eq to allow sdiv/smod bitblasting (@bollu)

    • #5491 adds BitVec.toNat_[abs|sdiv|smod] (@tobiasgrosser)

    • #5492 BitVec.(not_sshiftRight, not_sshiftRight_not, getMsb_not, msb_not) (@luisacicolini)

    • #5499 BitVec.Lemmas - drop non-terminal simps (@tobiasgrosser)

    • #5505 unsimps BitVec.divRec_succ'

    • #5508 adds BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight… (@tobiasgrosser)

    • #5554 adds Bitvec.[add, sub, mul]_eq_xor and width_one_cases (@luisacicolini)

  • List

    • #5242 improve naming for List.mergeSort lemmas

    • #5302 provide mergeSort comparator autoParam

    • #5373 fix name of List.length_mergeSort

    • #5377 upstream map_mergeSort

    • #5378 modify signature of lemmas about mergeSort

    • #5245 avoid importing List.Basic without List.Impl

    • #5260 review of List API

    • #5264 review of List API

    • #5269 remove HashMap's duplicated Pairwise and Sublist

    • #5271 remove @[simp] from List.head_mem and similar

    • #5273 lemmas about List.attach

    • #5275 reverse direction of List.tail_map

    • #5277 more List.attach lemmas

    • #5285 List.count lemmas

    • #5287 use boolean predicates in List.filter

    • #5289 List.mem_ite_nil_left and analogues

    • #5293 cleanup of List.findIdx / List.take lemmas

    • #5294 switch primes on List.getElem_take

    • #5300 more List.findIdx theorems

    • #5310 fix List.all/any lemmas

    • #5311 fix List.countP lemmas

    • #5316 List.tail lemma

    • #5331 fix implicitness of List.getElem_mem

    • #5350 List.replicate lemmas

    • #5352 List.attachWith lemmas

    • #5353 List.head_mem_head?

    • #5360 lemmas about List.tail

    • #5391 review of List.erase / List.find lemmas

    • #5392 List.fold / attach lemmas

    • #5393 List.fold relators

    • #5394 lemmas about List.maximum?

    • #5403 theorems about List.toArray

    • #5405 reverse direction of List.set_map

    • #5448 add lemmas about List.IsPrefix (@Command-Master)

    • #5460 missing List.set_replicate_self

    • #5518 rename List.maximum? to max?

    • #5519 upstream List.fold lemmas

    • #5520 restore @[simp] on List.getElem_mem etc.

    • #5521 List simp fixes

    • #5550 List.unattach and simp lemmas

    • #5594 induction-friendly List.min?_cons

  • Array

    • #5246 cleanup imports of Array.Lemmas

    • #5255 split Init.Data.Array.Lemmas for better bootstrapping

    • #5288 rename Array.data to Array.toList

    • #5303 cleanup of List.getElem_append variants

    • #5304 Array.not_mem_empty

    • #5400 reorganization in Array/Basic

    • #5420 make Array functions either semireducible or use structural recursion

    • #5422 refactor DecidableEq (Array α)

    • #5452 refactor of Array

    • #5458 cleanup of Array docstrings after refactor

    • #5461 restore @[simp] on Array.swapAt!_def

    • #5465 improve Array GetElem lemmas

    • #5466 Array.foldX lemmas

    • #5472 @[simp] lemmas about List.toArray

    • #5485 reverse simp direction for toArray_concat

    • #5514 Array.eraseReps

    • #5515 upstream Array.qsortOrd

    • #5516 upstream Subarray.empty

    • #5526 fix name of Array.length_toList

    • #5527 reduce use of deprecated lemmas in Array

    • #5534 cleanup of Array GetElem lemmas

    • #5536 fix Array.modify lemmas

    • #5551 upstream Array.flatten lemmas

    • #5552 switch obvious cases of array "bang"[]! indexing to rely on hypothesis (@TomasPuverle)

    • #5577 add missing simp to Array.size_feraseIdx

    • #5586 Array/Option.unattach

  • Option

    • #5272 remove @[simp] from Option.pmap/pbind and add simp lemmas

    • #5307 restoring Option simp confluence

    • #5354 remove @[simp] from Option.bind_map

    • #5532 Option.attach

    • #5539 fix explicitness of Option.mem_toList

  • Nat

    • #5241 add @[simp] to Nat.add_eq_zero_iff

    • #5261 Nat bitwise lemmas

    • #5262 Nat.testBit_add_one should not be a global simp lemma

    • #5267 protect some Nat bitwise theorems

    • #5305 rename Nat bitwise lemmas

    • #5306 add Nat.self_sub_mod lemma

    • #5503 restore @[simp] to upstreamed Nat.lt_off_iff

  • Int

    • #5301 rename Int.div/mod to Int.tdiv/tmod

    • #5320 add ediv_nonneg_of_nonpos_of_nonpos to DivModLemmas (@sakehl)

  • Fin

    • #5250 missing lemma about Fin.ofNat'

    • #5356 Fin.ofNat' uses NeZero

    • #5379 remove some @[simp]s from Fin lemmas

    • #5380 missing Fin @[simp] lemmas

  • HashMap

    • #5244 (DHashMap|HashMap|HashSet).(getKey?|getKey|getKey!|getKeyD)

    • #5362 remove the last use of Lean.(HashSet|HashMap)

    • #5369 HashSet.ofArray

    • #5370 HashSet.partition

    • #5581 Singleton/Insert/Union instances for HashMap/Set

    • #5582 HashSet.all/any

    • #5590 adding Insert/Singleton/Union instances for HashMap/Set.Raw

    • #5591 HashSet.Raw.all/any

  • Monads

    • #5463 upstream some monad lemmas

    • #5464 adjust simp attributes on monad lemmas

    • #5522 more monadic simp lemmas

  • Simp lemma cleanup

    • #5251 remove redundant simp annotations

    • #5253 remove Int simp lemmas that can't fire

    • #5254 variables appearing on both sides of an iff should be implicit

    • #5381 cleaning up redundant simp lemmas

Compiler, runtime, and FFI

  • #4685 fixes a typo in the C run_new_frontend signature

  • #4729 has IR checker suggest using noncomputable

  • #5143 adds a shared library for Lake

  • #5437 removes (syntactically) duplicate imports (@euprunin)

  • #5462 updates src/lake/lakefile.toml to the adjusted Lake build process

  • #5541 removes new shared libs before build to better support Windows

  • #5558 make lean.h compile with MSVC (@kant2002)

  • #5564 removes non-conforming size-0 arrays (@eric-wieser)

Lake

  • Reservoir build cache. Lake will now attempt to fetch a pre-built copy of the package from Reservoir before building it. This is only enabled for packages in the leanprover or leanprover-community organizations on versions indexed by Reservoir. Users can force Lake to build packages from the source by passing --no-cache on the CLI or by setting the LAKE_NO_CACHE environment variable to true. #5486, #5572, #5583, #5600, #5641, #5642.

  • #5504 lake new and lake init now produce TOML configurations by default.

  • #5878 fixes a serious issue where Lake would delete path dependencies when attempting to cleanup a dependency required with an incorrect name.

Breaking changes

  • #5641 A Lake build of target within a package will no longer build a package's dependencies package-level extra target dependencies. At the technical level, a package's extraDep facet no longer transitively builds its dependencies’ extraDep facets (which include their extraDepTargets).

Documentation fixes

  • #3918 @[builtin_doc] attribute (@digama0)

  • #4305 explains the borrow syntax (@eric-wieser)

  • #5349 adds documentation for groupBy.loop (@vihdzp)

  • #5473 fixes typo in BitVec.mul docstring (@llllvvuu)

  • #5476 fixes typos in Lean.MetavarContext

  • #5481 removes mention of Lean.withSeconds (@alexkeizer)

  • #5497 updates documentation and tests for toUIntX functions (@TomasPuverle)

  • #5087 mentions that inferType does not ensure type correctness

  • Many fixes to spelling across the doc-strings, (@euprunin): #5425 #5426 #5427 #5430 #5431 #5434 #5435 #5436 #5438 #5439 #5440 #5599

Changes to CI

  • #5343 allows addition of release-ci label via comment (@thorimur)

  • #5344 sets check level correctly during workflow (@thorimur)

  • #5444 Mathlib's lean-pr-testing-NNNN branches should use Batteries' lean-pr-testing-NNNN branches

  • #5489 commit lake-manifest.json when updating lean-pr-testing branches

  • #5490 use separate secrets for commenting and branching in pr-release.yml