fun_prop with grind as the discharger

Stream: mathlib4

[Frédéric Dupuis]

I suspect that there's a bug in fun_prop that prevents using grind as the discharger. Here's a reasonably minimal example.

The following lemma can be found in mathlib:

@[fun_prop]
theorem ContinuousOn.log (hf : ContinuousOn f s) (h₀ : ∀ x ∈ s, f x ≠ 0) :
    ContinuousOn (fun x => log (f x)) s := sorry

The side condition needs a discharger, and in many cases grind should be able to do the job. However, fun_prop seems to be unable to handle the proofs constructed by grind (I think it has to do with the fact that grind generates auxiliary lemmas in its proofs):

import Mathlib.Analysis.SpecialFunctions.Log.Basic

open Set

/-- This works -/
example : ContinuousOn (fun x => Real.log (x - 1)) (Ioi 1) := by
  refine ContinuousOn.log ?_ ?_
  · -- goal here: `ContinuousOn (fun x ↦ x - 1) (Ioi 1)`
    fun_prop
  · -- goal here: `∀ x ∈ Ioi 1, x - 1 ≠ 0`
    grind

/-- This works as well -/
example : ContinuousOn (fun x => Real.log (x - 1)) (Ioi 1) := by
  have : ∀ x ∈ Ioi (1 : ℝ), x - 1 ≠ 0 := by grind
  fun_prop (disch := assumption)

/-- This however fails with error:
  Unknown constant `_example._proof_1` -/
example : ContinuousOn (fun x => Real.log (x - 1)) (Ioi 1) := by
  fun_prop (disch := grind)

Perhaps @Tomas Skrivan could have a look at some point?

[Robin Arnez]

fun_prop presumably runs it through something like withoutModifyingEnv; this doesn't work here since grind creates a declaration in the environment

[Tomas Skrivan]

Correct, it uses withoutModifyingStateWithInfoAndMessages here.

Is grind working as simp discharger? The tacticToDischarge function in simp is a bit more complicated but it also uses withoutModifyingState .

Doing the same thing as simp's tacticToDischarge might resolve the issue.