## Stream: Is there code for X?

### Topic: Automating over structures

#### Aaron Anderson (Jul 25 2020 at 04:02):

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 (Jul 25 2020 at 04:02):

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

#### Aaron Anderson (Jul 25 2020 at 04:03):

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 (Jul 25 2020 at 04:17):

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 (Jul 25 2020 at 04:18):

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 (Jul 25 2020 at 04:29):

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...

Last updated: May 19 2021 at 02:10 UTC