This PR adds the options `pp.piBinderNames` and
`pp.piBinderNames.hygienic`. Enabling `pp.piBinderNames` causes
non-dependent pi binder names to be pretty printed, rather than be
omitted. When `pp.piBinderNames.hygienic` is false (the default) then
only non-hygienic such biner names are pretty printed. Setting `pp.all`
enables `pp.piBinderNames` if it is not otherwise explicitly set.
Implementation note: this is exposing the secret pretty printer option
`pp.piBinderNames` that was being used within the signature pretty
printer.
Closes#1134.
This PR fixes a few bugs in the `rw` tactic: it could "steal" goals
because they appear in the type of the rewrite, it did not do an occurs
check, and new proof goals would not be synthetic opaque. This PR also
lets the `rfl` tactic assign synthetic opaque metavariables so that it
is equivalent to `exact rfl`.
Implementation note: filtering old vs new is not sufficient. This PR
partially addresses the bug where the rw tactic creates natural
metavariables for each of the goals; now new proof goals are synthetic
opaque.
Metaprogramming API: Instead of `Lean.MVarId.rewrite` prefer
`Lean.Elab.Tactic.elabRewrite` for elaborating rewrite theorems and
applying rewrites to expressions.
Closes#10172
This PR adds a `pp.unicode` option and a `unicode("→", "->")` syntax
description alias for the lower-level `unicodeSymbol "→" "->"` parser.
The syntax is added to the `notation` command as well. When `pp.unicode`
is true (the default) then the first form is used when pretty printing,
and otherwise the second ASCII form is used. A variant, `unicode("→",
"->", preserveForPP)` causes the `->` form to be preferred; delaborators
can insert `→` directly into the syntax, which will be pretty printed
as-is; this allows notations like `fun` to use custom options such as
`pp.unicode.fun` to opt into the unicode form when pretty printing.
Additionally:
- Adds more documentation for the `symbol` and `nonReservedSymbol`
parser descriptions.
- Adds documentation for the
`infix`/`infixr`/`infixl`/`prefix`/`postfix` commands.
- The parenthesizers for symbols are improved to backtrack if the atom
doesn't match.
- Fixes a bug where `&"..."` symbols aren't validated.
This is partial progress for issue #1056. What remains is enabling
`unicode(...)` for mixfix commands and then making use of it for core
notation.
This PR explicitly imports `Lake.Util` submodules in `Lake`, ensuring
Lake utilities are consistently available by default in configuration
files.
It also simplifies the Lake globs for the core build to ensure all Lake
submodules are built (even if they are not imported).
This PR ensures that the infotree recognizes `Classical.propDecidable`
as an instance, when below a `classical` tactic.
The `classical` tactic modifies the environment that the subsequent
sequence of tactics runs in (by making `Classical.propDecidable` an
instance). However, it does not add a corresponding `InfoTree.context`
node, so its effects are not visible when we want to replay a tactic
sequence (for example when running a tactic in the tactic analysis
framework). We should add a call to `Lean.Elab.withSafeInfoContext` to
remedy this issue.
There are two potential places to add this class: in the meta-level
`Lean.Elab.Tactic.classical` wrapper, or the tactic-level
`evalClassical` tactic elaborator. I chose the latter since meta-level
does not have access to info tree operations (unless we add many
parameters to `Lean.Elab.Tactic.classical`: `[MonadNameGenerator m]
[MonadOptions m] [MonadMCtx m] [MonadResolveName m] [MonadFileMap m]`).
A testcase that uses the tactic analysis framework is available here:
https://github.com/leanprover-community/mathlib4/pull/29501
This PR adds syntax for defining compile-time initializers under the
module system, with other initializers to be restricted from running at
compile time in a follow-up PR.
This PR uses the per-constructor `noConfusion` principles (from #10315)
in the `mkNoConfusion` app builder, if possible. This means they are
used by `injection`, `grind`, `simp` and other places. This brings
notable performance improvements when dealing with inductives with a
large number of constructors.
This PR adds `T.ctor.noConfusion` declarations, which are
specializations of `T.noConfusion` to equalities between `T.ctor`. The
point is to avoid reducing the `T.noConfusionType` construction every
time we use `injection` or a similar tactic.
```lean
Vec.cons.noConfusion.{u_1, u} {α : Type u} (P : Sort u_1) {n : Nat}
(x : α) (xs : Vec α n) (x' : α) (xs' : Vec α n)
(h : Vec.cons x xs = Vec.cons x' xs')
(k : n = n → x = x' → xs ≍ xs' → P) : P
```
The constructions are not as powerful as `T.noConfusion` when the
indices of the inductive type are not just constructor parameters (or
constructor applications of these parameters), so the full
`T.noConfusion` construction is still needed as a fallback.
It may seem costly to generate these eagerly, but given that we eagerly
generate injectivity theorems already, and we will use them there, it
seems reasonable for now.
To further reduce the cost, we only generate them for constructors with
fields (for others, the `T.noConfusion` theorem doesn't provide any
information), and we use `macro_inline` to prevent the compiler from
creating code for these, given that the compiler has special support for
`T.noConfusion` that we want it to use).
An earlier version of this PR also removed trivial equations and
un-HEq-ed others, leading to
```
(k : x = x' → xs = xs' → P)
```
in the example above. I backed out of that change, as it makes it harder
for tactics like `injectivity` to know how often to `intro`, so better
to keep things uniform.
This PR adds range support to`BitVec` and the `UInt*` types. This means
that it is now possible to write, for example, `for i in (1 : UInt8)...5
do`, in order to loop over the values 1, 2, 3 and 4 of type `UInt8`.
This PR adds more lemmas about the `toList` and `toArray` functions on
ranges and iterators. It also renames `Array.mem_toArray` into
`List.mem_toArray`.
This PR adds the type `Std.Internal.Parsec.Error`, which contains the
constructors `.eof` (useful for checking if parsing failed due to not
having enough input and then retrying when more input arrives that is
useful in the HTTP server) and `.other`, which describes other errors.
It also adds documentation to many functions, along with some new
functions to the `ByteArray` Parsec, such as `peekWhen?`, `octDigit`,
`takeWhile`, `takeUntil`, `skipWhile`, and `skipUntil`.
This PR is followup to the change in grind pattern heuristics from
#10342, typically resolving the discrepancy by writing out an explicit
`grind_pattern` for the intended pattern. The new behaviour is more
aggressive, because it selects smaller patterns.
This PR allows the interpreter to jump to native code of `[export]`
declarations, which can increase performance as well as the
effectiveness of `interpreter.prefer_native=true` during bootstrapping.
This PR reimplements `mkNoConfusionType` in lean, thus removing the
remaining C code related to this construction.
Also uses the ctor elimination principles only when there are more than
three ctors.
This PR completes the review of `@[grind]` annotations without a sigil
(e.g. `=` or `←`), replacing most of them with more specific annotations
or patterns.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
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 moves the definitions and basic facts about `Function.Injective`
and `Function.Surjective` up from Mathlib. We can do a better job of
arguing via injectivity in `grind` if these are available.
This PR updates `@[grind]` annotations which should be `@[grind =]`, for
robustness (and, presumably, in some fraction of cases the existing
heuristic for `@[grind]` is already too liberal).
This PR shares common functionality relate to equalities between same
constructors, and when these are type-correct. In particular it uses the
more complete logic from `mkInjectivityThm` also in other places, such
as `CasesOnSameCtor` and the deriving code for `BEq`, `DecidableEq`,
`Ord`, for more consistency and better error messages.
This PR implements `mkNoConfusionImp` in Lean rather than in C. This
reduces our reliance on C, and may bring performance benefits from not
reducing `noConfusionType` during elaboration time (it still gets
reduced by the kernel when type-checking).
This PR makes it possible to write custom interpolation notation which
treats interpolated `String`s specially.
Sometimes it is desirable for `let w := "world"; foo!"hello {w}"` and
`foo!"hello world"` to mean different things; for instance, if debugging
and wanting to show all interpolands with `repr`. The current approach
forces `hello` to also be rendered with `repr`, which is not desirable.
This doesn't modify any existing formatters.
Requested in [#lean4 > ✔ dbg_trace should use `Repr` instance @
💬](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.E2.9C.94.20dbg_trace.20should.20use.20.60Repr.60.20instance/near/495082575)
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
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 fixes a performance issue in `grind linarith`. It was creating
unnecessary `NatModule`/`IntModule` structures for commutative rings
without an order. This kind of type should be handled by `grind ring`
only.
This PR implements model-based theory combination for types `A` which
implement the `ToInt` interface. Examples:
```lean
example {C : Type} (h : Fin 4 → C) (x : Fin 4)
: 3 ≤ x → x ≤ 3 → h x = h (-1) := by
grind
example {C : Type} (h : UInt8 → C) (x y z w : UInt8)
: y + 1 + w ≤ x + w → x + w ≤ z → z ≤ y + w + 1 → h (x + w) = h (y + w + 1) := by
grind
example {C : Type} (h : Fin 8 → C) (x y w r : Fin 8)
: y + 1 + w ≤ r → r ≤ y + w + x → x = 1 → h r = h (y + w + 1) := by
grind
```
This PR removes `grind →` annotations that fire too often, unhelpfully.
It would be nice for `grind` to instantiate these lemmas, but only if
they already see `xs ++ ys` and `#[]` in the same equivalence class, not
just as soon as it sees `xs ++ ys`.
In the meantime, let's see what is using these.
This PR introduces limited functionality frontends `cutsat` and
`grobner` for `grind`. We disable theorem instantiation (and case
splitting for `grobner`), and turn off all other solvers. Both still
allow `grind` configuration options, so for example one can use `cutsat
+ring` (or `grobner +cutsat`) to solve problems that require both.
For `cutsat`, it is helpful to instantiate a limited set of theorems
(e.g. `Nat.max_def`). Currently this isn't supported, but we intend to
add this later.
