Aesop and Lambdas

Stream: mathlib4

[Moritz Doll]

Aesop (more precisely the continuity macro) seems to have a major problem when dealing with lambdas. For example we have the continuity lemma Continuous (fun x => f x - f y) (provided f and g are continuous), but aesop is incapable of proving Continuous (f - g) from that.

[Moritz Doll]

We did add a duplicate theorem for Function.const, but I don't think that is a good solution, since it will come up more and more

[Moritz Doll]

Maybe we need an aesop rule set that unfolds all the fancy names into lambdas and then we flag only the applied version with continuity.

[Jannis Limperg]

Do you know what Lean 3 continuity did to make this work?

[Frédéric Dupuis]

What happens with Continuous ((fun x => f x) - (fun x => g x))?

[Floris van Doorn]

I don't think this is a regression compared to Lean 3. In a random file that imports a bunch of continuity stuff, I get

example {f g : ℝ → ℝ} (hf : continuous f) (hg : continuous g) : continuous (λ x, f x - g x) :=
by continuity -- succeeds

example {f g : ℝ → ℝ} (hf : continuous f) (hg : continuous g) : continuous (f - g) :=
by continuity -- fails

[Floris van Doorn]

Note that continuity! does succeed on both, which applies lemmas up to semireducible transparency.

[Jannis Limperg]

This makes sense, but Aesop should be applying lemmas up to default transparency anyway. I'll investigate. @Moritz Doll if you could extract the relevant defs into an MWE, that would be very helpful.

[Eric Wieser]

Isn't default transparency "don't unfold semireducible"?

[Jannis Limperg]

In Lean 4, default transparency is the same as Lean 3's semireducible afaik.

[Eric Wieser]

Does "apply lemmas up to r" mean "unfold everything more reducible than r", or does it also include unfolding things with reducibility r?

[Jannis Limperg]

I intended it to mean 'unfold constants with reducibility r and lower' (where reducible < instances < default < irreducible). Not sure whether that's standard terminology.

[Kyle Miller]

@Eric Wieser Default transparency unfolds semireducible (think what rfl can do by default). Example:

def f (n : Nat) : Nat := n + 1

example : f n = n + 1 := by rfl
example : f n = n + 1 := by with_reducible rfl -- fails

attribute [reducible] f

example : f n = n + 1 := by with_reducible rfl -- succeeds

[Moritz Doll]

@Jannis Limperg
thank you so much for looking into this (and for creating aesop in the first place).

import Mathlib.Topology.Algebra.Group.Basic

variable [TopologicalSpace X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y]

example (f g : X → Y) (hf : Continuous f) (hg : Continuous g) : Continuous (f - g) := by
  continuity

example (f g : X → Y) (hf : Continuous f) (hg : Continuous g) : Continuous (fun x => f x - g x) := by
  continuity

example (f g : X → Y) : f - g = fun x => f x - g x := by rfl

[Moritz Doll]

There is something very weird going on. I've tried to remove the Mathlib.Topology.Algebra.Group.Basic dependency and now everything works..

import Mathlib.Topology.Algebra.Group.Basic

variable [TopologicalSpace X] [TopologicalSpace Y] [Sub Y] [ContinuousSub Y]

variable (p : (X → Y) → Prop)

@[continuity] lemma sub' (f g : X → Y) (hf : p f) (hg : p g) : p (fun x => f x - g x) := sorry

example (f g : X → Y) (hf : p f) (hg : p g) : p (f - g) := by
  continuity

example (f g : X → Y) (hf : Continuous f) (hg : Continuous g) : Continuous (f - g) := by
  continuity

example (f g : X → Y) (hf : Continuous f) (hg : Continuous g) : Continuous (fun x => f x - g x) := by
  continuity

[Moritz Doll]

more mwe'ified: this works, so the problem is probably not in aesop.

import Mathlib.Tactic.Continuity
import Mathlib.Algebra.Group.Pi

def p (f : X → Y) : Prop := sorry

variable [Sub Y]

@[continuity] theorem sub' (f g : X → Y) (hf : p f) (hg : p g) : p (fun x => f x - g x) := sorry

example (f g : X → Y) (hf : p f) (hg : p g) : p (f - g) := by
  continuity

[Moritz Doll]

I will look into this tomorrow.

[Moritz Doll]

Ok, my previous example had too many sorrys and was succeeding because of that. New mwe without any topology and sorry-free.

import Mathlib.Tactic.Continuity
import Mathlib.Algebra.Group.Pi

variable [AddGroup X] [AddGroup Y]

def p (h : X → Y) : Prop := h 0 = 0

@[aesop safe apply (rule_sets [Continuous])] theorem sub (f g : X → Y) (hf : p f) (hg : p g) :
    p (f - g) := by
  rw [p] at *
  simp [hf, hg]

theorem sub' (f g : X → Y) (hf : p f) (hg : p g) : p (fun x => f x - g x) := by
  aesop (rule_sets [Continuous])

[Moritz Doll]

(aesop also fails to prove the statement of sub with the knowledge of sub')

[Moritz Doll]

I am starting to wonder whether we should just have a intermediate step that transforms functions into the λ version and then have all lemmas for λ. In a recent PR for mathlib3 the same issue came up, where a variant for f + g and λ x, f x + g x was needed and for many operations there several un-applied ways (bundled up to different structures) to spell the same thing.

[Kyle Miller]

Maybe we could do something like the @[elementwise] attribute that's used in category theory (or @[higher_order]), where we generate one of the lemmas from the other. @[elementwise] takes a lemma that's an equation involving morphisms and creates a new lemma that's an equation involving those morphisms applied to some value.

We could also have a tactic that eta expands functions and applies some simp lemmas, to turn f + g into fun x => f x + g x for example. I'm not sure what a general interface would be... but doing it for specific arguments to functions like Continuous is easy enough.

[Moritz Doll]

I think having several two (or more) copies of each continuity statement is cluttering the library too much (I want to use aesop to prove UniformContinuous, Differentiable, and ContDiff as well, so we would have lots of duplicate lemmas). Your second suggestion is what I was thinking of.
Maybe we don't even need that, we can just write all continuity-lemmas and in the λ-expanded variant and I have some hope that everything might just fit together.

[Moritz Doll]

I think I found an aesop bug. According to the trace, aesop fails to apply any lemmas in the second case. @Jannis Limperg

import Mathlib.Topology.Algebra.Group.Basic
-- Plus an import that imports Aesop and contains the line `declare_aesop_rule_sets [Continuous2]`

attribute [aesop unsafe apply (rule_sets [Continuous2])] continuous_id'
attribute [aesop unsafe apply (rule_sets [Continuous2])] continuous_const
attribute [aesop unsafe apply (rule_sets [Continuous2])] Continuous.mul

variable [TopologicalSpace M] [Mul M] [ContinuousMul M]

set_option trace.aesop.steps true

example (y : M) :
    Continuous (fun x => x * y) := by
  aesop (rule_sets [Continuous2]) -- no problem

example (y : M) :
    Continuous (fun x => y * x) := by
  aesop (rule_sets [Continuous2]) -- fails

[Moritz Doll]

If I take an arbitrary function instead of the identity, then everything works in both cases:

example (f : M → M) (hf : Continuous f) (y : M):
    Continuous (fun x => f x * y) := by
  aesop (rule_sets [Continuous2])

example (f : M → M) (hf : Continuous f) (y : M) :
    Continuous (fun x => y * f x) := by
  aesop (rule_sets [Continuous2])

[Jireh Loreaux]

I'm not sure that's a bug because the first contains no explicit identity. What if you add continuous_mul to the list of continuity lemmas?

[Moritz Doll]

If one proof is continuous_id'.mul continuous_const and the other is continuous_const.mul continuous_id' then I expect aesop to find them, but of course it is Jannis' call what is a bug and what is intended behaviour.
Adding continuous_mul does not help, however.

[Moritz Doll]

example (y : M) :
    Continuous (Function.const M y * id) := by
  change Continuous (fun _ => _)
  aesop (rule_sets [Continuous2])

does not work either and that has a rather explicit identity in there.

[Moritz Doll]

(aesop normalizes to the function to fun x => y * x first and then fails)