convert is often slow

Stream: mathlib4

[Michael Stoll]

I have observed that convert often is fairly slow. My impression is that this is because it tries and fails to find Subsingleton instances. E.g.:

import Mathlib

open Nat BigOperators

set_option profiler true

lemma foo {R : Type*} [NormedCommRing R]
    [CompleteSpace R] {f : ℕ → R} (hf₁ : f 1 = 1)
    (hmul : ∀ {m n}, Nat.Coprime m n → f (m * n) = f m * f n)
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (N : ℕ) :
    Summable (fun m : N.smoothNumbers ↦ ‖f m‖) ∧
      HasSum (fun m : N.smoothNumbers ↦ f m) (∏ p in N.primesBelow, ∑' (n : ℕ), f (p ^ n)) := by
  sorry

set_option trace.Meta.synthInstance true in
lemma bar {F : Type*} [NormedField F]
    [CompleteSpace F] {f : ℕ →* F} (h : ∀ {p : ℕ}, p.Prime → ‖f p‖ < 1) (N : ℕ) :
    Summable (fun m : N.smoothNumbers ↦ ‖f m‖) ∧
      HasSum (fun m : N.smoothNumbers ↦ f m) (∏ p in N.primesBelow, (1 - f p)⁻¹) := by
  have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
  -- ~3000 heartbeats
  convert foo f.map_one hmul ?_ N with M hM <;> sorry

/-
MathlibLatest.lean:28:2
[Meta.synthInstance] [0.009281s] ❌ Subsingleton Prop ▶
[Meta.synthInstance] [0.008945s] ❌ Subsingleton Prop ▶
[Meta.synthInstance] [0.000009s] ❌ Subsingleton Prop ▶
[Meta.synthInstance] [0.007182s] ❌ Subsingleton α ▶
[Meta.synthInstance] [0.026846s] ❌ Subsingleton F ▶
[Meta.synthInstance] [0.000009s] ❌ Subsingleton F ▶
[Meta.synthInstance] [0.008626s] ❌ Subsingleton (Inv α) ▶
[Meta.synthInstance] [0.007122s] ❌ Subsingleton α ▶
[Meta.synthInstance] [0.000011s] ✅ Inv F ▶
[Meta.synthInstance] [0.008401s] ❌ Subsingleton (AddCommMonoid α) ▶
[Meta.synthInstance] [0.015745s] ❌ Subsingleton (TopologicalSpace α) ▶
[Meta.synthInstance] [0.061848s] ❌ Subsingleton (β → α) ▶
[Meta.synthInstance] [0.000010s] ❌ Subsingleton F ▶
-/

(this is extracted from Mathlib.NumberTheory.EulerProduct.Basic, before the changes made in #12161).

Looking at docs#Congr!.Config, I don't see an option to switch off the Subsingleton check. Would it make sense to have this? I assume in most cases, the check is not really relevant (so maybe not doing it is even the better default), and without it, convert should be quite a bit faster.

[Kyle Miller]

That Subsingleton check is one of the key features of convert/congr!. It's used to solve for equalities for Fintype and Decidable instances.

[Kyle Miller]

Potentially we could make a special typeclass for this automation. A FastSubsingleton class that's meant to both succeed and fail fast?

[Mario Carneiro]

we should do some statistics on what kind of subsingleton goals are actually proved by convert. Maybe it's just Fintype and Decidable?

[Mario Carneiro]

I was thinking even more than that, just skip typeclass resolution completely and look for those types (or some lightly extensible variation of that)

[Kyle Miller]

Btw, I'm in the process of rewriting congr! to be more efficient. During this I could look into how much mathlib relies on its use of the general Subsingleton class.

[Yaël Dillies]

In my experience it's always Fintype or Decidable

[Michael Stoll]

See here for hard data supporting my claim.

[Mario Carneiro]

Mario Carneiro said:

we should do some statistics on what kind of subsingleton goals are actually proved by convert. Maybe it's just Fintype and Decidable?

@Michael Stoll since you are in a stats gathering mood, what do you think about collecting this info? That is, when convert is successfully able to prove Subsingleton, what type was it applied to? Bucketed into the categories "Propositional goal" + "non-propositional type with head X"

[Michael Stoll]

At least as interesting is to collect information on the unsucessful searches, as these are what takes all the time.
In any case, that would be great, but to me looks like it requires metaprogramming, which I'm not into (yet?).

[Kyle Miller]

Feel free to not collect this information, since my plan for congr! is to special case certain types when generating congruence theorems (rather than checking for a Subsingleton instance on every argument to every function!), and then see how much Subsingleton is actually used to close congr goals.

[Mario Carneiro]

right, my thought regarding collecting the positive cases is to know what we need to put in the whitelist to avoid breaking mathlib too much. Everything else will become a fast failing case for congr!, and while presumably there are many interesting types showing up there we don't really care, except insofar as it will tell us how much we stand to gain

[Kyle Miller]

mathlib4#12495 adds an extra zero or two in front of each of the timing numbers for the example in this thread.

[Meta.synthInstance] [0.000215s] ❌ Lean.Meta.FastSubsingleton Prop ▶
[Meta.synthInstance] [0.000173s] ❌ Lean.Meta.FastSubsingleton Prop ▶
[Meta.synthInstance] [0.000006s] ❌ Lean.Meta.FastSubsingleton Prop ▶
[Meta.synthInstance] [0.000096s] ❌ Lean.Meta.FastSubsingleton α ▶
[Meta.synthInstance] [0.000080s] ❌ Lean.Meta.FastSubsingleton F ▶
[Meta.synthInstance] [0.000005s] ❌ Lean.Meta.FastSubsingleton F ▶
[Meta.synthInstance] [0.000085s] ❌ Lean.Meta.FastSubsingleton (Inv α) ▶
[Meta.synthInstance] [0.000071s] ❌ Lean.Meta.FastSubsingleton α ▶
[Meta.synthInstance] [0.000517s] ✅ Inv F ▶
[Meta.synthInstance] [0.000089s] ❌ Lean.Meta.FastSubsingleton (AddCommMonoid α) ▶
[Meta.synthInstance] [0.000077s] ❌ Lean.Meta.FastSubsingleton (TopologicalSpace α) ▶
[Meta.synthInstance] [0.000281s] ❌ Lean.Meta.FastSubsingleton (β → α) ▶
[Meta.synthInstance] [0.000005s] ❌ Lean.Meta.FastSubsingleton F ▶

[Kyle Miller]

This isn't the final implementation, but "the perfect is the enemy of the good", and it has a favorable benchmark.

[Kyle Miller]

One change you can see in the PR is that sometimes you need apply Subsingleton.elim. I think one could argue that having congr! try to synthesize Subsingleton instances in general doesn't need to be within its purview (maybe there should be a subsingleton tactic that just does apply Subsingleton.elim?). The intent of this tactic is to try to equate dissimilar subexpressions, and it doesn't need to be its responsibility to try too hard.

Something #12495 does is let you hint what Subsingleton instances are important by adding them to the local context.

I could add an option to toggle trying Subsingleton.elim though. I imagine there's not that big of a performance impact to turn it on in general, since it could be used just for cleaning up goals once the congruence algorithm is done.

[Michael Stoll]

It would be interesting to compare the effect of this with that of lean4#4003 (once the latter is generally available).

[Kyle Miller]

maybe there should be a subsingleton tactic that just does apply Subsingleton.elim?

I went ahead and implemented such a tactic in #12525, but it's more careful than just doing apply Subsingleton.elim. There's this funny fact that you can use it to prove that every type is trivial :smile: :

example (α : Sort _) (x y : α) : x = y := by apply Subsingleton.elim

The subsingleton tactic does a bit more than this too, with a lot of subsingleton functionality extracted from congr!.

• it tries applying docs#Subsingleton.elim (without the above trap!)
• it tries docs#proof_irrel_heq
• it tries proving BEq instances are equal by synthesizing LawfulBEq instances
• it tries reducing a HEq to an Eq using docs#Subsingleton.helim (I'm not sure about this one for this tactic, since it doesn't close the goal)
• it starts with doing intros, since intros; apply Subsingleton.elim is common

The syntax also lets you write subsingleton [inst] rather than have := inst; subsingleton. This isn't just a convenience, since inst doesn't need all its metavariables be solved for (not even universe level metavariables!). I'm pleased that subsingleton [CharP.CharOne.subsingleton] works — CharP.CharOne.subsingleton has a couple unsolved instance variables in there.

I'm imagining that subsingleton could be among the tactics that congr! might call as a discharger.