From 392343d21ce33d3afd31005bd7e8cbed5b12354b Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 10 Feb 2026 14:41:00 +0100 Subject: [PATCH 1/4] Add divisibility of exponentials --- CHANGELOG.md | 6 ++++++ src/Data/Nat/Divisibility.agda | 11 +++++++++++ 2 files changed, 17 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 598b3e519c..672045bb1b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -259,6 +259,12 @@ Additions to existing modules map : P ⊆ Q → All P xs → All Q xs ``` +* In `Data.Nat.Divisiblity`: + ```agad + m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o + n≤o⇒m^n∣m^o : ∀ m → n ≤ o → m ^ n ∣ m ^ o + ``` + * In `Data.Nat.Logarithm` ```agda 2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index c5d42a2c90..946e204428 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -257,6 +257,17 @@ m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m (p + q) * d ∎ where open ∣-Reasoning +------------------------------------------------------------------------ +-- Properties of _∣_ and _^_ + +m∣n⇒m^o∣n^o : ∀ {m n} o → m ∣ n → m ^ o ∣ n ^ o +m∣n⇒m^o∣n^o zero m∣n = ∣-refl +m∣n⇒m^o∣n^o (suc o) m∣n = *-pres-∣ m∣n (m∣n⇒m^o∣n^o o m∣n) + +n≤o⇒m^n∣m^o : ∀ m {n o} → n ≤ o → m ^ n ∣ m ^ o +n≤o⇒m^n∣m^o m z≤n = 1∣ _ +n≤o⇒m^n∣m^o m (s≤s n≤o) = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m n≤o) + ------------------------------------------------------------------------ -- Properties of _∣_ and _/_ From 564e468d8db83782d488279702758516c77e2c50 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 11 Feb 2026 08:44:44 +0100 Subject: [PATCH 2/4] Make inequality irrelevant --- CHANGELOG.md | 2 +- src/Data/Nat/Divisibility.agda | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 672045bb1b..6ef2b7eb43 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -262,7 +262,7 @@ Additions to existing modules * In `Data.Nat.Divisiblity`: ```agad m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o - n≤o⇒m^n∣m^o : ∀ m → n ≤ o → m ^ n ∣ m ^ o + n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o ``` * In `Data.Nat.Logarithm` diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 946e204428..906a044e84 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -264,9 +264,9 @@ m∣n⇒m^o∣n^o : ∀ {m n} o → m ∣ n → m ^ o ∣ n ^ o m∣n⇒m^o∣n^o zero m∣n = ∣-refl m∣n⇒m^o∣n^o (suc o) m∣n = *-pres-∣ m∣n (m∣n⇒m^o∣n^o o m∣n) -n≤o⇒m^n∣m^o : ∀ m {n o} → n ≤ o → m ^ n ∣ m ^ o -n≤o⇒m^n∣m^o m z≤n = 1∣ _ -n≤o⇒m^n∣m^o m (s≤s n≤o) = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m n≤o) +n≤o⇒m^n∣m^o : ∀ m {n o} → .(n ≤ o) → m ^ n ∣ m ^ o +n≤o⇒m^n∣m^o m {zero} {o} n≤o = 1∣ _ +n≤o⇒m^n∣m^o m {suc n} {suc o} n≤o = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m (s≤s⁻¹ n≤o)) ------------------------------------------------------------------------ -- Properties of _∣_ and _/_ From 88ee964b6ea5376f667796f2795dfc7f737c291b Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 11 Feb 2026 11:16:49 +0100 Subject: [PATCH 3/4] =?UTF-8?q?Simplify=20m=E2=88=A3n=E2=87=92m^o=E2=88=A3?= =?UTF-8?q?n^o=20definition=20by=20reusing=20^-distrib=CA=B3-*?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Divisibility.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 906a044e84..a7d13222e4 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -261,8 +261,7 @@ m*n∣⇒n∣ m n rewrite *-comm m n = m*n∣⇒m∣ n m -- Properties of _∣_ and _^_ m∣n⇒m^o∣n^o : ∀ {m n} o → m ∣ n → m ^ o ∣ n ^ o -m∣n⇒m^o∣n^o zero m∣n = ∣-refl -m∣n⇒m^o∣n^o (suc o) m∣n = *-pres-∣ m∣n (m∣n⇒m^o∣n^o o m∣n) +m∣n⇒m^o∣n^o o (divides-refl m/n) = divides (m/n ^ o) (^-distribʳ-* o m/n _) n≤o⇒m^n∣m^o : ∀ m {n o} → .(n ≤ o) → m ^ n ∣ m ^ o n≤o⇒m^n∣m^o m {zero} {o} n≤o = 1∣ _ From 62d61466b36f3804716bece3e6023120f7590116 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 11 Feb 2026 11:21:58 +0100 Subject: [PATCH 4/4] Fiddling with variable names --- src/Data/Nat/Divisibility.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index a7d13222e4..cba883efab 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -264,8 +264,8 @@ m∣n⇒m^o∣n^o : ∀ {m n} o → m ∣ n → m ^ o ∣ n ^ o m∣n⇒m^o∣n^o o (divides-refl m/n) = divides (m/n ^ o) (^-distribʳ-* o m/n _) n≤o⇒m^n∣m^o : ∀ m {n o} → .(n ≤ o) → m ^ n ∣ m ^ o -n≤o⇒m^n∣m^o m {zero} {o} n≤o = 1∣ _ -n≤o⇒m^n∣m^o m {suc n} {suc o} n≤o = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m (s≤s⁻¹ n≤o)) +n≤o⇒m^n∣m^o m {zero} 0≤o = 1∣ _ +n≤o⇒m^n∣m^o m {suc _} {suc _} sn≤so = *-monoʳ-∣ m (n≤o⇒m^n∣m^o m (s≤s⁻¹ sn≤so)) ------------------------------------------------------------------------ -- Properties of _∣_ and _/_