instance search timeouts in !4#2547

Stream: mathlib4

[Arien Malec]

Could I ask an instance search whisperer to take a look at the timeouts in isUniformOne? I don't understand well enough why Lean 4 goes off the rails for things that used to work in Lean 3...

[Anne Baanen]

If we look at the error:

▶ 253:12-253:30: error:
failed to synthesize
  (a : ?m.99455) → Decidable (?m.99457 a)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

the problem here seems to be the the parameter [inst✝ : DecidablePred p] to Finset.card_filter_le: Lean tries to find an instance for DecidablePred without having figured out what p is supposed to be. You can see this from the metavariable ?m.99457 a instead of the actual predicate (fun uv => ¬SimpleGraph.IsUniform G 1 uv.fst uv.snd). The easiest solution I know is to fill in the predicate in the hole:

theorem isUniformOne : P.IsUniform G (1 : 𝕜) := by
  rw [IsUniform, mul_one, Nat.cast_le]
  refine' (card_filter_le _
    (fun uv => ¬SimpleGraph.IsUniform G 1 (Prod.fst uv) (Prod.snd uv))).trans _
  rw [offDiag_card, Nat.mul_sub_left_distrib, mul_one]
#align finpartition.is_uniform_one Finpartition.isUniformOne

[Anne Baanen]

In Lean 3, the type of the goal helps refine to find a value of p before starting the search, apparently this doesn't happen in Lean 4. I'm not aware of another tactic that will mimic refine perfectly here.

[Arien Malec]

Thanks! I’d have understood a type inference error here, but this error confused me.

[Arien Malec]

Is there a trick in Lean 3 to see how it's filling in the type holes?

[Floris van Doorn]

either #print is_uniform_one or show_term { <tactic> } print (parts of) produced terms. You might need to set set_option pp.implicit true to see the information you want.