isBoundedDefault not triggering

Stream: metaprogramming / tactics

[Damien Thomine]

When working with liminf and limsup, there are some boundedness hypotheses which may have to be checked on some spaces (such as reals) but are automatically satisfied on other spaces (such as extended reals).

In order to avoid duplicate theorems, and not having to fill these hypotheses by hand when they are trivially satisfied, the current philosophy is to have each theorem in the largest generality (with these boundedness hypotheses), and an isBoundedDefault tactic which automatically fills these hypotheses (defined in Mathlib.Order.LiminfLimsup).

The problem is that isBoundedDefault does trigger in direct proof terms (or exact, have...), but not on apply. Some kind of minimal example is:

import Mathlib.Data.Real.EReal
import Mathlib.Order.LiminfLimsup

open Filter

theorem proof_term {α : Type*} {f : Filter α} {u v : α → EReal} (h : u ≤ᶠ[f] v) :
    limsup u f ≤ limsup v f :=
  limsup_le_limsup h

theorem by_exact {α : Type*} {f : Filter α} {u v : α → EReal} (h : u ≤ᶠ[f] v) :
    limsup u f ≤ limsup v f := by
  exact limsup_le_limsup h

theorem by_apply {α : Type*} {f : Filter α} {u v : α → EReal} (h : u ≤ᶠ[f] v) :
    limsup u f ≤ limsup v f := by
  apply limsup_le_limsup
  · exact h
  · use ⊥; simp
  · use ⊤; simp

This makes the proofs more awkward and cluttered than they need to be. Would it be possible to modify isBoundedDefault to trigger on apply?

Paging @Sébastien Gouëzel

[Sébastien Gouëzel]

I'd like to mention that I think it's an important issue. Unfortunately, I am not competent on this, we need some metaprogramming understanding here I'd say.

[Damiano Testa]

Is it just a matter of a missing assumption? In the example above, this works:

  repeat first
    | apply isCobounded_le_of_bot
    | apply isCobounded_ge_of_top
    | apply isBounded_le_of_top
    | apply isBounded_ge_of_bot
    | assumption

[Damiano Testa]

I tried looking at the lean3 code and it uses applyc. Looking into that, it may be that applyc did try some form of assumption on the goals, so this may be indeed a fix.

[Damiano Testa]

If you have more examples where this fails, I can look into it!

[Damiano Testa]

#14617

[Damien Thomine]

Let me sum up here the discussion in #14617:

• There is a distinction between

by apply limsup_le_limsup h

which has always worked, and

by apply limsup_le_limsup; exact h

which we would like to have.

• The latter is not fixed by adding assumption.
• In the meantime, there are a few imperfect solutions: refine limsup_le_limsup ?_, apply limsup_le_limsup ?_, apply (limsup_le_limsup).

Thank you for your efforts. I must say that this behaviour is puzzling for somebody like me who does not know the intricacies of Lean.

[Damiano Testa]

My vague understanding of the issue is that apply does not pass information about the meta variables that it leaves behind until it is too late for the auto-param to realize that it could have made progress. The workarounds above either give more context to the remaining goals or delay them a bit.