This PR fixes an issue when running Mathlib's `FintypeCat` as code,
where an erased type former is passed to a polymorphic function. We were
lowering the arrow type to`object`, which conflicts with the runtime
representation of an erased value as a tagged scalar.
This PR modifies the generation of induction and partial correctness
lemmas for `mutual` blocks defined via `partial_fixpoint`. Additionally,
the generation of lattice-theoretic induction principles of functions
via `mutual` blocks is modified for consistency with `partial_fixpoint`.
The lemmas now come in two variants:
1. A conjunction variant that combines conclusions for all elements of
the mutual block. This is generated only for the first function inside
of the mutual block.
2. Projected variants for each function separately
## Example 1
```lean4
axiom A : Type
axiom B : Type
axiom A.toB : A → B
axiom B.toA : B → A
mutual
noncomputable def f : A := g.toA
partial_fixpoint
noncomputable def g : B := f.toB
partial_fixpoint
end
```
Generated `fixpoint_induct` lemmas:
```lean4
f.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_1 f
g.fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1)
(adm_2 : admissible motive_2) (h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA)
(h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) : motive_2 g
```
Mutual (conjunction) variant:
```lean4
f.mutual_fixpoint_induct (motive_1 : A → Prop) (motive_2 : B → Prop) (adm_1 : admissible motive_1) (adm_2 : admissible motive_2)
(h_1 : ∀ (g : B), motive_2 g → motive_1 g.toA) (h_2 : ∀ (f : A), motive_1 f → motive_2 f.toB) :
motive_1 f ∧ motive_2 g
```
## Example 2
```lean4
mutual
def f (n : Nat) : Option Nat :=
g (n + 1)
partial_fixpoint
def g (n : Nat) : Option Nat :=
if n = 0 then .none else f (n + 1)
partial_fixpoint
end
```
Generated `partial_correctness` lemmas (in a projected variant):
```lean4
f.partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r)
(n r✝ : Nat) : f n = some r✝ → motive_1 n r✝
g.partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r)
(n r✝ : Nat) : g n = some r✝ → motive_2 n r✝
```
Mutual (conjunction) variant:
```
f.mutual_partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
(h_1 :
∀ (g : Nat → Option Nat),
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
(h_2 :
∀ (f : Nat → Option Nat),
(∀ (n r : Nat), f n = some r → motive_1 n r) →
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r) :
(∀ (n r : Nat), f n = some r → motive_1 n r) ∧ ∀ (n r : Nat), g n = some r → motive_2 n r
```
This PR modifies `intro` to create tactic info localized to each
hypothesis, making it possible to see how `intro` works
variable-by-variable. Additionally:
- The tactic supports `intro rfl` to introduce an equality and
immediately substitute it, like `rintro rfl` (recall: the `rfl` pattern
is like doing `intro h; subst h`). The `rintro` tactic can also now
support `HEq` in `rfl` patterns if `eq_of_heq` applies.
- In `intro (h : t)`, elaboration of `t` is interleaved with unification
with the type of `h`, which prevents default instances from causing
unification to fail.
- Tactics that change types of hypotheses (including `intro (h : t)`,
`delta`, `dsimp`) now update the local instance cache.
In `intro x y z`, tactic info ranges are `intro x`, `y`, and `z`. The
reason for including `intro` with `x` is to make sure the info range is
"monotonic" while adding the first argument to `intro`.
This PR cleans up `optParam`/`autoParam`/etc. annotations before
elaborating definition bodies, theorem bodies, `fun` bodies, and `let`
function bodies. Both `variable`s and binders in declaration headers are
supported.
There are no changes to `inductive`/`structure`/`axiom`/etc. processing,
just `def`/`theorem`/`example`/`instance`.
This PR ensures that equations in the `grind cutsat` module are
maintained in solved form. That is, given an equation `a*x + p = 0` used
to eliminate `x`, the linear polynomial `p` must not contain other
eliminated variables. Before this PR, equations were maintained in
triangular form. We are going to use the solved form to linearize
nonlinear terms.
This PR removes the option `grind +ringNull`. It provided an alternative
proof term construction for the `grind ring` module, but it was less
effective than the default proof construction mode and had effectively
become dead code.
This PR also optimizes semiring normalization proof terms using the
infrastructure added in #9946.
**Remark:** After updating stage0, we can remove several background
theorems from the `Init/Grind` folder.
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 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 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 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 is initially motivated by noticing `Lean.Grind.Preorder.toLE`
appearing in long Mathlib typeclass searches; this change will prevent
these searches. These changes are also helpful preparation for
potentially dropping the custom `Lean.Grind.*` typeclasses, and unifying
with the new typeclasses introduced in #9729.
This PR adds improved support for proof-by-reflection to the kernel type
checker. It addresses the performance issue exposed by #9854. With this
PR, whenever the kernel type-checks an argument of the form `eagerReduce
_`, it enters "eager-reduction" mode. In this mode, the kernel is more
eager to reduce terms. The new `eagerReduce _` hint is often used to
wrap `Eq.refl true`. The new hint should not negatively impact any
existing Lean package.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
