exact? can't find theorem

Stream: lean4

[Alex Meiburg]

theorem blah {α : Sort u} (h : Prop) [Decidable h] {x y : α} {p : α → Prop} (hx : h → p x) (hy : ¬h → p y) :
    p (if h then x else y) := by
  exact iteInduction hx hy

this (with no imports) works fine. But exact? does not close the goal, even though iteInduction is a ??totally normal?? theorem, and the only arguments are hx and hy, and everything is an exact expression equality afaict (no "merely" defeq fits going on). Can someone explain to me why?

[Aaron Liu]

iteInduction doesn't seem to be used a lot

[Alex Meiburg]

Yes, for good reason, it's kind of awkward (split or split_ifs is usually better). It's more a question of why exact? doesn't find it.

[Aaron Liu]

Probably the answer is that your conclusion is a free variable applied to stuff

[Aaron Liu]

so it's hard to unify

[Alex Meiburg]

ah! Like there's no key for the discrimination tree? Did I say that right? That would make sense.

[Alex Meiburg]

I guess it just finds p as the head, doesn't know what to do with that, and gives up. Hm.

[Alex Meiburg]

That's too bad. I like to think of exact? as "if there's one theorem in the library that will solve this, find it and use it!". But no.

[Kevin Buzzard]

It also often won't find theorems whose conclusion is A = B.

[Jovan Gerbscheid]

Yep, theorems whose conclusion is a free variable, or an equality of free variables where the type is a free variable, are not indexed by exact? for efficiency reasons.

[Patrick Massot]

This is really a huge trap for new users. It would be really nice if exact? could detect that the goal looks like this and print a warning message suggesting to try some new slow_exact? doing what the Lean 3 version was doing (simply try to apply all lemmas).

[Kim Morrison]

Yes please, I would merge that PR! :-)

[Kim Morrison]

Probably just a flag exact? +all would do. I like the warning idea, that hadn't occurred to me!

[Alex Meiburg]

There's actually a spot more than "try to apply all lemmas": you can do exfalso first and then trying applying all lemmas. :) (Or, by_contra first, which is slightly stronger.)

Example:

example (f : Filter ℕ) [f.NeBot] (x y z : Set ℕ) (hx : x ∈ f) (hy : y ∈ f) (hf : Disjoint x y) : x = z := by
  solve_by_elim [Filter.NeBot.not_disjoint]

Here solve_by_elim is able to (with the help of one extra library lemma) prove False and close the goal. exact? and exfalso; exact? both don't work. If there was a slow_exact?, I would hope it could catch things like this too!

[Alex Meiburg]

Another example:

import Mathlib

example {m n : ℕ} (h1 : m ∣ n) (h2 : 1 ≠ m) (h3 : Nat.Prime n) : m = n := by
  by_contra
  solve_by_elim [Nat.not_prime_of_dvd_of_ne]

[Kevin Buzzard]

This feels like mission creep really.

[Jovan Gerbscheid]

Fundamentally apply?, and hence exact?, are backwards reasoning tactics. This means that they infer what to apply directly from the shape of the goal. If the goal is False, or a free variable, then this strategy is simply too inefficient. Though feel free to try and implement a better strategy :).

[Alex Meiburg]

That's fair to call it mission creep! I just like automation that helps people find relevant stuff. So maybe this isn't "exact?" any more, but it's functionality I would enjoy seeing exist... Maybe under a different name, like find_one_lemma or something

What is "simply too inefficient"? Like this would take five minutes, an hour?

[Jovan Gerbscheid]

Hmm, good question, I'm not sure how long such a thing would actually take. But another question is, even if the speed was there, how useful would it be to apply recursor-like theorems. Applying a recursor is hard, and will only work if the conclusion has exactly the right shape. This is the case in your original example, but if you replace p with a more complicated thing, it won't work at all.

[Kim Morrison]

@Alex Meiburg, @Patrick Massot, lean#11494 ensures that this lemma is found. In fact, hopefully we recover the old mathlib3 behaviour, as now all "unindexable" lemmas (i.e. DiscrTree keys [*] and [Eq.eq, *, *, *]) are tried in a second pass automatically. You can disable this with exact? -start.

[Kim Morrison]

I'm particularly interested if anyone has reports of exact? timing out or being very slow, as I have a PR ready to install parallelism in exact? at lean#11369, but I don't yet have convincing evidence it helps!

(In particular, making this useful probably requires not parallelising every task, but chunking to limit the task overhead, and I need some good slow examples to tune this on.)

[Alex Meiburg]

Exciting! I'll be curious to try this out. :)

[Kim Morrison]

@Alex Meiburg, I'm looking forward to you trying out the new exact? +grind. Sometimes it is too expensive (examples where it is slow very welcome!!) but it gives some lovely results. (It's the same first stage as exact?, but instead of solely relying on solve_by_elim to discharge the hypotheses, it can also use grind. So often slight mismatches get covered by grind, particularly small arithmetical differences.)

[Julian Berman]

Is the idea to evaluate possibly making grind the default discharger? Or just stay an alternate?

[Alex Meiburg]

What kind of terms does exact? +grind produce? Is it always grind [one_extra_library_thm]?

[Robin Arnez]

I think exact some_kind_of_theorem x y hxy (by grind) (by grind)

[Kim Morrison]

Julian Berman said:

Is the idea to evaluate possibly making grind the default discharger? Or just stay an alternate?

I would need many more user reports about its effectiveness / speed before considering this.

[Kim Morrison]

If you're looking for suggestions like grind [one_extra_library_thm], please try grind +suggestions (and, for those with in house AIs, please try out set_library_suggestions, and see if you can get your AI to make good suggestions!)

[Alex Meiburg]

I see, yeah it makes sense what Robin said, and I see why that falls much more naturally under exact? than what I was thinking. :)