This PR adds a `recommended_spelling` command, which can be used for
recording the recommended spelling of a notation (for example, that the
recommended spelling of `∧` in identifiers is `and`). This information
is then appended to the relevant docstrings for easy lookup.
The function `Lean.Elab.Term.Doc.allRecommendedSpellings` may be used to
obtain a list of all recommended spellings, for example to create a
table that is part of a style guide. In the future, it might be
desirable to be able to partition such a table into smaller tables by
category. This can be added in a future PR.
The implementation is heavily inspired by #4490.
This PR changes how the unfold theorems for well-founded recursion are
created. They are created eagerly (anticipating that the behaivor may be
affected by simp sets soon), and without the detour of going through
equational theorems.
This PR adds a builtin tactic and a builtin attribute that are required
for the tree map. The tactic, `as_aux_lemma`, can generally be used to
wrap the proof term generated by a tactic sequence into a separate
auxiliary lemma in order to keep the proof term small. This can, in rare
cases, be necessary if the proof term will appear multiple times in the
encompassing term. The new attribute, `Std.Internal.tree_tac`, is
internal and should not be used outside of `Std`.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR adds the `try?` tactic. This is the first draft, but it can
already solve examples such as:
```lean
example (e : Expr) : e.simplify.eval σ = e.eval σ := by
try?
```
in `grind_constProp.lean`. In the example above, it suggests:
```lean
induction e using Expr.simplify.induct <;> grind?
```
In the same test file, we have
```lean
example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
try?
```
and the following suggestion is produced
```lean
induction σ₁, σ₂ using State.join.induct <;> grind?
```
This PR adds the `grind` configuration option `verbose`. For example,
`grind -verbose` disables all diagnostics. We are going to use this flag
to implement `try?`.
This PR changes the `simpMatch` function, used inside the equation
generator for WF-rec functions, to not do eta-expansion.
This makes the process a bit more robust and disciplined, and avoids
removing match-statements (and introduce projections and dependencies)
that we'd rather split instead.
Also adds more tracing to the equational theorem generator.
Extracted from #6898.
This PR teaches bv_normalize to replace subtractions on one side of an
equality with an addition on the other side, this re-write eliminates a
not + addition in the normalized form so it is easier on the solver.
Note that I also make a point to normalize (1 + ~~~x) to (~~~x + 1) to
limit the amount of boilerplate symmetry theorems we require.
This PR adds the new attributes `[grind =>]` and `[grind <=]` for
controlling pattern selection and minimizing the number of places where
we have to use verbose `grind_pattern` command. It also fixes a bug in
the new pattern selection procedure, and improves the automatic pattern
selection for local lemmas.
The tests `grind_constProp.lean` and `no_grind_constProp.lean` are the
same use case with and without `grind`.
This PR fixes a few `grind` issues exposed by the `grind_constProp.lean`
test.
- Support for equational theorem hypotheses created before invoking
`grind`. Example: applying an induction principle.s
- Support of `Unit`-like types.
- Missing recursion depth checks.
This PR fixes a bug in the pattern selection heuristic used in `grind`.
It was unfolding definitions/abstractions that were not supposed to be
unfolded. See `grind_constProp.lean` for examples affected by this bug.
This PR adds basic lemmas about `Ordering`, describing the interaction
of `isLT`/`isLE`/`isGE`/`isGT`, `swap` and the constructors.
Additionally, it refactors the instance derivation code such that a
`LawfulBEq Ordering` instance is also derived automatically.
Some of these lemmas are helpful for the `TreeMap` verification.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This PR changes how WF.Eqns unfolds the fixpoint. Instead of delta'ing
until we have `fix`, and then blindly applying `fix_eq`, we delta one
step less and preserve the function on the right hand side. This leads
to smaller terms in the next step, so easier to debug, possibly faster,
possibly more robust.
This PR adds BitVec lemmas required to cancel multiplicative negatives,
and plumb support through to bv_normalize to make use of this result in
the normalized twos-complement form.
I include some bmod lemmas I found useful to prove this result, the two
helper lemmas I add use the same naming/proofs as their emod
equivalents.
This PR makes `take`/`drop`/`extract` available for each of
`List`/`Array`/`Vector`. The simp normal forms differ, however: in
`List`, we simplify `extract` to `take+drop`, while in `Array` and
`Vector` we simplify `take` and `drop` to `extract`. We also provide
`Array/Vector.shrink`, which simplifies to `take`, but is implemented by
repeatedly popping. Verification lemmas for `Array/Vector.extract` to
follow in a subsequent PR.
This PR adds a convenience for inductive predicates in `grind`. Now,
give an inductive predicate `C`, `grind [C]` marks `C` terms as
case-split candidates **and** `C` constructors as E-matching theorems.
Here is an example:
```lean
example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
grind [BigStep]
```
Users can still use `grind [cases BigStep]` to only mark `C` as a case
split candidate.
This PR makes `bv_normalize` rewrite shifts by `BitVec` constants to
shifts by `Nat` constants. This is part of the greater effort in
providing good support for constant shift simplification in
`bv_normalize`.
This PR fixes#6789 by ensuring metadata generated for inaccessible
variables in pattern-matches is consumed in `casesOnStuckLHS`
accordingly.
Closes#6789
This PR adds missing monadic higher order functions on
`List`/`Array`/`Vector`. Only the most basic verification lemmas
(relating the operations on the three container types) are provided for
now.
This PR adds add/sub injectivity lemmas for BitVec, and then adds
specialized forms with additional symmetries for the `bv_normalize`
normal form.
Since I need `neg_inj`, I add `not_inj`/`neg_inj` at once, and use it in
`BitVec.not_beq_not` instead of re-proving it.
This PR ensures `grind` can use constructors and axioms for heuristic
instantiation based on E-matching. It also allows patterns without
pattern variables for theorems such as `theorem evenz : Even 0`.
This PR adds "performance" counters (e.g., number of instances per
theorem) to `grind`. The counters are always reported on failures, and
on successes when `set_option diagnostics true`.
This PR adds injectivity theorems for inductives that did not get them
automatically (because they are defined too early) but also not yet
manuall later.
It also adds a test case to notice when new ones fall through.o
It does not add them for clearly meta-programming related types that are
not yet defined in `Init/Core.lean`, and uses `#guard_msgs` as an
allowlist.
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
This PR adds a BitVec lemma that `(x >> x) = 0` and plumbs it through to
bv_normalize. I also move some theorems I found useful to the top of the
ushiftRight section.
This PR adds a few builtin case-splits for `grind`. They are similar to
builtin `simp` theorems. They reduce the noise in the tactics produced
by `grind?`.
This PR adds a number of simple comparison lemmas to the top/bottom
element for BitVec. Then they are applied to teach bv_normalize that
`(a<1) = (a==0)` and to remove an intermediate proof that is no longer
necessary along the way.
This PR fixes a significant auto-completion performance regression that
was introduced in #5666, i.e. v4.14.0.
#5666 introduced tactic docstrings, which were attempted to be collected
for every single completion item. This is slow for hundreds of thousands
of completion items. To fix this, this PR moves the docstring
computation into the completion item resolution, which is only called
when users select a specific completion item in the UI.
A downside of this approach is that we currently can't test completion
item resolution, so we lose a few tests that cover docstrings in
completions in this PR.
