{-# 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 : ℕ
open Base public
using (_P_; _C_)
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
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 ∎
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
... | 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 ∎
... | 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 ∎
... | 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]