Add specialized associative List folds

[joehendrix]

This uses the associativity, commutativity and identity classes recently added to Lean core to define folds with simplification lemmas that can move intermediate results outside the fold for better use in tactics.

[digama0]

Note that these classes in mathlib are deprecated and slated for removal; they were in lean 3 core as part of a refactor that never happened, and they are rarely used. I think we should add these on an as-needed basis.

[joehendrix]

I'm open to other approaches then reviving these classes, but it did seem like a way to get the monoid properties I wanted for writing fold/sum lemmas.

IsSymmOp isn't strictly needed but it seemed to naturally go with the other properties, and the associated Symm tactic is already in Std.

[fgdorais]

Is the only reason not to use the Lean core classes that these classes are Prop?

[joehendrix]

The associativity and commutative ones don't have a good reason. Perhaps I should use the Lean core versions. The Identity classes use an out parameter for the identity/neutral element.

[fgdorais]

Maybe it would be better to add the missing outParam in core? Perhaps also make these classes Prop to avoid diamonds? This kind of PR to core can backfire in interesting ways but that would give more guidance what to do in Std.

Another option is to move ac_rfl to Std. That way we could more freely turn it into something more useful. It doesn't seem to be used in core at a quick glance.

[Edit: This was accidentally posted at the wrong place earlier.] I experimented with deleting ac_rfl from core and nothing seems to break: https://github.com/fgdorais/lean4/tree/ac_rfl

[joehendrix]

I'm looking into both changing the core axioms and/or moving/removing ac_rfl.

If ac_rfl is removed from core, then technically the classes could live in Std. However, I think it's good for tactics that don't use Std (potentially so they can migrate to Std) to have a common classes for this.

[joehendrix]

I'll revisit this when leanprover/lean4#3195 is merged.

[kim-em]

Let's make sure this has a Mathlib adaptation branch passing CI before we merge!

[kim-em]

I've changed the base of the PR to main, as it is now on v4.6.0-rc1 which includes the upstream changes. I've also set the lean-toolchain to v4.6.0-rc1 to resolve the conflict.

[joehendrix]

@semorrison

Let's make sure this has a Mathlib adaptation branch passing CI before we merge!

I've started an adaptation branch here at leanprover-community/mathlib4#10336. It could use some help.

[fgdorais]

All the prereqs are good now, so this could be merged soon.

[fgdorais]

Looks like the only issue left is the to_additive problem in Mathlib. We need an expert to deal with that...

[fgdorais]

This PR was marked will-merge-soon since Februrary 16, I removed that tag on July 20. Presumably something went wrong along the way... What is the current status of this PR?