Releases · leanprover/lean4

03 Feb 12:09

github-actions

v4.17.0-rc1

93d4ae6

v4.17.0-rc1 Pre-release

Pre-release

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

Assets 14

03 Feb 07:17

github-actions

v4.16.0

128a1e6

v4.16.0

Highlights

Unique `sorry`s

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

Contributors

kmill

Assets 14

14 Jan 02:02

github-actions

v4.16.0-rc2

128a1e6

v4.16.0-rc2 Pre-release

Pre-release

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

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

Contributors

kmill

Assets 14

04 Jan 04:42

github-actions

v4.16.0-rc1

0c9a488

v4.16.0-rc1 Pre-release

Pre-release

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

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

Contributors

kmill

Assets 14

04 Jan 02:41

github-actions

v4.15.0

1165156

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

Contributors

hrmacbeth

Assets 16

02 Dec 01:25

github-actions

v4.15.0-rc1

ffac974

v4.15.0-rc1 Pre-release

Pre-release

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

Contributors

juhp, Kha, and 27 other contributors

Assets 16

01 Dec 23:57

github-actions

v4.14.0

410fab7

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

Contributors

juhp, eric-wieser, and 12 other contributors

Assets 16

29 Nov 02:14

github-actions

v4.14.0-rc3

410fab7

v4.14.0-rc3 Pre-release

Pre-release

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.

Assets 16

05 Nov 23:52

github-actions

v4.14.0-rc2

7dc1ceb

v4.14.0-rc2 Pre-release

Pre-release

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

Assets 16

04 Nov 00:11

github-actions

v4.14.0-rc1

df54bec

v4.14.0-rc1 Pre-release

Pre-release

chore: set LEAN_VERSION_IS_RELEASE

Assets 16

Releases: leanprover/lean4

v4.17.0-rc1

v4.17.0-rc1

Language

Uh oh!

v4.16.0

v4.16.0

Highlights

Unique sorrys

Separators in numeric literals

Additional new featues

Library updates

Breaking changes

Language

Contributors

Uh oh!

v4.16.0-rc2

v4.16.0-rc2

Language

Contributors

Uh oh!

v4.16.0-rc1

v4.16.0-rc1

Language

Contributors

Uh oh!

v4.15.0

v4.15.0

Language

Contributors

Uh oh!

v4.15.0-rc1

What's Changed

Contributors

Uh oh!

v4.14.0

Language features, tactics, and metaprograms

Contributors

Uh oh!

v4.14.0-rc3

Uh oh!

v4.14.0-rc2

Uh oh!

v4.14.0-rc1

Uh oh!

Unique `sorry`s