continuity -> fun_prop

Stream: mathlib4

[Yury G. Kudryashov]

In #12661 I'm trying to migrate from continuity to fun_prop. @Tomas Skrivan Could you please have a look at some failures, e.g., in Topology/ContinuousFunction/Basic?

[Jireh Loreaux]

@Yury G. Kudryashov is the fun_prop update PR ready / merged yet? If not, I think we should focus on that. I'm on mobile, so finding the PR now is a bit hard.

[Yury G. Kudryashov]

I guess, I missed this PR.

[Yury G. Kudryashov]

Is it #11092?

[Jireh Loreaux]

More than likely some of the failures will be fixed by that PR (especially regarding eta-expansion)

[Jireh Loreaux]

You could merge that and see if it resolves your issues here.

[Yury G. Kudryashov]

I'll do it later today.

[Yury G. Kudryashov]

Still fails to prove Continuous fun b ↦ Function.const α b, Continuous fun ig ↦ (f ig.fst) ig.snd etc

[Tomas Skrivan]

If you look at the error message of fun_prop it says:

No theorems found for `Function.const` in order to prove Continuous fun b ↦ Function.const α b

and

No theorems found for `Function.eval` in order to prove Continuous fun f ↦ Function.eval i f

Adding a continuity theorems for Function.const and Function.eval would fix the issues. However fun_prop unfolds id, Function.comp, Function.HasUncurry.uncurry and Function.uncurry by default even though they are not marked as reducible.

Should I add Function.const and Function.eval to this list? Or should we add continuity theorems for them? I'm not sure what is the mathlib convention on this.

I have to think a bit more about the third problem:

Continuous fun ig ↦ (f ig.fst) ig.snd

[Tomas Skrivan]

Actually, what is the manual proof of (f : ∀ i, C(X i, A)) → Continuous fun ig ↦ (f ig.fst) ig.snd ?

[Tomas Skrivan]

Uff I do not work with sigma types very often so I'm surprised by this:

import Mathlib

variable {I A : Type*} [TopologicalSpace A]
#synth TopologicalSpace (I×A)     -- fails
#synth TopologicalSpace ((_:I)×A) -- works

I'm afraid that this might require some major changes to fun_prop as I have never considered the case when you have a generic type I and object(in categorical sense e.g. topological space in this case) A then I×A or (_:I)×A is an object again.

[Tomas Skrivan]

I would recommend providing the continuity proof in ContinuousMap.sigma by hand for now and send me any other examples every time you encounter something similar.

[Mitchell Lee]

Tomas Skrivan said:

Actually, what is the manual proof of (f : ∀ i, C(X i, A)) → Continuous fun ig ↦ (f ig.fst) ig.snd ?

The manual proof is to use docs#continuous_sigma.

Also, the most obvious topology on I × A is the product topology. That's why you need TopologicalSpace I in order to synthesize TopologicalSpace (I × A). If you want to think of I × A as a disjoint union of I copies of A, then you need to put the discrete topology on I.

[Yury G. Kudryashov]

Note that fun_prop tries to apply continuous_sigma, then fails, possibly because it fails to simplify Sigma.fst (Sigma.mk i x) to i to unify the goal with map_continuous

[Tomas Skrivan]

Yes something odd is happening when applying continuous_sigma but I didn't manage to resolve it yet.

[Yury G. Kudryashov]

Can it run dsimp so that it unfolds all definitions with @[simp] theorem myFun_apply?

[Tomas Skrivan]

I can try it but I'm a bit worried that would make the tactic slower.

Anyway, you can always set that the default tactic proving continuity in ContinuousMap to dsimp; fun_prop instead of just fun_prop.

[Yury G. Kudryashov]

The issue is that sometimes it has to run dsimp after applying a rule. Can it be an option? Or a backup option if the main route fails?

[Tomas Skrivan]

Can you give me a concrete example where it is really the case? I think the example with Sigma breaks earlier and sends the tactic on the wrong path. If I fix the earlier issue then normalisation is not necessary.

Anyhow, I can add an optional normalization tactic but I'm afraid that people would use it to fix issues that should be fixed differently and then run into performance issues.

I'm using the tactic a lot and so far I never needed normalization.

[Yury G. Kudryashov]

I'll test it tomorrow with more lemmas instead of normalization.

[Yury G. Kudryashov]

I got distracted by day job etc. One more question: Is it possible to make fun_prop use docs#IsProperMap.continuous, or it's out of scope?

[Yury G. Kudryashov]

continuity can use it because it uses aesop.

[Tomas Skrivan]

Yes you can already mark that theorem with fun_prop. I call these theorems "transition", if you turn on trace.Meta.Tactic.fun_prop.attr you should see a message saying that. Similarly you can mark theorem implying continuity from differentiability etc. However, it is the user's responsibility to not introduce a cycle.

[Tomas Skrivan]

Some care needs to be taken with transition theorems. Once I added all the theorems saying that a linear map between finite dimensional vector spaces is a nice(continuous, differentiable,...) and it caused noticeable slowdown.

[Yury G. Kudryashov]

In branch#YK-continuity, fun_prop breaks on Mathlib/Topology/ProperMap.

Failed to prove necessary assumption IsProperMap fun a0 ↦ g a0 when applying theorem IsProperMap.continuous.

while IsProperMap g is one of the assumption.

[Tomas Skrivan]

You should mark IsProperMap with fun_prop attribute too.

Alternatively you can run fun_prop with a discharger, fun_prop (disch:=assumption)

[Floris van Doorn]

I also ran against fun_prop not finding local hypothesis in the following example:

import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

@[fun_prop]
theorem Real.continuous_rpow_const {q : ℝ} (h : 0 < q) :
    Continuous (fun x : ℝ => x ^ q) :=
  continuous_iff_continuousAt.mpr fun x ↦ continuousAt_rpow_const x q (.inr h)

example (p : ℝ) (hp : 0 < p) : Continuous (fun x : ℝ ↦ x ^ p) := by
  fail_if_success fun_prop -- I expected this to work
  have := Real.continuous_rpow_const hp
  fun_prop

Can we have with_reducible assumption as the default decharger for fun_prop? It is quite common in Lean that tactics freely use local hypotheses (e.g. the default termination_by discharger uses local hypotheses).

[Jireh Loreaux]

Tomas Skrivan said:

You should mark IsProperMap with fun_prop attribute too.

Alternatively you can run fun_prop with a discharger, fun_prop (disch:=assumption)

Ha! I didn't see this discussion until just now, but I ran into the problem that IsProperMap wasn't marked as fun_prop and fixed this in #13538, which is on the queue now @Yury G. Kudryashov

[Yury G. Kudryashov]

What's the right fun_prop-based tactic that could replace continuity in "auto" fields? I tried dsimp; fun_prop in #14040 but it looks like the increase in dsimp time is greater than the decrease in aesop time (both are small).

[Yury G. Kudryashov]

I don't know how to get a better benchmark here.

[Tomas Skrivan]

Do you have examples where the normalization with dsimp is necessary?

[Tomas Skrivan]

Maybe running dsimp (config:={singlePass:=true}) only could be enough?

[Yury G. Kudryashov]

I'll try that.

[Yury G. Kudryashov]

There is no singlePass config option for dsimp.

[Tomas Skrivan]

But I'm really curious to see cases where you need normalization.

[Yury G. Kudryashov]

Without any dsimp it gets goals like Continuous (Equiv.invFun {toFun := .., invFun := .., ..}) and tries to look for a lemma about Equiv.invFun.

[Tomas Skrivan]

Oh I see, maybe I should modify the algorithm for functions like invFun. Giving me all the examples where it fails would be really useful!

[Yury G. Kudryashov]

I removed dsimp; in #14040, now it's going to give you all the errors.

[Yury G. Kudryashov]

Do you prefer to change fun_prop, or try use by dsimp only; fun_prop first? Anyway, feel free to push to this branch.

[Tomas Skrivan]

I'm curious about the cases that require normalization as I'm still not convinced that it is really required if the tactic is tweaked properly. But of course just using dsimp only; fun_prop would be easier if it works and is fast enough.

[Yury G. Kudryashov]

Let's wait for the failures of the current commit (without dsimp only) first, then I'll test if dsimp only fixes compile.

[Yury G. Kudryashov]

It compiles with dsimp only. I called !bench but I'm not very good at reading the report.

[Yury G. Kudryashov]

My guess: this adds only several calls to dsimp only; fun_prop, so any change in performance is of the order of a random noise in the rest of Mathlib.

[Michael Rothgang]

By the way: #13959, #14009 and #13994 perform some "easy" continuity -> fun_prop replacements; review is welcome. (The last one has some changes worth discussing, around changing default proof fields from by continuity to by fun_prop, which doesn't always work.)

[Jireh Loreaux]

For replacing default proof fields, I think we should wait until #11092 is finished.

[Jireh Loreaux]

currently there are a few nasty behaviors in fun_prop which can cause it to loop (basically, metavariables it can work around), and crash the server. We wouldn't want this happening in default fields. That would be a recipe for tremendous pain.