How to avoid the id-comp loop in aesop?

Stream: mathlib4

[Moritz Doll]

I am in the process of porting Topology.ContinuousFunction.Basic, which makes quite some use of the continuity tactic and if I remember correctly, we wanted to replace that by aesop. In continuity there was the issue that the naive implementation would try refine continuous_id.comp _ forever. How does aesop avoids this and how do I have to tag the identity and comp lemmas?

[Yury G. Kudryashov]

AFAIK, we don't have the continuity tactic, so I'm just replacing tags with

-- porting note: todo: restore @[continuity]

[Yury G. Kudryashov]

Clearly, the answer to your question depends on how the continuity tactic will be implemented in Lean 4.

[Jireh Loreaux]

Moritz, I was considering trying to port the continuity tactic earlier today, but I'm not exactly sure how to make the right kind of attribute. If you want we can try to find some time to work on it together this weekend. Just DM me if so.

[Yaël Dillies]

Isn't the naive implementation working now that function.comp is semireducible?

[Moritz Doll]

I have no idea. I am trying to get aesop to fail, but it seems to totally fine even when the comp and id lemmas have higher priority

[Reid Barton]

The original implementation would literally just try to use refine continuous.comp _ _, so no it doesn't matter that function.comp is semireducible.

[Reid Barton]

Or hmm, I guess maybe it depends on how the details of higher-order unification work, but if it does matter, then it probably also breaks some cases in which continuity works in mathlib 3

[Moritz Doll]

The one example from the comments in the Lean 3 tactic works just fine, is there a nontrivial example that has higher chance of breaking?

import Mathlib.Topology.Basic

declare_aesop_rule_sets [Continuous]

variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ]

@[aesop norm apply (rule_sets [Continuous])]
theorem continuous_id' : Continuous (id : α → α) := continuous_id

@[aesop safe apply (rule_sets [Continuous])]
theorem Continuous.comp' {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) :
    Continuous (g ∘ f) := Continuous.comp hg hf

@[aesop unsafe 10% apply (rule_sets [Continuous])]
theorem continuous_const' {b : β} : Continuous fun _ : α => b := continuous_const

example {x : γ} {f : α → β} (hf : Continuous f) :
    Continuous ((fun _ : β => x) ∘ f) := by aesop (rule_sets [Continuous])

example {f : α → α} (hf : Continuous f) :
  Continuous (fun x => f x) := by aesop (rule_sets [Continuous])

[Moritz Doll]

(attributes are stupid, I really want to see aesop fail)

[Reid Barton]

Can it prove Continuous (fun x => g (f x)) from Continuous f, Continuous g?

[Moritz Doll]

nope, that fails

[Reid Barton]

If you add this lemma as a Continuous.comp'', then do you end up with loops?

[Reid Barton]

(I mean add as an aesop lemma alongside the ones you have already)

[Moritz Doll]

no loops for the triple composition at least

[Jannis Limperg]

I'm not sure about the specifics here, but conceptually, there are two ways to deal with a lemma that always applies:

• You can register it as a very low-probability unsafe rule, so Aesop will only use it as a last resort. This is generally fine if Aesop succeeds, but if Aesop can't prove the goal, it'll only fail after it has reached 200 rule applications or search depth 30. (The limits are configurable.)
• You can make a little special-purpose tactic that applies continuous_id.comp _ only if the conditions from Lean 3 are met, then register that as an Aesop rule.

I'd be very happy to help with this; replacing continuity and similar tactics was one of the original motivations for Aesop.

[Jireh Loreaux]

I played around with aesop as a replacement for continuity over the weekend, and in my tests it seemed to do okay. I even heinously marked all the basic things as safe (continuous_id, Continuous.comp, continuous_const and variants to get around reducibility issues) and I couldn't make it fail or loop.

[Moritz Doll]

I've started a PR in !4#2145, feel free change my macros if you have something more sophisticated.

[Moritz Doll]

I've now restored all the continuity attributes and the except for two cases all the by continuity proofs. in one case continuity! was used and in the other we need to change the aesop config, so that it unfolds the definition. I will not continue to work on that branch this evening, so if anyone wants to do stuff they are very welcome to do so