Releases · leanprover/lean4

For this release, 414 changes landed. In addition to the 164 feature additions and 74 fixes listed below there were 13 refactoring changes, 29 documentation improvements, 31 performance improvements, 9 improvements to the test suite and 92 other changes.

Language

#5182 makes functions defined by well-founded recursion use an
opaque well-founded proof by default. This reliably prevents kernel
reduction of such definitions and proofs, which tends to be
prohibitively slow (fixes #2171), and which regularly causes
hard-to-debug kernel type-checking failures. This changes renders
unseal ineffective for such definitions. To avoid the opaque proof,
annotate the function definition with @[semireducible].
#5998 lets omega always abstract its own proofs into an auxiliary
definition. The size of the olean of Vector.Extract goes down from 20MB
to 5MB with this, overall stdlib olean size and build instruction count
go down 5%.
#6325 ensures that environments can be loaded, repeatedly, without
executing arbitrary code
#7075 ensures that names suggested by tactics like simp? are not
shadowed by auxiliary declarations in the local context and that names
of let rec and where declarations are correctly resolved in tactic
blocks.
#7084 enables the elaboration of theorem bodies, i.e. proofs, to
happen in parallel to each other as well as to other elaboration tasks.
#7166 extends the notion of “fixed parameter” of a recursive function
also to parameters that come after varying function. The main benefit is
that we get nicer induction principles.
#7247 makes generation of match equations and splitters compatible
with parallelism.
#7256 introduces the assert! variant debug_assert! that is
activated when compiled with buildType debug.
#7261 ensures all equation, unfold, induction, and partial fixpoint
theorem generators in core are compatible with parallelism.
#7298 adds rewrites to bv_decide's preprocessing that concern
combinations of if-then-else and operation such as multiplication or
negation.
#7302 changes how fields are elaborated in the structure/class
commands and also makes default values respect the structure resolution
order when there is diamond inheritance. Before, the details of
subobjects were exposed during elaboration, and in the local context any
fields that came from a subobject were defined to be projections of the
subobject field. Now, every field is represented as a local variable.
All parents (not just subobject parents) are now represented in the
local context, and they are now local variables defined to be parent
constructors applied to field variables (inverting the previous
relationship). Other notes:
- The entire collection of parents is processed, and all parent
  projection names are checked for consistency. Every parent appears in
  the local context now.
- For classes, every parent now contributes an instance, not just the
  parents represented as subobjects.
- Default values are now processed according to the parent resolution
  order. Default value definition/override auxiliary definitions are
  stored at StructName.fieldName._default, and inherited values are
  stored at StructName.fieldName._inherited_default. Metaprograms no
  longer need to look at parents when doing calculations on default
  values.
- Default value omission for structure instance notation pretty printing
  has been updated in consideration of this.
- Now the elaborator generates a _flat_ctor constructor that will be
  used for structure instance elaboration. All types in this constructor
  are put in "field normal form" (projections of parent constructors are
  reduced, and parent constructors are eta reduced), and all fields with
  autoParams are annotated as such. This is not meant for users, but it
  may be useful for metaprogramming.
- While elaborating fields, any metavariables whose type is one of the
  parents is assigned to that parent. The hypothesis is that, for the
  purpose of elaborating structure fields, parents are fixed: there is
  only one instance of any given parent under consideration. See the
  Magma test for an example of this being necessary. The hypothesis may
  not be true when there are recursive structures, since different values
  of the structure might not agree on parent fields.
#7304 fixes an issue where nested let rec declarations within
match expressions or tactic blocks failed to compile if they were
nested within, and recursively called, a let rec that referenced a
variable bound by a containing declaration.
#7309 fixes a bug where bv_decide's new structure support would
sometimes not case split on all available structure fvars as their type
was an mvar.
#7312 implements proof term generation for cooper_dvd_left and its
variants in 8000 the cutsat procedure for linear integer arithmetic.
#7314 changes elaboration of structure parents so that each must be
fully elaborated before the next one is processed.
#7315 implements the Cooper conflict resolution in cutsat. We still
need to implement the backtracking and disequality case.
#7324 changes the internal construction of well-founded recursion, to
not change the type of fix’s induction hypothesis in non-defeq ways.
#7329 adds support to bv_decide for simple pattern matching on enum
inductives. By simple we mean non dependent match statements with all
arms written out.
#7333 allows aux decls (like generated by match) to be generated by
decreasing_by tactics.
#7335 modifies elabTerminationByHints in a way that the type of the
recursive function used for elaboration of the termination measure is
striped of from optional parameters. It prevents introducing
dependencies between the default values for arguments, that can cause
the termination checker to fail.
#7339 implements cooper conflict resolution in the cutsat procedure.
It also fixes several bugs in the proof term construction. We still need
to add more tests, but we can already solve the following example that
omega fails to solve:
```
example (x y : Int) :
    27 ≤ 11*x + 13*y →
    11*x + 13*y ≤ 45 →
    -10 ≤ 7*x - 9*y →
    7*x - 9*y ≤ 4 → False := by
  grind
```
#7347 upgrades the CaDiCal we ship and use for bv_decide to version
2.1.2. Additionally it enables binary LRAT proofs on windows by default
as arminbiere/cadical#112 has been fixed.
#7348 ensures all equation and unfold theorem generators in core are
compatible with parallelism.
#7351 ensures cutsat does not have to perform case analysis in the
univariate polynomial case. That it, it can close a goal whenever there
is no solution for a divisibility constraint in an interval. Example of
theorem that is now proved in a single step by cutsat:
```
example (x : Int) : 100 ≤ x → x ≤ 10000 → 20000 ∣ 3*x → False := by
  grind
```
#7353 changes abstractNestedProofs so that it also visits the
subterms in the head of an application.
#7355 fixes a bug in the markNestedProofs preprocessor used in the
grind tactic.
#7357 adds support for / and % to the cutsat procedure.
#7362 allows simp dischargers to add aux decls to the environment.
This enables tactics like native_decide to be used here, and unblocks
improvements to omega in #5998.
#7369 uses let-declarations for each polynomial occurring in a proof
term generated by the cutsat procedure.
#7370 simplifies the proof term due to the Cooper's conflict
resolution in cutsat.
#7373 implements the last missing case for the cutsat procedure and
fixes a bug. During model construction, we may encounter a bounded
interval containing integer solutions that satisfy the divisibility
constraint but fail to satisfy known disequalities.
#7381 refactors the AIG datastructures that underly bv_decide in order
to allow a better tracking of negations in the circuit. This refactor
has two effects, for one adding full constant folding to the AIG
framework and secondly enabling us to add further simplifications from
the Brummayer Biere paper...

This is the v4.18.0 release of Lean.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Language

Contributors

Uh oh!

Uh oh!

Uh oh!

Releases: leanprover/lean4

v4.20.0-rc5

Uh oh!

v4.20.0-rc4

Uh oh!

v4.20.0-rc3

Uh oh!

v4.20.0-rc2

Uh oh!

v4.20.0-rc1

Uh oh!

v4.19.0

Uh oh!

v4.19.0-rc3

Uh oh!

v4.19.0-rc2

Language

Contributors

Uh oh!

v4.19.0-rc1

Uh oh!

v4.18.0

Uh oh!