unnecessarily big instances

Stream: general

[Daniel Selsam]

I traced a performance problem in binported mathlib to a surprising idiom in lean3: many instances are unnecessarily big. For example, many of the + occurrences in the fields of ring.mk actually involve instances such as

       (@has_add.add.{u} α
          (@add_zero_class.to_has_add.{u} α
             (@add_monoid.to_add_zero_class.{u} α
                (@sub_neg_monoid.to_add_monoid.{u} α
                   (@sub_neg_monoid.mk.{u} α add add_assoc zero zero_add add_zero nsmul nsmul_zero' nsmul_succ' neg sub
                      sub_eq_add_neg
                      gsmul
                      gsmul_zero'
                      gsmul_succ'
                      gsmul_neg'))))

and some of the + occurences in sub_neg_monoid.mk are actually

(@has_add.add.{u} G
            (@add_zero_class.to_has_add.{u} G
               (@add_monoid.to_add_zero_class.{u} G
                  (@add_monoid.mk.{u} G add add_assoc zero zero_add add_zero nsmul nsmul_zero' nsmul_succ')))

and so forth. Note that although the lean3 kernel knows not to try the self_opt with the to_* instances, type_context_old doesn't actually check this flag, and so is_def_eq will do a lot more work than necessary and is only saved from constantly doing exponential work thanks to its is_def_eq cache (which has been removed from MetaM in lean4). I can address this during binport, but you may find that it speeds up lean3 if you eagerly reduce these before sending them to the kernel.

[Mario Carneiro]

This is caused by the way the (old?) structure command handles notations coming from parent instances inside the structure definition. If you have something like:

class ring (A) extends add_group A :=
(bla : a + b = b + a)

then the constructor for ring.mk doesn't have an add_group instance available but needs one in order for the typeclass argument to has_add.add to be resolved. So there is some hackery to add what amounts to letI add_group A := { add := add, ... } where add is the local constant provided as a hypothesis to ring.mk, and so the type of the field becomes has_add.add (add_group.has_add { add := add, ... }) a b instead of just add a b. If we were to write add a b = add b a, using the name add which is an inherited field from add_group, directly, then this wouldn't happen, but then we won't be able to use notation which kind of sucks

[Mario Carneiro]

In short, it's not something that mathlib can easily do something about - this would have to be addressed in the C++ where the hackery is