This PR optimizes the proof terms produced by `grind linarith`. It is
similar to #9945, but for the `linarith` module in `grind`.
It removes unused entries from the context objects when generating the
final proof, significantly reducing the amount of junk in the resulting
terms.
This PR optimizes the proof terms produced by `grind cutsat`. It removes
unused entries from the context objects when generating the final proof,
significantly reducing the amount of junk in the resulting terms.
Example:
```lean
/--
trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
let ctx := RArray.leaf (f 2);
let p_1 := Poly.add 1 0 (Poly.num 0);
let p_2 := Poly.add (-1) 0 (Poly.num 1);
let p_3 := Poly.num 1;
le_unsat ctx p_3 (eagerReduce (Eq.refl true)) (le_combine ctx p_2 p_1 p_3 (eagerReduce (Eq.refl true)) h_8 h_1)
-/
#guard_msgs in -- Context should contain only `f 2`
open Lean Int Linear in
set_option trace.grind.debug.proof true in
example (f : Nat → Int) :
f 1 <= 0 → f 2 <= 0 → f 3 <= 0 → f 4 <= 0 → f 5 <= 0 →
f 6 <= 0 → f 7 <= 0 → f 8 <= 0 → -1 * f 2 + 1 <= 0 → False := by
grind
```
This PR expands `mvcgen using invariants | $n => $t` to `mvcgen; case
inv<$n> => exact $t` to avoid MVar instantiation mishaps observable in
the test case for #9581.
Closes#9581.
This PR implements extended `induction`-inspired syntax for `mvcgen`,
allowing optional `using invariants` and `with` sections.
```lean
mvcgen
using invariants
| 1 => Invariant.withEarlyReturn
(onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
(onContinue := fun traversalState seen =>
⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
with mleave -- mleave is a no-op here, but we are just testing the grammar
| vc1 => grind
| vc2 => grind
| vc3 => grind
| vc4 => grind
| vc5 => grind
```
This PR guards the `Std.Tactic.Do.MGoalEntails` delaborator by a check
ensuring that there are at least 3 arguments present, preventing
potential panics.
This PR fixes the `forIn` function, that previously caused the resulting
Promise to be dropped without a value when an exception was thrown
inside of it. It also corrects the parameter order of the `background`
function.
This PR changes `internalizeCode` to replace all substitutions with
non-param-bound fvars in `Expr`s (which are all types) with `lcAny`,
preserving the invariant that there are no such dependencies. The
violation of this invariant across files caused test failures in a
pending PR, but it is difficult to write a direct test for it. In the
future, we should probably change the LCNF checker to detect this.
This change also speeds up some compilation-heavy benchmarks much more
than I would've expected, which is a pleasant surprise. This indicates
we might get more speedups from reducing the amount of type information
we preserve in LCNF.
This PR fixes a panic in the delaborator for `Std.PRange`. It also
modifies the delaborators for both `Std.Range` and `Std.PRange` to not
use `let_expr`, which cleans up annotations and metadata, since
delaborators must follow the structures of expressions. It adds support
for `pp.notation` and `pp.explicit` options. It also adds tests for
these delaborators.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
This PR adds a guard for a delaborator that is causing panics in
doc-gen4. This is a band-aid solution for now, and @sgraf812 will take a
look when they're back from leave.
This PR ensures `grind cutsat` does not rely on div/mod terms to have
been normalized. The `grind` preprocessor has normalizers for them, but
sometimes they cannot be applied because of type dependencies.
Closes#9907
This PR addresses a missing check in the module system where private
names that remain in the public environment map for technical reasons
(e.g. inductive constructors generated by the kernel and relied on by
the code generator) accidentally were accessible in the public scope.
This PR reviews `grind` annotations for `Option`, preferring to use
`@[grind =]` instead of `@[grind]` (and fixing a few problems revealed
by this), and making sure `@[grind =]` theorems are "fully applied".
This PR lets the unused simp argument linter explain that the given hint
of removing `←` arguments may be too strong, and that replacing them
with `-` arguments can be needed. Fixes#9909.
This PR adds a JSON schema for `lakefile.toml`. Importantly, this schema
is *not* intended for validating `lakefile.toml`, but is instead
optimized for auto-completion and hovers using the [Even Better
TOML](https://marketplace.visualstudio.com/items?itemName=tamasfe.even-better-toml)
VS Code extension.
Once merged, I will attempt to contribute a link to this schema to the
[JSON Schema store](https://github.com/SchemaStore/schemastore). When
that is done, we can integrate the Lean 4 VS Code extension with Even
Better TOML, providing us with language server support in
`lakefile.toml`.
The schema contributed by this PR has the following known deficiencies:
- Superfluous properties do not produce an error.
- The structure of complicated structures (e.g. path or version
patterns) is deliberately not accurately reflected in the schema. Even
Better TOML doesn't seem to handle these structures well in
auto-completion.
- Due to the lack of an accurate declarative spec of the lakefile.toml
format and several deviations from the format to provide better
auto-completions, this schema will have to be kept in sync manually with
the code in Lake, at least for now.
This PR ensures that `Nat.cast` and `Int.cast` of numerals are
normalized by `grind`.
It also adds a `simp` flag for controlling how bitvector literals are
represented. By default, the bitvector simprocs use `BitVec.ofNat`. This
representation is problematic for the `grind ring` and `grind cutsat`
modules. The new flag allows the use of `OfNat.ofNat` and `Neg.neg` to
represent literals, consistent with how they are represented for other
commutative rings.
Closes#9321
This PR improves the heuristic used to select patterns for local
`forall` expressions occurring in the goal being solved by `grind`. It
now considers all singleton patterns in addition to the selected
multi-patterns. Example:
```lean
example (p : Nat → Prop) (h₁ : x < n) (h₂ : ¬ p x) : ∃ i, i < n ∧ ¬ p i := by
grind
```
This PR makes `mvcgen` aggressively eta-expand before trying to apply a
spec. This ensures that `mspec` will be able to frame hypotheses
involving uninstantiated loop invariants in goals for the inductive step
of a loop instead of losing them in a destructive world update.
This PR moves `List.range'_elim` to `List.eq_of_range'_eq_append_cons`
and adds a couple of `grind` annotations for `List.range'`. This will
make it more convenient to work with proof obligations produced by
`mvcgen`.
