Combinatorics.agda

------------------------------------------------------------------------
-- The Agda standard library
--
-- Combinatorial operations
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Nat.Combinatorics where

open import Data.Nat.Base using (ℕ; zero; suc; _!; _∸_; z≤n; s≤s; _≤_;
  _+_; _*_; _<_; s<s; ≢-nonZero)
open import Data.Nat.DivMod using (_/_; n/1≡n; /-congˡ; /-congʳ; m*n/n≡m;
  m/n/o≡m/[n*o]; n/n≡1; +-distrib-/-∣ˡ; m*n/m*o≡n/o)
open import Data.Nat.Divisibility using (_∣_; *-monoʳ-∣)
open import Data.Nat.Properties
open import Relation.Binary.Definitions using (tri>; tri≈; tri<)
open import Relation.Binary.PropositionalEquality.Core
  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

private
  variable
    n k : ℕ

------------------------------------------------------------------------
-- Definitions

open Base public
  using (_P_; _C_)

------------------------------------------------------------------------
-- Properties of _P_

open Specification public
  using (nPk≡n!/[n∸k]!; k>n⇒nPk≡0; [n∸k]!k!∣n!)

nPn≡n! : ∀ n → n P n ≡ n !
nPn≡n! n = begin-equality
  n P n           ≡⟨ nPk≡n!/[n∸k]! (≤-refl {n}) ⟩
  n ! / (n ∸ n) ! ≡⟨ /-congʳ (cong _! (n∸n≡0 n)) ⟩
  n ! / 0 !       ≡⟨⟩
  n ! / 1         ≡⟨ n/1≡n (n !) ⟩
  n !             ∎
  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_

open Specification public
  using (nCk≡n!/k![n-k]!; k>n⇒nCk≡0)

nCk≡nC[n∸k] : k ≤ n → n C k ≡ n C (n ∸ k)
nCk≡nC[n∸k] {k} {n} k≤n = begin-equality
  n C k                               ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩
  n ! / (k ! * (n ∸ k) !)             ≡⟨ /-congʳ (*-comm ((n ∸ k) !) (k !)) ⟨
  n ! / ((n ∸ k) ! * k !)             ≡⟨ /-congʳ (cong ((n ∸ k) ! *_) (cong _! (m∸[m∸n]≡n k≤n))) ⟨
  n ! / ((n ∸ k) ! * (n ∸ (n ∸ k)) !) ≡⟨ nCk≡n!/k![n-k]! (m≤n⇒n∸m≤n k≤n) ⟨
  n C (n ∸ k)                         ∎
  where instance
    _ = (n ∸ k) !* k !≢0
    _ = k !* (n ∸ k) !≢0
    _ = (n ∸ k) !* (n ∸ (n ∸ k)) !≢0

nCk≡nPk/k! : k ≤ n → n C k ≡ ((n P k) / k !) {{k !≢0}}
nCk≡nPk/k! {k} {n} k≤n = begin-equality
  n C k                   ≡⟨ nCk≡n!/k![n-k]! k≤n ⟩
  n ! / (k ! * (n ∸ k) !) ≡⟨ /-congʳ (*-comm ((n ∸ k)!) (k !)) ⟨
  n ! / ((n ∸ k) ! * k !) ≡⟨ m/n/o≡m/[n*o] (n !) ((n ∸ k) !) (k !) ⟨
  (n ! / (n ∸ k) !) / k ! ≡⟨ /-congˡ (nPk≡n!/[n∸k]! k≤n) ⟨
  (n P k) / k !           ∎
  where instance
    _ = k !≢0
    _ = (n ∸ k) !≢0
    _ = (n ∸ k) !* k !≢0
    _ = k !* (n ∸ k) !≢0

nCn≡1 : ∀ n → n C n ≡ 1
nCn≡1 n = begin-equality
  n C n          ≡⟨ nCk≡nPk/k! (≤-refl {n}) ⟩
  (n P n) / n !  ≡⟨ /-congˡ (nPn≡n! n) ⟩
  n ! / n !      ≡⟨ n/n≡1 (n !) ⟩
  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]