Automating over structures

Stream: Is there code for X?

[Aaron Anderson]

I see that lots of work is being put into refactoring the ideas of submonoid, subgroup, subring, etc. I've written a definition based on flypitch for a substructure of an arbitrary first-order structure, which should in theory generalize all of these, for the right choices of language. If we had an accepted mathlib definition for what a substructure should be in that context, how far away would we be from being able to actually apply it to all relevant structures?

[Aaron Anderson]

(my code for substructure so far: https://github.com/leanprover-community/mathlib/blob/fol-attempt/src/model_theory/substructure.lean#L9)

[Aaron Anderson]

Is this the kind of thing that could be done with a tactic like to_additive, a significantly harder-to-write tactic, or is it somehow beyond what Lean can do at the moment?

[Yury G. Kudryashov]

I wonder if it's possible to generate something definitionally equal to the current lemmas based on the type of mk etc.

[Yury G. Kudryashov]

I mean, if you have a list of types of functions, then you can generate fun_mem using some list.foldl or list.foldr.

[Johan Commelin]

Aaron Anderson said:

Is this the kind of thing that could be done with a tactic like to_additive, a significantly harder-to-write tactic, or is it somehow beyond what Lean can do at the moment?

I think this would be your best bet, but it also sounds like it will be quite a bit harder-to-write...