This PR adds the lemma `Acc.inv_of_transGen`, a generalization of
`Acc.inv`. While `Acc.inv` shows that `Acc r x` implies `Acc r y` given
that `r y x`, the new lemma shows that this also holds if `y` is only
*transitively* related to `x`.
This PR sets the `irreducible` attribute before generating the equations
for recursive definitions. This prevents these equations to be marked as
`defeq`, which could lead to `simp` generation proofs that do not type
check at default transparency.
This issue is surfacing more easily since well-founded recursion on
`Nat` is implemented with a dedicated fix point operator (#7965). Before
that, `WellFounded.fix` was used, which is inherently not reducing, so
we did get the desired result even without the explicit reducibility
setting.
Fixes#12398.
This PR refactors the main loop of the `cbv` tactic. Rather than using
multiple simprocs, a central pre simproc is introduced. Moreover, let
expressions are no longer immediately zeta-reduced due to performance on
one of the benchmarks (`leroy.lean`).
Stacked on top of #12416
This PR introduces `Rat.abs` and adds missing lemmas about `Int` and
`Rat`.
For `Int`:
- Lemmas about the interaction of negation and order: `neg_le_iff`,
`le_neg_iff`, `neg_lt_iff`, `lt_neg_iff`
For `Rat`:
- Declaration of `Rat.abs`
- Lemmas for `Rat.abs`, `Rat.floor` and `Rat.ceil`
- More basic lemmas that would all be provable with `grind` but might
still be good to have in the library
- Type class instances: `Std.Associative`, `Std.Commutative`,
`Std.LawfulIdentity` for addition
This PR adds a finishing `decide_cbv` tactic, which applies
`of_decide_eq_true` and then tries to discharge the remaining goal using
`cbv`.
Stacked on top of #12408.
---------
Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>
This PR adds caching to `replaceRecApps`, the procedure responsible for
replacing recursive applications for wellfounded recursion, improving
performance when many references to the same recursive call exist, e.g.
when recursive calls exist in proof terms.
Closes#12404
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR adds a user facing `cbv` tactic that can be used outside of the
`conv` mode.
Example usage:
```lean4
example : "hello" ++ " " ++ "world" = "hello world" := by cbv
```
---------
Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>
This PR gives a proof of `LawfulToForwardSearcherModel` for `Slice`
patterns, which amounts to proving that our implementation of KMP is
correct.
Note that this PR also changes the KMP implementation to make it
slightly more efficient and easier to verify. I also have a correctness
proof for the old implementation, so there were no bugs in the old
implementation.
This PR fixes a bug in `mvcgen` caused by incomplete `match` splitting.
In particular, if a program `match s with ...` matches on a state
variable `s` (presumably the result of a call to `get`), then `s` will
also occur in the stateful goal `H ⊢ₛ wp⟦match s with ...⟧ Q s`
*outside* the program expression; this was not anticipated before.
This PR adds `LawfulOrderOrd` instances for `Nat`, `Int`, and all
fixed-width integer types (`Int8`, `Int16`, `Int32`, `Int64`, `ISize`,
`UInt8`, `UInt16`, `UInt32`, `UInt64`, `USize`). These instances
establish that the `Ord` instances for these types are compatible with
their `LE` instances. Additionally, this PR adds a few missing lemmas
and `grind` patterns.
This PR changes the alters the file format of outputs stored in the
local Lake cache to include an identifier indicating the service (if
any) the output came from. This will be used to enable lazily
downloading artifacts on-demand during builds.
This PR adds comprehensive test running instructions to
`.claude/CLAUDE.md`,
replacing the single `test_single.sh` example with the full range of
test
commands documented in `doc/dev/testing.md`: full suite, filtered by
name,
rerun failures, and direct ctest usage.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR is similar to #12403.
We previously conjectured that "all type class fields that are types
should be marked as reducible." The problem is that propositions are
types, but they are also used as data (with `Decidable`). For example,
we often see the proposition `x <= y` as a Boolean. So, we refined the
conjecture to:
"All type class fields that are types (and not propositions) should be
marked as reducible."
This PR adds `mvcgen` support for specifications in the local context.
Example:
```lean
import Std.Tactic.Do
open Std.Do
set_option mvcgen.warning false
def foo (x : Id Nat → Id Nat) : Id Nat := do
let r₁ ← x (pure 42)
let r₂ ← x (pure 26)
pure (r₁ + r₂)
theorem foo_spec
(x : Id Nat → Id Nat)
(x_spec : ∀ (k : Id Nat) (_ : ⦃⌜True⌝⦄ k ⦃⇓r => ⌜r % 2 = 0⌝⦄), ⦃⌜True⌝⦄ x k ⦃⇓r => ⌜r % 2 = 0⌝⦄) :
⦃⌜True⌝⦄ foo x ⦃⇓r => ⌜r % 2 = 0⌝⦄ := by
mvcgen [foo, x_spec] <;> grind
def bar (k : Id Nat) : Id Nat := do
let r ← k
if r > 30 then return 12 else return r
example : ⦃⌜True⌝⦄ foo bar ⦃⇓r => ⌜r % 2 = 0⌝⦄ := by
mvcgen [foo_spec, bar] -- unfold `bar` and automatically apply the spec for the higher-order argument `k`
```
This PR improves the slice API with lemmas for `drop`/`take` operations
on `Subarray` and more lemmas about `Std.Slice.fold`, `Std.Slice.foldM`
and `Std.Slice.forIn`. It also changes the `simp` and `grind`
annotations for `Slice`-related lemmas. Lemmas converting between slices
of different shapes are no longer `simp`/`grind`-annotated because they
often complicated lemmas and hindered automation.
This PR adds a custom simproc to handle `Decidable.rec`, where we force
the rewrite in the argument of the `Decidable` type, that normally is
not rewritten due to being a subsingleton.
Closes#12386
This PR develops custom simprocs for dealing with `ite`/`dite`
expressions in `cbv` tactics, based on equivalent simprocs from
`Sym.simp`, with the difference that if the condition is not reduced to
`True`/`False`, we make use of the decidable instance and calculate to
what the condition reduces to.
Stacked on top of #12391.
This PR adds `IO.FS.Metadata.numLinks`, which contains the number of
hard links to a file.
This changes the implementation of `System.FilePath.metadata` and
`System.FilePath.symlinkMetadata` to use libuv. Otherwise, `st_nlink`
was not properly set on Windows. This also has the side benefit of
provided sub-second precision for file times on Windows (fulfilling an
old TODO). Also, while libuv supports `lstat` for Windows, enabling that
is left to a future PR.
This PR fixes a platform inconsistency in `IO.FS.removeFile` where it
could not delete read-only files on Windows.
The implementation now uses `uv_fs_unlink` instead of `std::remove`, as
libuv can delete read-only files. The PR also fixes a inconsistency in
`IO_test.lean` where it would generate files in the wrong directory when
run interactively.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR fixes an issue in LCNF simp where it would attempt to act on
type incorrect `cases`
statements and look for a branch, otherwise panic. This issue did not
yet manifest in production as
various other invariants upheld by LCNF simp help mask it but will start
to become an issue with the
upcoming changes.
This is the proper fix for #6957.
This PR provides a `LawfulForwardPatternModel` instance for string
patterns, i.e., it proves correctness of the `dropPrefix?` and
`startsWith` functions for string patterns.
Note that this is "just" the correctness proof; there isn't a way to
actually use it yet. API lemmas will follow.
This PR adds identifying information about a module available to `lean`
(e.g., its name and package identifier) to the module's dependency
trace. This ensures modules with different identification have different
input hashes even if their source files and imports are identical.
This PR adds a few unification hints that we will need after
`backward.isDefEq.respectTransparency` is `true` by default.
See #12338
It was part of #12179.
This PR makes disabling the artifact cache (e.g., via
`LAKE_ARTIFACT_CACHE=false` or `enableArtifactCache = false`) now stop
Lake from fetching from the cache (whereas it previously only stopped
writing to it).
There are now 3 possible configuration of the local artifact cache for a
package:
* `true`: Artifacts will be fetched from the cache before building (if
available) and built artifacts will be cached.
* `false:`: Lake will neither fetch artifacts from the cache or store
them into it.
* **default** (no configuration set): Lake will fetch artifacts from the
cache but not store them into it. A key motivation for this is to, by
default, reuse artifacts downloaded into the cache from a remote
service.
This PR tags `List.reduceOption` with `@[expose]`. #12348 accidentally
moved the definition out of an `@[expose] section` which caused problems
in mathlib because `List.reduceOption` was expected to be exposed.
This PR extends shake with tracking of attribute names passed to
`simp`/`grind`.
On the way there, it also fixes `register_simp/grind_attr` uses outside
`public meta section` as well as go-to-definition on declaration-level
uses of the created attributes (tactic-level goto would be a separate
todo).
