Add a couple lemmas about product in Data.List.Properties (#2460)

* 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

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

src/Data/List/Properties.agda

@@ -842,6 +842,22 @@ 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} (nzn ∷ nzns) = m*n≢0 n (product ns)
+  where instance
+    _ = nzn
+    _ = product≢0 nzns
+
+∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
+∈⇒≤product {ns = n ∷ ns} (_ ∷ nzns) (here refl) =
+  m≤m*n n (product ns)
+  where instance _ = product≢0 nzns
+∈⇒≤product {ns = n ∷ _} (nz ∷ nzns) (there n∈ns) =
+  m≤n⇒m≤o*n n (∈⇒≤product nzns n∈ns)
+  where instance _ = nz
+
+
 ------------------------------------------------------------------------
 -- applyUpTo
 

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}}

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