Ssreflect Users Discussion List

[Georges Gonthier <>]

  Nice pearl!
I basically agree with the additions, perhaps generalizing slightly the 
lemmas:
   bin_up n m : n * n * 'C(n.-1, m) = (n - m) * 'C(n, m)
   bin_diag n m : n * 'C(n.-1, m) = m.+1 * 'C(n, m.+1)
which seem to somewhat simplify proofs, and make bin_right a simple 
combination.
  I 'll make a note this and a few other technical observations in the PR 
discussion.

Georges
-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Yves Bertot
Sent: 15 September 2016 07:51
To: 

Subject: Re: [ssreflect] binomial

In a work published with A. Mahboubi and F. Guilhot in 2010, ( 
https://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fhal.inria.fr%2finria-00503017v2&data=02%7c01%7cgonthier%40microsoft.com%7ccaf4a6605cdc4db5f68508d3dd34a199%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636095190555349421&sdata=fTcNWxQXqceO2FxIApI99f%2f%2bOwXTV41hKcsrthlTUmk%3d
 -- page 23) we also needed an extra formula about binomials. Would this 
identity also be worth adding?

Yves


On 09/14/2016 04:54 PM, Laurent Thery wrote:
>
> Hi,
>
> I've formalized the proof pearl
>
>  
> https://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fts.da
> ta61.csiro.au%2fpublications%2fnictaabstracts%2f9267.pdf&data=02%7c01%
> 7cgonthier%40microsoft.com%7ccaf4a6605cdc4db5f68508d3dd34a199%7c72f988
> bf86f141af91ab2d7cd011db47%7c1%7c1%7c636095190555349421&sdata=GrSqsk3Z
> G6wwUB1e8%2fKQDsdn%2b5nhH8T%2fNGHsMTgnWZQ%3d
>
> the result can be found here:
>
> https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fwww-so
> p.inria.fr%2fmarelle%2fmath-comp-tut-16%2fMathCompWS%2flesson2.html&da
> ta=02%7c01%7cgonthier%40microsoft.com%7ccaf4a6605cdc4db5f68508d3dd34a1
> 99%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636095190555359428&sda
> ta=UmVm%2f83FbQKL1SS%2f3BHAl2Dw75ffUEtv2cn6PJohJn4%3d
>
> the binomial library contained all the theorems I needed except two:
>
> forall m n, m.+1 * 'C(m, n) = (m.+1 - n) * 'C(m.+1, n).
> forall m n, n.+1 * 'C(m, n.+1) = (m - n) * 'C(m, n).
>
>
> I was wondering if we could include them to the library and replace :
>
> Lemma mul_Sm_binm m n : m.+1 * 'C(m, n) = n.+1 * 'C(m.+1, n.+1).
> Proof.
> elim: m n => [|m IHm] [|n] //; first by rewrite bin0 bin1 muln1 mul1n.
> by rewrite mulSn {2}binS mulnDr addnCA !IHm -mulnDr.
> Qed.
>
> by
>
> Lemma bin_up m n : m.+1 * 'C(m, n) = (m.+1 - n) * 'C(m.+1, n).
> Proof.
> elim: m n => [|m IHm] [|n] //.
> rewrite subSS mulSn {2}binS mulnDr !IHm addnA subSS -mulSn.
> case: (leqP m.+1 n)=> [mLn|mLn]; first by rewrite bin_small // muln0 
> (eqP mLn).
> by rewrite -subSn // -mulnDr -binS.
> Qed.
>
> Lemma bin_right m n : n.+1 * 'C(m, n.+1) = (m - n) * 'C(m, n).
> Proof.
> elim: m n => [|m IHm][|n] //; first by rewrite bin0 bin1 subn0 mul1n 
> muln1.
> rewrite [in RHS]binS subSS mulnDr -IHm -mulnDl -mul_Sm_binm.
> case: (leqP n m)=> [H|H]; first by rewrite addnS subnK.
> by rewrite bin_small ?muln0 // ltnW.
> Qed.
>
> so the theorem  mul_Sm_binm is now a direct consequence:
>
> Lemma bin_diag m n : m.+1 * 'C(m, n) = n.+1 * 'C(m.+1, n.+1).
> Proof. by rewrite bin_up bin_right. Qed.
>
> --
> Laurent
>
>