This PR makes `fun_induction` and `fun_cases` (try to) unfold the
function application of interest in the goal. The old behavior can be
enabled with `set_option tactic.fun_induction.unfolding false`. For
`fun_cases` this does not work yet when the function’s result type
depends on one of the arguments, see issue #8296.
This PR makes it possible for `bv_decide` to tackle situations for its
enum type preprocessing where the enums themselves are use in a
dependently type context (for example inside of a `GetElem` body) and
thus not trivially accessible to `simp` for rewriting. To do this we
drop`GetElem` on `BitVec` as well as `dite` as early as possible in the
pipeline.
This PR lets `cases` fail gracefully when the motive has an complex
argument whose type is dependent type on the targets. While the
`induction` tactic can handle this well, `cases` does not. This change
at least gracefully degrades to not instantiating that motive parameter.
See issue #8296 for more details on this issue.
This PR improves the generation of `.induct_unfolding` by rewriting
`match` statements more reliably, using the new “congruence equations”
introduced in #8284. Fixes#8195.
This PR adds a new variant of equations for matchers, namely “congruence
equations” that generalize the normal matcher equations. They have
unrestricted left-hand-sides, extra equality assumptions relating the
discriminiants with the patterns and thus prove heterogenous equalities.
In that sense they combine congruence with rewriting. They can be used
to rewrite matcher applications where, due to dependencies, `simp` would
fail to rewrite the discriminants, and will be used when producing the
unfolding induction theorems.
This PR optimizes lean_nat_shiftr for scalar operands. The new compiler
converts Nat divisions into right shifts, so this now shows up as hot in
some profiles.
This PR improves the type-as-hole error message. Type-as-hole error for
theorem declarations should not admit the possibility of omitting the
type entirely.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR changes `addPPExplicitToExposeDiff` to show universe differences
and to visit into projections, e.g.:
```
error: tactic 'rfl' failed, the left-hand side
(Test.mk (∀ (x : PUnit.{1}), True)).1
is not definitionally equal to the right-hand side
(Test.mk (∀ (x : PUnit.{2}), True)).1
```
for
```lean
inductive Test where
| mk (x : Prop)
example : (Test.mk (∀ _ : PUnit.{1}, True)).1 = (Test.mk (∀ _ : PUnit.{2}, True)).1 := by
rfl
```
This PR makes `#guard_msgs` to treat `trace` messages separate from
`info`, `warning` and `error`. It also introduce the ability to say
`#guard_msgs (pass info`, like `(drop info)` so far, and also adds
`(check info)` as the explicit form of `(info)`, for completeness.
Fixes#8266
This PR adjusts the error message when `apply` fails to unify. It is
clearer about distinguishing the term being applied and the goal, as
well as distinguishing the "conclusion" of the given term and the term
itself.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR rewords the `application type mismatch` error message by more
specifically mentioning that the problem is with the final argument.
This is useful when the same argument is passed to the function multiple
times.
We decided against using a wording which specifically mentions the
"function expression", because users who are not used to currying might
not think of the `f a` in `f a b` as a function.
This PR adds additional infrastructure for error message formatting.
Specifically, it adds convenience formatters for hints and notes,
including the ability to attach code actions to hint messages using a
"Try This"-like widget, along with several convenience formatters for
message data.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR fixes unintended inlining of `ToJson`, `FromJson`, and `Repr`
instances, which was causing exponential compilation times in `deriving`
clauses for large structures.
This PR omits cases from functional induction/cases principles that are
implemented `by contradiction` (or, more generally, `False.elim`,
`absurd` or `noConfusion). Breaking change in the sense that there are
fewer goals to prove after using functional induction.
Fixes#8103.
This PR changes the behaviour of `apply?` so that the `sorry` it uses to
close the goal is non-synthetic. (Recall that correct use of synthetic
sorries requires that the tactic also generates an error message, which
we don't want to do in this situation.) Either this PR or #8230 are
sufficient to defend against the problem reported in #8212.
This PR adds the `--setup` option to the `lean` CLI. It takes a path to
a JSON file containing information about a module's imports and
configuration, superseding that in the module's own file header. This
will be used by Lake to specify paths to module artifacts (e.g., oleans
and ileans) separate from the `LEAN_PATH` schema.
To facilitate JSON serialization of the header data structure, `NameMap`
JSON instances have been added to core, and `LeanOptions` now makes use
of them.
This PR fixes an issue in the theory propagation used in `grind`. When
two equivalence classes are merged, the core may need to push additional
equalities or disequalities down to the satellite theory solvers (e.g.,
`cutsat`, `comm ring`, etc). Some solvers (e.g. `cutsat`) assume that
all of the core’s invariants hold before they receive those facts.
Propagating immediately therefore risks violating a solver’s
pre-conditions midway through the merge. To decouple the merge operation
from propagation and to keep the core solver-agnostic, this PR adds the
helper type `PendingTheoryPropagation`.
This PR improves the E-matching pattern inference procedure in `grind`.
Consider the following theorem:
```lean
@[grind →]
theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ∧ ys = #[] :=
append_eq_empty_iff.mp h
```
Before this PR, `grind` inferred the following pattern:
```lean
@HAppend.hAppend _ _ _ _ #2#1
```
Note that this pattern would match any `++` application, even if it had
nothing to do with arrays. With this PR, the inferred pattern becomes:
```lean
@HAppend.hAppend (Array #3) (Array _) (Array _) _ #2#1
```
With the new pattern, the theorem will not be considered by `grind` for
goals that do not involve `Array`s.
This PR implements **stepwise proof terms** in the commutative ring
procedure used by `grind`. These terms serve as an alternative
representation to the traditional Nullstellensatz certificates, aiming
to address the **exponential worst-case complexity** often associated
with certificate construction.
While various compression techniques for Nullstellensatz certificates
exist, they are not implemented in our procedure. Moreover, many of
these techniques rely on additional properties not available in
arbitrary commutative rings. In contrast, the stepwise proof terms
encode the **actual derivation** used during simplification, offering
significantly better scalability in practice.
Here is a motivating example:
```lean
example {α} [CommRing α] [IsCharP α 0] (d t c : α) (d_inv PSO3_inv : α)
(Δ40 : d^2 * (d + t - d * t - 2) * (d + t + d * t) = 0)
(Δ41 : -d^4 * (d + t - d * t - 2) *
(2 * d + 2 * d * t - 4 * d * t^2 + 2 * d * t^4 + 2 * d^2 * t^4 - c * (d + t + d * t)) = 0)
(_ : d * d_inv = 1)
(_ : (d + t - d * t - 2) * PSO3_inv = 1) :
t^2 = t + 1 := by grind +ring
```
In this case, the Nullstellensatz certificate generated by our procedure
contains **over 20,000 terms**, which overwhelms the Lean kernel during
verification. @kim-em also computed certificates using Mathematica with
various variable orderings, producing results between **500 and 2,000
terms**: still quite large.
By switching to stepwise derivations:
- `grind` completes the goal in **under 10 ms**
- The Lean kernel checks the resulting proof term in **under 1 second**
This change dramatically improves both the performance and robustness of
`grind` for nontrivial algebraic goals.
This PR adds support for inductive and coinductive predicates defined
using lattice theoretic structures on `Prop`. These are syntactically
defined using `greatest_fixpoint` or `least_fixpoint` termination
clauses for recursive `Prop`-valued functions. The functionality relies
on `partial_fixpoint` machinery and requires function definitions to be
monotone. For non-mutually recursive predicates, an appropriate
(co)induction proof principle (given by Park induction) is generated.
Summary of changes:
- `Interal.Order.Basic` now contains `CompleteLattice` class, as well as
version of Knaster-Tarski fixpoint theorem (with an associated Park
induction principle) for the internal use for defining (co)inductive
predicates. `Prop` is shown to have two complete lattice structures (one
given by implication order for defining inductive predicates, and one
given by reverse implication for defining coinductive predicates).
Additionally, proofs that lattices are closed under products and
function spaces are included.
- Partial fixpoint's `EqnInfo` now additionally carries an information
whether something is defined as a lattice-theoretic fixpoint or via
CCPOs.
- When constructing a (co)inductive predicate,`PartialFixpoint/Main`
builds an appropriate lattice structure on the type of the predicate
using product lattice, function space lattice and an appropriate lattice
instance on `Prop`.
- `PartialFixpoint/Eqns` is modified to be able to perform rewrite under
lattice-theoretic fixpoint construction
- `PartialFixpoint/Induction`contains a case split for handling of the
(co)inductive predicates. In the case of lattice-theoretic fixpoints, it
appropriately desugars the Park induction principle.
This PR adds support for the following import variants to the
experimental module system:
* `private import`: Makes the imported constants available only in
non-exported contexts such as proofs. In particular, the import will not
be loaded, or required to exist at all, when the current module is
imported into other modules.
* `import all`: Makes non-exported information such as proofs of the
imported module available in non-exported contexts in the current
module. Main purpose is to allow for reasoning about imported
definitions when they would otherwise be opaque. TODO: adjust name
resolution so that imported `private` decls are accessible through
syntax.
They can be combined into `private import all`, which will likely be the
most common usage of `import all`.
This PR lets `induction` accept eliminator where the motive application
in the conclusion has complex arguments; these are abstracted over using
`kabstract` if possible. This feature will go well with unfolding
induction principles (#8088).
This PR adds simprocs to simplify appends of non-overlapping Bitvector
adds. We add a simproc instead of just a `simp` lemma to ensure that we
correctly rewrite bitvector appends. Since bitvector appends lead to
computation at the bitvector width level, it seems to be more stable to
write a simproc.
As I write this, I realize that I can maybe write the `simp` lemma using
`no_index` to recover the same behaviour, so I'll try that too.
This PR fixes a bug when constructing the proof term for a
Nullstellensatz certificate produced by the new commutative ring
procedure in `grind`. The kernel was rejecting the proof term.
