Add Data.Nat.Combinatorics (#1463)

Author: MatthewDaggitt

CHANGELOG.md

@@ -672,6 +672,13 @@ Deprecated names
   id-↔   ↦   ↔-id
   ```
 
+* Factorial, combinations and permutations for ℕ.
+  ```
+  Data.Nat.Combinatorics
+  Data.Nat.Combinatorics.Base
+  Data.Nat.Combinatorics.Spec
+  ```
+
 * In `Function.Construct.Symmetry`:
   ```
   sym-⤖   ↦   ⤖-sym
@@ -1033,21 +1040,37 @@ Other minor changes
   n≮0       : n ≮ 0
   n+1+m≢m   : n + suc m ≢ m
   m*n≡0⇒m≡0 : .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0
+  n>0⇒n≢0   : n > 0 → n ≢ 0
   m^n≢0     : .{{_ : NonZero m}} → NonZero (m ^ n)
-
-
+  m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
+  m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
+  
+  1≤n!    : 1 ≤ n !
+  _!≢0    : NonZero (n !)
+  _!*_!≢0 : NonZero (m ! * n !)
+  
   anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
   allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
   ```
 
+* Added new functions in `Data.Nat`:
+  ```agda
+  _! : ℕ → ℕ
+  ```
+
 * Added new proofs in `Data.Nat.DivMod`:
   ```agda
-  m%n≤n : .{{_ : NonZero n}} → m % n ≤ n
+  m%n≤n          : .{{_ : NonZero n}} → m % n ≤ n
+  m*n/m!≡n/[m∸1]! : .{{_ : NonZero m}} → m * n / m ! ≡ n / (pred m) !
   ```
 
 * Added new proofs in `Data.Nat.Divisibility`:
   ```agda
-  n∣m*n*o : n ∣ m * n * o
+  n∣m*n*o       : n ∣ m * n * o
+  m*n∣⇒m∣       : m * n ∣ i → m ∣ i
+  m*n∣⇒n∣       : m * n ∣ i → n ∣ i
+  m≤n⇒m!∣n!     : m ≤ n → m ! ∣ n !
+  m/n/o≡m/[n*o] : .{{NonZero n}} .{{NonZero o}} → n * o ∣ m → (m / n) / o ≡ m / (n * o)
   ```
 
 * Added new patterns in `Data.Nat.Reflection`:

README/Data/Default.agda

@@ -10,7 +10,7 @@
 module README.Data.Default where
 
 open import Data.Default
-open import Data.Nat.Base
+open import Data.Nat.Base hiding (_!)
 open import Relation.Binary.PropositionalEquality
 
 -- An argument of type `WithDefault {a} {A} x` is an argument of type

src/Data/Nat/Base.agda

@@ -17,7 +17,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
 open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred)
 
 ------------------------------------------------------------------------
@@ -123,6 +123,7 @@ open import Agda.Builtin.Nat
 pred : ℕ → ℕ
 pred n = n ∸ 1
 
+infix  8 _!
 infixl 7 _⊓_ _/_ _%_
 infixl 6 _+⋎_ _⊔_
 
@@ -183,6 +184,12 @@ m / (suc n) = div-helper 0 n m n
 _%_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
 m % (suc n) = mod-helper 0 n m n
 
+-- Factorial
+
+_! : ℕ → ℕ
+zero  ! = 1
+suc n ! = suc n * n !
+
 ------------------------------------------------------------------------
 -- Alternative definition of _≤_
 

src/Data/Nat/Combinatorics.agda

@@ -0,0 +1,87 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Combinatorial operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Nat.Combinatorics where
+
+open import Data.Nat.Base
+open import Data.Nat.DivMod
+open import Data.Nat.Divisibility
+open import Data.Nat.Properties
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; cong; subst)
+
+import Data.Nat.Combinatorics.Base          as Base
+import Data.Nat.Combinatorics.Specification as Specification
+
+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
+
+------------------------------------------------------------------------
+-- 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∸k]!k!∣n! k≤n) ⟩
+  (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

src/Data/Nat/Combinatorics/Base.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Combinatorics operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --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) !
+
+-- Base definition. Only valid for k ≤ n.
+
+_P′_ : ℕ → ℕ → ℕ
+n P′ zero    = 1
+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 0
+
+------------------------------------------------------------------------
+-- 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) !)
+
+-- 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 0