control.fold

Stream: general

[Kevin Buzzard]

@Sean Leather @Simon Hudon (or anyone else who knows about what goes on in src/control): I have been removing unbundled monoid homomorphisms (f : M -> N) [is_monoid_hom f] from mathlib and replacing them with bundled monoid homs (f : M ->* N). Right now at the edge of this refactor we have src/control/fold (with you two listed as authors) which as you can see on master now has an import deprecated.group which I want to nuke. This file does not seem to be imported anywhere else in mathlib.

There are two ways to do the port to bundled monoid homs. The first way is not to touch the definitions you made like foldl.of_free_monoid and make a new definition:

def fold_foldl_monoid_hom (f : β → α → β) :free_monoid α →* monoid.foldl β :=
{ to_fun := foldl.of_free_monoid f,
...

The disadvantage of this is that it makes proofs a bit more inconvenient, because ⇑(fold_foldl_monoid_hom f) is not syntactically equal to foldl.of_free_monoid, so one needs extra moves (show or some definitional rewrites) to fix up the proofs. I tried implementing this fix yesterday and the diff looks like this. Around line 204 you can see the change I made -- instead of a lemma proving is_monoid_hom I make a def of a new monoid hom. Now take a look around line 315 at the consequences -- the new h2 is told to have type mentioning only foldl.of_free_monoid whereas in fact the term that generates it has a type involving fold_foldl_monoid_hom. This issue stops the old proof from working. Another approach is to add a simp lemma saying fold_foldl_monoid_hom coerced to function is just foldl.of_free_monoid and I could certainly go down that route.

But another approach is simply to nuke the definition of foldl.of_free_monoid completely (and free.map and all the other functions which are actually monoid homs) and replace it with the monoid hom itself. This would be a very convenient approach for this particular file and all the proofs wouldn't need to be edited, you would just move the is_monoid_hom proofs into the definitions of the functions. However this might break upstream stuff which you have so I am reluctant to do it without checking with you first.

Comments?

[Mario Carneiro]

My impression is that there isn't much downstream use of this outside mathlib, so I think we should go ahead with your suggested change assuming mathib itself doesn't break too badly. (These authors have also not been active for a while, so this is at most contributing to bitrot of an unused repository. It would still be good to hear if they have something to add though.)

[Kevin Buzzard]

I am not sure if this file is used anywhere in mathlib either. While you're here, how do you feel about redefining multiset.map to be a monoid hom?

[Simon Hudon]

I think the simpler solution is a good choice.

[Kevin Buzzard]

Is "your suggested change" the "add new definitions" solution? Is "the simpler solution" the one where we nuke the existing definitions?

[Simon Hudon]

Yes, that's it. I assume you still keep foldl, foldr, mfold and the lemmas that depend on them

[Mario Carneiro]

Kevin Buzzard said:

Is "your suggested change" the "add new definitions" solution? Is "the simpler solution" the one where we nuke the existing definitions?

I was referring to this:

But another approach is simply to nuke the definition of foldl.of_free_monoid completely (and free.map and all the other functions which are actually monoid homs) and replace it with the monoid hom itself.

[Kevin Buzzard]

So I have one expert telling me to do one thing and another expert telling me to do another thing? :-/

[Mario Carneiro]

I don't think we've disagreed anywhere?

[Kevin Buzzard]

Oh Ok great! So I'm nuking the definitions!

[Simon Hudon]

I also thought there was a disagreement actually. I thought the proposal was to delete the file altogether

[Mario Carneiro]

I think we're just replacing uses of foldl.of_free_monoid with ⇑(fold_foldl_monoid_hom f)