Adding / modifying Aesop lemmas

Stream: mathlib4

[Artie Khovanov]

After working on top of Mathlib for a while, I have some ideas for how to improve what is tagged as a lemma for Aesop, to make automation easier.

Is there any particular process to go through for discussing changes to Aesop tagging? Or should I just make a PR and see what happens?

[Johan Commelin]

Making a PR is certainly an option. But if you feel like you can write down some concise guidelines, that might be much more valuable.

[Johan Commelin]

Because that will help us review similar PRs in the future. And it could be a basis on which we could start a crowdsourced project to aesopify much more of mathlib.

[Artie Khovanov]

I haven't got anything too general, just a couple of observations.

(1) Lemmas like add_mem and mul_mem lemmas should be tagged unsafe 90% rather than safe: if all you have is AddZeroClass or whatever, then you're always going to want to apply them, but the more complicated structures I'm working with have lemmas like mul_self_mem.

(2) I want to add some automation for proving "obvious" IsSquare results like IsSquare x -> IsSquare (x * (y * y)), similar to the SetLike automation described in (1).

[Artie Khovanov]

I suppose the reason more stuff isn't tagged with Aesop is running time concerns. Is there an easy way for me to audit this in case I'm trying out some new Aesop tags?

[Johan Commelin]

If you make a PR, you can comment with !bench and that will show if performance regresses.

[Johan Commelin]

But I think there is a more mundane reason that "more stuff isn't tagged with Aesop": there were a million lines of mathlib before Aesop was born. Who is going to :detective: through all of those, and mark suitable results with @[aesop]?

[Johan Commelin]

That needs a community effort. And such a community effort needs someone to take the lead.

[Johan Commelin]

Just didn't happen yet.

[Artie Khovanov]

Johan Commelin said:

But I think there is a more mundane reason that "more stuff isn't tagged with Aesop": there were a million lines of mathlib before Aesop was born. Who is going to :detective: through all of those, and mark suitable results with @[aesop]?

Yeah for sure
But if I tagged every lemma I found locally useful into global Aesop, eg Set.Nonempty.some_mem, then there would surely be a performance drop across Mathlib as a whole.

[Artie Khovanov]

I would be happy to do some work around Aesop for membership of algebraic structures -- that's something where just tagging everything with simp doesn't work well and Aesop has a lot of potential ime

[Martin Dvořák]

Artie Khovanov said:

But if I tagged every lemma I found locally useful into global Aesop, eg Set.Nonempty.some_mem, then there would surely be a performance drop across Mathlib as a whole.

Honestly, the fact that Fintype.card_ofIsEmpty and Fintype.card_ofSubsingleton have @[simp] on them is quite inconvenient for me. Should there be a category for "this can be a simp lemma but I don't want aesop to use it" ?

[Artie Khovanov]

hmm
I think that would be a bit weird, because lemmas you want Aesop to use generally expect simp normal form as input right?
what sort of context do those lemmas cause issues in?
(btw I have no idea how familiar you are with Aesop, but, in case you don't know, you can write aesop (erase simp <rule>) for one-off cases)

[Jireh Loreaux]

@Martin Dvořák if those are inconvenient simp lemmas, it suggests there is something else wrong with your approach, not that those shouldn't be marked simp.

[Martin Dvořák]

Jireh Loreaux said:

Martin Dvořák if those are inconvenient simp lemmas, it suggests there is something else wrong with your approach, not that those shouldn't be marked simp.

I minimized the code from #mathlib4 > TU block matrix #19607 and the result exhibits the following behavior depending on whether Fintype.card_ofIsEmpty and Fintype.card_ofSubsingleton have @[simp] on them.

import Mathlib.Tactic

attribute [-simp] Fintype.card_ofIsEmpty Fintype.card_ofSubsingleton -- try commenting this line

--count_heartbeats in -- 12718 vs 74031
example {X Y T α : Type} [Fintype T] [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
    {x : X → α} {y : Y → α} {f : T → X ⊕ Y}
    (eX : Fin (Fintype.card { _x : T × X // f _x.fst = Sum.inl _x.snd }) ≃ X)
    (eY : Fin (Fintype.card { _y : T × Y // f _y.fst = Sum.inr _y.snd }) ≃ Y)
    :
    Sum.elim x y = Sum.elim (x ∘ eX) (y ∘ eY) ∘ Equiv.sumCongr eX.symm eY.symm := by
  aesop

--count_heartbeats in -- 2128 vs 4826
example {X X' Y Y' α : Type} [Fintype X'] [Fintype Y']
    (x : X → α) (eX : Fin (Fintype.card X') ≃ X)
    (y : Y → α) (eY : Fin (Fintype.card Y') ≃ Y)
    :
    Sum.elim x y = Sum.elim (x ∘ eX) (y ∘ eY) ∘ Equiv.sumCongr eX.symm eY.symm := by
  aesop

--count_heartbeats in -- no difference
example {X X' Y Y' α : Type} (x : X → α) (y : Y → α) (eX : X' ≃ X) (eY : Y' ≃ Y) :
    Sum.elim x y = Sum.elim (x ∘ eX) (y ∘ eY) ∘ Equiv.sumCongr eX.symm eY.symm := by
  aesop

[Jireh Loreaux]

Can you narrow it down to just a simp call that exhibits the difference, as opposed to aesop?

[Martin Dvořák]

Jireh Loreaux said:

Can you narrow it down to just a simp call that exhibits the difference, as opposed to aesop?

import Mathlib.Tactic

attribute [-simp] Fintype.card_ofIsEmpty Fintype.card_ofSubsingleton -- try commenting this line

--count_heartbeats in -- 297 vs 752
example {X X' Y Y' α : Type} [Fintype X'] [Fintype Y']
    (x : X → α) (eX : Fin (Fintype.card X') ≃ X)
    (y : Y → α) (eY : Fin (Fintype.card Y') ≃ Y)
    :
    Sum.elim x y = Sum.elim (x ∘ eX) (y ∘ eY) ∘ Equiv.sumCongr eX.symm eY.symm := by
  ext i
  rw [Function.comp_apply, Equiv.sumCongr_apply]
  cases i with
  | inl => simp -- here
  | inr => sorry

[Martin Dvořák]

For practical purposes, the difference in a single simp evaluation is not the problem.
However, aesop can reach over million heartbeats in nontrivial examples, which is annoying.

[Jireh Loreaux]

Hmmm.... looking at the trace of the simp call, you can see repeated attempts to try and unify the Fintype instances with Fintype.ofSubsingleton and Fintype.ofIsEmpty, which obviously fail. It seems that they are not cached, but I'm not sure why. @Kyle Miller do you know why this would be the case? This may need to be minimized further and posted in #lean4, as it seems quite suspicious to me.

[Jireh Loreaux]

looking at the position of Fintype.card X' (as the argument to Fin), I'm wondering if this could be caused by some no_indexing of some simp lemmas for Fin _. (Maybe this is far off base)

[Jireh Loreaux]

Either way, @Martin Dvořák since these lemmas are about these Fintype.ofSubsingleton and Fintype.ofIsEmpty instances (I didn't realize this when you first posted about them, my bad), I'm betting Mathlib would build without @[simp] on these lemmas. Do you want to try, and then benchmark the resulting PR?

[Artie Khovanov]

Is there a way of seeing what lemmas are in a particular Aesop ruleset? Say, SetLike? I know I can do a syntactic library search, but I'm wondering if there is something I can extract from the actual Aesop tactic.

[Artie Khovanov]

I have made a PR with some first, tentative changes to specifically the SetLike ruleset: #20477

[Artie Khovanov]

@Jannis Limperg do you have thoughts on this? ^

[Artie Khovanov]

OK, here is a weird thing I found:

import Mathlib.Algebra.Group.Hom.Defs
import Mathlib.Algebra.Group.Subsemigroup.Defs

attribute [- aesop] mul_mem
attribute [aesop unsafe 90% apply (rule_sets := [SetLike])] mul_mem

theorem test_1 {A B : Type*} [Group A] [Group B]
    {f : A →* B} {S : Subsemigroup A}
    (y : A) (hy : y ∈ S) (hy' : y⁻¹ ∈ S) :
    ∃ x ∈ S, f x = (f y)⁻¹ := by
  aesop? -- finds proof

attribute [- aesop] mul_mem
attribute [aesop unsafe 99% apply (rule_sets := [SetLike])] mul_mem

theorem test_2 {A B : Type*} [Group A] [Group B]
    {f : A →* B} {S : Subsemigroup A}
    (y : A) (hy : y ∈ S) (hy' : y⁻¹ ∈ S) :
    ∃ x ∈ S, f x = (f y)⁻¹ := by
  aesop? -- fails

attribute [- aesop] mul_mem
attribute [aesop safe apply (rule_sets := [SetLike])] mul_mem

theorem test_3 {A B : Type*} [Group A] [Group B]
    {f : A →* B} {S : Subsemigroup A}
    (y : A) (hy : y ∈ S) (hy' : y⁻¹ ∈ S) :
    ∃ x ∈ S, f x = (f y)⁻¹ := by
  aesop? -- finds proof

[Artie Khovanov]

I would expect that increasing the priority of an unsafe Aesop rule brings its behaviour monotonically closer to that rule being safe, but this does not appear to be the case. The example above is minimised from one of two examples of this behaviour I came across in practice. I'm not sure exactly where the spurious mul_mem calls are coming from, but it's to do with the presence of the hypothesis hy: without it, Aesop succeeds in all cases.

[Artie Khovanov]

I think Aesop is somehow looping mul_mem indefinitely, but surely if that is the case then the safe version should fail too?

[Jireh Loreaux]

I'm tempted to say that you shouldn't be asking aesop to supply witnesses for you, especially when there are multiple choices in context.

[Artie Khovanov]

Jireh Loreaux said:

I'm tempted to say that you should be asking aesop to supply witnesses for you, especially when there are multiple choices in context.

(Shouldn't, presumably)
Yes, I was surprised the proof worked in the first place! But now I want to try to figure out why this change makes it stop working.

[Jireh Loreaux]

Artie Khovanov said:

(Shouldn't, presumably)

edited

[Jireh Loreaux]

My thought, perhaps unfounded, is that aesop tries to supply y * y⁻¹ as the witness at some point? Thus invoking mul_mem. Have you enabled the trace?

[Artie Khovanov]

Ah! Aesop applies a 10% priority penalty to safe rules that introduce new metavariables (eg in filling an existential), but not to unsafe rules that do the same. The traces of test_1 and test_3 are identical!
Perhaps this behaviour should be made uniform across safe and unsafe rules?

edit: here's the documentation

[Kyle Miller]

@Jireh Loreaux I've thought before that Fintype.card_ofSubsingleton seemed like a sketchy @[simp] lemma. It's sort of ok because it's only for Fintype.ofSubsingleton, which thankfully isn't an instance, but it's going to try being applied to all Fintype.card expressions, which we can check with #discr_tree_simp_key:

#discr_tree_simp_key Fintype.card_ofSubsingleton
-- Fintype.card _ _

[Artie Khovanov]

(deleted)

[Artie Khovanov]

@Jireh Loreaux: I think it's fine to ask Aesop to synthesise a witness here, because it's one of the hypotheses.

[Jireh Loreaux]

I disagree, as there are multiple options, but :shrug:

[Jireh Loreaux]

Kyle, that doesn't explain why it's trying to do the same unification repeatedly.

[Artie Khovanov]

The other proof that broke asks for a more complicated witness:

theorem extracted_1 {A B : Type*} [CommRing A] [CommRing B]
    {f : A →+* B} {P : Subsemiring A} (hf : Function.Surjective ⇑f) (y : A)
    (hsupp : ↑(RingHom.ker f) ⊆ {x | x ∈ P ∧ -x ∈ P}) : ∃ x ∈ P, f x = f y * f y := by
  aesop

Not fully minimised but you get the idea. I think it's fine for aesop to fail here. The witness is any preimage of f y * f y, but the proof it's in P requires synthesising new terms using add_mem and metavariables.

[Jireh Loreaux]

I think likely nothing will break if we remove the simp attribute from docs#Fintype.card_ofSubsingleton, but I still want to know why the same unification problem appears a bunch of times in the simp trace.

[Artie Khovanov]

Artie Khovanov said:

Ah! Aesop applies a 10% priority penalty to safe rules that introduce new metavariables (eg in filling an existential), but not to unsafe rules that do the same. The traces of test_1 and test_3 are identical!
Perhaps this behaviour should be made uniform across safe and unsafe rules?

edit: here's the documentation

The other conclusion to draw is that perhaps no unsafe rule should be given >90% success probability. 99% success probability increases decay time for a loop by a factor of ~10 vs 90%.

[Kyle Miller]

@Jireh Loreaux I'm not too familiar with isDefEq caching, but I know that if there are metavariables (or if there's a non-default configuration), then it uses a "transient" cache. There are definitely metavariables in this particular isDefEq problem, since the Subsingleton instance hasn't been solved for yet.

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

#20524

[Artie Khovanov]

Artie Khovanov said:

I have made a PR with some first, tentative changes to specifically the SetLike ruleset

I've made another, independent, PR reworking the automation for Even / IsSquare: #20558

Any thoughts very welcome :smile:

[Artie Khovanov]

@Yaël Dillies has suggested adding a library note describing the principles I'm following in #20477. Where should this go? Perhaps in Algebra/HeirarchyDesign?

[Kim Morrison]

Seems reasonable! That document is pretty old, but maybe adding more to it will encourage others to update it!

[Edward van de Meent]

I'd like to mention the fact that because that file is not imported, #help note never finds it... Is this something we care about?

[Artie Khovanov]

Edward van de Meent said:

I'd like to mention the fact that because that file is not imported, #help note never finds it... Is this something we care about?

Just came across this with [reducible non_instances]. It feels like certain operations should be able to (syntactically) see all of Mathlib..

[Anne Baanen]

Should we import the hierarchy design file in Mathlib.Init maybe?

[Edward van de Meent]

either that, or seperately in every file which mentions the notes in the design file?

[Artie Khovanov]

Edward van de Meent said:

either that, or seperately in every file which mentions the notes in the design file?

this doesn't feel maintainable when new files are added

[Jannis Limperg]

Finally getting to this, sorry for the delay.

Artie Khovanov said:

Is there a way of seeing what lemmas are in a particular Aesop ruleset? Say, SetLike?

#aesop_rules SetLike will show you the rules in the SetLike rule set. #aesop_rules by itself will show you the rules in all available rule sets.

Artie Khovanov said:

Ah! Aesop applies a 10% priority penalty to safe rules that introduce new metavariables (eg in filling an existential), but not to unsafe rules that do the same. The traces of test_1 and test_3 are identical!
Perhaps this behaviour should be made uniform across safe and unsafe rules?

This sounds very reasonable. aesop#191

I'll look at the SetLike PR. Thank you very much for your efforts, @Artie Khovanov!

[Jannis Limperg]

Reviewed the PR.

[Artie Khovanov]

@Jannis Limperg what do you think of the pattern @[simp, aesop safe apply], to maintain metavariable capabilities?
I had tried just changing all aesop safe apply in the ruleset SetLike to simp, but a couple of proofs broke because they were using aesop rules to fill "obvious" existentials (in both cases, nonemptiness assertions).

[Jannis Limperg]

Ah! Very interesting; I hadn't considered this use case. Yes, with metavariables around, simp + aesop safe makes sense.

[Jannis Limperg]

Could you add a note about this to the design notes (if it isn't already there)?

[Artie Khovanov]

I'll go back and apply the pattern to all the aesop safe rules that really are safe to apply. I don't think there's a meaningful performance decrease compared to tagging only with simp.

[Artie Khovanov]

@Jireh Loreaux what is the "SetLike tactic" mentioned in Mathlib/Tactic/SetLike?

[Artie Khovanov]

I am very confused. I thought SetLike was an Aesop ruleset?

[Jireh Loreaux]

I was going to make a separate tactic, and then was convinced that it should just be a rule set. If there's reference to a tactic somewhere you can probably remove it. I don't have time to think about it at the moment though. Maybe in a few days.

[Artie Khovanov]

It's just a reference in some documentation, and I'm writing up full documentation for the SetLike ruleset. I'll invite you to review the PR for when you have a moment; it's not getting merged anytime soon.