apply? failure

Stream: general

[Patrick Massot]

@Scott Morrison my students found a very surprising apply? failure.

import Mathlib

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

example {v : E → E} (hv : ContDiff ℝ ⊤ v) :
    ContDiff ℝ 1 v := by
  exact hv.of_le le_top


example {n : ℕ} {v : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n) } (hv : ContDiff ℝ ⊤ v) :
    ContDiff ℝ 1 v := by
  sorry
  -- apply?

Trying apply? in the first proof return a lot of junk not including the relevant lemma. We really need suggestions that include the head symbol of the goal to appear first. In the second more concrete version it simply times out.

[Floris van Doorn]

I was wondering about better orderings for apply? suggestions. Every lemma that apply? tries comes with a discrimination tree, right? I think the size of this discrimination tree (number of nodes / number of non-* nodes, something like that) would be a reasonably good measure to how useful a lemma is: it means that you choose lemmas first that are more specific to the particular goal you're currently proving.

[Patrick Massot]

In the example I gave there is really no challenge at all: the goal is ContDiff ... and the relevant lemma has conclusion ContDiff ....

[Scott Morrison]

Floris van Doorn said:

I was wondering about better orderings for apply? suggestions. Every lemma that apply? tries comes with a discrimination tree, right? I think the size of this discrimination tree (number of nodes / number of non-* nodes, something like that) would be a reasonably good measure to how useful a lemma is: it means that you choose lemmas first that are more specific to the particular goal you're currently proving.

Yes, this would be a nice. I haven't done this so far because it is slightly annoying to actually discover the indexing keys for the returned lemmas from a DiscrTree! We would need some additional plumbing to retrieve these as part of the lookup.

I agree they could be used to give much nicer results.

[Scott Morrison]

@Patrick Massot, for me the second example returns quite quickly, maybe you could double check this with current master. (I did fix a problem in exact? mid last week.)

[Scott Morrison]

What lemma are you hoping to see at the top of the list in the second example?

[Scott Morrison]

For the first example, of_le is returned as the 14th result. Not ideal, but at least it is still there.

The reason apply? does not use of_le to close the goal is because of the side condition 1 ≤ ⊤ generated after using the hypothesis hv. Although this can be discharged by the tactic trivial, solve_by_elim only tries the term trivial, which can't solve this.

We could boost the power of the solve_by_elim discharger for apply? by allowing it to in turn call trivial, ... but this is scope creep, and does come with a (maybe small?) performance cost.

[Patrick Massot]

I confirm the problem no longer occurs on master. However The suggestion is

Try this: refine ContDiff.of_le ?h ?hmn
Remaining subgoals:
⊢ ℕ∞
⊢ ContDiff ℝ ?n v
⊢ 1 ≤ ?n

instead of refine ContDiff.of_le hv ?hmn. Do you understand why?

[Patrick Massot]

@Robert Trosten This is the apply bug from last week. Things would get better if you update the dependencies of your project.

[Scott Morrison]

Patrick Massot said:

I confirm the problem no longer occurs on master. However The suggestion is

Try this: refine ContDiff.of_le ?h ?hmn
Remaining subgoals:
⊢ ℕ∞
⊢ ContDiff ℝ ?n v
⊢ 1 ≤ ?n

instead of refine ContDiff.of_le hv ?hmn. Do you understand why?

@Patrick Massot, it does this because it is not certain that using hv is a good idea. In particular, hv assigns the value of some other metavariable (the ℕ∞ goal), but then we can't automatically close the remaining goal which depends on that, namely 1 ≤ ?n.

It we made the discharging process more powerful by allowing it to use the trivial tactic in addition to the trivial term, this would be resolved, because by trivial : 1 ≤ ⊤ does actually work.

[Scott Morrison]

Alternatively, we could just make the exact? discharger much more aggressive about using local hypotheses, even when it is not "sure" they are correct.

[Patrick Massot]

I think it makes sense to be more aggressive because you can always delete hv from the suggestion if you don't like it (although it requires paying more attention to the suggestion).

[Scott Morrison]

Okay. This is one of those "sounds easy, but actually annoying" changes. Not right now, but request heard! :-)

[Patrick Massot]

This is really not crucial. The crucial thing was to get any output at all, and it now works.