exact? failure

Stream: mathlib4

[Michael Stoll]

import Mathlib

example (s t : Finset ℕ) (p : ℕ) (h : p ∈ t) (h' : t ∈ s.powerset) : p ∈ s := by
  exact? -- `Finset.mem_powerset.mp h' h` works
-- `exact?` could not close the goal. Try `apply?` to see partial suggestions.

[Kim Morrison]

Finset.mem_powerset.{u_1} {α : Type u_1} {s t : Finset α} : s ∈ Finset.powerset t ↔ s ⊆ t

The RHS does not syntactically match the goal, so this lemma is not even tried by exact?.

[Michael Stoll]

OK; seems I have to adjust my mental model of exact?.

[Michael Stoll]

What about this one?

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecificLimits.Normed

example {z : ℂ} (hz : ‖z‖ < 1) : Filter.Tendsto (fun k ↦ z ^ k) Filter.atTop (nhds 0) := by
  -- exact? -- (deterministic) timeout at 'whnf'
  -- apply? using hz -- (deterministic) timeout at 'isDefEq'
  exact tendsto_pow_atTop_nhds_0_of_norm_lt_1 hz

@Scott Morrison
Off-topic: Why is docs#tendsto_pow_atTop_nhds_0_of_norm_lt_1 (similarly for some other lemmas nearby) not called tendsto_pow_atTop_nhds_zero_of_norm_lt_one? The literal 0 and 1 make it difficult to find, since they are unexpected.

[Kim Morrison]

PR welcome! Those names are certainly incorrect.

[Kim Morrison]

Sorry, away from my computer for a bit. But timeouts are a bad sign. What happens with this example with std_exact??

[Michael Stoll]

std_exact? and std_apply? also lead to timeouts.
Would it be possible in principle to limit the heartbeats used when checking each of the candidates (possibly storing the "continuation" so that it can be continued later if no quick solution was found)? My suspicion is that when exact? (say) tries to match the conclusion of some lemma, it initiates a slow TCI search (which maybe would eventually fail) and so loses time before getting to the relevant ones.

[Michael Stoll]

Scott Morrison said:

PR welcome! Those names are certainly incorrect.

What is the syntax for a deprecated alias? (I assume the good practice now is to not remove the old names immediately, but to keep them as deprecated.)

[Yaël Dillies]

@[deprecated] alias

[David Renshaw]

with #10052, adding with_reducible makes it work:

example {z : ℂ} (hz : ‖z‖ < 1) : Filter.Tendsto (fun k ↦ z ^ k) Filter.atTop (nhds 0) := by
  with_reducible exact?

[David Renshaw]

Actually, it seems that with_reducible exact? works even without the help of #10052

[Michael Stoll]

How do I know when to use with_reducible in this context? (I.e., is there a better answer than "just try it when exact? throws a timeout"?) Should this be the default, or are there downsides?

[Mario Carneiro]

seems like it should be the default

[Mario Carneiro]

the discrimination tree used by exact? already only works up to reducible unfolding, so anything that requires additional unfolding is a coin toss

[Mario Carneiro]

the downside of setting the reducibility in a tactic to something other than "inherited" is that you can't use combinators like with_reducible or with_unfolding_all to change the behavior to something else

[Michael Stoll]

Scott Morrison said:

PR welcome! Those names are certainly incorrect.

#10077
This was quite a bit more work than I expected!

[Michael Stoll]

(There are some others like docs#zero_ne_one_or_forall_eq_0 and docs#Polynomial.C_0 , but I'll leave these to somebody else.)

[Michael Stoll]

@Kevin Buzzard asks in a comment on #10077 whether the

@{deprecated] alias bla := Bla

lines are correct without full namespace qualification on bla and Bla. Can somebody who knows about this chime in?

[Ruben Van de Velde]

Doesn't it show the full name if you hover over it? This is also something that leaff would be great for

[Yaël Dillies]

It should be correct, as in namespace Foo @[deprecated] alias bar := bla creates Foo.bar.

[Michael Stoll]

Then maybe one or two more people can look at it?

[Mario Carneiro]

Name resolution in alias is the same as other defs: the thing being defined has the current namespaces prepended, and the thing being referenced is resolved using the current namespace and open declarations

[Kevin Buzzard]

I only asked because they were each right next to an #align which was following a different system

[Michael Stoll]

I've opened a thread on the name-changing PR here, as this discussion is rather off-topic for this thread.

[Yaël Dillies]

Example from PFR:

import Mathlib.Algebra.BigOperators.Order

example {B : Type*} [Fintype B] (v w : B → ℕ) :
    (Finset.univ.sum (v * w))^2 ≤ Finset.univ.sum (v^2) * Finset.univ.sum (w^2) := by
  exact? -- fails to find Finset.sum_mul_sq_le_sq_mul_sq _ _ _

[Johan Commelin]

The standard infinite-primes demo saw quite a slowdown. And std_exact? even times out.

import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

open Nat

theorem Euclid (n : ℕ) :
    ∃ p > n, p.Prime := by
  let N := n ! + 1
  let p := minFac N
  use p
  have hp : p.Prime
  · refine minFac_prime ?hp.n1
    observe : n ! > 0
    linarith
  have hpn : p > n
  · by_contra! hpn : p ≤ n
    observe that : ¬ p ∣ 1
    apply that
    observe : p ∣ (n !)
    observe : p ∣ N
    show p ∣ 1
    exact? -- slow
    -- std_exact? -- timeout
  tauto
  done

[Kim Morrison]

Yaël Dillies said:

Example from PFR:

import Mathlib.Algebra.BigOperators.Order

example {B : Type*} [Fintype B] (v w : B → ℕ) :
    (Finset.univ.sum (v * w))^2 ≤ Finset.univ.sum (v^2) * Finset.univ.sum (w^2) := by
  exact? -- fails to find Finset.sum_mul_sq_le_sq_mul_sq _ _ _

@Yaël Dillies, we've seen this many times before: v * w does match (according to a DiscrTree with fun i => f i * g i, so the lemma isn't even retrieved (let along tried).

Options: restate the lemma with just f * g instead, or switch out to Jovan's DiscrTree tree, which, if I recall correctly, can handle this.

[Kim Morrison]

The second option is logistically very difficult, as we are almost about to replace exact? with the new implementation in Std, and so the alternate DiscrTree would need to move up to Std. I won't have time for this, but if you or anyone else is interested in working on this I'm happy to advise! :-)

[Kim Morrison]

Johan Commelin said:

The standard infinite-primes demo saw quite a slowdown. And std_exact? even times out.

I can't reproduce std_exact? timing out.

[Kim Morrison]

Note that something pretty close to this is already checked in as a test in test/observe.lean. (You mentioned that we should have a regression test, and I agreed, forgetting we already did. :-)

[Yaël Dillies]

Sorry, your brackets don't match so I'm not sure how to parse your message. Are you saying that v * w gets expanded to fun i ↦ v i * w i in the DiscrTree?

[Kim Morrison]

No. The lemma statement for Finset.sum_mul_sq_le_sq_mul_sq includes fun i ↦ v i * w i, but that doesn't appear in the goal.

[Kim Morrison]

The DiscrTree lookup sees the v * w in the goal, which doesn't match against the fun i ↦ v i * w i in the key for Finset.sum_mul_sq_le_sq_mul_sq, so it doesn't get retrieved.

[Yaël Dillies]

Ah, I see

[Kevin Buzzard]

So what's the fix? Does this mean that the lemma in mathlib should be stated in another way?

[Kim Morrison]

I think the only viable options are:

• be sad that exact? doesn't find this
• adopt @Jovan Gerbscheid's modified DiscrTree tree
• make copies of the lemmas (perhaps with _no_lambda in the name? perhaps exact? could find these and then suggest the real one?)

[Kim Morrison]

I investigated previously just changing the statement, but then simp is often unhappy! I can't find the thread in which we talked about this previously, at the moment.

[Johan Commelin]

Scott Morrison said:

Note that something pretty close to this is already checked in as a test in test/observe.lean. (You mentioned that we should have a regression test, and I agreed, forgetting we already did. :-)

You clearly weren't the only one that forgot.

[Johan Commelin]

Should we adjust the default heartbeats on that test, to make sure it doesn't just pass, but also remains reasonably fast?

[Jovan Gerbscheid]

My version of discrtree also does not see that fun x -> f x + g x is the same as f + g, but this was on my TODO list to figure out how to implement it.

[Jovan Gerbscheid]

The equivalence is not applied at the root expression, because we still want the lemma fun x => x = id to be useable for rewriting

[Jovan Gerbscheid]

Related to this I recently added to my discrtree that it sees that fun x => x and id are the same when it is not a root expression. exact? also has problems with lemmas involving id that can be written in either form (and sometimes a lemma is duplicated to have both forms)

[Jovan Gerbscheid]

Somehow the previous 2 messages have been sent in the wrong order

[Kim Morrison]

Johan Commelin said:

Should we adjust the default heartbeats on that test, to make sure it doesn't just pass, but also remains reasonably fast?

Yes, please!

[Jovan Gerbscheid]

I've made an update, and now my DiscrTree indexes f + g and fun x => f x + g x in the same way. I've implemented it for +, *, - and /. In principle this can also be done for some other pointwise defined operators such as ⁻¹.

[Johan Commelin]

I just want to record that on (random commit in the past)

commit 1de7e6632c661b383aecc389f7e89d7033d3ab46 (HEAD)
Author: Jz Pan <acme_pjz@hotmail.com>
Date:   Mon Jan 8 09:51:29 2024 +0000

the test in test/observe.lean needed less than 6000 heartbeats.

On current master it needs ~ 100 000.

I will do a proper bisect in a moment.

[Johan Commelin]

commit 718437417b23d1bfbde949afdf430e1d7f20d134
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Feb 6 09:06:17 2024 +0000

needs ~ 25 000.

The bisect continues. But this suggests that there might be multiple regressions.

[Johan Commelin]

I'm going to call this commit bad. But a bisect in the other path would also be useful, I think.

[Johan Commelin]

[5876928aa973de8045e91fd2b70d184ca806f6b2] feat: formalize IMO 1959 Q2 (#9884)
~ 95 000 hearbeats

[Johan Commelin]

Which is an older commit. So this heartbeat count is going up and down and up again.

[Sebastian Ullrich]

Is it deterministic at least?

[Johan Commelin]

Seems to be

[Johan Commelin]

This seems to be the culprit:

d3a6c9f3bd17193b002fdc5e540789c883605cc3 is the first bad commit
commit d3a6c9f3bd17193b002fdc5e540789c883605cc3
Author: Scott Morrison <scott@tqft.net>
Date:   Tue Jan 30 01:07:06 2024 +0000

    chore: bump Std to leanprover/std4#242 (#10104)

[Johan Commelin]

git bisect start
# status: waiting for both good and bad commits
# bad: [abd9e6428d55b6ef591e971679ac80db2d10f166] perf(test/observe): set low maxHeartbeats for test
git bisect bad abd9e6428d55b6ef591e971679ac80db2d10f166
# status: waiting for good commit(s), bad commit known
# good: [1de7e6632c661b383aecc389f7e89d7033d3ab46] chore(FieldTheory/SeparableDegree): add `Separable.natSepDegree_eq_natDegree` and golf (#9525)
git bisect good 1de7e6632c661b383aecc389f7e89d7033d3ab46
# good: [cb8ebafbf496d7273b27c5424ffbc4a195f4bda5] refactor(Probability/Kernel/CondCdf): mv prod_iInter (#10037)
git bisect good cb8ebafbf496d7273b27c5424ffbc4a195f4bda5
# bad: [718437417b23d1bfbde949afdf430e1d7f20d134] chore: tidy various files (#10269)
git bisect bad 718437417b23d1bfbde949afdf430e1d7f20d134
# bad: [e64d0a161b8ccdd45cb8d9db09910eb461f5d0f7] refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file (#10165)
git bisect bad e64d0a161b8ccdd45cb8d9db09910eb461f5d0f7
# bad: [5876928aa973de8045e91fd2b70d184ca806f6b2] feat: formalize IMO 1959 Q2 (#9884)
git bisect bad 5876928aa973de8045e91fd2b70d184ca806f6b2
# good: [86ffe042ba78d8e2f72717176e5ed6cd0c3445df] chore(Order/Filter/ListTraverse): move from `Basic` (#10048)
git bisect good 86ffe042ba78d8e2f72717176e5ed6cd0c3445df
# bad: [d3a6c9f3bd17193b002fdc5e540789c883605cc3] chore: bump Std to leanprover/std4#242 (#10104)
git bisect bad d3a6c9f3bd17193b002fdc5e540789c883605cc3
# good: [89f9777575aaa0e4190c64c8247b03f7864f67e8] chore: fix Punit->PUnit in CommMon_ (#10089)
git bisect good 89f9777575aaa0e4190c64c8247b03f7864f67e8
# good: [7458f0e73e0f7d6acb16aec54166314351250412] feat(Topology/Separation): define R₁ spaces, review API (#10085)
git bisect good 7458f0e73e0f7d6acb16aec54166314351250412
# good: [132e5112a4627495177b8b165a8cfcc8992a87df] feat: Integral curves are either injective or periodic (#9343)
git bisect good 132e5112a4627495177b8b165a8cfcc8992a87df
# first bad commit: [d3a6c9f3bd17193b002fdc5e540789c883605cc3] chore: bump Std to leanprover/std4#242 (#10104)

[Johan Commelin]

After that bad commit, the heartbeats in test/observe.lean went from < 3000 to > 95000.

[Johan Commelin]

cc @Scott Morrison

[Eric Rodriguez]

Did we get rid of old exact? with std_exact? in that commit?

[David Renshaw]

at #9962 the std commit was updated to 0d0ac1c43e1ec1965e0806af9e7a32999ea31096
and then at #10104 (which was implicated by Johan's git bisect) the std commit was updated to 128fd8e663353da2a3666167605b510824fe2eb5

[Johan Commelin]

#10498 is setting a "low" maxHeartbeats. But we should strive to make that at least 10x lower.

[David Renshaw]

$ git log --oneline 0d0ac1c43e1ec1965e0806af9e7a32999ea31096..128fd8e663353da2a3666167605b510824fe2eb5
128fd8e Revert "chore: don't call symmSaturate repeatedly in solve_by_elim (#547)" again. (#567)
92fb0a9 chore: upstream classical tactic (#242)
6f352d4 feat: upstream addHaveSuggestion and addRewriteSuggestion (#210)
5368bbb feat: commit `lake-manifest.json` (#560)
fff46c3 feat: module docs (#237)
b275827 feat: more `Bool` lemmas (#464)
1a0e00d feat: add `ByteArray.ofFn` (#526)
61ef066 feat: solve_by_elim uses intros and constructor by default (#551)

[Johan Commelin]

Is 61ef066 feat: solve_by_elim uses intros and constructor by default (#551) the suspicious one?

[Eric Rodriguez]

The symm_saturate stuff is really quite slow. Me and Scott were discussing that a while ago, but we didn't really come to a conclusion about the best way to fix it.

[Eric Rodriguez]

Those seem like fast tactics

[Johan Commelin]

Ooh wait, the other one is a "revert"! So now it is in fact calling symmSaturate repeatedly...

[Patrick Massot]

I think the default exact? should be really fast so that you can basically try it all the time. And then we can have a exact?! that tries a lot harder when you are sure this should be somewhere.

[Eric Rodriguez]

I think this is configurable in the solve by elim config so it should be easy to try a patch and see if it is indeed this

[Eric Rodriguez]

I think turning off symm doesn't do anything: https://github.com/leanprover-community/mathlib4/compare/ericrbg/check_observe

[Kim Morrison]

It is solve_by_elim calling constructor. I've turned it off in library_search, and it drops to about 6500 heartbeats.

[Kim Morrison]

I pushed the change.

[Kim Morrison]

std#642 is corresponding change in std_exact? so we don't lose it when we do the switchover.

[Johan Commelin]

Thanks for debugging this!

[Floris van Doorn]

Here is another exact? failure that surprised me.

lemma dvd_of_mul_dvd_mul_left' {R : Type*} [CancelMonoidWithZero R] {a b c : R} (hc : c ≠ 0)
    (H : c * a ∣ c * b) : a ∣ b := by
  exact? -- fails
  exact mul_dvd_mul_iff_left hc |>.mp H -- succeeds

(e.g. on commit 98b2339d0d)

[Damiano Testa]

Btw, with apply?, one of the suggestions is

refine (mul_dvd_mul_iff_left (?_ (id (Ne.symm hc)))).mp (?_ (id (Ne.symm hc)))

(which does not work but gives the right lemma!)

[Sébastien Gouëzel]

Recently, I've got many nondeterministic failures of exact?, in the following form: when working on a heavy proof, at some point exact? times out in the sense that I get the warning that the lemma is taking too many heartbeats and that I should increase the heartbeats (I don't get the message on exact?, but on the lemma name). From this point on, exact? is unusable (even a stupid lemma like lemma foo (n : ℕ) : 0 ≤ n := by exact? will fail). Increasing heartbeats doesn't make any difference (even more, even when I increase them to 500000 say I get the standard message mentioning 200000 heartbeats). Apart from exact?, Lean seems to still be working fine. The only solution I found in this situation is to restart Lean -- then the exact? that failed initially will work fine, and everything is fixed.

The outcome is that every 10 or 15 minutes I have to restart Lean. Not too bad, but not very nice. Sorry I can't give more details or a reproductible use case...

[Patrick Massot]

@Joe Hendrix :up:

[Floris van Doorn]

related: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60exact.3F.60.20timing.20out/near/429675849

[Joe Hendrix]

@Patrick Massot Thanks for the ping. @Sébastien Gouëzel There were a few changes in the Lean 4 migration, and at least one will be fixed in #3769. There may also be a heartbeat issue in initialization. I'm planning to have #3769 in the next nightly.

[Joe Hendrix]

There's still a bit of testing, but I think lean4#3769 will resolve the issues and should be ready in time for the next release candidate.

If exact? or apply? work, but seems slow (especially on first run), it'd be useful to see profiling numbers. e.g,

import Mathlib
set_option profiler true
set_option profiler.threshold 1
example (x y : Nat) : x + y = y + x := by apply?
-- lazy discriminator import initialization took 2.3s
-- tactic execution of Lean.Parser.Tactic.apply? took 3.6ms

The initialization performance after recent changes seems to have degraded from about 1.5s to 2.3s. That is not ideal, but still seems reasonable to me (though I have a M2). It'd be good to know if it's prohibitively slow on other's machines.

[Floris van Doorn]

On a recent version of Mathlib I get similar numbers:

-- librarySearch launch took 2.01s
-- librarySearch took 1.43s
-- (some other things that take <10ms)

[Floris van Doorn]

And of course I'm perfectly happy with such numbers as a one-time cost.