From e272571b5cc88375f92e9a784261ba9149307e1b Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 26 Sep 2025 12:57:27 +0200 Subject: [PATCH 1/3] More distributivity properties for nats --- CHANGELOG.md | 8 ++++++++ src/Data/Nat/ListAction/Properties.agda | 22 ++++++++++++++++++---- src/Data/Nat/Properties.agda | 11 +++++++++++ 3 files changed, 37 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 081dda5b66..f5b3f12422 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -72,10 +72,18 @@ Additions to existing modules ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j ``` +* In `Data.Nat.ListAction.Properties` + ```agda + *-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns) + *-distribʳ-sum : ∀ m ns → sum ns * m ≡ sum (map (_* m) ns) + ^-distribʳ-product : ∀ m ns → product ns ^ m ≡ product (map (_^ m) ns) + ``` + * In `Data.Nat.Properties`: ```agda ≟-≢ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m) + ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m ``` * In `Data.Vec.Properties`: diff --git a/src/Data/Nat/ListAction/Properties.agda b/src/Data/Nat/ListAction/Properties.agda index 708bc2dc15..4405fa9862 100644 --- a/src/Data/Nat/ListAction/Properties.agda +++ b/src/Data/Nat/ListAction/Properties.agda @@ -12,7 +12,7 @@ module Data.Nat.ListAction.Properties where open import Algebra.Bundles using (CommutativeMonoid) -open import Data.List.Base using (List; []; _∷_; _++_) +open import Data.List.Base using (List; []; _∷_; _++_; map) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ) @@ -20,15 +20,17 @@ open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (foldr-commMonoid) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Any using (here; there) -open import Data.Nat.Base using (ℕ; _+_; _*_; NonZero; _≤_) +open import Data.Nat.Base using (ℕ; _+_; _*_; _^_; NonZero; _≤_) open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n) open import Data.Nat.ListAction using (sum; product) open import Data.Nat.Properties using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n - ; +-0-commutativeMonoid; *-1-commutativeMonoid) + ; +-0-commutativeMonoid; *-1-commutativeMonoid + ; *-zeroˡ; *-zeroʳ; *-distribˡ-+; *-distribʳ-+ + ; ^-zeroˡ; ^-distribʳ-*) open import Relation.Binary.Core using (_Preserves_⟶_) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; sym; cong) + using (_≡_; refl; sym; trans; cong) open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning) @@ -51,6 +53,14 @@ sum-++ (m ∷ ms) ns = begin (m + sum ms) + sum ns ∎ where open ≡-Reasoning +*-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns) +*-distribˡ-sum m [] = *-zeroʳ m +*-distribˡ-sum m (n ∷ ns) = trans (*-distribˡ-+ m n (sum ns)) (cong (m * n +_) (*-distribˡ-sum m ns)) + +*-distribʳ-sum : ∀ m ns → sum ns * m ≡ sum (map (_* m) ns) +*-distribʳ-sum m [] = *-zeroˡ m +*-distribʳ-sum m (n ∷ ns) = trans (*-distribʳ-+ m n (sum ns)) (cong (n * m +_) (*-distribʳ-sum m ns)) + sum-↭ : sum Preserves _↭_ ⟶ _≡_ sum-↭ p = foldr-commMonoid ℕ-+-0.setoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p) where module ℕ-+-0 = CommutativeMonoid +-0-commutativeMonoid @@ -78,6 +88,10 @@ product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}} ∈⇒≤product (n≢0 ∷ ns≢0) (here refl) = m≤m*n _ _ {{product≢0 ns≢0}} ∈⇒≤product (n≢0 ∷ ns≢0) (there n∈ns) = m≤n⇒m≤o*n _ {{n≢0}} (∈⇒≤product ns≢0 n∈ns) +^-distribʳ-product : ∀ m ns → product ns ^ m ≡ product (map (_^ m) ns) +^-distribʳ-product m [] = ^-zeroˡ m +^-distribʳ-product m (n ∷ ns) = trans (^-distribʳ-* m n (product ns)) (cong (n ^ m *_) (^-distribʳ-product m ns)) + product-↭ : product Preserves _↭_ ⟶ _≡_ product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p) where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 6102400d68..5daa761327 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1067,6 +1067,17 @@ m Date: Fri, 26 Sep 2025 13:15:17 +0200 Subject: [PATCH 2/3] Simplify proof using existing lemma --- src/Data/Nat/Properties.agda | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 5daa761327..052a87356c 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1071,11 +1071,7 @@ m Date: Mon, 29 Sep 2025 08:48:39 +0200 Subject: [PATCH 3/3] Use lemma instead of refl In principle this lets us translate more easily to an arbitrary semiring --- src/Data/Nat/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 052a87356c..dc40f03132 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1068,7 +1068,7 @@ m