Binomial combinatorics

[jamesmckinna]

This is a stand-alone contribution, which proves the hard combinatorial part of the Binomial Theorem (cf #1287 ), viz.

nCk+nC[k+1]≡[n+1]C[k+1] : n C k + n C (suc k) ≡ suc n C suc k

together with some miscellaneous additional supporting lemmas.

[MatthewDaggitt]

Otherwise looks great! Thank you so much!

[jamesmckinna]

All good suggestions... and I've a long train journey tomorrow...

[jamesmckinna]

Aaargh. More branch merge nonsense. Will revert. Blast!
Still didn't nail it down. Grrr... trying to do too much, too quickly.
Try again tomorrow!

[MatthewDaggitt]

Yup it looks like the merge has gone wrong again. It seems to be a similar problem each time. What is the series of commands you're using to merge?

[jamesmckinna]

Matthew, it seems to be a combination of things:

• first fatal mistake: doing too many things at once, and doing them while too tired to concentrate;
• having two copies of the same branch on two different local machines, each pushing to a single remote branch on jamesmckinna/agda-stdlib;
• the two copies having out-of-sync versions of the agda:master branch from which they were (originally) derived;
• pushing from one local to the remote, and then pulling from there to the other
• generating an explicit merge-commit cycle, (at which point everything is in fact screwed up)
• compounding the error by pushing to the remote
• now, the third, 'unbroken' local branch can't be pushed to the remote because of the push/pull merge conflict this has generated

There are then second-order effects arising from (still!) not getting right how to revert such changes far enough back to undo the mess, and then re-committing the 'good' commits---I seem always to be off-by-one in one direction of time or the other.

I'm snowed under with other things right now, so it will be next week now before I dig my way back out of this one. One copy I have is still (relatively) clean, so I may simply push commits from there to a fresh branch. Sorry that this will screw up the reviewing, but it seems more reliable than trying to fix up a broken tree on the remote branch. But I will also investigate that as well.

I should by now have learnt that being prompted to record a merge commit message is sign of doing something wrong; if I I fetch before attempting to merge (ie don't pull, only fetch), can I somehow preview what will happen and forestall this kind of screw-up again?

[jamesmckinna]

OK... @MatthewDaggitt can you review the latest round of commits to make sure that this is OK... there still seem to be some spurious commits associated with CHANGELOG1.7.2, but I haven't been able to track those down to eliminate them :-(

It appears I have (once again: time to put me out to pasture, perhaps) reverted an irrelevant change, in this case Jacques' "minor whitespace violation" #1922 . Any way, when merging the present branch, to avoid these two? Sigh...

UPDATED: OK, hopefully that last commit really should be the last...

[jamesmckinna]

Thanks @MatthewDaggitt but I think you should have squashed those commits... they each seem to have contributed to my tally on the contributors page, which is the wrong arithmetic, i think.