cc performance issue and mysterious Subsingleton

Stream: mathlib4

[Patrick Massot]

I now the following is contrived but I’d still like to understand what happens. In

import Mathlib.Tactic

set_option linter.all false
set_option trace.profiler true

example (n : ℤ) : Even (n^2) → Even n := by
  contrapose
  have h : (¬ Even n ↔ Odd n)  := Int.not_even_iff_odd
  have h' : (¬ Even (n^2) ↔ Odd (n^2)) := Int.not_even_iff_odd
  have h'' : Odd n → Odd (n^2) := sorry
  cc

cc is spending ages on things like

  [Meta.synthInstance] [0.347315] ❌️ Subsingleton ({α : Type} → [inst : Add α] → α → Prop)

@Miyahara Kō

[Patrick Massot]

And it’s not only one such goal. There are also

  [Meta.synthInstance] [0.087367] ❌️ Subsingleton ([inst : Add ℤ] → ℤ → Prop)
  [Meta.synthInstance] [0.347315] ❌️ Subsingleton ({α : Type} → [inst : Add α] → α → Prop) ▶
  [Meta.synthInstance] [0.066226] ❌️ Subsingleton ([inst : Semiring ℤ] → ℤ → Prop)
  [Meta.synthInstance] [0.246105] ❌️ Subsingleton ({α : Type} → [inst : Semiring α] → α → Prop) ▶
  [Meta.synthInstance] [0.286901] ❌️ Subsingleton ({β : Type} → {γ : outParam Type} → [self : HPow ℤ β γ] → ℤ → β → γ) ▶
  [Meta.synthInstance] [0.309101] ❌️ Subsingleton ({α β : Type} → {γ : outParam Type} → [self : HPow α β γ] → α → β → γ) ▶
  [Meta.synthInstance] [0.192482] ❌️ Subsingleton ({γ : outParam Type} → [self : HPow ℤ ℕ γ] → ℤ → ℕ → γ) ▶
  [Meta.synthInstance] [0.068559] ❌️ Subsingleton ([self : HPow ℤ ℕ ℤ] → ℤ → ℕ → ℤ)
  [Meta.synthInstance] [0.171375] ❌️ Subsingleton ((x : ℕ) → [self : OfNat ℕ x] → ℕ) ▶
  [Meta.synthInstance] [0.189954] ❌️ Subsingleton ({α : Type} → (x : ℕ) → [self : OfNat α x] → α) ▶
  [Meta.synthInstance] [0.065345] ❌️ Subsingleton ([self : OfNat ℕ 2] → ℕ)

[Bhavik Mehta]

I recall quite a few simp lemmas have been un-simped precisely because they caused too much time to be spent trying to synth subsingleton instances. I wonder if similarly the usage of Subsingleton.elim or similar here should be minimised...

[Patrick Massot]

I’m sorry about the crazy example. Actually the same issue arises in a much more reasonable:

import Mathlib.Tactic

set_option linter.all false
set_option trace.profiler true

example (a b : ℝ) (hb : b = 2) : a + a*b = a + a*2 := by
  cc

[Patrick Massot]

Which takes more than 2sec and says

  [Meta.synthInstance] [0.175531] ❌️ Subsingleton ((x : ℕ) → [self : OfNat ℝ x] → ℝ) ▶
  [Meta.synthInstance] [0.188547] ❌️ Subsingleton ({α : Type} → (x : ℕ) → [self : OfNat α x] → α) ▶
  [Meta.synthInstance] [0.061574] ❌️ Subsingleton ([self : OfNat ℝ 2] → ℝ)
  [Meta.synthInstance] [0.354659] ❌️ Subsingleton ({β : Type} → {γ : outParam Type} → [self : HAdd ℝ β γ] → ℝ → β → γ) ▶
  [Meta.synthInstance] [0.288117] ❌️ Subsingleton ({α β : Type} → {γ : outParam Type} → [self : HAdd α β γ] → α → β → γ) ▶
  [Meta.synthInstance] [0.181760] ❌️ Subsingleton ({γ : outParam Type} → [self : HAdd ℝ ℝ γ] → ℝ → ℝ → γ) ▶
  [Meta.synthInstance] [0.065789] ❌️ Subsingleton ([self : HAdd ℝ ℝ ℝ] → ℝ → ℝ → ℝ)
  [Meta.synthInstance] [0.273405] ❌️ Subsingleton ({β : Type} → {γ : outParam Type} → [self : HMul ℝ β γ] → ℝ → β → γ) ▶
  [Meta.synthInstance] [0.290024] ❌️ Subsingleton ({α β : Type} → {γ : outParam Type} → [self : HMul α β γ] → α → β → γ) ▶
  [Meta.synthInstance] [0.181451] ❌️ Subsingleton ({γ : outParam Type} → [self : HMul ℝ ℝ γ] → ℝ → ℝ → γ) ▶
  [Meta.synthInstance] [0.063565] ❌️ Subsingleton ([self : HMul ℝ ℝ ℝ] → ℝ → ℝ → ℝ)

[Patrick Massot]

I think this ruins my idea of using cc as a relaxed rw for teaching.

[Kyle Miller]

Maybe cc doesn't need to be using Subsingleton itself. We have docs#Lean.Meta.FastSubsingleton for mathlib tactics (used for instance by convert/congr!)

[Miyahara Kō]

Patrick Massot @Kyle Miller
Thank you to tell me!
I will create the PR that replace Subsingleton with FastSubsingleton.

[Miyahara Kō]

#20723

[Patrick Massot]

Thanks a lot. The PR was not building because of a broken lemma in the sum of squares files. On master this proof is by aesop taking almost 10 seconds on my laptop to produce a proof that does not use cc and which can be replaced by an easy proof term. So I pushed a commit fixing this proof. There are also suspicious import changes, but I guess those are temporary.

[Patrick Massot]

Note there is no hurry to merge this PR for me. I’m simply including the patch inside Verbose Lean for now. And it indeed solves my issue, so thank a lot to both of you!

[Artie Khovanov]

Patrick Massot said:

Thanks a lot. The PR was not building because of a broken lemma in the sum of squares files. On master this proof is by aesop taking almost 10 seconds on my laptop to produce a proof that does not use cc and which can be replaced by an easy proof term. So I pushed a commit fixing this proof. There are also suspicious import changes, but I guess those are temporary.

Oh yep sorry this proof is fast by aesop given my proposed refactor but I forgot that that hasn't been merged yet when refactoring the sums of squares file!
Fixed as part of #16094