From dd8717c0b0a502885a664c587c2baa1a5e7c4a5c Mon Sep 17 00:00:00 2001 From: = Date: Sun, 4 Apr 2021 22:13:41 +0800 Subject: [PATCH 1/6] Add Data.Nat.(Factorial/Combinatorics) --- CHANGELOG.md | 16 ++- src/Data/Nat/Base.agda | 1 - src/Data/Nat/Combinatorics.agda | 127 +++++++++++++++++ src/Data/Nat/Combinatorics/Base.agda | 63 +++++++++ .../Nat/Combinatorics/CoreProperties.agda | 130 ++++++++++++++++++ src/Data/Nat/Divisibility.agda | 8 +- src/Data/Nat/Factorial.agda | 51 +++++++ src/Data/Nat/Properties.agda | 18 ++- 8 files changed, 406 insertions(+), 8 deletions(-) create mode 100644 src/Data/Nat/Combinatorics.agda create mode 100644 src/Data/Nat/Combinatorics/Base.agda create mode 100644 src/Data/Nat/Combinatorics/CoreProperties.agda create mode 100644 src/Data/Nat/Factorial.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 46ea2a6d9c..f21d74eea8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -168,6 +168,13 @@ New modules Data.Nat.PseudoRandom.LCG ``` +* Factorial, combinations and permutations for ℕ. + ``` + Data.Nat.Factorial + Data.Nat.Combinatorics + Data.Nat.Combinatorics.Base + ``` + * Broke up `Data.List.Relation.Binary.Pointwise` and introduced: ``` Data.List.Relation.Binary.Pointwise.Base @@ -298,6 +305,8 @@ Other minor additions * Added new proofs to `Data.Nat.Divisibility`: ```agda *-pres-∣ : o ∣ m → p ∣ n → o * p ∣ m * n + m*n∣⇒m∣ : m * n ∣ i → m ∣ i + m*n∣⇒n∣ : m * n ∣ i → n ∣ i ``` * Added new proofs to `Data.Nat.GCD`: @@ -352,11 +361,10 @@ Other minor additions pred[n]≤n : pred n ≤ n + n>0⇒n≢0 : n > 0 → n ≢ 0 n<1⇒n≡0 : n < 1 → n ≡ 0 mn⇒nPk≡0 : ∀ {n k} → k > n → n P k ≡ 0 +k>n⇒nPk≡0 {n} {k} k>n with k ≤ᵇ n | inspect (k ≤ᵇ_) n +... | true | [ k≤ᵇn ] = contradiction (≤ᵇ⇒≤′ k≤ᵇn) (<⇒≱ k>n) +... | false | _ = refl + +------------------------------------------------------------------------ +-- Properties derived from spec + +nPn≡n! : ∀ n → n P n ≡ n ! +nPn≡n! n = begin-equality + n P n ≡⟨ k≤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 ! ∎ + +------------------------------------------------------------------------ +-- Properties of _C_ +------------------------------------------------------------------------ +-- Spec + +k≤n⇒nCk≡n!/k![n-k]! : ∀ {n k} → k ≤ n → n C k ≡ n ! / (k ! * (n ∸ k) !) +k≤n⇒nCk≡n!/k![n-k]! {n} {k} k≤n with k ≤ᵇ n | inspect (k ≤ᵇ_) n +... | false | [ k≰ᵇn ] = contradiction (≤⇒≤ᵇ k≤n) (subst T k≰ᵇn) +... | true | _ with ⊓-sel k (n ∸ k) +... | inj₁ eq rewrite eq = nC′k≡n!/k![n-k]! k≤n +... | inj₂ eq rewrite eq = trans (C′-sym k≤n) (nC′k≡n!/k![n-k]! k≤n) + +k>n⇒nCk≡0 : ∀ {n k} → k > n → n C k ≡ 0 +k>n⇒nCk≡0 {n} {k} k>n with k ≤ᵇ n | inspect (k ≤ᵇ_) n +... | true | [ k≤ᵇn ] = contradiction (≤ᵇ⇒≤′ k≤ᵇn) (<⇒≱ k>n) +... | false | _ = refl + +------------------------------------------------------------------------ +-- Properties derived from spec + +nCk≡nC[n∸k] : ∀ {n k} → k ≤ n → n C k ≡ n C (n ∸ k) +nCk≡nC[n∸k] {n} {k} k≤n = begin-equality + n C k ≡⟨ k≤n⇒nCk≡n!/k![n-k]! k≤n ⟩ + n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ {n≢0 = (n ∸ k) !* k !≢0} (*-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)) !) ≡˘⟨ k≤n⇒nCk≡n!/k![n-k]! (m≤n⇒n∸m≤n k≤n) ⟩ + n C (n ∸ k) ∎ + +nCk≡nPk/k! : ∀ {n k} → k ≤ n → n C k ≡ (n P k / k !) {k !≢0} +nCk≡nPk/k! {n} {k} k≤n = begin-equality + n C k ≡⟨ k≤n⇒nCk≡n!/k![n-k]! k≤n ⟩ + n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ {n≢0 = (n ∸ k) !* k !≢0} (*-comm ((n ∸ k)!) (k !)) ⟩ + n ! / ((n ∸ k) ! * k !) ≡˘⟨ m/n/o≡m/[n*o] ((n ∸ k) !) (k !) ([n∸k]!k!∣n! k≤n) ⟩ + (n ! / (n ∸ k) !) / k ! ≡˘⟨ /-congˡ {o≢0 = k !≢0} (k≤n⇒nPk≡n!/[n∸k]! k≤n) ⟩ + (n P k) / k ! ∎ + +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ˡ {o≢0 = n !≢0} (nPn≡n! n) ⟩ + n ! / n ! ≡⟨ n/n≡1 (n !) ⟩ + 1 ∎ diff --git a/src/Data/Nat/Combinatorics/Base.agda b/src/Data/Nat/Combinatorics/Base.agda new file mode 100644 index 0000000000..e28f75258a --- /dev/null +++ b/src/Data/Nat/Combinatorics/Base.agda @@ -0,0 +1,63 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Combinatorics operations +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Data.Bool using (true; false) +open import Data.Nat.Base +open import Data.Nat.DivMod +open import Data.Nat.Properties +open import Data.Nat.Factorial +open import Relation.Nullary using (yes; no; does) +open import Relation.Nullary.Decidable using (False; fromWitnessFalse) + +module Data.Nat.Combinatorics.Base where + +private + _!≢0 : ∀ n → False (n ! ≟ 0) + n !≢0 = fromWitnessFalse (n!≢0 n) + +------------------------------------------------------------------------ +-- 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 with k ≤ᵇ n +... | false = 0 +... | true = n P′ k + +------------------------------------------------------------------------ +-- 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 !) {k !≢0} + +-- Main definition. Valid for all k. +-- Deals with boundary case and exploits symmetry to improve performance. + +_C_ : ℕ → ℕ → ℕ +n C k with k ≤ᵇ n +... | false = 0 +... | true = n C′ (k ⊓ (n ∸ k)) diff --git a/src/Data/Nat/Combinatorics/CoreProperties.agda b/src/Data/Nat/Combinatorics/CoreProperties.agda new file mode 100644 index 0000000000..ec37293565 --- /dev/null +++ b/src/Data/Nat/Combinatorics/CoreProperties.agda @@ -0,0 +1,130 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Core properties of combinatorics operations +------------------------------------------------------------------------ +-- This module should not be imported directly! Please use +-- `Data.Nat.Combinatorics` instead. + +{-# OPTIONS --without-K --safe #-} + +module Data.Nat.Combinatorics.CoreProperties where + +open import Data.Bool using (true; false) +open import Data.Nat.Base +open import Data.Nat.DivMod +open import Data.Nat.Divisibility +open import Data.Nat.Properties +open import Data.Nat.Factorial +open import Data.Nat.Combinatorics.Base +open import Data.Sum using (inj₁; inj₂) +open import Relation.Binary.PropositionalEquality using (_≡_; trans; _≢_) +import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as *-CS +import Algebra.Properties.CommutativeSemigroup +-commutativeSemigroup as +-CS +open import Relation.Nullary using (yes; no; does) +open import Relation.Nullary.Decidable using (False; fromWitnessFalse) +open import Relation.Nullary.Negation using (contradiction) +open import Relation.Binary.PropositionalEquality using (subst; refl; sym; cong; cong₂) + +------------------------------------------------------------------------ +-- Prelude + +private + _!≢0 : ∀ n → False (n ! ≟ 0) + n !≢0 = fromWitnessFalse (n!≢0 n) + + _!*_!≢0 : ∀ m n → False (m ! * n ! ≟ 0) + m !* n !≢0 = fromWitnessFalse (m≢0∧n≢0⇒m*n≢0 (n!≢0 m) (n!≢0 n)) + + -- This proof should really live in `Data.Nat.DivMod` but + -- the dependences between this and `Data.Nat.Divisibility` are so + -- messed up that it's impossible at the moment. Until it's sorted + -- out it'll live here. + m/n/o≡m/[n*o] : ∀ {m n o} {n≢0} {o≢0} {no≢0} → n * o ∣ m → + ((m / n) {n≢0} / o) {o≢0} ≡ (m / (n * o)) {no≢0} + m/n/o≡m/[n*o] {m} n@{suc _} o@{suc _} n*o∣m = *-cancelˡ-≡ (pred (n * o)) (begin-equality + (n * o) * (m / n / o) ≡⟨ *-assoc n o _ ⟩ + n * (o * (m / n / o)) ≡⟨ cong (n *_) (m*[n/m]≡n (m*n∣o⇒n∣o/m n o n*o∣m)) ⟩ + n * (m / n) ≡⟨ m*[n/m]≡n (m*n∣⇒m∣ n o n*o∣m) ⟩ + m ≡˘⟨ m*[n/m]≡n n*o∣m ⟩ + (n * o) * (m / (n * o)) ∎) + where open ≤-Reasoning + +------------------------------------------------------------------------ +-- Properties of _P′_ + +nP′k≡n!/[n∸k]! : ∀ {n k} → k ≤ n → n P′ k ≡ (n ! / (n ∸ k) !) {(n ∸ k) !≢0} +nP′k≡n!/[n∸k]! {n} {zero} z≤n = sym (n/n≡1 (n !)) +nP′k≡n!/[n∸k]! {n} {suc k} k0 = begin-equality + (n ∸ k) * (n P′ k) ≡⟨ cong ((n ∸ k) *_) (nP′k≡n!/[n∸k]! (<⇒≤ k-nonZero n∸k>0}} ⟩ + n ! / (pred (n ∸ k) !) ≡⟨ /-congʳ (cong _! (pred[m∸n]≡m∸[1+n] n k)) ⟩ + n ! / (n ∸ suc k) ! ∎ + where open ≤-Reasoning + +nP′k≡n[n∸1P′k∸1] : ∀ n k → {NonZero n} → {NonZero k} → n P′ k ≡ n * (pred n P′ pred k) +nP′k≡n[n∸1P′k∸1] n (suc zero) = refl +nP′k≡n[n∸1P′k∸1] n@(suc n-1) k@(suc k-1@(suc k-2)) = begin-equality + n P′ k ≡⟨⟩ + (n ∸ k-1) * n P′ k-1 ≡⟨ cong ((n ∸ k-1) *_) (nP′k≡n[n∸1P′k∸1] n k-1) ⟩ + (n ∸ k-1) * (n * n-1 P′ k-2) ≡⟨ x∙yz≈y∙xz (n ∸ k-1) n (n-1 P′ k-2) ⟩ + n * ((n ∸ k-1) * n-1 P′ k-2) ≡⟨⟩ + n * n-1 P′ k-1 ∎ + where open ≤-Reasoning; open *-CS + +P′-rec : ∀ {n k} → k ≤ n → {NonZero k} → + n P′ k ≡ k * (pred n P′ pred k) + pred n P′ k +P′-rec n@{suc n-1} k@{suc k-1} k≤n = begin-equality + n P′ k ≡⟨ nP′k≡n[n∸1P′k∸1] n k ⟩ + n * n-1 P′ k-1 ≡˘⟨ cong (_* n-1 P′ k-1) (m+[n∸m]≡n {k} {n} k≤n) ⟩ + (k + (n ∸ k)) * n-1 P′ k-1 ≡⟨ *-distribʳ-+ (n-1 P′ k-1) k (n ∸ k) ⟩ + k * (n-1 P′ k-1) + (n-1 ∸ k-1) * n-1 P′ k-1 ≡⟨⟩ + k * (n-1 P′ k-1) + n-1 P′ k ∎ + where open ≤-Reasoning + +nP′n≡n! : ∀ n → n P′ n ≡ n ! +nP′n≡n! n = begin-equality + n P′ n ≡⟨ nP′k≡n!/[n∸k]! (≤-refl {n}) ⟩ + n ! / (n ∸ n) ! ≡⟨ /-congʳ (cong _! (n∸n≡0 n)) ⟩ + n ! / 0 ! ≡⟨⟩ + n ! / 1 ≡⟨ n/1≡n (n !) ⟩ + n ! ∎ + where open ≤-Reasoning + +k!∣nP′k : ∀ {n k} → k ≤ n → k ! ∣ n P′ k +k!∣nP′k {n} {zero} k≤n = ∣-refl +k!∣nP′k n@{suc n-1} k@{suc k-1} k≤n@(s≤s k-1≤n-1) with k-1 ≟ n-1 +... | yes refl = ∣-reflexive (sym (nP′n≡n! n)) +... | no k≢n = begin + k ! ≡⟨⟩ + k * k-1 ! ∣⟨ ∣m∣n⇒∣m+n (*-monoʳ-∣ k (k!∣nP′k k-1≤n-1)) ( k!∣nP′k {n-1} {k} (≤∧≢⇒< k-1≤n-1 k≢n)) ⟩ + k * (n-1 P′ k-1) + (n-1 P′ k) ≡˘⟨ P′-rec k≤n ⟩ + n P′ k ∎ + where open ∣-Reasoning + +[n∸k]!k!∣n! : ∀ {n k} → k ≤ n → (n ∸ k) ! * k ! ∣ n ! +[n∸k]!k!∣n! {n} {k} k≤n = m∣n/o⇒o*m∣n (m≤n⇒m!∣n! (m∸n≤m n k)) + (subst (k ! ∣_) (nP′k≡n!/[n∸k]! k≤n) (k!∣nP′k k≤n)) + +------------------------------------------------------------------------ +-- Properties of _C′_ + +nC′k≡n!/k![n-k]! : ∀ {n k} → k ≤ n → n C′ k ≡ (n ! / (k ! * (n ∸ k) !)) {k !* (n ∸ k) !≢0} +nC′k≡n!/k![n-k]! {n} {k} k≤n = begin-equality + n C′ k ≡⟨⟩ + (n P′ k) / k ! ≡⟨ /-congˡ {o≢0 = k !≢0} (nP′k≡n!/[n∸k]! k≤n) ⟩ + (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ʳ {n≢0 = (n ∸ k) !* k !≢0} (*-comm ((n ∸ k)!) (k !)) ⟩ + n ! / (k ! * (n ∸ k) !) ∎ + where open ≤-Reasoning + +C′-sym : ∀ {n k} → k ≤ n → n C′ (n ∸ k) ≡ n C′ k +C′-sym {n} {k} k≤n = begin-equality + n C′ (n ∸ k) ≡⟨ nC′k≡n!/k![n-k]! {n} {n ∸ k} (m≤n⇒n∸m≤n k≤n) ⟩ + n ! / ((n ∸ k) ! * (n ∸ (n ∸ k)) !) ≡⟨ /-congʳ (cong ((n ∸ k) ! *_) (cong _! (m∸[m∸n]≡n k≤n))) ⟩ + n ! / ((n ∸ k) ! * k !) ≡⟨ /-congʳ {n≢0 = (n ∸ k) !* k !≢0} (*-comm ((n ∸ k) !) (k !)) ⟩ + n ! / (k ! * (n ∸ k) !) ≡˘⟨ nC′k≡n!/k![n-k]! k≤n ⟩ + n C′ k ∎ + where open ≤-Reasoning diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 7dcfd2e342..14a4e6258a 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -174,7 +174,13 @@ m∣m*n n = divides n (*-comm _ n) ∣m⇒∣m*n {i} {m} n (divides q refl) = ∣-trans (n∣m*n q) (m∣m*n n) ∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n -∣n⇒∣m*n {i} m {n} i∣n = subst (i ∣_) (*-comm n m) (∣m⇒∣m*n m i∣n) +∣n⇒∣m*n m {n} rewrite *-comm m n = ∣m⇒∣m*n m + +m*n∣⇒m∣ : ∀ {i} m n → m * n ∣ i → m ∣ i +m*n∣⇒m∣ m n (divides q refl) = ∣n⇒∣m*n q (m∣m*n n) + +m*n∣⇒n∣ : ∀ {i} m n → m * n ∣ i → n ∣ i +m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m *-monoʳ-∣ : ∀ {i j} k → i ∣ j → k * i ∣ k * j *-monoʳ-∣ {i} {j} k (divides q refl) = divides q $ begin-equality diff --git a/src/Data/Nat/Factorial.agda b/src/Data/Nat/Factorial.agda new file mode 100644 index 0000000000..723dc347ba --- /dev/null +++ b/src/Data/Nat/Factorial.agda @@ -0,0 +1,51 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Combinatorics operations +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Data.Nat.Factorial 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 (_≡_; _≢_) +open import Relation.Nullary.Decidable using (False; fromWitnessFalse) +open import Relation.Binary.PropositionalEquality using (refl; sym; cong) + +------------------------------------------------------------------------ +-- Base definition + +infix 8 _! + +_! : ℕ → ℕ +zero ! = 1 +suc n ! = suc n * n ! + +------------------------------------------------------------------------ +-- Properties + +1≤n! : ∀ n → 1 ≤ n ! +1≤n! zero = s≤s z≤n +1≤n! (suc n) = *-mono-≤ (s≤s (z≤n {n = n})) (1≤n! n) + +n!≢0 : ∀ n → n ! ≢ 0 +n!≢0 (suc n) n!≡0 = m≢0∧n≢0⇒m*n≢0 (1+n≢0 {n}) (n!≢0 n) n!≡0 + +private + _!≢0 : ∀ n → False (n ! ≟ 0) + n !≢0 = fromWitnessFalse (n!≢0 n) + +m≤n⇒m!∣n! : ∀ {m n} → m ≤ n → m ! ∣ n ! +m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n) + where + help : ∀ {m n} → m ≤′ n → m ! ∣ n ! + help {m} {n} ≤′-refl = ∣-refl + help {m} {suc n} (≤′-step m≤′n) = ∣n⇒∣m*n (suc n) (help m≤′n) + +mn/m!≡n/[m∸1]! : ∀ m n → {{.(NonZero m)}} → + (m * n / m !) {m !≢0} ≡ (n / (pred m) !) {pred m !≢0} +mn/m!≡n/[m∸1]! (suc m) n = m*n/m*o≡n/o (suc m) n (m !) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 490de71a37..07c71858f3 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -34,7 +34,7 @@ open import Relation.Binary.Consequences using (flip-Connex) open import Relation.Binary.PropositionalEquality open import Relation.Nullary hiding (Irrelevant) open import Relation.Nullary.Decidable using (True; via-injection; map′) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary.Negation using (contradiction; contradiction₂) open import Relation.Nullary.Reflects using (fromEquivalence) open import Algebra.Definitions {A = ℕ} _≡_ @@ -407,6 +407,9 @@ n<1+n n = ≤-refl n<1⇒n≡0 : ∀ {n} → n < 1 → n ≡ 0 n<1⇒n≡0 (s≤s n≤0) = n≤0⇒n≡0 n≤0 +n>0⇒n≢0 : ∀ {n} → n > 0 → n ≢ 0 +n>0⇒n≢0 {suc n} _ () + n≢0⇒n>0 : ∀ {n} → n ≢ 0 → n > 0 n≢0⇒n>0 {zero} 0≢0 = contradiction refl 0≢0 n≢0⇒n>0 {suc n} _ = 0<1+n @@ -883,10 +886,13 @@ m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0 m*n≡0⇒m≡0∨n≡0 zero {n} eq = inj₁ refl m*n≡0⇒m≡0∨n≡0 (suc m) {zero} eq = inj₂ refl +m≢0∧n≢0⇒m*n≢0 : ∀ {m n} → m ≢ 0 → n ≢ 0 → m * n ≢ 0 +m≢0∧n≢0⇒m*n≢0 m≢0 n≢0 m*n≡0 = contradiction₂ (m*n≡0⇒m≡0∨n≡0 _ m*n≡0) m≢0 n≢0 + m*n≡1⇒m≡1 : ∀ m n → m * n ≡ 1 → m ≡ 1 -m*n≡1⇒m≡1 (suc zero) n _ = refl -m*n≡1⇒m≡1 (suc (suc m)) (suc zero) () -m*n≡1⇒m≡1 (suc (suc m)) zero eq = +m*n≡1⇒m≡1 (suc zero) n _ = refl +m*n≡1⇒m≡1 (suc (suc m)) (suc zero) () +m*n≡1⇒m≡1 (suc (suc m)) zero eq = contradiction (trans (sym $ *-zeroʳ m) eq) λ() m*n≡1⇒n≡1 : ∀ m n → m * n ≡ 1 → n ≡ 1 @@ -1478,6 +1484,10 @@ m∸n≢0⇒nn⇒m∸n≢0 : ∀ {m n} → m > n → m ∸ n ≢ 0 m>n⇒m∸n≢0 {n = suc n} (s≤s m>n) = m>n⇒m∸n≢0 m>n +m≤n⇒n∸m≤n : ∀ {m n} → m ≤ n → n ∸ m ≤ n +m≤n⇒n∸m≤n z≤n = ≤-refl +m≤n⇒n∸m≤n (s≤s m≤n) = ≤-step (m≤n⇒n∸m≤n m≤n) + --------------------------------------------------------------- -- Properties of _∸_ and _+_ From abea51d6ab71cb8c3b4fd5f42b11344be54128d8 Mon Sep 17 00:00:00 2001 From: = Date: Tue, 15 Feb 2022 17:52:17 +0000 Subject: [PATCH 2/6] Brought up to date --- src/Data/Nat/Combinatorics.agda | 101 ++++---------- src/Data/Nat/Combinatorics/Base.agda | 28 ++-- ...CoreProperties.agda => Specification.agda} | 131 +++++++++++------- src/Data/Nat/Divisibility.agda | 10 ++ src/Data/Nat/Factorial.agda | 15 +- src/Data/Nat/Properties.agda | 4 +- 6 files changed, 140 insertions(+), 149 deletions(-) rename src/Data/Nat/Combinatorics/{CoreProperties.agda => Specification.agda} (52%) diff --git a/src/Data/Nat/Combinatorics.agda b/src/Data/Nat/Combinatorics.agda index 8db0bf972e..f5060beaea 100644 --- a/src/Data/Nat/Combinatorics.agda +++ b/src/Data/Nat/Combinatorics.agda @@ -1,79 +1,37 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Combinatorics operations +-- Combinatorial operations ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.Nat.Combinatorics where -open import Data.Bool using (true; false; T) open import Data.Nat.Base open import Data.Nat.DivMod open import Data.Nat.Divisibility open import Data.Nat.Properties open import Data.Nat.Factorial -open import Data.Nat.Combinatorics.Base -open import Data.Nat.Combinatorics.CoreProperties -open import Data.Sum using (inj₁; inj₂) -open import Relation.Binary.PropositionalEquality using (_≡_; trans; _≢_) -open import Relation.Nullary using (yes; no; does) -open import Relation.Nullary.Decidable using (False; fromWitnessFalse) -open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; cong; cong₂; inspect; [_]; subst) + using (_≡_; refl; sym; cong; subst) -open ≤-Reasoning - -private - _!≢0 : ∀ n → False (n ! ≟ 0) - n !≢0 = fromWitnessFalse (n!≢0 n) - - _!*_!≢0 : ∀ m n → False (m ! * n ! ≟ 0) - m !* n !≢0 = fromWitnessFalse (m≢0∧n≢0⇒m*n≢0 (n!≢0 m) (n!≢0 n)) - - ≤ᵇ⇒≤′ : ∀ {m n} → (m ≤ᵇ n) ≡ true → m ≤ n - ≤ᵇ⇒≤′ {m} {n} eq = ≤ᵇ⇒≤ m n (subst T (sym eq) _) +import Data.Nat.Combinatorics.Base as Base +import Data.Nat.Combinatorics.Specification as Specification - -- This proof should really live in `Data.Nat.DivMod` but - -- the dependences between this and `Data.Nat.Divisibility` are so - -- messed up that it's impossible at the moment. Until it's sorted - -- out it'll live here. - m/n/o≡m/[n*o] : ∀ {m} n o {n≢0} {o≢0} {no≢0} → n * o ∣ m → - ((m / n) {n≢0} / o) {o≢0} ≡ (m / (n * o)) {no≢0} - m/n/o≡m/[n*o] {m} n@(suc _) o@(suc _) n*o∣m = *-cancelˡ-≡ (pred (n * o)) (begin-equality - (n * o) * (m / n / o) ≡⟨ *-assoc n o _ ⟩ - n * (o * (m / n / o)) ≡⟨ cong (n *_) (m*[n/m]≡n (m*n∣o⇒n∣o/m n o n*o∣m)) ⟩ - n * (m / n) ≡⟨ m*[n/m]≡n (m*n∣⇒m∣ n o n*o∣m) ⟩ - m ≡˘⟨ m*[n/m]≡n n*o∣m ⟩ - (n * o) * (m / (n * o)) ∎) - where open ≤-Reasoning +open ≤-Reasoning ------------------------------------------------------------------------ -- Definitions ------------------------------------------------------------------------- -open import Data.Nat.Combinatorics.Base public +open Base public using (_P_; _C_) ------------------------------------------------------------------------ -- Properties of _P_ ------------------------------------------------------------------------- --- Spec -k≤n⇒nPk≡n!/[n∸k]! : ∀ {n k} → k ≤ n → n P k ≡ (n ! / (n ∸ k) !) {(n ∸ k) !≢0} -k≤n⇒nPk≡n!/[n∸k]! {n} {k} k≤n with k ≤ᵇ n | inspect (k ≤ᵇ_) n -... | true | _ = nP′k≡n!/[n∸k]! k≤n -... | false | [ k≰ᵇn ] = contradiction (≤⇒≤ᵇ k≤n) (subst T k≰ᵇn) - -k>n⇒nPk≡0 : ∀ {n k} → k > n → n P k ≡ 0 -k>n⇒nPk≡0 {n} {k} k>n with k ≤ᵇ n | inspect (k ≤ᵇ_) n -... | true | [ k≤ᵇn ] = contradiction (≤ᵇ⇒≤′ k≤ᵇn) (<⇒≱ k>n) -... | false | _ = refl - ------------------------------------------------------------------------- --- Properties derived from spec +open Specification public + using (k≤n⇒nPk≡n!/[n∸k]!; k>n⇒nPk≡0; [n∸k]!k!∣n!) nPn≡n! : ∀ n → n P n ≡ n ! nPn≡n! n = begin-equality @@ -82,46 +40,45 @@ nPn≡n! n = begin-equality n ! / 0 ! ≡⟨⟩ n ! / 1 ≡⟨ n/1≡n (n !) ⟩ n ! ∎ + where instance + _ = (n ∸ n) !≢0 ------------------------------------------------------------------------ -- Properties of _C_ ------------------------------------------------------------------------- --- Spec -k≤n⇒nCk≡n!/k![n-k]! : ∀ {n k} → k ≤ n → n C k ≡ n ! / (k ! * (n ∸ k) !) -k≤n⇒nCk≡n!/k![n-k]! {n} {k} k≤n with k ≤ᵇ n | inspect (k ≤ᵇ_) n -... | false | [ k≰ᵇn ] = contradiction (≤⇒≤ᵇ k≤n) (subst T k≰ᵇn) -... | true | _ with ⊓-sel k (n ∸ k) -... | inj₁ eq rewrite eq = nC′k≡n!/k![n-k]! k≤n -... | inj₂ eq rewrite eq = trans (C′-sym k≤n) (nC′k≡n!/k![n-k]! k≤n) - -k>n⇒nCk≡0 : ∀ {n k} → k > n → n C k ≡ 0 -k>n⇒nCk≡0 {n} {k} k>n with k ≤ᵇ n | inspect (k ≤ᵇ_) n -... | true | [ k≤ᵇn ] = contradiction (≤ᵇ⇒≤′ k≤ᵇn) (<⇒≱ k>n) -... | false | _ = refl - ------------------------------------------------------------------------- --- Properties derived from spec +open Specification public + using (k≤n⇒nCk≡n!/k![n-k]!; k>n⇒nCk≡0) nCk≡nC[n∸k] : ∀ {n k} → k ≤ n → n C k ≡ n C (n ∸ k) nCk≡nC[n∸k] {n} {k} k≤n = begin-equality n C k ≡⟨ k≤n⇒nCk≡n!/k![n-k]! k≤n ⟩ - n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ {n≢0 = (n ∸ k) !* k !≢0} (*-comm ((n ∸ k) !) (k !)) ⟩ + 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)) !) ≡˘⟨ k≤n⇒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! : ∀ {n k} → k ≤ n → n C k ≡ (n P k / k !) {k !≢0} +nCk≡nPk/k! : ∀ {n k} → k ≤ n → n C k ≡ (n P k / k !) {{k !≢0}} nCk≡nPk/k! {n} {k} k≤n = begin-equality n C k ≡⟨ k≤n⇒nCk≡n!/k![n-k]! k≤n ⟩ - n ! / (k ! * (n ∸ k) !) ≡˘⟨ /-congʳ {n≢0 = (n ∸ k) !* k !≢0} (*-comm ((n ∸ k)!) (k !)) ⟩ - n ! / ((n ∸ k) ! * k !) ≡˘⟨ m/n/o≡m/[n*o] ((n ∸ k) !) (k !) ([n∸k]!k!∣n! k≤n) ⟩ - (n ! / (n ∸ k) !) / k ! ≡˘⟨ /-congˡ {o≢0 = k !≢0} (k≤n⇒nPk≡n!/[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ˡ (k≤n⇒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ˡ {o≢0 = n !≢0} (nPn≡n! n) ⟩ + (n P n) / n ! ≡⟨ /-congˡ (nPn≡n! n) ⟩ n ! / n ! ≡⟨ n/n≡1 (n !) ⟩ 1 ∎ + where instance + _ = n !≢0 diff --git a/src/Data/Nat/Combinatorics/Base.agda b/src/Data/Nat/Combinatorics/Base.agda index e28f75258a..93909839f6 100644 --- a/src/Data/Nat/Combinatorics/Base.agda +++ b/src/Data/Nat/Combinatorics/Base.agda @@ -6,19 +6,16 @@ {-# OPTIONS --without-K --safe #-} -open import Data.Bool using (true; false) +module Data.Nat.Combinatorics.Base where + +open import Data.Bool.Base using (if_then_else_) open import Data.Nat.Base -open import Data.Nat.DivMod -open import Data.Nat.Properties open import Data.Nat.Factorial -open import Relation.Nullary using (yes; no; does) -open import Relation.Nullary.Decidable using (False; fromWitnessFalse) -module Data.Nat.Combinatorics.Base where - -private - _!≢0 : ∀ n → False (n ! ≟ 0) - n !≢0 = fromWitnessFalse (n!≢0 n) +-- 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 @@ -37,9 +34,7 @@ n P′ (suc k) = (n ∸ k) * (n P′ k) -- Main definition. Valid for all k as deals with boundary case. _P_ : ℕ → ℕ → ℕ -n P k with k ≤ᵇ n -... | false = 0 -... | true = n P′ k +n P k = if k ≤ᵇ n then n P′ k else 0 ------------------------------------------------------------------------ -- Combinations / binomial coefficient @@ -52,12 +47,11 @@ n P k with k ≤ᵇ n -- Base definition. Only valid for k ≤ n. _C′_ : ℕ → ℕ → ℕ -n C′ k = ((n P′ k) / k !) {k !≢0} +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 with k ≤ᵇ n -... | false = 0 -... | true = n C′ (k ⊓ (n ∸ k)) +n C k = if k ≤ᵇ n then n C′ (k ⊓ (n ∸ k)) else 0 diff --git a/src/Data/Nat/Combinatorics/CoreProperties.agda b/src/Data/Nat/Combinatorics/Specification.agda similarity index 52% rename from src/Data/Nat/Combinatorics/CoreProperties.agda rename to src/Data/Nat/Combinatorics/Specification.agda index ec37293565..375709e143 100644 --- a/src/Data/Nat/Combinatorics/CoreProperties.agda +++ b/src/Data/Nat/Combinatorics/Specification.agda @@ -1,16 +1,16 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Core properties of combinatorics operations +-- The specification for combinatorics operations ------------------------------------------------------------------------ -- This module should not be imported directly! Please use -- `Data.Nat.Combinatorics` instead. {-# OPTIONS --without-K --safe #-} -module Data.Nat.Combinatorics.CoreProperties where +module Data.Nat.Combinatorics.Specification where -open import Data.Bool using (true; false) +open import Data.Bool using (T; true; false) open import Data.Nat.Base open import Data.Nat.DivMod open import Data.Nat.Divisibility @@ -18,55 +18,45 @@ open import Data.Nat.Properties open import Data.Nat.Factorial open import Data.Nat.Combinatorics.Base open import Data.Sum using (inj₁; inj₂) -open import Relation.Binary.PropositionalEquality using (_≡_; trans; _≢_) -import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as *-CS -import Algebra.Properties.CommutativeSemigroup +-commutativeSemigroup as +-CS +open import Relation.Binary.PropositionalEquality + using (_≡_; trans; _≢_) open import Relation.Nullary using (yes; no; does) -open import Relation.Nullary.Decidable using (False; fromWitnessFalse) open import Relation.Nullary.Negation using (contradiction) -open import Relation.Binary.PropositionalEquality using (subst; refl; sym; cong; cong₂) +open import Relation.Binary.PropositionalEquality + using (subst; refl; sym; cong; cong₂) + +import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as *-CS ------------------------------------------------------------------------ -- Prelude private - _!≢0 : ∀ n → False (n ! ≟ 0) - n !≢0 = fromWitnessFalse (n!≢0 n) - - _!*_!≢0 : ∀ m n → False (m ! * n ! ≟ 0) - m !* n !≢0 = fromWitnessFalse (m≢0∧n≢0⇒m*n≢0 (n!≢0 m) (n!≢0 n)) - - -- This proof should really live in `Data.Nat.DivMod` but - -- the dependences between this and `Data.Nat.Divisibility` are so - -- messed up that it's impossible at the moment. Until it's sorted - -- out it'll live here. - m/n/o≡m/[n*o] : ∀ {m n o} {n≢0} {o≢0} {no≢0} → n * o ∣ m → - ((m / n) {n≢0} / o) {o≢0} ≡ (m / (n * o)) {no≢0} - m/n/o≡m/[n*o] {m} n@{suc _} o@{suc _} n*o∣m = *-cancelˡ-≡ (pred (n * o)) (begin-equality - (n * o) * (m / n / o) ≡⟨ *-assoc n o _ ⟩ - n * (o * (m / n / o)) ≡⟨ cong (n *_) (m*[n/m]≡n (m*n∣o⇒n∣o/m n o n*o∣m)) ⟩ - n * (m / n) ≡⟨ m*[n/m]≡n (m*n∣⇒m∣ n o n*o∣m) ⟩ - m ≡˘⟨ m*[n/m]≡n n*o∣m ⟩ - (n * o) * (m / (n * o)) ∎) - where open ≤-Reasoning + ≤ᵇ⇒≤′ : ∀ {m n} → (m ≤ᵇ n) ≡ true → m ≤ n + ≤ᵇ⇒≤′ {m} {n} eq = ≤ᵇ⇒≤ m n (subst T (sym eq) _) ------------------------------------------------------------------------ -- Properties of _P′_ -nP′k≡n!/[n∸k]! : ∀ {n k} → k ≤ n → n P′ k ≡ (n ! / (n ∸ k) !) {(n ∸ k) !≢0} -nP′k≡n!/[n∸k]! {n} {zero} z≤n = sym (n/n≡1 (n !)) -nP′k≡n!/[n∸k]! {n} {suc k} k0 = begin-equality +nP′k≡n!/[n∸k]! : ∀ {n k} → k ≤ n → n P′ k ≡ (n ! / (n ∸ k) !) {{(n ∸ k) !≢0}} +nP′k≡n!/[n∸k]! {n} {zero} z≤n = sym (n/n≡1 (n !) {{n !≢0}}) +nP′k≡n!/[n∸k]! {n} {suc k} k-nonZero n∸k>0}} ⟩ - n ! / (pred (n ∸ k) !) ≡⟨ /-congʳ (cong _! (pred[m∸n]≡m∸[1+n] n k)) ⟩ - n ! / (n ∸ suc k) ! ∎ - where open ≤-Reasoning - -nP′k≡n[n∸1P′k∸1] : ∀ n k → {NonZero n} → {NonZero k} → n P′ k ≡ n * (pred n P′ pred k) -nP′k≡n[n∸1P′k∸1] n (suc zero) = refl -nP′k≡n[n∸1P′k∸1] n@(suc n-1) k@(suc k-1@(suc k-2)) = begin-equality + (n ∸ k) * (n ! / (n ∸ k) !) ≡˘⟨ *-/-assoc (n ∸ k) (m≤n⇒m!∣n! (m∸n≤m n k)) ⟩ + (((n ∸ k) * n !) / (n ∸ k) !) ≡⟨ mn/m!≡n/[m∸1]! (n ∸ k) (n !) ⟩ + (n ! / (pred (n ∸ k) !)) ≡⟨ /-congʳ (cong _! (pred[m∸n]≡m∸[1+n] n k)) ⟩ + (n ! / (n ∸ suc k) !) ∎ + where + open ≤-Reasoning + instance + _ = (n ∸ k) !≢0 + _ = (pred (n ∸ k)) !≢0 + _ = (n ∸ suc k) !≢0 + _ = >-nonZero (mn⇒nPk≡0 : ∀ {n k} → k > n → n P k ≡ 0 +k>n⇒nPk≡0 {n} {k} k>n with k ≤ᵇ n in eq +... | true = contradiction (≤ᵇ⇒≤′ eq) (<⇒≱ k>n) +... | false = refl ------------------------------------------------------------------------ -- Properties of _C′_ -nC′k≡n!/k![n-k]! : ∀ {n k} → k ≤ n → n C′ k ≡ (n ! / (k ! * (n ∸ k) !)) {k !* (n ∸ k) !≢0} +nC′k≡n!/k![n-k]! : ∀ {n k} → k ≤ n → n C′ k ≡ (n ! / (k ! * (n ∸ k) !)) {{k !* (n ∸ k) !≢0}} nC′k≡n!/k![n-k]! {n} {k} k≤n = begin-equality n C′ k ≡⟨⟩ - (n P′ k) / k ! ≡⟨ /-congˡ {o≢0 = k !≢0} (nP′k≡n!/[n∸k]! k≤n) ⟩ - (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ʳ {n≢0 = (n ∸ k) !* k !≢0} (*-comm ((n ∸ k)!) (k !)) ⟩ + (n P′ k) / k ! ≡⟨ /-congˡ (nP′k≡n!/[n∸k]! k≤n) ⟩ + (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ʳ (*-comm ((n ∸ k)!) (k !)) ⟩ n ! / (k ! * (n ∸ k) !) ∎ - where open ≤-Reasoning + where + open ≤-Reasoning + instance + _ = k !≢0 + _ = (n ∸ k) !≢0 + _ = (n ∸ k) !* k !≢0 + _ = k !* (n ∸ k) !≢0 C′-sym : ∀ {n k} → k ≤ n → n C′ (n ∸ k) ≡ n C′ k C′-sym {n} {k} k≤n = begin-equality n C′ (n ∸ k) ≡⟨ nC′k≡n!/k![n-k]! {n} {n ∸ k} (m≤n⇒n∸m≤n k≤n) ⟩ n ! / ((n ∸ k) ! * (n ∸ (n ∸ k)) !) ≡⟨ /-congʳ (cong ((n ∸ k) ! *_) (cong _! (m∸[m∸n]≡n k≤n))) ⟩ - n ! / ((n ∸ k) ! * k !) ≡⟨ /-congʳ {n≢0 = (n ∸ k) !* k !≢0} (*-comm ((n ∸ k) !) (k !)) ⟩ + n ! / ((n ∸ k) ! * k !) ≡⟨ /-congʳ (*-comm ((n ∸ k) !) (k !)) ⟩ n ! / (k ! * (n ∸ k) !) ≡˘⟨ nC′k≡n!/k![n-k]! k≤n ⟩ n C′ k ∎ - where open ≤-Reasoning + where + open ≤-Reasoning + instance + _ = (n ∸ k) !* k !≢0 + _ = k !* (n ∸ k) !≢0 + _ = (n ∸ k) !* (n ∸ (n ∸ k)) !≢0 + +------------------------------------------------------------------------ +-- Properties of _C_ + +k≤n⇒nCk≡n!/k![n-k]! : ∀ {n k} → k ≤ n → + n C k ≡ (n ! / (k ! * (n ∸ k) !)) {{k !* (n ∸ k) !≢0}} +k≤n⇒nCk≡n!/k![n-k]! {n} {k} k≤n with k ≤ᵇ n in eq2 +... | false = contradiction (≤⇒≤ᵇ k≤n) (subst T eq2) +... | true with ⊓-sel k (n ∸ k) +... | inj₁ k⊓[n∸k]≡k rewrite k⊓[n∸k]≡k = nC′k≡n!/k![n-k]! k≤n +... | inj₂ k⊓[n∸k]≡n∸k rewrite k⊓[n∸k]≡n∸k = trans (C′-sym k≤n) (nC′k≡n!/k![n-k]! k≤n) + +k>n⇒nCk≡0 : ∀ {n k} → k > n → n C k ≡ 0 +k>n⇒nCk≡0 {n} {k} k>n with k ≤ᵇ n in eq +... | true = contradiction (≤ᵇ⇒≤′ eq) (<⇒≱ k>n) +... | false = refl diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index bdf64dec78..b37395885a 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -268,6 +268,16 @@ m∣n*o⇒m/n∣o {_} {n@(suc _)} {o} (divides p refl) pn∣on = begin o ∎ where open ∣-Reasoning +m/n/o≡m/[n*o] : ∀ m n o .{{_ : NonZero n}} .{{_ : NonZero o}} → n * o ∣ m → + ((m / n) / o) ≡ (m / (n * o)) {{m≢0∧n≢0⇒m*n≢0 n o}} +m/n/o≡m/[n*o] m n@(suc _) o@(suc _) n*o∣m = *-cancelˡ-≡ (n * o) (begin-equality + (n * o) * (m / n / o) ≡⟨ *-assoc n o _ ⟩ + n * (o * (m / n / o)) ≡⟨ cong (n *_) (m*[n/m]≡n (m*n∣o⇒n∣o/m n o n*o∣m)) ⟩ + n * (m / n) ≡⟨ m*[n/m]≡n (m*n∣⇒m∣ n o n*o∣m) ⟩ + m ≡˘⟨ m*[n/m]≡n n*o∣m ⟩ + (n * o) * (m / (n * o)) ∎) + where open ≤-Reasoning + ------------------------------------------------------------------------ -- Properties of _∣_ and _%_ diff --git a/src/Data/Nat/Factorial.agda b/src/Data/Nat/Factorial.agda index c1b77486a7..41e79b2022 100644 --- a/src/Data/Nat/Factorial.agda +++ b/src/Data/Nat/Factorial.agda @@ -12,22 +12,21 @@ 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 (_≡_; _≢_) -open import Relation.Binary.PropositionalEquality using (refl; sym; cong) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; sym; cong) ------------------------------------------------------------------------ -- Properties 1≤n! : ∀ n → 1 ≤ n ! 1≤n! zero = ≤-refl -1≤n! (suc n) = *-mono-≤ (s≤s (z≤n {n = n})) (1≤n! n) +1≤n! (suc n) = *-mono-≤ (m≤m+n 1 n) (1≤n! n) -n!≢0 : ∀ n → n ! ≢ 0 -n!≢0 (suc n) n!≡0 = m≢0∧n≢0⇒m*n≢0 (1+n≢0 {n}) (n!≢0 n) n!≡0 +_!≢0 : ∀ n → NonZero (n !) +n !≢0 = >-nonZero (1≤n! n) -private - _!≢0 : ∀ n → NonZero (n !) - n !≢0 = ≢-nonZero (n!≢0 n) +_!*_!≢0 : ∀ m n → NonZero (m ! * n !) +m !* n !≢0 = m≢0∧n≢0⇒m*n≢0 _ _ {{m !≢0}} {{n !≢0}} mn/m!≡n/[m∸1]! : ∀ m n .{{_ : NonZero m}} → (m * n / m !) {{m !≢0}} ≡ (n / (pred m) !) {{pred m !≢0}} diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index e5b0c7d1f6..b925212a5f 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -902,8 +902,8 @@ m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0 m*n≡0⇒m≡0∨n≡0 zero {n} eq = inj₁ refl m*n≡0⇒m≡0∨n≡0 (suc m) {zero} eq = inj₂ refl -m≢0∧n≢0⇒m*n≢0 : ∀ {m n} → m ≢ 0 → n ≢ 0 → m * n ≢ 0 -m≢0∧n≢0⇒m*n≢0 m≢0 n≢0 m*n≡0 = contradiction₂ (m*n≡0⇒m≡0∨n≡0 _ m*n≡0) m≢0 n≢0 +m≢0∧n≢0⇒m*n≢0 : ∀ m n → .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n) +m≢0∧n≢0⇒m*n≢0 (suc m) (suc n) = _ m*n≡0⇒m≡0 : ∀ m n .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0 m*n≡0⇒m≡0 zero (suc _) eq = refl From d8bb7bd5eebf362a93160d0f6065a8e5f99f6d8c Mon Sep 17 00:00:00 2001 From: = Date: Tue, 15 Feb 2022 17:59:14 +0000 Subject: [PATCH 3/6] Removed Factorial module --- src/Data/Nat/Combinatorics.agda | 27 +++++++------ src/Data/Nat/Combinatorics/Base.agda | 2 +- src/Data/Nat/Combinatorics/Specification.agda | 11 +++-- src/Data/Nat/DivMod.agda | 4 ++ src/Data/Nat/Divisibility.agda | 10 +++++ src/Data/Nat/Factorial.agda | 40 ------------------- src/Data/Nat/Properties.agda | 13 ++++++ 7 files changed, 48 insertions(+), 59 deletions(-) delete mode 100644 src/Data/Nat/Factorial.agda diff --git a/src/Data/Nat/Combinatorics.agda b/src/Data/Nat/Combinatorics.agda index f5060beaea..1a5885f0fc 100644 --- a/src/Data/Nat/Combinatorics.agda +++ b/src/Data/Nat/Combinatorics.agda @@ -12,7 +12,6 @@ open import Data.Nat.Base open import Data.Nat.DivMod open import Data.Nat.Divisibility open import Data.Nat.Properties -open import Data.Nat.Factorial open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; subst) @@ -21,6 +20,10 @@ import Data.Nat.Combinatorics.Specification as Specification open ≤-Reasoning +private + variable + n k : ℕ + ------------------------------------------------------------------------ -- Definitions @@ -31,11 +34,11 @@ open Base public -- Properties of _P_ open Specification public - using (k≤n⇒nPk≡n!/[n∸k]!; k>n⇒nPk≡0; [n∸k]!k!∣n!) + 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 ≡⟨ k≤n⇒nPk≡n!/[n∸k]! (≤-refl {n}) ⟩ + 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 !) ⟩ @@ -47,26 +50,26 @@ nPn≡n! n = begin-equality -- Properties of _C_ open Specification public - using (k≤n⇒nCk≡n!/k![n-k]!; k>n⇒nCk≡0) + using (nCk≡n!/k![n-k]!; k>n⇒nCk≡0) -nCk≡nC[n∸k] : ∀ {n k} → k ≤ n → n C k ≡ n C (n ∸ k) -nCk≡nC[n∸k] {n} {k} k≤n = begin-equality - n C k ≡⟨ k≤n⇒nCk≡n!/k![n-k]! k≤n ⟩ +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)) !) ≡˘⟨ k≤n⇒nCk≡n!/k![n-k]! (m≤n⇒n∸m≤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! : ∀ {n k} → k ≤ n → n C k ≡ (n P k / k !) {{k !≢0}} -nCk≡nPk/k! {n} {k} k≤n = begin-equality - n C k ≡⟨ k≤n⇒nCk≡n!/k![n-k]! k≤n ⟩ +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ˡ (k≤n⇒nPk≡n!/[n∸k]! k≤n) ⟩ + (n ! / (n ∸ k) !) / k ! ≡˘⟨ /-congˡ (nPk≡n!/[n∸k]! k≤n) ⟩ (n P k) / k ! ∎ where instance _ = k !≢0 diff --git a/src/Data/Nat/Combinatorics/Base.agda b/src/Data/Nat/Combinatorics/Base.agda index 93909839f6..1ded9b5717 100644 --- a/src/Data/Nat/Combinatorics/Base.agda +++ b/src/Data/Nat/Combinatorics/Base.agda @@ -10,7 +10,7 @@ module Data.Nat.Combinatorics.Base where open import Data.Bool.Base using (if_then_else_) open import Data.Nat.Base -open import Data.Nat.Factorial +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. diff --git a/src/Data/Nat/Combinatorics/Specification.agda b/src/Data/Nat/Combinatorics/Specification.agda index 375709e143..1979405c80 100644 --- a/src/Data/Nat/Combinatorics/Specification.agda +++ b/src/Data/Nat/Combinatorics/Specification.agda @@ -15,7 +15,6 @@ open import Data.Nat.Base open import Data.Nat.DivMod open import Data.Nat.Divisibility open import Data.Nat.Properties -open import Data.Nat.Factorial open import Data.Nat.Combinatorics.Base open import Data.Sum using (inj₁; inj₂) open import Relation.Binary.PropositionalEquality @@ -102,8 +101,8 @@ k!∣nP′k n@{suc n-1} k@{suc k-1} k≤n@(s≤s k-1≤n-1) with k-1 ≟ n-1 ------------------------------------------------------------------------ -- Properties of _P_ -k≤n⇒nPk≡n!/[n∸k]! : ∀ {n k} → k ≤ n → n P k ≡ (n ! / (n ∸ k) !) {{(n ∸ k) !≢0}} -k≤n⇒nPk≡n!/[n∸k]! {n} {k} k≤n with k ≤ᵇ n in eq +nPk≡n!/[n∸k]! : ∀ {n k} → k ≤ n → n P k ≡ (n ! / (n ∸ k) !) {{(n ∸ k) !≢0}} +nPk≡n!/[n∸k]! {n} {k} k≤n with k ≤ᵇ n in eq ... | true = nP′k≡n!/[n∸k]! k≤n ... | false = contradiction (≤⇒≤ᵇ k≤n) (subst T eq) @@ -147,9 +146,9 @@ C′-sym {n} {k} k≤n = begin-equality ------------------------------------------------------------------------ -- Properties of _C_ -k≤n⇒nCk≡n!/k![n-k]! : ∀ {n k} → k ≤ n → - n C k ≡ (n ! / (k ! * (n ∸ k) !)) {{k !* (n ∸ k) !≢0}} -k≤n⇒nCk≡n!/k![n-k]! {n} {k} k≤n with k ≤ᵇ n in eq2 +nCk≡n!/k![n-k]! : ∀ {n k} → k ≤ n → + n C k ≡ (n ! / (k ! * (n ∸ k) !)) {{k !* (n ∸ k) !≢0}} +nCk≡n!/k![n-k]! {n} {k} k≤n with k ≤ᵇ n in eq2 ... | false = contradiction (≤⇒≤ᵇ k≤n) (subst T eq2) ... | true with ⊓-sel k (n ∸ k) ... | inj₁ k⊓[n∸k]≡k rewrite k⊓[n∸k]≡k = nC′k≡n!/k![n-k]! k≤n diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index 547d1dc69d..2bdb2dcac6 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -270,6 +270,10 @@ m*n/m*o≡n/o m@(suc m-1) n o = helper (<-wellFounded n) (o * (m / o)) * (p * (n / p)) ≡⟨ [m*n]*[o*p]≡[m*o]*[n*p] o (m / o) p (n / p) ⟩ (o * p) * ((m / o) * (n / p)) ∎) +mn/m!≡n/[m∸1]! : ∀ m n .{{_ : NonZero m}} → + (m * n / m !) {{m !≢0}} ≡ (n / (pred m) !) {{pred m !≢0}} +mn/m!≡n/[m∸1]! (suc m) n = m*n/m*o≡n/o (suc m) n (m !) {{m !≢0}} {{suc m !≢0}} + ------------------------------------------------------------------------ -- A specification of integer division. diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index b37395885a..ff5a53dfa6 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -301,6 +301,16 @@ m/n/o≡m/[n*o] m n@(suc _) o@(suc _) n*o∣m = *-cancelˡ-≡ (n * o) (begin-eq (a ∸ ad/n * b) * d ∎ where open ≤-Reasoning; ad/n = a * d / n +------------------------------------------------------------------------ +-- Properties of _∣_ and !_ + +m≤n⇒m!∣n! : ∀ {m n} → m ≤ n → m ! ∣ n ! +m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n) + where + help : ∀ {m n} → m ≤′ n → m ! ∣ n ! + help {m} {n} ≤′-refl = ∣-refl + help {m} {suc n} (≤′-step m≤′n) = ∣n⇒∣m*n (suc n) (help m≤′n) + ------------------------------------------------------------------------ -- DEPRECATED - please use new names as continuing support for the old -- names is not guaranteed. diff --git a/src/Data/Nat/Factorial.agda b/src/Data/Nat/Factorial.agda deleted file mode 100644 index 41e79b2022..0000000000 --- a/src/Data/Nat/Factorial.agda +++ /dev/null @@ -1,40 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Combinatorics operations ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Data.Nat.Factorial 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) - ------------------------------------------------------------------------- --- Properties - -1≤n! : ∀ n → 1 ≤ n ! -1≤n! zero = ≤-refl -1≤n! (suc n) = *-mono-≤ (m≤m+n 1 n) (1≤n! n) - -_!≢0 : ∀ n → NonZero (n !) -n !≢0 = >-nonZero (1≤n! n) - -_!*_!≢0 : ∀ m n → NonZero (m ! * n !) -m !* n !≢0 = m≢0∧n≢0⇒m*n≢0 _ _ {{m !≢0}} {{n !≢0}} - -mn/m!≡n/[m∸1]! : ∀ m n .{{_ : NonZero m}} → - (m * n / m !) {{m !≢0}} ≡ (n / (pred m) !) {{pred m !≢0}} -mn/m!≡n/[m∸1]! (suc m) n = m*n/m*o≡n/o (suc m) n (m !) {{m !≢0}} {{suc m !≢0}} - -m≤n⇒m!∣n! : ∀ {m n} → m ≤ n → m ! ∣ n ! -m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n) - where - help : ∀ {m n} → m ≤′ n → m ! ∣ n ! - help {m} {n} ≤′-refl = ∣-refl - help {m} {suc n} (≤′-step m≤′n) = ∣n⇒∣m*n (suc n) (help m≤′n) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index b925212a5f..084cab4f80 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1873,6 +1873,19 @@ m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n) ⌈n/2⌉-nonZero (1≤n! n) + +_!*_!≢0 : ∀ m n → NonZero (m ! * n !) +m !* n !≢0 = m≢0∧n≢0⇒m*n≢0 _ _ {{m !≢0}} {{n !≢0}} + ------------------------------------------------------------------------ -- Properties of _≤′_ and _<′_ ------------------------------------------------------------------------ From 2aedce3307edeebbd9d17e022c42f637c46a329d Mon Sep 17 00:00:00 2001 From: = Date: Tue, 15 Feb 2022 18:08:21 +0000 Subject: [PATCH 4/6] More tweaks and CHANGELOG update --- CHANGELOG.md | 36 ++++++++++--------- src/Data/Nat/Combinatorics/Specification.agda | 2 +- src/Data/Nat/DivMod.agda | 4 +-- src/Data/Nat/Divisibility.agda | 2 +- src/Data/Nat/Properties.agda | 6 ++-- 5 files changed, 27 insertions(+), 23 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index de11d3d5d0..f20c6932b7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -674,9 +674,9 @@ Deprecated names * Factorial, combinations and permutations for ℕ. ``` - Data.Nat.Factorial Data.Nat.Combinatorics Data.Nat.Combinatorics.Base + Data.Nat.Combinatorics.Spec ``` * In `Function.Construct.Symmetry`: @@ -1040,33 +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*m : 0 < n → m ≤ n * m - m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n - m≢0∧n≢0⇒m*n≢0 : m ≢ 0 → n ≢ 0 → m * n ≢ 0 - [m*n]*[o*p]≡[m*o]*[n*p] : (m * n) * (o * p) ≡ (m * o) * (n * p) - n>0⇒n≢0 : n > 0 → n ≢ 0 - n<1⇒n≡0 : n < 1 → n ≡ 0 - m-nonZero (1≤n! n) _!*_!≢0 : ∀ m n → NonZero (m ! * n !) -m !* n !≢0 = m≢0∧n≢0⇒m*n≢0 _ _ {{m !≢0}} {{n !≢0}} +m !* n !≢0 = m*n≢0 _ _ {{m !≢0}} {{n !≢0}} ------------------------------------------------------------------------ -- Properties of _≤′_ and _<′_ From e32a16d64433adaa658d3512314e7b6285f6a2e0 Mon Sep 17 00:00:00 2001 From: = Date: Tue, 15 Feb 2022 18:16:40 +0000 Subject: [PATCH 5/6] Fixed clash with Data.Default --- README/Data/Default.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README/Data/Default.agda b/README/Data/Default.agda index cf41ec8d5a..0b7d1c0a01 100644 --- a/README/Data/Default.agda +++ b/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 From 277bf047c08db550b7a3cc8de5a5f1131719fc52 Mon Sep 17 00:00:00 2001 From: = Date: Tue, 15 Feb 2022 18:37:37 +0000 Subject: [PATCH 6/6] Actually fix it this time --- README/Data/Default.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README/Data/Default.agda b/README/Data/Default.agda index 0b7d1c0a01..82ff5fcd7d 100644 --- a/README/Data/Default.agda +++ b/README/Data/Default.agda @@ -10,7 +10,7 @@ module README.Data.Default where open import Data.Default -open import Data.Nat.Base hiding (!_) +open import Data.Nat.Base hiding (_!) open import Relation.Binary.PropositionalEquality -- An argument of type `WithDefault {a} {A} x` is an argument of type