This PR fixes a bug where the single-quote character `Char.ofNat 39`
would delaborate as `'''`, which causes a parse error if pasted back in
to the source code.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
This PR changes the `show t` tactic to match its documentation.
Previously it was a synonym for `change t`, but now it finds the first
goal that unifies with the term `t` and moves it to the front of the
goal list.
This PR adds grind annotations for `List/Array/Vector.ofFn` theorems and
additional `List.Impl` find operations.
The annotations are added to theorems that correspond to those already
annotated in the List implementation, ensuring consistency across all
three container types (List, Array, Vector) for ofFn operations and
related functionality.
Key theorems annotated include:
- Element access theorems (`getElem_ofFn`, `getElem?_ofFn`)
- Construction and conversion theorems (`ofFn_zero`, `toList_ofFn`,
`toArray_ofFn`)
- Membership theorems (`mem_ofFn`)
- Head/tail operations (`back_ofFn`)
- Monadic operations (`ofFnM_zero`, `toList_ofFnM`, `toArray_ofFnM`,
`idRun_ofFnM`)
- List.Impl find operations (`find?_singleton`, `find?_append`,
`findSome?_singleton`, `findSome?_append`)
This PR adds grind annotations for `Array/Vector.mapIdx` and `mapFinIdx`
theorems.
The annotations are added to theorems that correspond to those already
annotated in the List implementation, ensuring consistency across all
three container types (List, Array, Vector) for indexed mapping
operations.
Key theorems annotated include:
- Size and element access theorems (`size_mapIdx`, `getElem_mapIdx`,
`getElem?_mapIdx`)
- Construction theorems (`mapIdx_empty`, `mapIdx_push`, `mapIdx_append`)
- Membership and equality theorems (`mem_mapIdx`, `mapIdx_mapIdx`)
- Conversion theorems (`toList_mapIdx`, `mapIdx_toArray`, etc.)
- Reverse and composition operations
- Similar annotations for `mapFinIdx` variants
This PR adds an equivalence relation to tree maps akin to the existing
one for hash maps. In order to get many congruence lemmas to eventually
use for defining functions on extensional tree maps, almost all of the
remaining tree map functions have also been given lemmas to relate them
to list functions, although these aren't currently used to prove lemmas
other than congruence lemmas.
This PR introduces an explicit `defeq` attribute to mark theorems that
can be used by `dsimp`. The benefit of an explicit attribute over the
prior logic of looking at the proof body is that we can reliably omit
theorem bodies across module boundaries. It also helps with intra-file
parallelism.
If a theorem is syntactically defined by `:= rfl`, then the attribute is
assumed and need not given explicitly. This is a purely syntactic check
and can be fooled, e.g. if in the current namespace, `rfl` is not
actually “the” `rfl` of `Eq`. In that case, some other syntax has be
used, such as `:= (rfl)`. This is also the way to go if a theorem can be
proved by `defeq`, but one does not actually want `dsimp` to use this
fact.
The `defeq` attribute will look at the *type* of the declaration, not
the body, to check if it really holds definitionally. Because of
different reduction settings, this can sometimes go wrong. Then one
should also write `:= (rfl)`, if one does not want this to be a defeq
theorem. (If one does then this is currently not possible, but it’s
probably a bad idea anyways).
The `set_option debug.tactic.simp.checkDefEqAttr true`, `dsimp` will
warn if could not apply a lemma due to a missing `defeq` attribute.
With `set_option backward.dsimp.useDefEqAttr.get false` one can revert
to the old behavior of inferring rfl-ness based on the theorem body.
Both options will go away eventually (too bad we can’t mark them as
deprecated right away, see #7969)
Meta programs that generate theorems (e.g. equational theorems) can use
`inferDefEqAttr` to set the attribute based on the theorem body of the
just created declaration.
This builds on #8501 to update Init to `@[expose]` a fair amount of
definitions that, if not exposed, would prevent some existing `:= rfl`
theorems from being `defeq` theorems. In the interest of starting
backwards compatible, I exposed these function. Hopefully many can be
un-exposed later again.
A mathlib adaption branch exists that includes both the meta programming
fixes and changes to the theorems (e.g. changing `:= by rfl` to `:=
rfl`).
With the module system there is now no special handling for `defeq`
theorem bodies, because we don’t look at the body anymore. The previous
hack is removed. The `defeq`-ness of the theorem needs to be checked in
the context of the theorem’s *type*; the error message contains a hint
if the defeq check fails because of the exported context.
This PR completes the `ToInt` family of typeclasses which `grind` will
use to embed types into the integers for `cutsat`. It contains instances
for the usual concrete data types (`Fin`, `UIntX`, `IntX`, `BitVec`),
and is extensible (e.g. for Mathlib's `PNat`).
This PR adds a simp lemma that simplifies T-division where the numerator
is a `Nat` into an E-division:
```lean
@[simp] theorem ofNat_tdiv_eq_ediv {a : Nat} {b : Int} : (a : Int).tdiv b = a / b :=
tdiv_eq_ediv_of_nonneg (by simp)
```
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR adds trichotomy lemmas for unsigned and signed comparisons,
stating that only one of three cases may happen: either `x < y`, `x =
y`, or `x > y` (for both signed and unsigned comparsions). We use
explicit arguments so that users can write `rcases slt_trichotomy x y
with hlt | heq | hgt`.
This PR removes the `NatCast (Fin n)` global instance (both the direct
instance, and the indirect one via `Lean.Grind.Semiring`), as that
instance causes causes `x < n` (for `x : Fin k`, `n : Nat`) to be
elaborated as `x < ↑n` rather than `↑x < n`, which is undesirable. Note
however that in Mathlib this happens anyway!
This PR adds a test case / use case example for `grind`, setting up the
very basics of `IndexMap`, modelled on Rust's
[`indexmap`](https://docs.rs/indexmap/latest/indexmap/). It is not
intended as a complete implementation: just enough to exercise `grind`.
(Thanks to @arthurpaulino for suggesting this as a test case.)
This PR uses `grind` to shorten some proofs in the LRAT checker. The
intention is not particularly to improve the quality or maintainability
of these proofs (although hopefully this is a side effect), but just to
give `grind` a work out.
There are a number of remaining notes, either about places where `grind`
fails with an internal error (for which #8608 is hopefully
representative, and we can fix after that), or `omega` works but `grind`
doesn't (to be investigated later).
Only in some of the files have I thoroughly used grind. In many files
I've just replaced leaves or branches of proofs with `grind` where it
worked easily, without setting up the internal annotations in the LRAT
library required to optimize the use of `grind`. It's diminishing
returns to do this in a proof library that is not high priority, so I've
simply drawn a line.
This PR provides the iterator combinator `drop` that transforms any
iterator into one that drops the first `n` elements.
Additionally, the PR removes the specialized `IteratorLoop` instance on
`Take`. It currently does not have a `LawfulIteratorLoop` instance,
which needs to exist for the loop consumer lemmas to work. Having the
specialized instance is low priority.
This PR makes the lemma `BitVec.extractLsb'_append_eq_ite` more usable
by using the "simple case" more often, and uses this simplification to
make `BitVec.extractLsb'_append_eq_of_add_lt` stronger, renaming it to
`BitVec.extractLsb'_append_eq_of_add_le`.
This PR fixes an issue when including a hard line break in a `Format`
that caused subsequent (ordinary) line breaks to be erroneously
flattened to spaces.
This issue is especially important for displaying notes and hints in
error messages, as these components could appear garbled due to improper
line-break rendering.
This PR removes the `@[reducible]` annotation on `Array.size`. This is
probably best gone anyway in order to keep separation between the `List`
and `Array` APIs, but it also helps avoid uselessly instantiating
`Array` theorems when `grind` is working on `List` problems.
This PR adds the `@[expose]` attribute to many functions (and changes
some theorems to be by `:= (rfl)`) in preparation for the `@[defeq]`
attribute change in #8419.
This PR adds `simp` lemmas for `toInt_*` and `toNat_*` with arithmetic
operation given the hypothesis of no-overflow
(`toNat_add_of_not_uaddOverflow`, `toInt_add_of_not_saddOverflow`,
`toNat_sub_of_not_usubOverflow`, `toInt_sub_of_not_ssubOverflow`,
`toInt_neg_of_not_negOverflow`, `toNat_mul_of_not_umulOverflow`,
`toInt_mul_of_not_smulOverflow`). In particular, these are `simp` since
(1) the `rhs` is strictly simpler than the `lhs` and (2) this version is
also simpler than the standard operation when the hypothesis is
available.
co-authored by @tobiasgrosser
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
