v4.17.0-rc1

v4.17.0-rc1

Language

• #5145 splits the environment used by the kernel from that used by the
  elaborator, providing the foundation for tracking of asynchronously
  elaborated declarations, which will exist as a concept only in the
  latter.

• #6261 adds foo.fun_cases, an automatically generated theorem that
  splits the goal according to the branching structure of foo, much like
  the Functional Induction Principle, but for all functions (not just
  recursive ones), and without providing inductive hypotheses.

• #6355 adds the ability to define possibly non-terminating functions
  and still be able to reason about them equationally, as long as they are
  tail-recursive or monadic.

• #6368 implements executing kernel checking in parallel to elaboration,
  which is a prerequisite for parallelizing elaboration itself.

• #6427 adds the Lean CLI option --src-deps which parallels --deps.
  It parses the Lean code's header and prints out the paths to the
  (transitively) imported modules' source files (deduced from
  LEAN_SRC_PATH).

• #6486 modifies the induction/cases syntax so that the with
  clause does not need to be followed by any alternatives. This improves
  friendliness of these tactics, since this lets them surface the names of
  the missing alternatives:

example (n : Nat) : True := by
  induction n with
/-            ~~~~
alternative 'zero' has not been provided
alternative 'succ' has not been provided
-/

• #6505 implements a basic async framework as well as asynchronously
  running timers using libuv.

• #6516 enhances the cases tactic used in the grind tactic and
  ensures that it can be applied to arbitrary expressions.

• #6521 adds support for activating relevant match-equations as
  E-matching theorems. It uses the match-equation lhs as the pattern.

• #6528 adds a missing propagation rule to the (WIP) grind tactic.

• #6529 adds support for let-declarations to the (WIP) grind tactic.

• #6530 fixes nondeterministic failures in the (WIP) grind tactic.

• #6531 fixes the support for let_fun in grind.

• #6533 adds support to E-matching offset patterns. For example, we want
  to be able to E-match the pattern f (#0 + 1) with term f (a + 2).

• #6534 ensures that users can utilize projections in E-matching
  patterns within the grind tactic.

• #6536 fixes different thresholds for controlling E-matching in the
  grind tactic.

• #6538 ensures patterns provided by users are normalized. See new test
  to understand why this is needed.

• #6539 introduces the [grind_eq] attribute, designed to annotate
  equational theorems and functions for heuristic instantiations in the
  grind tactic.
  When applied to an equational theorem, the [grind_eq] attribute
  instructs the grind tactic to automatically use the annotated theorem
  to instantiate patterns during proof search. If applied to a function,
  it marks all equational theorems associated with that function.

• #6543 adds additional tests for grind, demonstrating that we can
  automate some manual proofs from Mathlib's basic category theory
  library, with less reliance on Mathlib's @[reassoc] trick.

• #6545 introduces the parametric attribute [grind] for annotating
  theorems and definitions. It also replaces [grind_eq] with [grind =]. For definitions, [grind] is equivalent to [grind =].

• #6556 adds propagators for implication to the grind tactic. It also
  disables the normalization rule: (p → q) = (¬ p ∨ q)

• #6559 adds a basic case-splitting strategy for the grind tactic. We
  still need to add support for user customization.

• #6565 fixes the location of the error emitted when the rintro and
  intro tactics cannot introduce the requested number of binders.

• #6566 adds support for erasing the [grind] attribute used to mark
  theorems for heuristic instantiation in the grind tactic.

• #6567 adds support for erasing the [grind] attribute used to mark
  theorems for heuristic instantiation in the grind tactic.

• #6568 adds basic support for cast-like operators to the grind tactic.
  Example:

example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β)
        (h₁ : α = β)
        (h₂ : h₁ ▸ a₁ = b₁)
        (h₃ : a₁ = a₂)
        (h₄ : b₁ = b₂)
        : HEq a₂ b₂ := by
  grind

• #6569 adds support for case splitting on match-expressions in
  grind.
  We still need to add support for resolving the antecedents of
  match-conditional equations.

• #6575 ensures tactics are evaluated incrementally in the body of
  classical.

• #6578 fixes and improves the propagator for forall-expressions in the
  grind tactic.

• #6581 adds the following configuration options to Grind.Config:
  splitIte, splitMatch, and splitIndPred.

• #6582 adds support for creating local E-matching theorems for
  universal propositions known to be true.

• #6584 adds helper theorems to implement offset constraints in grind.

• #6585 fixes a bug in the grind canonicalizer.

• #6588 improves the grind canonicalizer diagnostics.

• #6593 adds support for the simp? and dsimp? tactics in conversion
  mode.

• #6595 improves the theorems used to justify the steps performed by the
  inequality offset module. See new test for examples of how they are
  going to be used.

• #6600 removes functions from compiling decls from Environment, and
  moves all users to functions on CoreM. This is required for supporting
  the new code generator, since its implementation uses CoreM.

• #6602 allows the dot ident notation to resolve to the current
  definition, or to any of the other definitions in the same mutual block.
  Existing code that uses dot ident notation may need to have nonrec
  added if the ident has the same name as the definition.

• #6603 implements support for offset constraints in the grind tactic.
  Several features are still missing, such as constraint propagation and
  support for offset equalities, but grind can already solve examples
  like the following:

• #6606 fixes a bug in the pattern selection in the grind.

• #6607 adds support for case-splitting on <-> (and @Eq Prop) in the
  grind tactic.

• #6608 fixes a bug in the simp_arith tactic. See new test.

• #6609 improves the case-split heuristic used in grind, prioritizing
  case-splits with fewer cases.

• #6610 fixes a bug in the grind core module responsible for merging
  equivalence classes and propagating constraints.

• #6611 fixes one of the sanity check tests used in grind.

• #6613 improves the case split heuristic used in the grind tactic,
  ensuring it now avoids unnecessary case-splits on Iff.

• #6614 improves the usability of the [grind =] attribute by
  automatically handling
  forbidden pattern symbols. For example, consider the following theorem
  tagged with this attribute:

getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]

Here, the selected pattern is xs.getLast? = some a, but Eq is a
forbidden pattern symbol.
Instead of producing an error, this function converts the pattern into a
multi-pattern,
allowing the attribute to be used conveniently.

• #6615 adds two auxiliary functions mkEqTrueCore and mkOfEqTrueCore
  that avoid redundant proof terms in proofs produced by grind.

• #6618 implements exhaustive offset constraint propagation in the
  grind tactic. This enhancement minimizes the number of case splits
  performed by grind. For instance, it can sol...

v4.16.0

v4.16.0

Highlights

Unique sorrys

#5757 makes it harder to create "fake" theorems about definitions that
are stubbed-out with sorry by ensuring that each sorry is not
definitionally equal to any other. For example, this now fails:

example : (sorry : Nat) = sorry := rfl -- fails

However, this still succeeds, since the sorry is a single
indeterminate Nat:

def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds

One can be more careful by putting parameters to the right of the colon:

def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails

Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on sorry in the Infoview, which brings you to its origin.
The option set_option pp.sorrySource true causes the pretty printer to
show source position information on sorries.

Separators in numeric literals

#6204 lets _ be used in numeric literals as a separator. For
example, 1_000_000, 0xff_ff or 0b_10_11_01_00. New lexical syntax:

numeral10 : [0-9]+ ("_"+ [0-9]+)*
numeral2  : "0" [bB] ("_"* [0-1]+)+
numeral8  : "0" [oO] ("_"* [0-7]+)+
numeral16 : "0" [xX] ("_"* hex_char+)+
float     : numeral10 "." numeral10? [eE[+-]numeral10]

Additional new featues

• #6300 adds the debug.proofAsSorry option. When enabled, the proofs
  of theorems are ignored and replaced with sorry.

• #6362 adds the --error=kind option (shorthand: -Ekind) to the
  lean CLI. When set, messages of kind (e.g.,
  linter.unusedVariables) will be reported as errors. This setting does
  nothing in interactive contexts (e.g., the server).

• #6366 adds support for Float32 and fixes a bug in the runtime.

Library updates

The Lean 4 library saw many changes that improve arithmetic reasoning, enhance data structure APIs,
and refine library organization. Key changes include better support for bitwise operations, shifts,
and conversions, expanded lemmas for Array, Vector, and List, and improved ordering definitions.
Some modules have been reorganized for clarity, and internal refinements ensure greater consistency and correctness.

Breaking changes

#6330 removes unnecessary parameters from the functional induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.

This highlights section was contributed by Violetta Sim.

For this release, 201 changes landed. In addition to the 74 feature additions and 44 fixes listed below there were 7 refactoring changes, 5 documentation improvements and 62 chores.

Language

• #3696 makes all message constructors handle pretty printer errors.

• #4460 runs all linters for a single command (together) on a separate
  thread from further elaboration, making a first step towards
  parallelizing the elaborator.

• #5757, see the highlights section above for details.

• #6123 ensures that the configuration in Simp.Config is used when
  reducing terms and checking definitional equality in simp.

• #6204, see the highlights section above for details.

• #6270 fixes a bug that could cause the injectivity tactic to fail in
  reducible mode, which could cause unfolding lemma generation to fail
  (used by tactics such as unfold). In particular,
  Lean.Meta.isConstructorApp'? was not aware that n + 1 is equivalent
  to Nat.succ n.

• #6273 modifies the "foo has been deprecated: use betterFoo instead"
  warning so that foo and betterFoo are hoverable.

• #6278 enables simp configuration options to be passed to norm_cast.

• #6286 ensure bv_decide uses definitional equality in its reflection
  procedure as much as possible. Previously it would build up explicit
  congruence proofs for the kernel to check. This reduces the size of
  proof terms passed to kernel speeds up checking of large reflection
  proofs.

• #6288 uses Lean.RArray in bv_decide's reflection proofs. Giving
  speedups on problems with lots of variables.

• #6295 sets up simprocs for all the remaining operations defined in
  Init.Data.Fin.Basic

• #6300, see the highlights section above for details.

• #6330, see the highlights section above for details.

• #6362, see the highlights section above for details.

• #6366, see the highlights section above for details.

• #6375 fixes a bug in the simplifier. It was producing terms with loose
  bound variables when eliminating unused let_fun expressions.

• #6378 adds an explanation to the error message when cases and
  induction are applied to a term whose type is not an inductive type.
  For Prop, these tactics now suggest the by_cases tactic. Example:

tactic 'cases' failed, major premise type is not an inductive type
  Prop

• #6381 fixes a bug in withTrackingZetaDelta and
  withTrackingZetaDeltaSet. The MetaM caches need to be reset. See new
  test.

• #6385 fixes a bug in simp_all? that caused some local declarations
  to be omitted from the Try this: suggestions.

• #6386 ensures that revertAll clears auxiliary declarations when
  invoked directly by users.

• #6387 fixes a type error in the proof generated by the contradiction
  tactic.

• #6397 ensures that simp and dsimp do not unfold definitions that
  are not intended to be unfolded by the user. See issue #5755 for an
  example affected by this issue.

• #6398 ensures Meta.check check projections.

• #6412 adds reserved names for congruence theorems used in the
  simplifier and grind tactics. The idea is prevent the same congruence
  theorems to be generated over and over again.

• #6413 introduces the following features to the WIP grind tactic:

• Expr internalization.
• Congruence theorem cache.
• Procedure for adding new facts
• New tracing options
• New preprocessing steps: fold projections and eliminate dangling
  Expr.mdata

• #6414 fixes a bug in Lean.Meta.Closure that would introduce
  under-applied delayed assignment metavariables, which would keep them
  from ever getting instantiated. This bug affected match elaboration
  when the expected type contained postponed elaboration problems, for
  example tactic blocks.

• #6419 fixes multiple bugs in the WIP grind tactic. It also adds
  support for printing the grind internal state.

• #6428 adds a new preprocessing step to the grind tactic:
  universe-level normalization. The goal is to avoid missing equalities in
  the congruence closure module.

• #6430 adds the predicate Expr.fvarsSet a b, which returns true if
  and only if the free variables in a are a subset of the free variables
  in b.

• #6433 adds a custom type and instance canonicalizer for the (WIP)
  grind tactic. The grind tactic uses congruence closure but
  disregards types, type formers, instances, and proofs. Proofs are
  ignored due to proof irrelevance. Types, type formers, and instances are
  considered supporting elements and are not factored into congruence
  detection. Instead, grind only checks whether elements are
  structurally equal, which, in the context of the grind tactic, is
  equivalent to pointer equality. See new tests for examples where the
  canonicalizer is important.

• #6435 implements the congruence table for the (WIP) grind tactic. It
  also fixes several bugs, and adds a new preprocessing step.

• #6437 adds support for detecting congruent terms in the (WIP) grind
  tactic. It also introduces the grind.debug option, which, when set to
  true, checks many invariants after each equivalence class is merged.
  This option is intended solely for debugging purposes.

• #6438 ensures norm_cast doesn't fail to act in the presence of
  no_index annotations

• #6441 adds basic ...

v4.16.0-rc2

v4.16.0-rc2

Language

• #3696 makes all message constructors handle pretty printer errors.

• #4460 runs all linters for a single command (together) on a separate
  thread from further elaboration, making a first step towards
  parallelizing the elaborator.

• #5757 makes it harder to create "fake" theorems about definitions that
  are stubbed-out with sorry by ensuring that each sorry is not
  definitionally equal to any other. For example, this now fails:

example : (sorry : Nat) = sorry := rfl -- fails

However, this still succeeds, since the sorry is a single
indeterminate Nat:

def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds

One can be more careful by putting parameters to the right of the colon:

def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails

Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on sorry in the Infoview, which brings you to its origin.
The option set_option pp.sorrySource true causes the pretty printer to
show source position information on sorries.

• #6123 ensures that the configuration in Simp.Config is used when
  reducing terms and checking definitional equality in simp.

• #6204 lets _ be used in numeric literals as a separator. For
  example, 1_000_000, 0xff_ff or 0b_10_11_01_00. New lexical syntax:

numeral10 : [0-9]+ ("_"+ [0-9]+)*
numeral2  : "0" [bB] ("_"* [0-1]+)+
numeral8  : "0" [oO] ("_"* [0-7]+)+
numeral16 : "0" [xX] ("_"* hex_char+)+
float     : numeral10 "." numeral10? [eE[+-]numeral10]

• #6270 fixes a bug that could cause the injectivity tactic to fail in
  reducible mode, which could cause unfolding lemma generation to fail
  (used by tactics such as unfold). In particular,
  Lean.Meta.isConstructorApp'? was not aware that n + 1 is equivalent
  to Nat.succ n.

• #6273 modifies the "foo has been deprecated: use betterFoo instead"
  warning so that foo and betterFoo are hoverable.

• #6278 enables simp configuration options to be passed to norm_cast.

• #6286 ensure bv_decide uses definitional equality in its reflection
  procedure as much as possible. Previously it would build up explicit
  congruence proofs for the kernel to check. This reduces the size of
  proof terms passed to kernel speeds up checking of large reflection
  proofs.

• #6288 uses Lean.RArray in bv_decide's reflection proofs. Giving
  speedups on problems with lots of variables.

• #6295 sets up simprocs for all the remaining operations defined in
  Init.Data.Fin.Basic

• #6300 adds the debug.proofAsSorry option. When enabled, the proofs
  of theorems are ignored and replaced with sorry.

• #6330 removes unnecessary parameters from the funcion induction
  principles. This is a breaking change; broken code can typically be adjusted
  simply by passing fewer parameters.

• #6330 removes unnecessary parameters from the funcion induction
  principles. This is a breaking change; broken code can typically be adjusted
  simply by passing fewer parameters.

• #6362 adds the --error=kind option (shorthand: -Ekind) to the
  lean CLI. When set, messages of kind (e.g.,
  linter.unusedVariables) will be reported as errors. This setting does
  nothing in interactive contexts (e.g., the server).

• #6366 adds support for Float32 and fixes a bug in the runtime.

• #6375 fixes a bug in the simplifier. It was producing terms with loose
  bound variables when eliminating unused let_fun expressions.

• #6378 adds an explanation to the error message when cases and
  induction are applied to a term whose type is not an inductive type.
  For Prop, these tactics now suggest the by_cases tactic. Example:

tactic 'cases' failed, major premise type is not an inductive type
  Prop

• #6381 fixes a bug in withTrackingZetaDelta and
  withTrackingZetaDeltaSet. The MetaM caches need to be reset. See new
  test.

• #6385 fixes a bug in simp_all? that caused some local declarations
  to be omitted from the Try this: suggestions.

• #6386 ensures that revertAll clears auxiliary declarations when
  invoked directly by users.

• #6387 fixes a type error in the proof generated by the contradiction
  tactic.

• #6397 ensures that simp and dsimp do not unfold definitions that
  are not intended to be unfolded by the user. See issue #5755 for an
  example affected by this issue.

• #6398 ensures Meta.check check projections.

• #6412 adds reserved names for congruence theorems used in the
  simplifier and grind tactics. The idea is prevent the same congruence
  theorems to be generated over and over again.

• #6413 introduces the following features to the WIP grind tactic:

• Expr internalization.
• Congruence theorem cache.
• Procedure for adding new facts
• New tracing options
• New preprocessing steps: fold projections and eliminate dangling
  Expr.mdata

• #6414 fixes a bug in Lean.Meta.Closure that would introduce
  under-applied delayed assignment metavariables, which would keep them
  from ever getting instantiated. This bug affected match elaboration
  when the expected type contained postponed elaboration problems, for
  example tactic blocks.

• #6419 fixes multiple bugs in the WIP grind tactic. It also adds
  support for printing the grind internal state.

• #6428 adds a new preprocessing step to the grind tactic:
  universe-level normalization. The goal is to avoid missing equalities in
  the congruence closure module.

• #6430 adds the predicate Expr.fvarsSet a b, which returns true if
  and only if the free variables in a are a subset of the free variables
  in b.

• #6433 adds a custom type and instance canonicalizer for the (WIP)
  grind tactic. The grind tactic uses congruence closure but
  disregards types, type formers, instances, and proofs. Proofs are
  ignored due to proof irrelevance. Types, type formers, and instances are
  considered supporting elements and are not factored into congruence
  detection. Instead, grind only checks whether elements are
  structurally equal, which, in the context of the grind tactic, is
  equivalent to pointer equality. See new tests for examples where the
  canonicalizer is important.

• #6435 implements the congruence table for the (WIP) grind tactic. It
  also fixes several bugs, and adds a new preprocessing step.

• #6437 adds support for detecting congruent terms in the (WIP) grind
  tactic. It also introduces the grind.debug option, which, when set to
  true, checks many invariants after each equivalence class is merged.
  This option is intended solely for debugging purposes.

• #6438 ensures norm_cast doesn't fail to act in the presence of
  no_index annotations

• #6441 adds basic truth value propagation rules to the (WIP) grind
  tactic.

• #6442 fixes the checkParents sanity check in grind.

• #6443 adds support for propagating the truth value of equalities in
  the (WIP) grind tactic.

• #6447 refactors grind and adds support for invoking the simplifier
  using the GrindM monad.

• #6448 declares the command builtin_grind_propagator for registering
  equation propagator for grind. It also declares the auxiliary the
  attribute.

• #6449 completes the implementation of the command
  builtin_grind_propagator.

• #6452 adds support for generating (small) proofs for any two
  expressions that belong to the same equivalence class in the grind
  tactic state.

• #6453 improves bv_decide's performance in the presence of large
  literals.

• #6455 fixes a bug in the equality...

v4.16.0-rc1

v4.16.0-rc1

Language

• #3696 makes all message constructors handle pretty printer errors.

• #4460 runs all linters for a single command (together) on a separate
  thread from further elaboration, making a first step towards
  parallelizing the elaborator.

• #5757 makes it harder to create "fake" theorems about definitions that
  are stubbed-out with sorry by ensuring that each sorry is not
  definitionally equal to any other. For example, this now fails:

example : (sorry : Nat) = sorry := rfl -- fails

However, this still succeeds, since the sorry is a single
indeterminate Nat:

def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds

One can be more careful by putting parameters to the right of the colon:

def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails

Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on sorry in the Infoview, which brings you to its origin.
The option set_option pp.sorrySource true causes the pretty printer to
show source position information on sorries.

• #6123 ensures that the configuration in Simp.Config is used when
  reducing terms and checking definitional equality in simp.

• #6204 lets _ be used in numeric literals as a separator. For
  example, 1_000_000, 0xff_ff or 0b_10_11_01_00. New lexical syntax:

numeral10 : [0-9]+ ("_"+ [0-9]+)*
numeral2  : "0" [bB] ("_"* [0-1]+)+
numeral8  : "0" [oO] ("_"* [0-7]+)+
numeral16 : "0" [xX] ("_"* hex_char+)+
float     : numeral10 "." numeral10? [eE[+-]numeral10]

• #6270 fixes a bug that could cause the injectivity tactic to fail in
  reducible mode, which could cause unfolding lemma generation to fail
  (used by tactics such as unfold). In particular,
  Lean.Meta.isConstructorApp'? was not aware that n + 1 is equivalent
  to Nat.succ n.

• #6273 modifies the "foo has been deprecated: use betterFoo instead"
  warning so that foo and betterFoo are hoverable.

• #6278 enables simp configuration options to be passed to norm_cast.

• #6286 ensure bv_decide uses definitional equality in its reflection
  procedure as much as possible. Previously it would build up explicit
  congruence proofs for the kernel to check. This reduces the size of
  proof terms passed to kernel speeds up checking of large reflection
  proofs.

• #6288 uses Lean.RArray in bv_decide's reflection proofs. Giving
  speedups on problems with lots of variables.

• #6295 sets up simprocs for all the remaining operations defined in
  Init.Data.Fin.Basic

• #6300 adds the debug.proofAsSorry option. When enabled, the proofs
  of theorems are ignored and replaced with sorry.

• #6330 removes unnecessary parameters from the funcion induction
  principles. This is a breaking change; broken code can typically be adjusted
  simply by passing fewer parameters.

• #6330 removes unnecessary parameters from the funcion induction
  principles. This is a breaking change; broken code can typically be adjusted
  simply by passing fewer parameters.

• #6362 adds the --error=kind option (shorthand: -Ekind) to the
  lean CLI. When set, messages of kind (e.g.,
  linter.unusedVariables) will be reported as errors. This setting does
  nothing in interactive contexts (e.g., the server).

• #6366 adds support for Float32 and fixes a bug in the runtime.

• #6375 fixes a bug in the simplifier. It was producing terms with loose
  bound variables when eliminating unused let_fun expressions.

• #6378 adds an explanation to the error message when cases and
  induction are applied to a term whose type is not an inductive type.
  For Prop, these tactics now suggest the by_cases tactic. Example:

tactic 'cases' failed, major premise type is not an inductive type
  Prop

• #6381 fixes a bug in withTrackingZetaDelta and
  withTrackingZetaDeltaSet. The MetaM caches need to be reset. See new
  test.

• #6385 fixes a bug in simp_all? that caused some local declarations
  to be omitted from the Try this: suggestions.

• #6386 ensures that revertAll clears auxiliary declarations when
  invoked directly by users.

• #6387 fixes a type error in the proof generated by the contradiction
  tactic.

• #6397 ensures that simp and dsimp do not unfold definitions that
  are not intended to be unfolded by the user. See issue #5755 for an
  example affected by this issue.

• #6398 ensures Meta.check check projections.

• #6412 adds reserved names for congruence theorems used in the
  simplifier and grind tactics. The idea is prevent the same congruence
  theorems to be generated over and over again.

• #6413 introduces the following features to the WIP grind tactic:

• Expr internalization.
• Congruence theorem cache.
• Procedure for adding new facts
• New tracing options
• New preprocessing steps: fold projections and eliminate dangling
  Expr.mdata

• #6414 fixes a bug in Lean.Meta.Closure that would introduce
  under-applied delayed assignment metavariables, which would keep them
  from ever getting instantiated. This bug affected match elaboration
  when the expected type contained postponed elaboration problems, for
  example tactic blocks.

• #6419 fixes multiple bugs in the WIP grind tactic. It also adds
  support for printing the grind internal state.

• #6428 adds a new preprocessing step to the grind tactic:
  universe-level normalization. The goal is to avoid missing equalities in
  the congruence closure module.

• #6430 adds the predicate Expr.fvarsSet a b, which returns true if
  and only if the free variables in a are a subset of the free variables
  in b.

• #6433 adds a custom type and instance canonicalizer for the (WIP)
  grind tactic. The grind tactic uses congruence closure but
  disregards types, type formers, instances, and proofs. Proofs are
  ignored due to proof irrelevance. Types, type formers, and instances are
  considered supporting elements and are not factored into congruence
  detection. Instead, grind only checks whether elements are
  structurally equal, which, in the context of the grind tactic, is
  equivalent to pointer equality. See new tests for examples where the
  canonicalizer is important.

• #6435 implements the congruence table for the (WIP) grind tactic. It
  also fixes several bugs, and adds a new preprocessing step.

• #6437 adds support for detecting congruent terms in the (WIP) grind
  tactic. It also introduces the grind.debug option, which, when set to
  true, checks many invariants after each equivalence class is merged.
  This option is intended solely for debugging purposes.

• #6438 ensures norm_cast doesn't fail to act in the presence of
  no_index annotations

• #6441 adds basic truth value propagation rules to the (WIP) grind
  tactic.

• #6442 fixes the checkParents sanity check in grind.

• #6443 adds support for propagating the truth value of equalities in
  the (WIP) grind tactic.

• #6447 refactors grind and adds support for invoking the simplifier
  using the GrindM monad.

• #6448 declares the command builtin_grind_propagator for registering
  equation propagator for grind. It also declares the auxiliary the
  attribute.

• #6449 completes the implementation of the command
  builtin_grind_propagator.

• #6452 adds support for generating (small) proofs for any two
  expressions that belong to the same equivalence class in the grind
  tactic state.

• #6453 improves bv_decide's performance in the presence of large
  literals.

• #6455 fixes a bug in the equality...

v4.15.0

v4.15.0

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 structu...

v4.15.0-rc1

What's Changed

• chore: begin development cycle for v4.15 by @kim-em in #5936
• chore: upstream lemmas about Fin.foldX by @kim-em in #5937
• chore: upstream List.ofFn and relate to Array.ofFn by @kim-em in #5938
• feat: List.mapFinIdx, lemmas, relate to Array version by @kim-em in #5941
• feat: introduce synthetic atoms in bv_decide by @hargoniX in #5942
• feat: add Int16/Int32/Int64 by @hargoniX in #5885
• feat: update toolchain on lake update by @tydeu in #5684
• fix: make all_goals admit goals on failure by @kmill in #5934
• chore: port release notes for v4.13.0 to master by @kim-em in #5947
• feat: List.pmap_eq_self by @vihdzp in #5927
• feat: add Option.or_some' by @vihdzp in #5926
• chore: remove @[simp] from BitVec.ofFin_sub and sub_ofFin by @kim-em in #5951
• feat: relate Array.takeWhile with List.takeWhile by @kim-em in #5950
• feat: relate Array.eraseIdx with List.eraseIdx by @kim-em in #5952
• chore: CI: check for GitHub Actions updates once per month by @Kha in #5954
• chore: CI: bump nwtgck/actions-netlify from 2.0 to 3.0 by @dependabot in #5956
• chore: CI: bump softprops/action-gh-release from 1 to 2 by @dependabot in #5955
• chore: CI: bump raven-actions/actionlint from 1 to 2 by @dependabot in #5957
• chore: CI: bump actions/stale from 8 to 9 by @dependabot in #5958
• chore: CI: give Linux Debug unlimited test stack size by @Kha in #5953
• chore: CI: bump lycheeverse/lychee-action from 1.9.0 to 2.0.2 by @dependabot in #5959
• chore: CI: bump actions/github-script from 6 to 7 by @dependabot in #5962
• chore: CI: bump dawidd6/action-download-artifact from 2 to 6 by @dependabot in #5964
• chore: CI: bump dcarbone/install-jq-action from 1.0.1 to 2.1.0 by @dependabot in #5965
• feat: define ISize and basic operations on it by @hargoniX in #5961
• fix: do not link statically against pthread/dl/rt by @TwoFX in #5966
• chore: fix all_goals test, simulate the max rec depth error by @kmill in #5967
• chore: deprecate Array.split in favour of identical Array.partition by @kim-em in #5970
• fix: arg conv tactic misreported number of arguments on error by @kmill in #5968
• feat: relate Array.isPrefixOf with List.isPrefixOf by @kim-em in #5971
• chore: consolidate decide_True and decide_true_eq_true by @kim-em in #5949
• feat: relate Array.zipWith/zip/unzip with List versions by @kim-em in #5972
• chore: exclude leanruntest_task_test_io for now by @TwoFX in #5973
• feat: add another List.find?_eq_some lemma by @kim-em in #5974
• chore: CI: bump mymindstorm/setup-emsdk from 12 to 14 by @dependabot in #5963
• chore: tag prerelease builds with -pre by @Kha in #5943
• feat: BitVec.twoPow in bv_decide by @hargoniX in #5979
• feat: minor lemmas about List.ofFn by @kim-em in #5982
• chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas by @kim-em in #5969
• feat: interactions between List.foldX and List.filterX by @kim-em in #5984
• feat: lemmas relating Array.findX and List.findX by @kim-em in #5985
• feat: BitVec.getMsbD in bv_decide by @hargoniX in #5987
• refactor: name the default SizeOf instance by @nomeata in #5981
• chore: fix test exclusion by @Kha in #5990
• style: fix style in bv_decide normalizer by @hargoniX in #5992
• feat: BitVec.sshiftRight' in bv_decide by @hargoniX in #5995
• chore: new PR changelog template by @Kha in #5976
• chore: revert "CI: give Linux Debug unlimited test stack size" by @Kha in #6001
• chore: List.modifyTailIdx naming fix by @kim-em in #6007
• chore: missing @[ext] attribute on monad transformer ext lemmas by @kim-em in #6008
• feat: verify keys method on HashMaps by @monsterkrampe in #5866
• fix: unset trailing for simpa? "try this" suggestion by @kmill in #5907
• feat: change bv_decide to an elaborated config by @hargoniX in #6010
• fix: ensure instantiateMVarsProfiling adds a trace node by @alexkeizer in #5501
• fix: avoid max heartbeat error in completion by @mhuisi in #5996
• perf: avoid negative environment lookup by @Kha in #5429
• chore: CI: exempt drafts from PR body check by @Kha in #6002
• feat: decide +revert and improvements to native_decide by @kmill in #5999
• feat: prop instance yields theorems by @kmill in #5856
• fix: avoid delaborating with field notation if object is a metavariable by @kmill in #6014
• fix: bv_decide benchmarks by @hargoniX in #6017
• chore: cleanup by @JovanGerb in #6021
• feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero by @bollu in #5616
• feat: variants of List.forIn_eq_foldlM by @kim-em in #6023
• chore: deprecate duplicated Fin.size_pos by @kim-em in #6025
• feat: change Array.set to take a Nat and a tactic provided bound by @kim-em in #5988
• feat: BitVec normalization rule for udiv by twoPow by @bollu in #6029
• fix: simp only [· ∈ ·] by @nomeata in #6030
• feat: bv_decide and flattening by @hargoniX in #6035
• fix: avoid new term info around def bodies by @Kha in #6031
• fix: bv_decide embedded constraint substitution changes models by @hargoniX in #6037
• feat: only direct parents of classes create projections by @kmill in #5920
• feat: change Array.get to take a Nat and a proof by @kim-em in #6032
• chore: review Array operations argument order by @kim-em in #6041
• feat: various minor changes to List/Array API by @kim-em in #6044
• chore: deprecate Array.sequenceMap by @kim-em in #6027
• chore: mark Meta.Context.config as private by @leodemoura in #6051
• refactor: mark the Simp.Context constructor as private by @leodemoura in #6054
• refactor: omega: avoid MVar machinery by @nomeata in #5991
• chore: pr-body: run as part of merge_group, but do not do anything by @nomeata in #6069
• fix: line break in simp? output by @Kha in #6048
• feat: Bool.to(U)IntX by @hargoniX in #6060
• test: synthetic simp_arith benchmark by @nomeata in #6061
• perf: optimize Nat.Linear.Expr.toPoly by @nomeata in #6062
• fix: make sure monad lift coercion elaborator has no side effects by @kmill in #6024
• perf: optimize Nat.Linear.Poly.norm by @nomeata in #6064
• feat: message kinds by @tydeu in #5945
• chore: add newline at end of file for lake new templates by @alissa-tung in #6026
• chore: remove >6 month old deprecations by @kim-em in #6057
• chore: upstream some NameMap functions by @kim-em in #6056
• feat: lemmas about for loops...

v4.14.0

Full Changelog: v4.13.0...v4.14.0

Language features, tactics, and metaprograms

• structure and inductive commands

  • #5517 improves universe level inference for the resulting type of an inductive or structure. Recall that a Prop-valued inductive type is a syntactic subsingleton if it has at most one constructor and all the arguments to the constructor are in Prop. Such types have large elimination, so they could be defined in Type or Prop without any trouble. The way inference has changed is that if a type is a syntactic subsingleton with exactly one constructor, and the constructor has at least one parameter/field, then the inductive/structure command will prefer creating a Prop instead of a Type. The upshot is that the : Prop in structure S : Prop is often no longer needed. (With @arthur-adjedj).
  • #5842 and #5783 implement a feature where the structure command can now define recursive inductive types:

    structure Tree where
      n : Nat
      children : Fin n → Tree
    
    def Tree.size : Tree → Nat
      | {n, children} => Id.run do
        let mut s := 0
        for h : i in [0 : n] do
          s := s + (children ⟨i, h.2⟩).size
        pure s

  • #5814 fixes a bug where Mathlib's Type* elaborator could lead to incorrect universe parameters with the inductive command.
  • #3152 and #5844 fix bugs in default value processing for structure instance notation (with @arthur-adjedj).
  • #5399 promotes instance synthesis order calculation failure from a soft error to a hard error.
  • #5542 deprecates := variants of inductive and structure (see breaking changes).

• Application elaboration improvements

  • #5671 makes @[elab_as_elim] require at least one discriminant, since otherwise there is no advantage to this alternative elaborator.
  • #5528 enables field notation in explicit mode. The syntax @x.f elaborates as @S.f with x supplied to the appropriate parameter.
  • #5692 modifies the dot notation resolution algorithm so that it can apply CoeFun instances. For example, Mathlib has Multiset.card : Multiset α →+ Nat, and now with m : Multiset α, the notation m.card resolves to ⇑Multiset.card m.
  • #5658 fixes a bug where 'don't know how to synthesize implicit argument' errors might have the incorrect local context when the eta arguments feature is activated.
  • #5933 fixes a bug where .. ellipses in patterns made use of optparams and autoparams.
  • #5770 makes dot notation for structures resolve using all ancestors. Adds a resolution order for generalized field notation. This is the order of namespaces visited during resolution when trying to resolve names. The algorithm to compute a resolution order is the commonly used C3 linearization (used for example by Python), which when successful ensures that immediate parents' namespaces are considered before more distant ancestors' namespaces. By default we use a relaxed version of the algorithm that tolerates inconsistencies, but using set_option structure.strictResolutionOrder true makes inconsistent parent orderings into warnings.

• Recursion and induction principles

  • #5619 fixes functional induction principle generation to avoid over-eta-expanding in the preprocessing step.
  • #5766 fixes structural nested recursion so that it is not confused when a nested type appears first.
  • #5803 fixes a bug in functional induction principle generation when there are let bindings.
  • #5904 improves functional induction principle generation to unfold aux definitions more carefully.
  • #5850 refactors code for Predefinition.Structural.

• Error messages

  • #5276 fixes a bug in "type mismatch" errors that would structurally assign metavariables during the algorithm to expose differences.
  • #5919 makes "type mismatch" errors add type ascriptions to expose differences for numeric literals.
  • #5922 makes "type mismatch" errors expose differences in the bodies of functions and pi types.
  • #5888 improves the error message for invalid induction alternative names in match expressions (@josojo).
  • #5719 improves calc error messages.

• #5627 and #5663 improve the #eval command and introduce some new features.

  • Now results can be pretty printed if there is a ToExpr instance, which means hoverable output. If ToExpr fails, it then tries looking for a Repr or ToString instance like before. Setting set_option eval.pp false disables making use of ToExpr instances.
  • There is now auto-derivation of Repr instances, enabled with the pp.derive.repr option (default to true). For example:

    inductive Baz
    | a | b
    
    #eval Baz.a
    -- Baz.a

    It simply does deriving instance Repr for Baz when there's no way to represent Baz.
  • The option eval.type controls whether or not to include the type in the output. For now the default is false.
  • Now expressions such as #eval do return 2, where monad is unknown, work. It tries unifying the monad with CommandElabM, TermElabM, or IO.
  • The classes Lean.Eval and Lean.MetaEval have been removed. These each used to be responsible for adapting monads and printing results. Now the MonadEval class is responsible for adapting monads for evaluation (it is similar to MonadLift, but instances are allowed to use default data when initializing state), and representing results is handled through a separate process.
  • Error messages about failed instance synthesis are now more precise. Once it detects that a MonadEval class applies, then the error message will be specific about missing ToExpr/Repr/ToString instances.
  • Fixes bugs where evaluating MetaM and CoreM wouldn't collect log messages.
  • Fixes a bug where let rec could not be used in #eval.

• partial definitions

  • #5780 improves the error message when partial fails to prove a type is inhabited. Add delta deriving.
  • #5821 gives partial inhabitation the ability to create local Inhabited instances from parameters.

• New tactic configuration syntax. The configuration syntax for all core tactics has been given an upgrade. Rather than simp (config := { contextual := true, maxSteps := 22}), one can now write simp +contextual (maxSteps := 22). Tactic authors can migrate by switching from (config)? to optConfig in tactic syntaxes and potentially deleting mkOptionalNode in elaborators. #5883, #5898, #5928, and #5932. (Tactic authors, see breaking changes.)

• simp tactic

  • #5632 fixes the simpproc for Fin literals to reduce more consistently.
  • #5648 fixes a bug in simpa ... using t where metavariables in t were not properly accounted for, and also improves the type mismatch error.
  • #5838 fixes the docstring of simp! to actually talk about simp!.
  • #5870 adds support for attribute [simp ←] (note the reverse direction). This adds the reverse of a theorem as a global simp theorem.

• decide tactic

  • #5665 adds decide! tactic for using kernel reduction (warning: this is renamed to decide +kernel in a future release).

• bv_decide tactic

  • #5714 adds inequality regression tests (@alexkeizer).
  • #5608 adds bv_toNat tag for toNat_ofInt (@bollu).
  • #5618 adds support for at in ac_nf and uses it in bv_normalize (@tobiasgrosser).
  • #5628 adds udiv support.
  • #5635 adds auxiliary bitblasters for negation and subtraction.
  • #5637 adds more getLsbD bitblaster theory.
  • #5652 adds umod support.
  • #5653 adds performance benchmark for modulo.
  • [#5655](#5655...

v4.14.0-rc3

feat: lake: detailed Reservoir fetch error (#6231)

This PR 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.

Closes #5330.

v4.14.0-rc2

fix: do not link statically against pthread/dl/rt (#5966)

v4.14.0-rc1

chore: set LEAN_VERSION_IS_RELEASE