From 355ac2548fb60adae218e32f5466160d15ecb1ef Mon Sep 17 00:00:00 2001
From: dolio <dan.doel@gmail.com>
Date: Thu, 22 Aug 2024 11:58:14 -0400
Subject: [PATCH] Add a couple lemmas about product in Data.List.Properties
 (#2460)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Add a couple lemmas about product in Data.List.Properties

* Rework product proofs to be cleaner

* Add CHANGELOG entries

* Get rid of unnecessary module use in product proofs

* Various product proof adjustments

- Renamed nonEmpty-product to product≢0
- Swapped argument order of ∈⇒≤product
- Factored the ordering proofs out into Data.Nat.Properties
- Removed the custom product≢0 proof in Primality

* Fix a CHANGELOG oversight

* Suggested minor changes to ∈⇒≤product

* Manually supply instances in product properties
---
 CHANGELOG.md                  | 14 +++++++++++++-
 src/Data/List/Properties.agda | 11 +++++++++++
 src/Data/Nat/Primality.agda   |  5 +----
 src/Data/Nat/Properties.agda  | 13 ++++++++-----
 4 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9ae126acd4..57222329ef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,12 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Data.List.Properties`:
+  ```agda
+  product≢0 : All NonZero ns → NonZero (product ns)
+  ∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
+  ```
+
 * In `Data.List.Relation.Unary.All`:
   ```agda
   search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
@@ -65,7 +71,13 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
-* New lemmas in `Data.Nat.Properties`: adjunction between `suc` and `pred`
+* New lemmas in `Data.Nat.Properties`:
+  ```agda
+  m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o
+  m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n
+  ```
+
+  adjunction between `suc` and `pred`
   ```agda
   suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
   m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index b9936f2a3b..f847d8a059 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -842,6 +842,17 @@ sum-++ (x ∷ xs) ys = begin
 ∈⇒∣product {n} {n ∷ ns} (here  refl) = divides (product ns) (*-comm n (product ns))
 ∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
 
+product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
+product≢0 [] = _
+product≢0 {n ∷ ns} (n≢0 ∷ ns≢0) = m*n≢0 n (product ns) {{n≢0}} {{product≢0 ns≢0}}
+
+∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
+∈⇒≤product {ns = n ∷ ns} (_ ∷ ns≢0) (here refl) =
+  m≤m*n n (product ns) {{product≢0 ns≢0}}
+∈⇒≤product {ns = n ∷ _} (n≢0 ∷ ns≢0) (there n∈ns) =
+  m≤n⇒m≤o*n n {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
+
+
 ------------------------------------------------------------------------
 -- applyUpTo
 
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index b07883ce9b..ad7283235e 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -9,6 +9,7 @@
 module Data.Nat.Primality where
 
 open import Data.List.Base using ([]; _∷_; product)
+open import Data.List.Properties using (product≢0)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
@@ -324,10 +325,6 @@ prime⇒¬composite (prime p) = p
 
 productOfPrimes≢0 : ∀ {as} → All Prime as → NonZero (product as)
 productOfPrimes≢0 pas = product≢0 (All.map prime⇒nonZero pas)
-  where
-  product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
-  product≢0 [] = _
-  product≢0 {n ∷ ns} (nzn ∷ nzns) = m*n≢0 n _ {{nzn}} {{product≢0 nzns}}
 
 productOfPrimes≥1 : ∀ {as} → All Prime as → product as ≥ 1
 productOfPrimes≥1 {as} pas = >-nonZero⁻¹ _ {{productOfPrimes≢0 pas}}
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 9911e2b9a1..b7a7c00511 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -1000,6 +1000,12 @@ m≤n*m m n@(suc _) = begin
   m * n ≡⟨ *-comm m n ⟩
   n * m ∎
 
+m≤n⇒m≤o*n : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ o * n
+m≤n⇒m≤o*n o m≤n = ≤-trans m≤n (m≤n*m _ o)
+
+m≤n⇒m≤n*o : ∀ o .{{_ : NonZero o}} → m ≤ n → m ≤ n * o
+m≤n⇒m≤n*o o m≤n = ≤-trans m≤n (m≤m*n _ o)
+
 m<m*n : ∀ m n .{{_ : NonZero m}} → 1 < n → m < m * n
 m<m*n m@(suc m-1) n@(suc (suc n-2)) (s≤s (s≤s _)) = begin-strict
   m           <⟨ s≤s (s≤s (m≤n+m m-1 n-2)) ⟩
@@ -1008,13 +1014,10 @@ m<m*n m@(suc m-1) n@(suc (suc n-2)) (s≤s (s≤s _)) = begin-strict
   m * n       ∎
 
 m<n⇒m<n*o : ∀ o .{{_ : NonZero o}} → m < n → m < n * o
-m<n⇒m<n*o {n = n} o m<n = <-≤-trans m<n (m≤m*n n o)
+m<n⇒m<n*o = m≤n⇒m≤n*o
 
 m<n⇒m<o*n : ∀ {m n} o .{{_ : NonZero o}} → m < n → m < o * n
-m<n⇒m<o*n {m} {n} o m<n = begin-strict
-  m     <⟨ m<n⇒m<n*o o m<n ⟩
-  n * o ≡⟨ *-comm n o ⟩
-  o * n ∎
+m<n⇒m<o*n = m≤n⇒m≤o*n
 
 *-cancelʳ-< : RightCancellative _<_ _*_
 *-cancelʳ-< zero    zero    (suc o) _     = 0<1+n