Potential consequences of large definitions?

Stream: general

[Joseph Tooby-Smith]

In PhysLean there is currently a large definition consisting of a lot of instances of a given data type satisfying certain conditions (related to something in string theory). See the link below:

• https://github.com/HEPLean/PhysLean/blob/master/PhysLean/StringTheory/FTheory/SU5U1/Charges/PhenoConstrained/Elems/Basic.lean

I am slightly worried about the potential consequences that having such a large definition might have long term. Are there any which spring to mind, which means things like this should be avoided? The quantity being defined appears in a fair number of lemmas, if that makes a difference.

[Floris van Doorn]

I don't think there is really any problem with long definitions, as long as the definition itself compiles fine, and cannot naturally be broken in smaller parts.
You could consider making it an @[irreducible] def (or even stronger, an irreducible_def), so that Lean will never unfold it, without you explicitly specifying that you want it to be unfolded.

[Robert Maxton]

Largely, the problems will come down to readability and ... reducibility has a technical meaning in Lean, let's say "separability" instead.

Basically, when you do proofs with that definition, are you ever going to have to take it apart and inspect its pieces, or will you basically always be working with it as an opaque object? If the former, then doing so with a definition that big will be incredibly obnoxious and you should endeavor to split it up; if the latter, then there's probably no real harm, though as Floris suggests irreducible_def may be warranted.

[Joseph Tooby-Smith]

Ok, many thanks both! I think it has the potential to give a Stack overflow error if it gets too big, but this is fine since at least it tells me something is wrong.

The sorts of proofs it appears in are of the form:

lemma isComplete_of_mem_nonPhenoConstrainedCharge_nextToNearestNeighbor :
    ∀ x ∈ (nonPhenoConstrainedCharges nextToNearestNeighbor).toMultiset, x.IsComplete := by
  decide

basically running over all elements and testing them for a condition. I'm making sure that these don't go over the heatbeat count limit so they are 'safe' in that sense.

I'll mess around wtih making things irreducible. Thanks again.