apply? failure

Stream: mathlib4

[Nir Paz]

Should apply? get this?

import Mathlib

def re (n m : ℕ) : Prop := n = m

instance reSetoid : Setoid ℕ where
  r     := re
  iseqv := ⟨Eq.refl, Eq.symm, Eq.trans⟩

example (a b : ℕ) (h : Quotient.mk' a = Quotient.mk' b) : re a b := by apply?

Quotient.exact h works.

[Eric Wieser]

No, because apply? isn't allowed to look at how you defined re

[Eric Wieser]

If you replace it with abbrev re instead of def re, which apply? is allowed to look through, then it works

[Nir Paz]

What about this?

import Mathlib

example (P Q : Prop) (h : P → Q) (h' : ¬Q) : ¬P := by exact?

[Patrick Massot]

I think this is simply not stated in Mathlib.

[Eric Rodriguez]

docs#mt I thought

[Eric Rodriguez]

But I thought this may be the performance optimisation stuff

[Patrick Massot]

Eric is right and I was wrong.

[Scott Morrison]

Eric, Patrick, and I were all wrong. In fact it was a bug (one of the horsemen!) fixed now in std4#368 and #8458.

[Nir Paz]

Cool! Is there a rule of thumb for when it's ok for apply to not find a single-theorem-solution, like due to "optimization stuff"?

[Nir Paz]

Because I always think of that as a problem and I guess sometimes it's not

[Nir Paz]

(Excluding things like my first example with defs)

[Scott Morrison]

As far as I know, after #8458 and #8459 land, I think the claim is:

if you can prove a goal via apply X; solve_by_elim* for some X, then exact? should work

and

if you can prove a collection of goals via apply X; apply Y; ...; apply Z, where all the X Y Z are hypotheses, then solve_by_elim* should work

These are probably wrong, but I'd be happy to see more examples where they are wrong!

[Joachim Breitner]

Great way to phrase the specification for these tactics. Maybe could be part of the docstring?

[Nir Paz]

import Mathlib.Tactic.LibrarySearch
import Mathlib.Order.RelIso.Basic

example {α} (r s t : α → α → Prop) (h : s ≃r r) (h' : r ≃r t) : α ↪ α := by
  have := h.injective
  have := h'.injective
  use fun a ↦ h' (h a)
  exact? --fails

fails, but works with use fun a ↦ (h' ∘ h) a. (apply Function.Injective.comp; solve_by_elim* works in both cases)

So does exact? not try all theorems with results defeq to the goal? If that's how it works then there must be lots of cases where it can't close goals where a single apply would work.

[Patrick Massot]

So this is not what it does. It used to do it in Lean 3 and it became unusable because Mathlib is now too large. So it uses some indexing now and this will not see through definitional equality.

[Jireh Loreaux]

Another way to say this: exact? in Lean 4 now requires that matches satisfy a stricter equality constraint.

[Nir Paz]

Is there a tactic that does what the old exact did? I often spend >2 minutes loogling and find a single theorem proof, and when it's obvious that what I want is somewhere in the library I'd rather just let that run for a minute.

[Kevin Buzzard]

You presumably mean exact? in your message. Yes it would be nice sometimes to have an exact?! or eexact? which tried harder.