Regression in continuity

Stream: mathlib4

[Bhavik Mehta]

import Mathlib.Analysis.Calculus.ContDiffDef

example {x : ℝ} {n : ℕ} : Continuous (fun t : ℝ => (x - t) ^ (n + 1)) :=
  by continuity

This fails, but the equivalent works in mathlib3. The error message is

aesop: exceeded maximum number of normalisation iterations (100). This means normalisation probably got stuck in an infinite loop.

[Scott Morrison]

I remain unconvinced that continuity should be implemented on top of aesop, and think that the mathlib3 implementation on top of solve_by_elim is likely to be more performant. It just doesn't need the full power of aesop.

[Jireh Loreaux]

Is this the HPow bug?

[Kevin Buzzard]

Can someone remind me why we haven't just merged that one line of gobble-de-gook which fixes it 9 times out of 10?

[Eric Wieser]

We don't even need to merge that one line, we can remove the line in core that makes us need the gobble-de-gook

[Eric Wieser]

I think the problem is that a better solution is in the pipeline, and so no one wants to think about the fast solution

[Bhavik Mehta]

Jireh Loreaux said:

Is this the HPow bug?

No - adding the usual incantation doesn't help, nor does it change how the goal here is elaborated

[Jireh Loreaux]

I'm curious how elaboration gets it right here but wrong everywhere else. That's strange.

[Yaël Dillies]

because it doesn't import Analysis.SpecialFunctions.Pow.Real

[Jannis Limperg]

The cause of the timeout is that npowRec is registered as an unfold rule. Aesop unfold works like the unfold tactic, so it'll unfold recursive functions over and over again, until timeout. (I should probably just forbid unfold rules for recursive declarations.) Registering npowRec as a simp rule instead makes progress:

import Mathlib.Analysis.Calculus.ContDiffDef

erase_aesop_rules [npowRec (rule_sets [Continuous])]

attribute [aesop simp] npowRec

example {x : ℝ} {n : ℕ} : Continuous (fun t : ℝ => (x - t) ^ (n + 1)) := by
  continuity

This leaves the goal Continuous (npowRec n).

[Bhavik Mehta]

Hmm, this still isn't a complete fix because in mathlib3 continuity closes the goal, rather than leaving another goal...

[Eric Wieser]

docs#npowRec shouldn't be a rule at all... It should be pow_succ or similar if we really want such a rule

[Eric Wieser]

npowRec is an implementation detail used to implement Monoid.npow for only some types.

[Moritz Doll]

This works:

import Mathlib.Analysis.Calculus.ContDiffDef

erase_aesop_rules [npowRec (rule_sets [Continuous])]

attribute [aesop apply norm] Continuous.pow

example {x : ℝ} {n : ℕ} : Continuous (fun t : ℝ => (x - t) ^ (n + 1)) := by
  continuity

[Jireh Loreaux]

I think we may need a separate theorem when the exponent is a numeric literal, but I may be wrong.

[Moritz Doll]

example {x : ℝ} : Continuous (fun t : ℝ => (x - t) ^ 5) := by
  continuity

works as well

[Moritz Doll]

the problem seems to be that the safe version does not fire, but the norm-one does and the standard way of adding continuity lemmas is through apply safe.

[Moritz Doll]

mathlib4#7909

[Junyan Xu]

I'm puzzled why the first two succeeds but the last fails:

import Mathlib.Topology.ContinuousOn

example {α} [TopologicalSpace α] : Continuous fun p : α × α ↦ p.1 := by continuity -- succeeds
example {α} [TopologicalSpace α] : Continuous fun p : {x : α // x = x} ↦ p.1 := by continuity -- succeeds

example {α} [TopologicalSpace α] : Continuous fun p : {p : α × α // p.1 = p.2} ↦ p.val.1 := by continuity
/- tactic 'aesop' failed, failed to prove the goal. Some goals were not explored because the
  maximum rule application depth (30) was reached. Set option 'maxRuleApplicationDepth' to
  increase the limit. -/

I have to switch to apply_rules [continuous_fst, continuous_subtype_val, Continuous.comp] here.

[Jannis Limperg]

Moritz Doll said:

the problem seems to be that the safe version does not fire, but the norm-one does and the standard way of adding continuity lemmas is through apply safe.

This is just a bandaid; please don't start adding continuity rules as norm rules. The underlying issue is:

• Aesop runs apply rules with default transparency.
• Usually, this is somewhat hidden because Aesop's index selects rules which match the goal at reducible transparency.
• The index doesn't seem to work well for continuity rules, in the sense that it just returns any rule matching Continuous _ (making it quite pointless :fear:).
• As a result, Continuous.mul is applied to the goal, since it is defeq to a multiplication after unfolding npowRec. Continuous.mul also happens to fire before Continuous.pow, so the latter doesn't get a chance any more.

The correct fix is to make sure that continuity rules are only applied at reducible transparency:

import Mathlib.Analysis.Calculus.ContDiffDef

erase_aesop_rules [npowRec (rule_sets [Continuous]), Continuous.mul (rule_sets [Continuous])]

attribute [aesop safe (apply (transparency! := reducible))] Continuous.pow Continuous.mul

example {x : ℝ} {n : ℕ} : Continuous (fun t : ℝ => (x - t) ^ (n + 1)) := by
  continuity

example {x : ℝ} : Continuous (fun t : ℝ => (x - t) ^ 5) := by
  continuity

(I learned all this from set_option trace.aesop true.)

[Jannis Limperg]

Jannis Limperg said:

The index doesn't seem to work well for continuity rules, in the sense that it just returns any rule matching Continuous _ (making it quite pointless :fear:).

This is a limitation of DiscrTree as currently implemented: it doesn't index lambdas, treating them as wildcards.

[Jannis Limperg]

Junyan Xu said:

I'm puzzled why the first two succeeds but the last fails:

import Mathlib.Topology.ContinuousOn

example {α} [TopologicalSpace α] : Continuous fun p : α × α ↦ p.1 := by continuity -- succeeds
example {α} [TopologicalSpace α] : Continuous fun p : {x : α // x = x} ↦ p.1 := by continuity -- succeeds

example {α} [TopologicalSpace α] : Continuous fun p : {p : α × α // p.1 = p.2} ↦ p.val.1 := by continuity
/- tactic 'aesop' failed, failed to prove the goal. Some goals were not explored because the
  maximum rule application depth (30) was reached. Set option 'maxRuleApplicationDepth' to
  increase the limit. -/

I have to switch to apply_rules [continuous_fst, continuous_subtype_val, Continuous.comp] here.

The issue here is that simp rewrites the goal

⊢ Continuous (β := α × α) fun (x : { p : α × α // p.1 = p.2 }) ↦ ↑x

to

⊢ (Continuous (β := α) fun (x : { p : α × α // p.1 = p.2 }) ↦ x.1.1) ∧
   Continuous (β := α) fun (x : { p : α × α // p.1 = p.2 }) ↦ x.1.2

and from there Aesop doesn't do anything useful any more. So Aesop with simp disabled solves it:

example {α} [TopologicalSpace α] : Continuous fun p : {p : α × α // p.1 = p.2} ↦ p.val.1 := by
  aesop (rule_sets [Continuous]) (simp_options := { enabled := false })

Possible fixes:

• Disable the simp rule in continuity (also good for performance).
• Erase this particular simp lemma.
• Teach Aesop how to make progress from the 'simplified' goal.

[Bhavik Mehta]

Without trying any of these, my feeling is that removing the simp rule from continuity is the most sensible. It brings continuity back to its old method (which seemed to work reasonably well) of trying continuity rules until you can't any more, it's a performance boost as you say, and it makes the continuity tactic more modular.

[Moritz Doll]

I am testing out these changes right now, let's hope that they don't break anything major.

[Notification Bot]

Adomas Baliuka has marked this topic as resolved.

[Notification Bot]

Adomas Baliuka has marked this topic as unresolved.

[Adomas Baliuka]

Sorry, I misclicked... (Wanted to mark the topic to get notifications)

To add some content to the useless apology, the idea of removing the simp rule also suggested itself while working on a new differentiability tactic modeled after continuity. Since I probably won't get any more comments on the PR or the previous topics discussing it: does anyone have insights into how much the two tactics should be the same? Is there any significant conceptual difference I should keep in mind?

[Jireh Loreaux]

@Adomas Baliuka can you link to the PR please?

[Adomas Baliuka]

PR, WIP. I asked about it here. It's basically exactly like continuity (maybe it should be slightly different) but it's slow (often needs heartbeat increase) and I'm confused by some of the behaviours, need to keep looking into it.

[Jannis Limperg]

@Moritz Doll let me know if you'd like me to take a look at this.

[Eric Wieser]

Jannis Limperg said:

Jannis Limperg said:

The index doesn't seem to work well for continuity rules, in the sense that it just returns any rule matching Continuous _ (making it quite pointless :fear:).

This is a limitation of DiscrTree as currently implemented: it doesn't index lambdas, treating them as wildcards.

Is there a tracking issue for this?

[Tomas Skrivan]

Eric Wieser said:

Is there a tracking issue for this?

I would be very interested in this! In the tactic I'm writing I stopped using DiscrTree for this exact reason as it was returning too many candidates.

Does anybody know how to properly index lambdas? At least in principle, I would be happy to implement it.

What I'm concerned is how to properly handle eta reduction such that Continuous fun x => Real.exp x matches Continuous fun x => Real.exp (f x) with f = fun x => x and Continuous fun x => exp x + x matches Continuous fun x => (f x) + (g x). Or what to do when there are move bound variables and they appear in the head of the lambda body like Continuous fun array i => array (i+1).

[Tomas Skrivan]

Eric Wieser said:

Is there a tracking issue for this?

I have created thread for it on #lean4 dev . If it is really considered an issue I can convert it into github issue.