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?