fun_prop and ContinuousOn

Stream: mathlib4

[Alex Meiburg]

I'm often confused by how fun_prop interacts with things like ContinuousOn vs. Continuous. I thought I had a good grasp on it, but then today:

import Mathlib

lemma Real.continuousOn_rpow_Ioi (x : ℝ) : ContinuousOn (fun r => x ^ r) (Set.Ioi 0) := by
  apply Continuous.continuousOn
  fun_prop

lemma Real.continuousOn_rpow_Ioi_2 (x : ℝ) : ContinuousOn (fun r => x ^ r) (Set.Ioi 0) := by
  fun_prop --fails?

despite Continuous.continuousOn being marked fun_prop.

[Tomas Skrivan]

This part of the trace reveals the issue

[Meta.Tactic.fun_prop] [❌️] ContinuousOn (fun r => x ^ r) (Set.Ioi 0) ▼
  [] candidate theorems for HPow.hPow #[]
  [] failed applying `ContinuousOn` theorems for `HPow.hPow`
               now trying to prove `ContinuousOn` from another function property
  [] candidate transition theorems: [@Continuous.continuousOn, @DifferentiableOn.continuousOn, @ContDiffOn.continuousOn_zero]
  [] [❌️] applying: Continuous.continuousOn ▼
    [] [❌️] Continuous fun r => x ^ r ▼
      [] candidate theorems for HPow.hPow #[Real.continuous_const_rpow, continuous_const_cpow]
      [] [❌️] applying: Real.continuous_const_rpow ▶
      [] [❌️] applying: continuous_const_cpow ▶
      [] failed applying `Continuous` theorems for `HPow.hPow`
                   now trying to prove `Continuous` from another function property
      [] maximum transition depth (1) reached
              if you want `fun_prop` to continue then increase the maximum depth with `fun_prop (maxTransitionDepth := 2)`

fun_prop changes from one function property ContinuousOn to another function property Continuous it uses so called "transition theorems" and right now it is allowed to use only one transition theorem. The rationale is that even with length two the number of paths could explode ContinuousOn <- Continuous <- ContDiff, ContinuousOn <- ContDiffOn <- ContDiff, ... but maybe this is not an issue in practice and the default depth should be higher.

import Mathlib

lemma Real.continuousOn_rpow_Ioi_2 (x : ℝ) : ContinuousOn (fun r => x ^ r) (Set.Ioi 0) := by
  fun_prop (maxTransitionDepth := 2)

Also when fun_prop hits the maximum transition depth here it should log it with logError such that it is reported back to user without digging through the trace.

[Tomas Skrivan]

Ha :) I think you incorrectly formalized the statement you got ContinuousOn (fun r : ℕ => x ^ r) (Set.Ioi 0) which is true because you have discrete topology on natural numbers.

[Tomas Skrivan]

Maybe you wanted to say this?

import Mathlib

lemma Real.continuousOn_rpow_Ioi (x : ℝ) (hx : x ≠ 0) : ContinuousOn (fun r : ℝ => x ^ r) (Set.Ioi 0) := by
  fun_prop (disch:=assumption)

[Tomas Skrivan]

I remember there was a request in the past to make assumption as the default discharger ... I havn't done it yet though

[Tomas Skrivan]

Alex Meiburg said:

I'm often confused by how fun_prop interacts with things like ContinuousOn vs. Continuous. I thought I had a good grasp on it, but then today:

To your original question, when working with the *On variants you almost always want to run fun_prop with a discharger to prove the side conditions.

[Alex Meiburg]

Oh, yes I did notice later that it was a bad statement, but mostly I was confused about it not being "transitive" :sweat_smile: but this makes sense. Yes, a nicer error message would be good, I just thought it wasn't able to find a path at all!

Thanks! :folded_hands:

[Yury G. Kudryashov]

BTW, should fun_prop know that a function on discrete topology is continuous?

[Alex Meiburg]

I'm pretty sure it does, and that's what it used here.

[David Ledvinka]

Yes the trace or show_term shows that it uses continuous_of_discreteTopology

[Jireh Loreaux]

Tomas Skrivan said:

but maybe this is not an issue in practice and the default depth should be higher.

I don't think that's what this is communicating. I think rather it means that we should be adding the intermediate lemmas for specific functions, even if we end up proving them using by fun_prop.

[Jireh Loreaux]

@Frédéric Dupuis I think this maxTransitionDepth has bitten us before, so I wanted to draw your attention to it.

[Tomas Skrivan]

Ahh right, I remember talking about this before and the conclusion was to add missing theorems rather than increasing the maximum transition depth.

So the error message could suggest increasing the transition depth as a temporary fix and suggest that there is a missing transition theorem. Unfortunately, it is not clear to me how to generate the statement of the missing theorem so you don't have to crawl through fun_prop trace and figure out what is missing.

[Alex Meiburg]

What about something like: if fun_prop fails, it re-runs itself with maxTransitionDepth one higher. If that passes, it still "fails" as a tactic, but prints out an error message explaining the situation. ("You can either pass maxTransitionDepth := 2 to use this tactic, but likely this means that there is a lemma you should have but don't. The following proof ... was found.")

... but I guess, does that run the issue where when fun_prop is used as a discharger or whatever, we still get the slowdown? But maybe we'd still want this behavior in that case?

[Alex Meiburg]

I mean I'm trying to think of a way to let people know that this can be done, and you should add the theorem, but keep it fast on solid proofs

[Tomas Skrivan]

I don't think a second run with higher transition depth is the way to go as fast failure is important too

[Alex Meiburg]

Mm. I wonder how easy it would be for a tactic to detect if it's a "top-level" tactic (that is, actual user input, as opposed to a discharger for something else) and then try harder... hmph

[Michael Rothgang]

Maybe we can have a variant fun_prop! that has the auto-rerunning behaviour?

[Jireh Loreaux]

I have a recent thread where I suggested that failing tactics should come with error messages that tell how to debug them. They could also come with "try this more expensive but more powerful suggestion, but beware it probably means you are missing X, Y or Z".

Basically, failing tactics shouldn't just fail, they should provide the user with a bunch of clickable options to try.

[Tomas Skrivan]

I guess the most common fun_prop failure is a missing theorem. Would it be a good idea to have a code action that would replace fun_prop with for example have : Continuous foo := sorry; fun_prop.

And it is users responsibility appropriately generalize foo to turn that have into free standing theorem.

[Jireh Loreaux]

I don't think there's any way to determine what foo should be, is there? As multiple lemmas might apply.

[Alex Meiburg]

It might be too verbose (I don't know), but a good outer approximation would be printing out all the terminal goals - any goals where fun_prop couldn't find any applicable theorem. (This is sort of similar to the error message it already prints, which is very good.)

[Anne Baanen]

Aesop (and therefore also continuity, etc) prints out the goals after applying only the safe subset of rules. Maybe we can do the same for fun_prop (and others)?

[Jireh Loreaux]

I don't know that there exist "safe" rules for fun_prop (certainly not formally, but even informally I'm not sure what would qualify). But certainly this kind of thing would be great for tactics in general.