Provide binomial theorem for commutative semiring

[uzytkownik]

[MatthewDaggitt]

Thanks for the PR, this looks great! There's just one tiny snag... It's all built on top off the deprecated Data.Table which will almost certainly be removed in version 2.0. I'm therefore reluctant to add in something that will necessarily be deprecated the moment it lands.

The replacement for Data.Table is Data.Vec.Functional.

[uzytkownik]

@MatthewDaggitt unfortunately Algebra.Properties.* depends on Data.Table.

[uzytkownik]

@MatthewDaggitt How do you want to handle it? Should it diverge from rest of Algebra.Properties which use sumₜ?

[MatthewDaggitt]

Apologies for the delay in replying, thanks for the prompt.

Should it diverge from rest of Algebra.Properties which use sumₜ?

Yes ideally the functions and proofs should be copied over to use Data.Vec.Functional instead of Data.Table, leaving sumₜ and it's fellows deprecated. I've been meaning to do this for a while, but completely failed to find the time.

Depending on how much work that is and whether your up for it, this PR could be split in two with non-algebra component and the algebra component submitted separately?

[jamesmckinna]

What's the current (2023-01-23) status of this PR? i.e. What's a sensible guesstimate of the amount of effort required to push it over the line, after everything else that has happened in the intervening 2+ years?

[MatthewDaggitt]

So we now have a much better combinatorics interface in Data.Nat.Combinatorics.

So what needs to be done is to port the main proof over. I'm guessing probably 3~4 hours work by someone.

[jamesmckinna]

Advice welcome!

EDITED: Algebra.Bundles.SemiringWithoutOne appears to fail to export a Setoid instance. I've filed issue #1917

[jamesmckinna]

@uzytkownik are you happy for someone else (me) to carry this PR forward?

[jamesmckinna]

I think the interface in Data.Nat.Combinatorics might be good for computation, but I have found myself wanting to prove various things, eg n C 1 ≡ n, and in turn needing to do fiddly reasoning with _<ᵇ_, eg n<ᵇ1+n ≡ true. The original proofs by @uzytkownik (shout-out for what is, under the surface, a very nice formalisation!) make use of a Fin-based version of n C k, and for the time being I have been working with that, cleaning it up to systematically exploit the following view of i : Fin (suc n) as being either the 'top' element (fromℕ n), or else inject₁ j for j : Fin n... with the intention (!) of avoiding all the grotty reasoning about 'not-being-equal-to-top' involved in the uses of Data.Fin.Base.lower₁ which pervade the earlier PR.

Separately, I've stumbled over the various Algebra interfaces in terms of what they do (and don't!) export, and some questions about where the eventual developments should live: for example, it currently lives (or: is intended to do so) under CommutativeSemiring, but the 'natural' (discuss) factorisation of the proof can take place in Semiring, subject to the local condition simply that the two elements x,y commute; then the theorem for CommutativeSemiring (and its richer kindred) follows immediately as a corollary.

Expect some followup PRs in Algebra.*, but also with some bits and bobs to do with Data.Nat.Combinatorics and Data.Nat.Properties (groan) and Data.Fin.Properties (ditto.).

At some point...

[jamesmckinna]

OK, I have a version working now, under certain caveats:

• lemmas which should belong under Algebra.Properties.SemiringWithoutOne are currently blocking on issue #1917 ; UPDATE: a candidate solution seems to be not to seek maximum generality, but to work only under the ambient assumptions of a Semiring (where the exports seems to work correctly), and leave generalising those parts which can be weakened to structures such as SemiringWithoutOne or SemiringWithoutAnnihilatingZero to another day;
• the theorem holds for commuting x,y in a Semiring, and is then reexported to CommutativeSemiring; DONE see PR #1927 for part of the way there;
• the proof of the lemma that (suc n) C (suc k) ≡ n C k + n C (suc k) is monstrous for the definitions given by Data.Nat.Combinatorics.{Base,Specification}, by contrast with the original definitional ones given for Fin; any advice on simplifying this would be gratefully received! DONE see PR #1926
• a lot of indirection via _ℕ-ℕ_ and its properties etc. can be, and have been, dispensed with; DONE see PR #1923
• a lot more tidying up would I'm sure be feasible, but I don't have much extra time for that right now.

So... I'll raise a PR in due course, but should I do so by pushing to this (very out-of-date) branch, or open a fresh one?

[jamesmckinna]

@JacquesCarette I think that @MatthewDaggitt indicated that the original definitions of _C_ on this branch are to be deprecated in favour of those specified/defined in the new Data.Nat.Combinatorics sub hierarchy. But indeed, even proving the single recurrence relation needed for the Binomial Theorem was a lot of work for the definitions there. But that's done now in PR #1926. I'm not clear how proposing the Maple solution helps when we are far from having complex numbers, let alone Gamma functions at our disposal. or did you mean something else? In any case, the (re)definition to allow arbitrary n and k in n C k doesn't obviate the need for some gruesome arithmetic.

My plan is to incrementally chip away at this until eventually the kernel of the original argument (which has quite a nice interplay between the Fin and Nat views of the indices in the expansion) can be left on its own, but there are various obstructions as noted above.

[JacquesCarette]

Sorry, I was unclear: of course I don't mean to go to complex numbers or any other such things. I meant to generalize _C_ to agree (semantically) with that generalized definition but take two Nat inputs. It generally means that for n C k when you currently have then undefined (because of Fin), it is defined to be 0.

The gruesome arithmetic can't go away. The gruesome Fin juggling can go away.

[jamesmckinna]

@MatthewDaggitt 's hint indeed pointed the way... and indeed the gruesome arithmetic could not be avoided! But the funny thing about @uzytkownik 's original is that the combinatorial lemma was true by definition for the Fin version... ;-)

So all (well, a lot of) the work was in mediating between the Fin version and the (easier) Nat version... but there was still some nice work in decomposing the binomial sum, and taking advantage of the Vector-based representation thereof... so Fin slips in by the back door in any case.

And with it, a use case for PR #1923 ... UPDATE so I hope that that one could be merged soon. Otherwise, I will need to reconsider the structure of @uzytkownik 's top-level lemmas to use... other methods.

[jamesmckinna]

UPDATED: closed by #1928 (and its supporting PRs, now merged)