------------------------------------------------------------------------
-- The Agda standard library
--
-- Combinatorics operations
------------------------------------------------------------------------

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

module Data.Nat.Combinatorics.Base where

open import Data.Bool.Base using (if_then_else_)
open import Data.Nat.Base
open import Data.Nat.Properties using (_!≢0)

-- NOTE: These operators are not implemented as efficiently as they
-- could be. See the following link for more details.
--
-- https://math.stackexchange.com/questions/202554/how-do-i-compute-binomial-coefficients-efficiently

------------------------------------------------------------------------
-- Permutations / falling factorial

-- The number of ways, including order, that k objects can be chosen
-- from among n objects.

-- n P k = n ! / (n ∸ k) !

infixl 6.5 _P′_ _P_

-- Base definition. Only valid for k ≤ n.

_P′_ : ℕ → ℕ → ℕ
n P′ zero    = 
n P′ (suc k) = (n ∸ k) * (n P′ k)

-- Main definition. Valid for all k as deals with boundary case.

_P_ : ℕ → ℕ → ℕ
n P k = if k ≤ᵇ n then n P′ k else 

------------------------------------------------------------------------
-- Combinations / binomial coefficient

-- The number of ways, disregarding order, that k objects can be chosen
-- from among n objects.

-- n C k = n ! / (k ! * (n ∸ k) !)

infixl 6.5 _C′_ _C_

-- Base definition. Only valid for k ≤ n.

_C′_ : ℕ → ℕ → ℕ
n C′ k = (n P′ k) / k !
  where instance _ = k !≢0

-- Main definition. Valid for all k.
-- Deals with boundary case and exploits symmetry to improve performance.

_C_ : ℕ → ℕ → ℕ
n C k = if k ≤ᵇ n then n C′ (k ⊓ (n ∸ k)) else