We use `no_index` to work around special-handling of `OfNat.ofNat` in
`DiscrTree`, which has been reported as an issue in
https://github.com/leanprover/lean4/issues/2867 and is currently in the
process of being fixed in https://github.com/leanprover/lean4/pull/3684.
As the potential fix seems non-trivial and might need some time to
arrive in-tree, we meanwhile add the `no_index` keyword to the
problematic subterm.
---------
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
We swap the arguments for `Membership.mem` so that when proceeded by a
`SetLike` coercion, as is often the case in Mathlib, the resulting
expression is recognized as eta expanded and reduce for many
computations. The most beneficial outcome is that the discrimination
tree keys for instances and simp lemmas concerning subsets become more
robust resulting in more efficient searches.
Closes `RFC` #4932
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This is part of #3983.
Fine-grained equational lemmas are useful even for non-recursive
functions, so this adds them.
The new option `eqns.nonrecursive` can be set to `false` to have the old
behavior.
### Breaking channge
This is a breaking change: Previously, `rw [Option.map]` would rewrite
`Option.map f o` to `match o with … `. Now this rewrite will fail
because the equational lemmas require constructors here (like they do
for, say, `List.map`).
Remedies:
* Split on `o` before rewriting.
* Use `rw [Option.map.eq_def]`, which rewrites any (saturated)
application of `Option.map`
* Use `set_option eqns.nonrecursive false` when *defining* the function
in question.
### Interaction with simp
The `simp` tactic so far had a special provision for non-recursive
functions so that `simp [f]` will try to use the equational lemmas, but
will also unfold `f` else, so less breakage here (but maybe performance
improvements with functions with many cases when applied to a
constructor, as the simplifier will no longer unfold to a large
`match`-statement and then collapse it right away).
For projection functions and functions marked `[reducible]`, `simp [f]`
won’t use the equational theorems, and will only use its internal
unfolding machinery.
### Implementation notes
It uses the same `mkEqnTypes` function as for recursive functions, so we
are close to a consistency here. There is still the wrinkle that for
recursive functions we don't split matches without an interesting
recursive call inside. Unifying that is future work.
The goal at the crucial step is
```
a : Array Nat
i : Fin ?m.27
⊢ ↑i < a.size
```
and after the `apply Fin.val_lt_of_le;` we have
```
a : Array Nat
i : Fin ?m.27
⊢ ?m.27 ≤ a.size
```
and now `apply Fin.val_lt_of_le` applies again, due to accidential
defeq. Adding `with_reducible` helps here.
fixes#5061
Defines `mergeSort`, a naive stable merge sort algorithm, replaces it
via a `@[csimp]` lemma with something faster at runtime, and proves the
following results:
* `mergeSort_sorted`: `mergeSort` produces a sorted list.
* `mergeSort_perm`: `mergeSort` is a permutation of the input list.
* `mergeSort_of_sorted`: `mergeSort` does not change a sorted list.
* `mergeSort_cons`: proves `mergeSort le (x :: xs) = l₁ ++ x :: l₂` for
some `l₁, l₂`
so that `mergeSort le xs = l₁ ++ l₂`, and no `a ∈ l₁` satisfies `le a
x`.
* `mergeSort_stable`: if `c` is a sorted sublist of `l`, then `c` is
still a sublist of `mergeSort le l`.
As discussed with @semorrison, feel free to do whatever to the branch.
---------
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Previously, the tactic state shown at `decreasing_by` would leak lots of
details about the translation, and mention `invImage`, `PSigma` etc.
This is not nice.
So this introduces `clean_wf`, which is like `simp_wf` but using
`simp`'s `only` mode, and runs this unconditionally. This should clean
up the goal to a reasonable extent.
Previously `simp_wf` was an unrestricted `simp […]` call, but we
probably don’t want arbitrary simplification to happen at this point, so
this now became `simp only` call. For backwards compatibility,
`decreasing_with` begins with `try simp`. The `simp_wf` tactic
is still available to not break too much existing code; it’s docstring
suggests to no longer use it.
With `set_option cleanDecreasingByGoal false` one can disable the use of
`clean_wf`. I hope this is only needed for debugging and understanding.
Migration advise: If your `decreasing_by` proof begins with `simp_wf`,
either remove that (if the proof still goes through), or replace with
`simp`.
I am a bit anxious about running even `simp only` unconditionally here,
as it may do more than some user might want, e.g. because of options
like `zetaDelta := true`. We'll see if we need to reign in this tactic
some more.
I wonder if in corner cases the `simp_wf` tactic might be able to close
the goal, and if that is a problem. If so, we may have to promote simp’s
internal `mayCloseGoal` parameter to a simp configuration option and use
that here.
fixes#4928
