This PR implements a new E-matching pattern inference procedure that is
faithful to the behavior documented in the reference manual regarding
minimal indexable subexpressions. The old inference procedure was
failing to enforce this condition. For example, the manual documents
`[grind ->]` as follows
`[@grind →]` selects a multi-pattern from the hypotheses of the theorem.
In other words, `grind` will use the theorem for forwards reasoning.
To generate a pattern, it traverses the hypotheses of the theorem from
left to right. Each time it encounters a **minimal indexable
subexpression** which covers an argument which was not previously
covered, it adds that subexpression as a pattern, until all arguments
have been covered.
That said, the new procedure is currently disabled, and the following
option must be used to enable it.
```
set_option backward.grind.inferPattern false
```
Users can inspect differences between the old a new procedures using the
option
```
set_option backward.grind.checkInferPatternDiscrepancy true
```
Example:
```lean
/--
warning: found discrepancy between old and new `grind` pattern inference procedures, old:
[@List.length #2 (@toList _ #1#0)]
new:
[@toList #2#1#0]
use `set_option backward.grind.inferPattern true` to force old procedure
-/
#guard_msgs in
set_option backward.grind.checkInferPatternDiscrepancy true in
@[grind] theorem Vector.length_toList' (xs : Vector α n) : xs.toList.length = n := by sorry
```
This PR upstreams the Verso parser and adds preliminary support for
Verso in docstrings. This will allow the compiler to check examples and
cross-references in documentation.
After a `stage0` update, a follow-up PR will add the appropriate
attributes that allow the feature to be used. The parser tests from
Verso also remain to be upstreamed, and user-facing documentation will
be added once the feature has been used on more internals.
This PR completes the `grind` solver extension design and ports the
`grind ac` solver to the new framework. Future PRs will document the API
and port the remaining solvers. An additional benefit of the new design
is faster build times.
This PR adds infrastructure for registering new `grind` solvers. `grind`
already includes many solvers, and this PR is the first step toward
modularizing the design and supporting user-defined solvers.
This PR adds “non-branching case statements”: For each inductive
constructor `T.con` this adds a function `T.con.with` that is similar
`T.casesOn`, but has only one arm (the one for `con`), and an additional
`t.toCtorIdx = 12` assumption.
For example:
```lean
inductive Vec (α : Type) : Nat → Type where
| nil : Vec α 0
| cons {n} : α → Vec α n → Vec α (n + 1)
/--
info: @[reducible] protected def Vec.cons.elim.{u} : {α : Type} →
{motive : (a : Nat) → Vec α a → Sort u} →
{a : Nat} →
(t : Vec α a) →
t.ctorIdx = 1 → ({n : Nat} → (a : α) → (a_1 : Vec α n) → motive (n + 1) (Vec.cons a a_1)) → motive a t
-/
#guard_msgs in
#print sig Vec.cons.elim
```
This is a building block for non-quadratic implementations of `BEq` and
`DecidableEq` etc.
Builds on top of #9951.
The compiled code for a these functions could presumably, without
branching on the inductive value, directly access the fields. Achieving
this optimization (and achieving it without a quadratic compilation
cost) is not in scope for this PR.
This PR adds a private `Lean.Name.getUtf8Byte'` to `Init.Meta` for a
future PR that optimizes `Lean.Name.escapePart`.
`Lean.Name.getUtf8Byte'` should be replaced with `String.getUtf8Byte`
once the string refactor is through.
This PR makes the generation of functional induction principles more
robust when the user `let`-binds a variable that is then `match`'ed on.
Fixes#10132.
this PR reorders the `DiscrTree.Key` constructors to match the order
given in the manually written `DiscrTree.Key.ctorIdx`. This allows us to
use the auto-generated one, and moreover lets this code benefit from
special compiler support for `.ctorIdx`, once that lands.
This PR generates `.ctorIdx` functions for all inductive types, not just
enumeration types. This can be a building block for other constructions
(`BEq`, `noConfusion`) that are size-efficient even for large
inductives.
It also renames it from `.toCtorIdx` to `.ctorIdx`, which is the more
idiomatic naming.
The old name exists as an alias, with a deprecation attribute to be
added after the next
stage0 update.
These functions can arguably compiled down to a rather efficient tag
lookup, rather than a `case` statement. This is future work (but
hopefully near future).
For a fair number of basic types the compiler is not able to compile a
function using `casesOn` until further definitions have been defined.
This therefore (ab)uses the `genInjectivity` flag and
`gen_injective_theorems%` command to also control the generation of this
construct.
For (slightly) more efficient kernel reduction one could use `.rec`
rather than `.casesOn`. I did not do that yet, also because it
complicates compilation.
This PR allows for more fine-grained control over what derived instances
have exposed definitions under the module system: handlers should not
expose their implementation unless either the deriving item or a
surrounding section is marked with `@[expose]`. Built-in handlers to be
updated after a stage 0 update.
This PR adds a stop position field to parser input contexts, allowing
the parser to be instructed to stop parsing prior to the end of a file.
This is step 1, prior to a stage0 update, to make run-time data
structures sufficiently compatible to avoid segfaults. After the update,
the actual code to stop parsing can be merged.
This PR enables core's `LakeMain` to be a `module` when core is built
without `USE_LAKE`.
This was a problem when porting Lake to the module system (#9749).
This PR changes Lake to not set `LEAN_GITHASH` when in core (i.e.
`bootstrap = true`). This avoids Lake rebuilding modules when the Lake
watchdog is on one build of Lean/Lake and the command line is on a
different one.
