apply? weakness

Stream: lean4

[Michael Stoll]

Consider the following:

def foo (n : Nat) : Nat := n * n

example (a b : Nat) : foo a = foo b := by
  apply? -- lots of unhelpful suggestions

example (a b : Nat) (h : a = b) : foo a = foo b := by
  apply? -- Try this: exact congrArg foo h

Why does apply? in the first example not come up with refine CongrArg foo ?_, leaving the goal a = b?

[Ruben Van de Velde]

Discrimination tree?

[Kevin Buzzard]

What is a discrimination tree and where can I read about it?

[Michael Stoll]

Does the discrimination tree include information on the hypotheses in context?
Note that the only difference in the two examples is the presence or otherwise of h.

[Michael Stoll]

Or is the reason that apply? tries exact? (and returns whatever it produces when successful) before looking at the discrimination tree?

[Michael Stoll]

My motivation for asking this is the observation that when my goal is an equality of real numbers (say), then apply? almost never gives a useful suggestion (and if it does, it is so far down the list that I lose patience scrolling before reaching it).
Can apply? be made more helpful with goals like this?

[Michael Stoll]

Compare also:

import Mathlib

example (a b : ℝ) : a.exp = b.exp := by
  apply? -- Try this: refine Real.exp_eq_exp.mpr ?_

example (a b : ℝ) : a.log = b.log := by
  apply? -- lots of unhelpful suggestions

Here there is a specialized lemma for Real.exp, which apply? finds (but there appears to be no lemma for Real.log).

[Kyle Miller]

Not answering your question, but congr is a useful tactic here (or mathlib's version, congr!)

[Michael Stoll]

I know, but that's not the point here.

[Adam Topaz]

@Kevin Buzzard the module docstring here has some info https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/DiscrTree.html

[Kevin Buzzard]

Well that's a lot more over-my-head than I was hoping for, I get stuck on line 2, but it sounds like this has probably got nothing to do with the question here -- is it true that apply? tries exact?? That would perhaps explain Michael's observation.

[Kim Morrison]

Michael Stoll said:

Consider the following:

def foo (n : Nat) : Nat := n * n

example (a b : Nat) : foo a = foo b := by
  apply? -- lots of unhelpful suggestions

example (a b : Nat) (h : a = b) : foo a = foo b := by
  apply? -- Try this: exact congrArg foo h

Why does apply? in the first example not come up with refine CongrArg foo ?_, leaving the goal a = b?

What is going on here is that apply? actually tried running solve_by_elim first!

This means that with h present, it can find the congrArg proof, even though this would be available via the discrimination tree based lookup of potentially relevant lemmas.

[Michael Stoll]

Kim Morrison said:

This means that with h present, it can find the congrArg proof, even though this would be available via the discrimination tree based lookup of potentially relevant lemmas.

Is there a "not" missing somewhere in this sentence? I.e., the discrimination tree based lookup does not find docs#congrArg ?

[Kim Morrison]

Indeed.