Release v4.16.0-rc1 · leanprover/lean4

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 proof generator in the (WIP) grind
tactic.
#6456 fixes another bug in the equality proof generator in the (WIP)
grind tactic.
#6457 adds support for generating congruence proofs for congruences
detected by the grind tactic.
#6458 adds support for compact congruence proofs in the (WIP) grind
tactic. The mkCongrProof function now verifies whether the congruence
proof can be constructed using only congr, congrFun, and congrArg,
avoiding the need to generate the more complex hcongr auxiliary
theorems.
#6459 adds the (WIP) grind tactic. It currently generates a warning
message to make it clear that the tactic is not ready for production.
#6461 adds a new propagation rule for negation to the (WIP) grind
tactic.
#6463 adds support for constructors to the (WIP) grind tactic. When
merging equivalence classes, grind checks for equalities between
constructors. If they are distinct, it closes the goal; if they are the
same, it applies injectivity.
#6464 completes support for literal values in the (WIP) grind
tactic. grind now closes the goal whenever it merges two equivalence
classes with distinct literal values.
#6465 adds support for projection functions to the (WIP) grind
tactic.
#6466 completes the implementation of addCongrTable in the (WIP)
grind tactic. It also adds a new test to demonstrate why the extra
check is needed. It also updates the field cgRoot (congruence root).
#6468 fixes issue #6467
#6469 adds support code for implementing e-match in the (WIP) grind
tactic.
#6470 introduces a command for specifying patterns used in the
heuristic instantiation of global theorems in the grind tactic. Note
that this PR only adds the parser.
#6472 implements the command grind_pattern. The new command allows
users to associate patterns with theorems. These patterns are used for
performing heuristic instantiation with e-matching. In the future, we
will add the attributes @[grind_eq], @[grind_fwd], and
@[grind_bwd] to compute the patterns automatically for theorems.
#6473 adds a deriving handler for the ToExpr class. It can handle
mutual and nested inductive types, however it falls back to creating
partial instances in such cases. This is upstreamed from the Mathlib
deriving handler written by @kmill, but has fixes to handle autoimplicit
universe level variables.
#6474 adds pattern validation to the grind_pattern command. The new
checkCoverage function will also be used to implement the attributes
@[grind_eq], @[grind_fwd], and @[grind_bwd].
#6475 adds support for activating relevant theorems for the (WIP)
grind tactic. We say a theorem is relevant to a grind goal if the
symbols occurring in its patterns also occur in the goal.
#6478 internalize nested ground patterns when activating ematch
theorems in the (WIP) grind tactic.
#6481 implements E-matching for the (WIP) grind tactic. We still
need to finalize and internalize the new instances.
#6484 addresses a few error messages where diffs weren't being
exposed.
#6485 implements Grind.EMatch.instantiateTheorem in the (WIP)
grind tactic.
#6487 adds source position information for structure parent
projections, supporting "go to definition". Closes #3063.
#6488 fixes and refactors the E-matching module for the (WIP) grind
tactic.
#6490 adds basic configuration options for the grind tactic.
#6492 fixes a bug in the theorem instantiation procedure in the (WIP)
grind tactic. For example, it was missing the following instance in
one of the tests:
#6497 fixes another theorem instantiation bug in the grind tactic.
It also moves new instances to be processed to Goal.
#6498 adds support in the grind tactic for propagating dependent
forall terms forall (h : p), q[h] where p is a proposition.
#6499 fixes the proof canonicalizer for grind.
#6500 fixes a bug in the markNestedProofs used in grind. See new
test.
#6502 fixes a bug in the proof assembly procedure utilized by the
grind tactic.
#6503 adds a simple strategy to the (WIP) grind tactic. It just
keeps internalizing new theorem instances found by E-matching. The
simple strategy can solve examples such as:
#6506 adds the monotonicity tactic, intended to be used inside the
partial_fixpoint feature.
#6508 fixes a bug in the sanity checkers for the grind tactic. See
the new test for an example of a case where it was panicking.
#6509 fixes a bug in the congruence closure data structure used in the
grind tactic. The new test includes an example that previously caused
a panic. A similar panic was also occurring in the test
grind_nested_proofs.lean.
#6510 adds a custom congruence rule for equality in grind. The new
rule takes into account that Eq is a symmetric relation. In the
future, we will add support for arbitrary symmetric relations. The
current rule is important for propagating disequalities effectively in
grind.
#6512 introduces support for user-defined fallback code in the grind
tactic. The fallback code can be utilized to inspect the state of
failing grind subgoals and/or invoke user-defined automation. Users
can now write grind on_failure <code>, where <code> should have the
type GoalM Unit. See the modified tests in this PR for examples.
#6513 adds support for (dependent) if-then-else terms (i.e., ite and
dite applications) in the grind tactic.
#6514 enhances the assertion of new facts in grind by avoiding the
creation of unnecessary metavariables.

Library

#6182 adds BitVec.[toInt|toFin]_concat and moves a couple of
theorems into the concat section, as BitVec.msb_concat is needed for
the toInt_concat proof.
#6188 completes the toNat theorems for the bitwise operations
(and, or, xor, shiftLeft, shiftRight) of the UInt types and
adds toBitVec theorems as well. It also renames and_toNat to
toNat_and to fit with the current naming convention.
#6238 adds theorems characterizing the value of the unsigned shift
right of a bitvector in terms of its 2s complement interpretation as an
integer.
Unsigned shift right by at least one bit makes the value of the
bitvector less than or equal to 2^(w-1),
makes the interpretation of the bitvector Int and Nat agree.
In the case when n = 0, then the shift right value equals the integer
interpretation.
#6244 changes the implementation of HashMap.toList, so the ordering
agrees with HashMap.toArray.
#6272 introduces the basic theory of permutations of Arrays and
proves Array.swap_perm.
#6282 moves IO.Channel and IO.Mutex from Init to Std.Sync and
renames them to Std.Channel and Std.Mutex.
#6294 upstreams List.length_flatMap, countP_flatMap and
count_flatMap from Mathlib. These were not possible to state before we
upstreamed List.sum.
#6315 adds protected to Fin.cast and BitVec.cast, to avoid
confusion with _root_.cast. These should mostly be used via
dot-notation in any case.
#6316 adds lemmas simplifying for loops over Option into
Option.pelim, giving parity with lemmas simplifying for loops of
List into List.fold.
#6317 completes the basic API for BitVec.ofBool.
#6318 generalizes the universe level for Array.find?, by giving it a
separate implementation from Array.findM?.
#6324 adds GetElem lemmas for the basic Vector operations.
#6333 generalizes the panic functions to a type of Sort u rather
than Type u. This better supports universe polymorphic types and
avoids confusing errors.
#6334 adds Nat theorems for distributing >>> over bitwise
operations, paralleling those of BitVec.
#6338 adds BitVec.[toFin|getMsbD]_setWidth and
[getMsb|msb]_signExtend as well as ofInt_toInt.
#6341 generalizes DecidableRel to allow a heterogeneous relation.
#6353 reproduces the API around List.any/all for Array.any/all.
#6364 makes fixes suggested by the Batteries environment linters,
particularly simpNF, and unusedHavesSuffices.
#6365 expands the Array.set and Array.setIfInBounds lemmas to
match existing lemmas for List.set.
#6367 brings Vector lemmas about membership and indexing to parity
with List and Array.
#6369 adds lemmas about Vector.set, anyM, any, allM, and
all.
#6376 adds theorems about == on Vector, reproducing those already
on List and Array.
#6379 replaces the inductive predicate List.lt with an upstreamed version of List.Lex from Mathlib.
(Previously Lex.lt was defined in terms of <; now it is generalized to take an arbitrary relation.)
This subtly changes the notion of ordering on List α.

List.lt was a weaker relation: in particular if l₁ < l₂, then a :: l₁ < b :: l₂ may hold according to List.lt even if a and b are merely incomparable (either neither a < b nor b < a), whereas according to List.Lex this would require a = b.

When < is total, in the sense that ¬ · < · is antisymmetric, then the two relations coincide.

Mathlib was already overriding the order instances for List α, so this change should not be noticed by anyone already using Mathlib.

We simultaneously add the boolean valued List.lex function, parameterised by a BEq typeclass and an arbitrary lt function. This will support the flexibility previously provided for List.lt, via a == function which is weaker than strict equality.
#6390 redefines Range.forIn' and Range.forM, in preparation for
writing lemmas about them.
#6391 requires that the step size in Std.Range is positive, to avoid
ill-specified behaviour.
#6396 adds lemmas reducing for loops over Std.Range to for loops
over List.range'.
#6399 adds basic lemmas about lexicographic order on Array and Vector,
achieving parity with List.
#6423 adds missing lemmas about lexicographic order on
List/Array/Vector.
#6477 adds the necessary domain theory that backs the
partial_fixpoint feature.

Compiler

#6311 adds support for HEq to the new code generator.
#6348 adds support for Float32 to the Lean runtime.
#6350 adds missing features and fixes bugs in the Float32 support
#6383 ensures the new code generator produces code for opaque
definitions that are not tagged as @[extern].
Remark: This is the behavior of the old code generator.
#6405 adds support for erasure of Decidable.decide to the new code
generator. It also adds a new Probe.runOnDeclsNamed function, which is
helpful for writing targeted single-file tests of compiler internals.
#6415 fixes a bug in the sharecommon module, which was returning
incorrect results for objects that had already been processed by
sharecommon. See the new test for an example that triggered the bug.
#6429 adds support for extern LCNF decls, which is required for parity
with the existing code generator.

Pretty Printing

#5689 adjusts the way the pretty printer unresolves names. It used to
make use of all exports when pretty printing, but now it only uses
exports that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.
#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

Documentation

#6450 adds a docstring to the @[app_delab] attribute.

Server

#6279 fixes a bug in structure instance field completion that caused
it to not function correctly for bracketed structure instances written
in Mathlib style.
#6408 fixes a regression where goals that don't exist were being
displayed. The regression was triggered by #5835 and originally caused
by #4926.

Lake

#6176 changes Lake's build process to no longer use leanc for
compiling C files or linking shared libraries and executables. Instead,
it directly invokes the bundled compiler (or the native compiler if
none) using the necessary flags.
#6289 adapts Lake modules to use prelude and includes them in the
check-prelude CI.
#6291 ensures the the log error position is properly preserved when
prepending stray log entries to the job log. It also adds comparison
support for Log.Pos.
#6388 merges BuildJob and Job, deprecating the former. Job now
contains a trace as part of its state which can be interacted with
monadically. also simplifies the implementation of OpaqueJob.
#6411 adds the ability to override package entries in a Lake manifest
via a separate JSON file. This file can be specified on the command line
with --packages or applied persistently by placing it at
.lake/package-overrides.json.
#6422 fixes a bug in #6388 where the Package.afterBuildCahe*
functions would produce different traces depending on whether the cache
was fetched.

Other

#6285 upstreams the ToLevel typeclass from mathlib and uses it to
fix the existing ToExpr instances so that they are truly universe
polymorphic (previously it generated malformed expressions when the
universe level was nonzero). We improve on the mathlib definition of
ToLevel to ensure the class always lives in Type, irrespective of
the universe parameter.
#6363 fixes errors at load time in the comparison mode of the Firefox
profiler.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

v4.16.0-rc1

v4.16.0-rc1

Language

Library

Compiler

Pretty Printing

Documentation

Server

Lake

Other

Contributors