Zulip Chat Archive

Stream: Is there code for X?

Topic: Automating over structures


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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