More distributivity properties for nats

[Taneb]

I based the types for the list action distributivity properties on Algebra.Properties.Semiring.Sum, which uses Vector rather than List (and of course is for an arbtirary Semiring)

[Taneb]

I use an explicit invocation of *-zeroˡ rather than refl to keep the proofs symmetric

[jamesmckinna]

I'm happy with the local details of this PR, but I'm starting (since already a while now) to be very dissatisfied with each of the underlying design decisions, notwithstanding my own refactorings which, like this one, have perpetuated suboptimal choices...

• Vector rather than Vec (but this ought to be inessential, in view of the following)
• sum as an instance of a Foldable operation/operation on a Foldable functor.

I'm grateful to Oleg Kiselyov for drawing my attention to various invited talks by Guy Steele over the 2010s about this in the context of parallel programming in general, and FORTRAN/Fortress in particular, but also to a (much) longer history (1970s? 1980s?) in the Dijkstra et al. lineage of so-called "Eindhoven Quantifier Notation" (discussed eg here), as well as Bertot et al. "Canonical Big Operators" in Coq/SSReflect (as it then was) in the 2000s.

We can, and should, do better!

(And yes, before @JacquesCarette feels obliged to remind me about about the good/perfect friend/enemy spectrum of trade-offs, I should lift this out as a separate library-design issue)

Shoutouts also to Johannes Waldmannn for his bracing 2018 essay on lists in haskell ...

[Taneb]

Vector rather than Vec (but this ought to be inessential, in view of the following)

@jamesmckinna

Is that relevant here? This PR is specifically about List, even though I chose the types based on an earlier implementation on Vector.

I accept that your point about a hypothetical Foldable stands, however.

[jamesmckinna]

Vector rather than Vec (but this ought to be inessential, in view of the following)

@jamesmckinna

Is that relevant here? This PR is specifically about List, even though I chose the types based on an earlier implementation on Vector.

I accept that your point about a hypothetical Foldable stands, however.

Sorry @Taneb I think I should look a bit more closely (and your review request means that I will, but perhaps not straightaway ;-) I'm getting over a very unpleasant bug just atm) at your code. The List version morally seems just as bad as any other choice of representation, but I suppose we do eventually have to pick one!?

[jamesmckinna]

Modulo the longer-term considerations in #2553 / #2834 this all seems great. Cut! Print!

Against that, I'm surprised that

• *-distribˡ-sum isn't easily derivable by commutativity of _*_ from *-distribʳ-sum
• that while *-distribʳ-sum and ^-distribʳ-product do have identical proofs, considered each of them as properties of an abstract monoid-action-as-fold, we don't have the same abstraction/similarity between *-distribʳ-+ and ^-distribʳ-*?

[Taneb]

Against that, I'm surprised that

* `*-distribˡ-sum` isn't _easily_ derivable by commutativity of `_*_` from `*-distribʳ-sum`

I hadn't previously even tried this. It can be done as the follows:

*-distribʳ-sum′ m ns = begin
  sum ns * m          ≡⟨ *-comm (sum ns) m ⟩
  m * sum ns          ≡⟨ *-distribˡ-sum m ns ⟩
  sum (map (m *_) ns) ≡⟨ cong sum (map-cong (*-comm m) ns) ⟩
  sum (map (_* m) ns) ∎

But this is longer than defining it directly, and there aren't any other uses for pulling out a lemma like Algebra.Consequences.Propositional.comm∧distrʳ⇒distrˡ

* that while `*-distribʳ-sum` and `^-distribʳ-product` do have _identical_ proofs, considered each of them as properties of an abstract monoid-action-as-fold, we don't have the same abstraction/similarity between `*-distribʳ-+` and `^-distribʳ-*`?

I think this is because _*_ is defined recursive on its first argument, whereas _^_ is recursive on its second argument.