This PR adjusts the experimental module system to make `private` the
default visibility modifier in `module`s, introducing `public` as a new
modifier instead. `public section` can be used to revert the default for
an entire section, though this is more intended to ease gradual adoption
of the new semantics such as in `Init` (and soon `Std`) where they
should be replaced by a future decl-by-decl re-review of visibilities.
This PR adds the following features to `simp`:
- A routine for simplifying `have` telescopes in a way that avoids
quadratic complexity arising from locally nameless expression
representations, like what #6220 did for `letFun` telescopes.
Furthermore, simp converts `letFun`s into `have`s (nondependent lets),
and we remove the #6220 routine since we are moving away from `letFun`
encodings of nondependent lets.
- A `+letToHave` configuration option (enabled by default) that converts
lets into haves when possible, when `-zeta` is set. Previously Lean
would need to do a full typecheck of the bodies of `let`s, but the
`letToHave` procedure can skip checking some subexpressions, and it
modifies the `let`s in an entire expression at once rather than one at a
time.
- A `+zetaHave` configuration option, to turn off zeta reduction of
`have`s specifically. The motivation is that dependent `let`s can only
be dsimped by let, so zeta reducing just the dependent lets is a
reasonable way to make progress. The `+zetaHave` option is also added to
the meta configuration.
- When `simp` is zeta reducing, it now uses an algorithm that avoids
complexity quadratic in the depth of the let telescope.
- Additionally, the zeta reduction routines in `simp`, `whnf`, and
`isDefEq` now all are consistent with how they apply the `zeta`,
`zetaHave`, and `zetaUnused` configurations.
The `letToFun` option is addressing a TODO in `getSimpLetCase` ("handle
a block of nested let decls in a single pass if this becomes a
performance problem").
Performance should be compared to before #8804, which temporarily
disabled the #6220 optimizations for `letFun` telescopes.
Good kernel performance depends on carefully handling the `have`
encoding. Due to the way the kernel instantiates bvars (it does *not*
beta reduce when instantiating), we cannot use congruence theorems of
the form `(have x := v; f x) = (have x ;= v'; f' x)`, since the bodies
of the `have`s will not be syntactically equal, which triggers zeta
reduction in the kernel in `is_def_eq`. Instead, we work with `f v = f'
v'`, where `f` and `f'` are lambda expressions. There is still zeta
reduction, but only when converting between these two forms at the
outset of the generated proof.
This PR implements non-chronological backtracking for the `grind`
tactic. This feature ensures that `grind` does not need to process
irrelevant branches after performing a case-split that is not relevant.
It is not just about performance, but also the size of the final proof
term. The new test demonstrates this feature in practice.
```lean
-- In the following test, the first 8 case-splits are irrelevant,
-- and non-choronological backtracking is used to avoid searching
-- (2^8 - 1) irrelevant branches
/--
trace:
[grind.split] p8 ∨ q8, generation: 0
[grind.split] p7 ∨ q7, generation: 0
[grind.split] p6 ∨ q6, generation: 0
[grind.split] p5 ∨ q5, generation: 0
[grind.split] p4 ∨ q4, generation: 0
[grind.split] p3 ∨ q3, generation: 0
[grind.split] p2 ∨ q2, generation: 0
[grind.split] p1 ∨ q1, generation: 0
[grind.split] ¬p ∨ ¬q, generation: 0
-/
#guard_msgs (trace) in
set_option trace.grind.split true in
theorem ex
: p ∨ q →
¬ p ∨ q →
p ∨ ¬ q →
¬ p ∨ ¬ q →
p1 ∨ q1 →
p2 ∨ q2 →
p3 ∨ q3 →
p4 ∨ q4 →
p5 ∨ q5 →
p6 ∨ q6 →
p7 ∨ q7 →
p8 ∨ q8 →
False := by
grind (splits := 10)
```
This PR implements tactics called `extract_lets` and `lift_lets` that
manipulate `let`/`let_fun` expressions. The `extract_lets` tactic
creates new local declarations extracted from any `let` and `let_fun`
expressions in the main goal. For top-level lets in the target, it is
like the `intros` tactic, but in general it can extract lets from deeper
subexpressions as well. The `lift_lets` tactic moves `let` and `let_fun`
expressions as far out of an expression as possible, but it does not
extract any new local declarations. The option `extract_lets +lift`
combines these behaviors.
This is a re-implementation of `extract_lets` and `lift_lets` from
mathlib. The new `extract_lets` is like doing `lift_lets; extract_lets`,
but it does not lift unextractable lets like `lift_lets`. The
`lift_lets; extract_lets` behavior is now handled by `extract_lets
+lift`. The new `lift_lets` tactic is a frontend to `extract_lets +lift`
machinery, which rather than creating new local definitions instead
represents the accumulated local declarations as top-level lets.
There are also conv tactics for both of these. The `extract_lets` has a
limitation due to the conv architecture; it can extract lets for a given
conv goal, but the local declarations don't survive outside conv. They
get zeta reduced immediately upon leaving conv.
This PR 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.
The default setting does change the existing behavior. Users can use
`simp -implicitDefEqProofs` to force `simp` to create a proof term for
`rfl`-theorems. This can positively impact proof checking time in the
kernel.
This PR also fixes an issue in the `split` tactic that has been exposed
by this feature. It was looking for `split` candidates in proofs and
implicit arguments. See new test for issue exposed by the previous
feature.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR makes it possible to write `rw (occs := [1,2]) ...` instead of
`rw (occs := .pos [1,2]) ...` by adding a coercion from `List.Nat` to
`Lean.Meta.Occurrences`.
this option was added in fb97275dcb to
prepare for #4595, due to boostrapping issues, but #4595 has not landed
yet. This is be very confusing when people discover this option and try
to use it (as I did).
So let's clearly mark this as not yet implemented on `master`, and add
the
docstring only with #4595.
The `simp` tactic uses a discrimination tree to select candidate
theorems that will be used to rewrite an expression. This indexing data
structure minimizes the number of theorems that need to be tried and
improves performance. However, indexing modulo reducibility is
challenging, and a theorem that could be applied, when taking reduction
into account, may be missed. For example, suppose we have a `simp`
theorem `foo : forall x y, f x (x, y).2 = y`, and we are trying to
simplify the expression `f a b <= b`. `foo` will not be tried by `simp`
because the second argument of `f a b` is not a projection of a pair.
However, `f a b` is definitionally equal to `f a (a, b).2` since we can
reduce `(a, b).2`.
In Lean 3, we had a much simpler indexing data structure where only the
head symbol was taken into account. For the theorem `foo`, the head
symbol is `f`. Thus, the theorem would be considered by `simp`.
This commit adds the option `Simp.Config.index`. When `simp (config := {
index := false })`, only the head symbol is considered when retrieving
theorems, as in Lean 3. Moreover, if `set_option diagnostics true`,
`simp` will check whether every applied theorem would also have been
applied if `index := true`, and report them. This feature can help users
diagnose tricky issues in code that has been ported from libraries
developed using Lean 3 and then ported to Lean 4. In the following
example, it will report that `foo` is a problematic theorem.
```lean
opaque f : Nat → Nat → Nat
@[simp] theorem foo : f x (x, y).2 = y := by sorry
example : f a b ≤ b := by
set_option diagnostics true in
simp (config := { index := false })
```
In the example above, the following diagnostic message is produced.
```lean
[simp] theorems with bad keys
foo, key: [f, *, Prod.1, Prod.mk, Nat, Nat, *, *]
```
With the information above, users can annotate theorems such as `foo`
using `no_index` for problematic subterms.
Example:
```lean
opaque f : Nat → Nat → Nat
@[simp] theorem foo : f x (no_index (x, y).2) = y := by sorry
example : f a b ≤ b := by
simp -- `foo` is still applied
```
cc @semorrison
cc @PatrickMassot
