replacing `exact?`

Stream: mathlib4

[Kim Morrison]

In Mathlib currently we have access to exact?, as well as a duplicate std_exact? provided by Std. We want to remove the existing exact?, and then rename std_exact? back to exact?.

The major differences are:

• std_exact? uses an (amazing!) new lazily initialised discrimination tree due to @Joe Hendrix, making std_exact? sufficiently fast that it doesn't need a cache anymore for Mathlib (~0.5s slowdown on the first call).
• There are some changes to the ordering of results.

I just ran some timing tests, by taking Mathlib's test/LibrarySearch/basic.lean, and making a copy std_basic in which I've replaced exact? by std_exact? and apply? with std_apply?. A few of the suggestions change, but to my mind the changes are all neutral or improvements, so I updated the #guard_msgs checks. Here are the timing results:

kim@carica mathlib4-2 % hyperfine "lake env lean test/LibrarySearch/std_basic.lean"
Benchmark 1: lake env lean test/LibrarySearch/std_basic.lean
  Time (mean ± σ):      2.236 s ±  0.011 s    [User: 8.818 s, System: 0.767 s]
  Range (min … max):    2.219 s …  2.256 s    10 runs

kim@carica mathlib4-2 % hyperfine "lake env lean test/LibrarySearch/basic.lean"
Benchmark 1: lake env lean test/LibrarySearch/basic.lean
  Time (mean ± σ):      1.590 s ±  0.011 s    [User: 1.208 s, System: 0.359 s]
  Range (min … max):    1.576 s …  1.608 s    10 runs

So it is a slight slowdown, but I am satisfied that this is not a significant problem.

[Kim Morrison]

The result ordering is potentially problematic. Previously, we made an effort to rank highly results which used local hypotheses (via solve_by_elim after applying a library lemma).

In test/LibrarySearch/IsCompact.lean we exercise this as follows:

example (f : ℝ → ℝ) {K : Set ℝ} (_hK : IsCompact K) : ∃ x ∈ K, ∀ y ∈ K, f x ≤ f y := by
  apply?

Here apply? returns refine IsCompact.exists_forall_le _hK ?_ ?_ as the first result, but std_apply? returns this only as the 11th result, after various unhelpful things like:

Try this: refine bex_def.mp ?a✝
Try this: refine Set.inter_nonempty.mp ?a✝
Try this: refine Set.inter_nonempty_iff_exists_left.mp ?a✝
Try this: refine Set.nonempty_def.mp ?a✝
Try this: refine Set.not_disjoint_iff.mp ?a✝

This is admittedly an unfair example, because this is the example that someone initially brought up that prompted me to add the sort-by-local-hypotheses-used rule!

[Kim Morrison]

It would be nice to have more comparison points re: how the two versions order results.

[Kim Morrison]

I can do some, but this thread is also an invitation of anyone to exercise std_apply? and report back!

[Kim Morrison]

If the ordering change is a pervasive problem, we can tweak it further, and potentially re-incorporate the ordering by number of hypotheses used.

If it is not a pervasive problem, perhaps we'll just stick with the current (simpler) implementation.

[David Renshaw]

import Mathlib.Tactic

set_option trace.profiler true in
example (n : ℕ) (a : ℝ) (ha : 0 ≤ a) (h1 : 1 ^ n < a ^ n) : 1 < a := by
  -- exact?
  -- Try this: exact lt_of_pow_lt_pow n ha h1
  -- in 1.19 seconds
  -- this lemma is deprecated

  std_exact?
  -- Try this: exact lt_of_pow_lt_pow_left n ha h1
  -- in 2.7 seconds
  -- this lemma is not deprecated

[David Renshaw]

Did this just get lucky, or will std_exact? always avoid deprecated items?

[Kim Morrison]

I wouldn't worry too much about the timings: the difference in timing is all in the first time std_exact? is invoked in each file.

[Kim Morrison]

As far as I'm aware this is luck, and there is no attempt to avoid deprecated results.

[Joe Hendrix]

That's luck that it's avoiding deprecated. It's probably a good default to avoid them though.

std_exact? and std_apply? results are sorted to return results ordered primarily by how many symbols in the head of the theorem found match the given term followed by returning earliest defined symbol first (using the module order defined internally in the Lean environment list).

It returns lt_of_pow_lt_pow_left because it is defined before lt_of_pow_lt_pow.

[Eric Rodriguez]

Scott Morrison said:

I wouldn't worry too much about the timings: the difference in timing is all in the first time std_exact? is invoked in each file.

Does this mean "per session"? Does it keep persistent cache after running once and then erasing itself through the suggestion?

[Michael Stoll]

@Scott Morrison Did you see this thread?

[Jireh Loreaux]

Scott Morrison said:

Here are the timing results:

kim@carica mathlib4-2 % hyperfine "lake env lean test/LibrarySearch/std_basic.lean"
Benchmark 1: lake env lean test/LibrarySearch/std_basic.lean
  Time (mean ± σ):      2.236 s ±  0.011 s    [User: 8.818 s, System: 0.767 s]
  Range (min … max):    2.219 s …  2.256 s    10 runs

kim@carica mathlib4-2 % hyperfine "lake env lean test/LibrarySearch/basic.lean"
Benchmark 1: lake env lean test/LibrarySearch/basic.lean
  Time (mean ± σ):      1.590 s ±  0.011 s    [User: 1.208 s, System: 0.359 s]
  Range (min … max):    1.576 s …  1.608 s    10 runs

@Scott Morrison something looks fishy in these timing results. The User+System times for std_basic are nowhere close to the mean (but for exact they are).

[Joe Hendrix]

Eric Rodriguez said:

Does this mean "per session"? Does it keep persistent cache after running once and then erasing itself through the suggestion?

Yes, it initializes a lazy discriminator tree for the environment imports the first time it is run in a Lean process, and then reuses that each time std_exact? is invoked. The discriminator tree built for constants in the current module is regenerated each time std_exact? is run, but that's really small.

When you apply the suggestion, the underlying lazy discriminator tree isn't changed; it is still resident in memory.

[Kim Morrison]

Jireh Loreaux said:

Scott Morrison something looks fishy in these timing results. The User+System times for std_basic are nowhere close to the mean (but for exact they are).

Yes, what is going on here is that std_basic is using quite a lot of parallelism as it lazily initialise the tree!

[Kim Morrison]

Thus that wall time (report in the mean numbers) are still relatively low, even though User+System is high.

[Kim Morrison]

That said, this does suggest we should run this benchmark on a much more representative machine than mine. :-) (i.e. a laptop with <= 4 cores)

[Kim Morrison]

Here are the benchmark results from my 8 year old laptop:

kim@arguta mathlib4 % hyperfine "lake env lean test/LibrarySearch/std_basic.lean"
Benchmark 1: lake env lean test/LibrarySearch/std_basic.lean
  Time (mean ± σ):      7.818 s ±  0.374 s    [User: 10.478 s, System: 1.147 s]
  Range (min … max):    7.345 s …  8.584 s    10 runs

kim@arguta mathlib4 % hyperfine "lake env lean test/LibrarySearch/basic.lean"
Benchmark 1: lake env lean test/LibrarySearch/basic.lean
  Time (mean ± σ):      5.255 s ±  0.143 s    [User: 4.082 s, System: 0.974 s]
  Range (min … max):    5.125 s …  5.561 s    10 runs

I think that is still an acceptable slow-down.

[David Renshaw]

import Mathlib.Data.Nat.ModEq
import Mathlib.Tactic.LibrarySearch

theorem foo (a b : ℕ) (h : a + b ≡ a [MOD 10]) : b ≡ 0 [MOD 10] := by
  --exact?
  -- "Try this: exact Nat.ModEq.add_left_cancel (id (Nat.ModEq.symm h)) rfl"
  -- (note the unneeded `id`)

  std_exact?
  -- "Try this: exact Nat.ModEq.symm (Nat.ModEq.add_left_cancel h rfl)"

[David Renshaw]

so it seems that std_exact? avoids issue #7068

[David Renshaw]

... but maybe just because it's searching in a different order?

[Kim Morrison]

I suspect that is just an accident of searching in a different order. The id is coming from symmSaturate.

[Kim Morrison]

Just reversing the hypothesis h exhibits the same problem with std_exact?.

[Kim Morrison]

This id is inserted by mkExpectedTypeHint here.

[Kim Morrison]

Do you want to see what happens if we omit it?

Perhaps we need a cleverer version of mkExpectedTypeHint which checks if the hint is identical to the inferred type, and if so omits the id.