Binomial combinatorics

CHANGELOG.md

@@ -2020,6 +2020,16 @@ Other minor changes
   allUpTo? : (P? : Decidable P) → ∀ v → Dec (∀ {n} → n < v → P n)
   ```
 
+* Added new proofs in `Data.Nat.Combinatorics`:
+  ```agda
+  [n-k]*[n-k-1]!≡[n-k]!   : k < n → (n ∸ k) * (n ∸ suc k) ! ≡ (n ∸ k) !
+  [n-k]*d[k+1]≡[k+1]*d[k] : k < n → (n ∸ k) * ((suc k) ! * (n ∸ suc k) !) ≡ (suc k) * (k ! * (n ∸ k) !)
+  k![n∸k]!∣n!              : k ≤ n → k ! * (n ∸ k) ! ∣ n !
+  nP1≡n                   : n P 1 ≡ n
+  nC1≡n                   : n C 1 ≡ n
+  nCk+nC[k+1]≡[n+1]C[k+1] : n C k + n C (suc k) ≡ suc n C suc k
+  ```
+
 * Added new proofs in `Data.Nat.DivMod`:
   ```agda
   m%n≤n           : .{{_ : NonZero n}} → m % n ≤ n

src/Data/Nat/Combinatorics.agda

@@ -12,11 +12,13 @@ open import Data.Nat.Base
 open import Data.Nat.DivMod
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
+open import Relation.Binary.Definitions 
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; subst)
 
 import Data.Nat.Combinatorics.Base          as Base
 import Data.Nat.Combinatorics.Specification as Specification
+import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
 
 open ≤-Reasoning
 
@@ -46,6 +48,15 @@ nPn≡n! n = begin-equality
   where instance
     _ = (n ∸ n) !≢0
 
+nP1≡n : ∀ n → n P 1 ≡ n
+nP1≡n zero        = refl
+nP1≡n n@(suc n-1) = begin-equality
+  n P 1          ≡⟨ nPk≡n!/[n∸k]! (s≤s (z≤n {n-1})) ⟩
+  n ! / n-1 !    ≡⟨ m*n/n≡m n (n-1 !) ⟩
+  n              ∎
+  where instance
+    _ = n-1 !≢0
+
 ------------------------------------------------------------------------
 -- Properties of _C_
 
@@ -85,3 +96,138 @@ nCn≡1 n = begin-equality
   1              ∎
   where instance
     _ = n !≢0
+
+nC1≡n : ∀ n → n C 1 ≡ n
+nC1≡n zero    = refl
+nC1≡n n@(suc n-1) = begin-equality
+  n C 1          ≡⟨ nCk≡nPk/k!  (s≤s (z≤n {n-1})) ⟩
+  (n P 1) / 1 !  ≡⟨ n/1≡n (n P 1) ⟩
+  n P 1          ≡⟨ nP1≡n n ⟩
+  n              ∎
+
+
+------------------------------------------------------------------------
+-- Arithmetic of (n C k)
+
+module _ {n k} (k<n : k < n) where
+
+  private
+
+    [n-k]            = n ∸ k
+    [n-k-1]          = n ∸ suc k
+
+    [n-k]!           = [n-k] !
+    [n-k-1]!         = [n-k-1] !
+
+    [n-k]≡1+[n-k-1]  : [n-k] ≡ suc [n-k-1]
+    [n-k]≡1+[n-k-1]  = +-∸-assoc 1 k<n
+
+
+  [n-k]*[n-k-1]!≡[n-k]! : [n-k] * [n-k-1]! ≡ [n-k]!
+  [n-k]*[n-k-1]!≡[n-k]! = begin-equality
+      [n-k] * [n-k-1]!
+        ≡⟨ cong (_* [n-k-1]!) [n-k]≡1+[n-k-1] ⟩
+      (suc [n-k-1]) * [n-k-1]!
+        ≡˘⟨ cong _! [n-k]≡1+[n-k-1] ⟩
+      [n-k]!                ∎
+
+  private
+
+    n!           = n !
+    k!           = k !
+    [k+1]!       = (suc k) !
+
+    d[k]         = k! * [n-k]!
+    [k+1]*d[k]   = (suc k) * d[k]
+    d[k+1]       = [k+1]! * [n-k-1]!
+    [n-k]*d[k+1] = [n-k] * d[k+1]
+
+  [n-k]*d[k+1]≡[k+1]*d[k] : [n-k]*d[k+1] ≡ [k+1]*d[k]
+  [n-k]*d[k+1]≡[k+1]*d[k] = begin-equality
+    [n-k]*d[k+1]
+      ≡⟨ x∙yz≈y∙xz [n-k] [k+1]! [n-k-1]! ⟩
+    [k+1]! * ([n-k] * [n-k-1]!)
+      ≡⟨ *-assoc (suc k) k! ([n-k] * [n-k-1]!) ⟩
+    (suc k) * (k! * ([n-k] * [n-k-1]!))
+       ≡⟨ cong ((suc k) *_) (cong (k! *_) [n-k]*[n-k-1]!≡[n-k]!) ⟩
+    [k+1]*d[k]             ∎
+    where open CommSemigroupProperties *-commutativeSemigroup
+
+k![n∸k]!∣n! : ∀ {n k} → k ≤ n → k ! * (n ∸ k) ! ∣ n !
+k![n∸k]!∣n! {n} {k} k≤n = subst (_∣ n !) (*-comm ((n ∸ k) !) (k !)) ([n∸k]!k!∣n! k≤n)
+
+nCk+nC[k+1]≡[n+1]C[k+1] : ∀ n k → n C k + n C (suc k) ≡ suc n C suc k
+nCk+nC[k+1]≡[n+1]C[k+1] n k with <-cmp k n
+{- case k>n, in which case 1+k>1+n>n -}
+... | tri> _ _ k>n = begin-equality
+  n C k + n C (suc k) ≡⟨ cong (_+ (n C (suc k))) (k>n⇒nCk≡0 k>n) ⟩
+  0 + n C (suc k)     ≡⟨⟩
+  n C (suc k)         ≡⟨ k>n⇒nCk≡0 (m<n⇒m<1+n k>n) ⟩
+  0                   ≡˘⟨ k>n⇒nCk≡0 (s<s k>n) ⟩
+  suc n C suc k       ∎
+{- case k≡n, in which case 1+k≡1+n>n -}
+... | tri≈ _ k≡n _ rewrite k≡n = begin-equality
+  n C n + n C (suc n) ≡⟨ cong (n C n +_) (k>n⇒nCk≡0 (n<1+n n)) ⟩
+  n C n + 0           ≡⟨ +-identityʳ (n C n) ⟩
+  n C n               ≡⟨ nCn≡1 n ⟩
+  1                   ≡˘⟨ nCn≡1 (suc n) ⟩
+  suc n C suc n       ∎
+{- case k<n, in which case 1+k<1+n and there's arithmetic to perform -}
+... | tri< k<n _ _ = begin-equality
+  n C k + n C (suc k)
+    ≡⟨ cong (n C k +_) (nCk≡n!/k![n-k]! k<n)  ⟩
+  n C k + (n! / d[k+1])
+    ≡˘⟨ cong (n C k +_) (m*n/m*o≡n/o (n ∸ k) n! d[k+1]) ⟩
+  n C k + [n-k]*n!/[n-k]*d[k+1]
+    ≡⟨ cong (_+ [n-k]*n!/[n-k]*d[k+1]) (nCk≡n!/k![n-k]! k≤n) ⟩
+  n! / d[k] + _
+    ≡˘⟨ cong (_+ [n-k]*n!/[n-k]*d[k+1]) (m*n/m*o≡n/o (suc k) n! d[k]) ⟩
+  (suc k * n!) / [k+1]*d[k] + _
+    ≡⟨ cong (((suc k * n!) / [k+1]*d[k]) +_) (/-congʳ ([n-k]*d[k+1]≡[k+1]*d[k] k<n)) ⟩
+  (suc k * n!) / [k+1]*d[k] + ((n ∸ k) * n! / [k+1]*d[k])
+    ≡˘⟨ +-distrib-/-∣ˡ _ (*-monoʳ-∣ (suc k) (k![n∸k]!∣n! k≤n)) ⟩
+  ((suc k) * n! + (n ∸ k) * n!) / [k+1]*d[k]
+    ≡˘⟨ cong (_/ [k+1]*d[k]) (*-distribʳ-+ (n !) (suc k) (n ∸ k)) ⟩
+  ((suc k + (n ∸ k)) * n !) / [k+1]*d[k]
+    ≡⟨ cong (λ z → z * n ! / [k+1]*d[k]) [k+1]+[n-k]≡[n+1] ⟩
+  ((suc n) * n !) / [k+1]*d[k]
+    ≡˘⟨ /-congʳ (*-assoc (suc k) (k !) ((n ∸ k) !)) ⟩
+  ((suc n) * n !) / (((suc k) * k !) * (n ∸ k) !)
+    ≡⟨⟩
+  suc n ! / (suc k ! * (suc n ∸ suc k) !)
+    ≡˘⟨ nCk≡n!/k![n-k]! [k+1]≤[n+1] ⟩
+  suc n C suc k ∎
+  where
+    k≤n                     : k ≤ n
+    k≤n                     = <⇒≤ k<n
+
+    [k+1]≤[n+1]             : suc k ≤ suc n
+    [k+1]≤[n+1]             = s≤s k≤n
+
+    [k+1]+[n-k]≡[n+1]       : (suc k) + (n ∸ k) ≡ suc n
+    [k+1]+[n-k]≡[n+1]       = m+[n∸m]≡n {suc k} [k+1]≤[n+1]
+
+    [n-k]                   = n ∸ k
+    [n-k-1]                 = n ∸ suc k
+
+    n!                      = n !
+    k!                      = k !
+    [k+1]!                  = (suc k) !
+    [n-k]!                  = [n-k] !
+    [n-k-1]!                = [n-k-1] !
+
+    d[k]                    = k! * [n-k]!
+    [k+1]*d[k]              = (suc k) * d[k]
+    d[k+1]                  = [k+1]! * [n-k-1]!
+    [n-k]*d[k+1]            = [n-k] * d[k+1]
+    n!/[n-k]*d[k+1]         = n ! / [n-k]*d[k+1]
+    [n-k]*n!/[n-k]*d[k+1]   = [n-k] * n! / [n-k]*d[k+1]
+    [n-k]*n!/[k+1]*d[k]     = [n-k] * n! / [k+1]*d[k]
+
+    instance
+      [k+1]!*[n-k]!≢0 = (suc k) !* [n-k] !≢0
+      d[k]≢0          = k !* [n-k] !≢0
+      d[k+1]≢0        = (suc k) !* (n ∸ suc k) !≢0
+      [k+1]*d[k]≢0    = m*n≢0 (suc k) d[k]
+      [n-k]≢0         = ≢-nonZero (m>n⇒m∸n≢0 k<n)
+      [n-k]*d[k+1]≢0  = m*n≢0 [n-k] d[k+1]