Miscellaneous improvements done during finite cycle group implementation (#1080)

Author: uzytkownik

CHANGELOG.md

@@ -21,6 +21,11 @@ Bug-fixes
 * The incorrectly named proof `p⊆q⇒∣p∣<∣q∣ : p ⊆ q → ∣ p ∣ ≤ ∣ q ∣` in
   `Data.Fin.Subset.Properties` now has the correct name `p⊆q⇒∣p∣≤∣q∣`.
 
+* The incorrectly named proofs `∀[m≤n⇒m≢o]⇒o<n : (∀ {m} → m ≤ n → m ≢ o) → n < o`
+  and `∀[m<n⇒m≢o]⇒o≤n : (∀ {m} → m < n → m ≢ o) → n ≤ o` in `Data.Nat.Properties`
+  now has the correct names `∀[m≤n⇒m≢o]⇒n<o` and `∀[m<n⇒m≢o]⇒n≤o`.
+
+
 * Changed the definition of `_⊓_` for `Codata.Conat`; it was mistakenly using
   `_⊔_` in a recursive call.
 
@@ -268,6 +273,12 @@ attached to all deprecated names to discourage their use.
   Any¬→¬All  ↦  Any¬⇒¬All
   ```
 
+* In `Data.Nat.Properties
+  ```agda
+  ∀[m≤n⇒m≢o]⇒o<n  ↦  ∀[m≤n⇒m≢o]⇒n<o
+  ∀[m<n⇒m≢o]⇒o≤n  ↦  ∀[m<n⇒m≢o]⇒n≤o
+  ```
+
 * In `Algebra.Morphism.Definitions` and `Relation.Binary.Morphism.Definitions`
   the type `Morphism A B` has been deprecated in favour of the standard
   function notation `A → B`.
@@ -409,6 +420,8 @@ Other major additions
 Other minor additions
 ---------------------
 
+* Added commutativeSemigroup to `Algebra.Bundles.CommutativeMonoid`
+
 * Added new record to `Algebra.Bundles`:
   ```
   +-rawGroup : RawGroup c ℓ
@@ -540,6 +553,21 @@ Other minor additions
   _∷ʳ_ : DiffList A → A → DiffList A
   ```
 
+* Added new proofs to `Data.Nat.DivMod`:
+  ```agda
+  %-distribˡ-* : (m * n) % d ≡ ((m % d) * (n % d)) % d
+  ```
+
+* Added new proofs to `Data.Nat.Properties`:
+  ```agda
+  ∸-cancelʳ-≡ : o ≤ m → o ≤ n → m ∸ o ≡ n ∸ o → m ≡ n
+  ⌊n/2⌋+⌈n/2⌉≡n : ⌊ n /2⌋ + ⌈ n /2⌉ ≡ n
+  ⌊n/2⌋≤n : ⌊ n /2⌋ ≤ n
+  ⌊n/2⌋<n : ⌊ suc n /2⌋ < suc n
+  ⌈n/2⌉≤n : ⌈ n /2⌉ ≤ n
+  ⌈n/2⌉<n : ⌈ suc (suc n) /2⌉ < suc (suc n)
+  ```
+
 * Added new properties to `Data.Fin.Subset`:
   ```agda
   _⊂_ : Subset n → Subset n → Set

src/Algebra/Bundles.agda

@@ -187,6 +187,9 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
 
+  commutativeSemigroup : CommutativeSemigroup _ _
+  commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }
+
   open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
 
 

src/Data/Nat/DivMod.agda

@@ -16,6 +16,7 @@ open import Data.Nat.Base as Nat
 open import Data.Nat.DivMod.Core
 open import Data.Nat.Divisibility.Core
 open import Data.Nat.Properties
+open import Data.Nat.Tactic.RingSolver
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (False)
 
@@ -115,6 +116,22 @@ m<[1+n%d]⇒m≤[n%d] {m} n (suc d-1) = k<1+a[modₕ]n⇒k≤a[modₕ]n 0 m n d-
   (m % d +  n % d + (n / d) * d)  % d ≡⟨ [m+kn]%n≡m%n (m % d + n % d) (n / d) d-1 ⟩
   (m % d +  n % d)                % d ∎
 
+%-distribˡ-* : ∀ m n d {≢0} → ((m * n) % d) {≢0} ≡ (((m % d) {≢0} * (n % d) {≢0}) % d) {≢0}
+%-distribˡ-* m n d@(suc d-1) = begin-equality
+  (m * n)                                             % d ≡⟨ cong (λ h → (h * n) % d) (m≡m%n+[m/n]*n m d-1) ⟩
+  ((m′ + k * d) * n)                                  % d ≡⟨ cong (λ h → ((m′ + k * d) * h) % d) (m≡m%n+[m/n]*n n d-1) ⟩
+  ((m′ + k * d) * (n′ + j * d))                       % d ≡⟨ cong (_% d) (lemma m′ n′ k j d) ⟩
+  (m′ * n′ + (m′ * j + (n′ + j * d) * k) * d)         % d ≡⟨ [m+kn]%n≡m%n (m′ * n′) (m′ * j + (n′ + j * d) * k) d-1 ⟩
+  (m′ * n′)                                           % d ≡⟨⟩
+  ((m % d) * (n % d)) % d ∎
+  where
+  m′ = m % d
+  n′ = n % d
+  k = m / d
+  j = n / d
+  lemma : ∀ m′ n′ k j d → (m′ + k * d) * (n′ + j * d) ≡ m′ * n′ + (m′ * j + (n′ + j * d) * k) * d
+  lemma = solve-∀
+
 %-remove-+ˡ : ∀ {m} n {d} {≢0} → d ∣ m → ((m + n) % d) {≢0} ≡ (n % d) {≢0}
 %-remove-+ˡ {m} n {d@(suc d-1)} (divides p refl) = begin-equality
   (p * d + n) % d ≡⟨ cong (_% d) (+-comm (p * d) n) ⟩

src/Data/Nat/Properties.agda

@@ -377,18 +377,18 @@ m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
 m<n⇒m≤1+n (s≤s z≤n)       = z≤n
 m<n⇒m≤1+n (s≤s (s≤s m<n)) = s≤s (m<n⇒m≤1+n (s≤s m<n))
 
-∀[m≤n⇒m≢o]⇒o<n : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
-∀[m≤n⇒m≢o]⇒o<n _       zero    m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)
-∀[m≤n⇒m≢o]⇒o<n zero    (suc o) _       = 0<1+n
-∀[m≤n⇒m≢o]⇒o<n (suc n) (suc o) m≤n⇒n≢o = s≤s (∀[m≤n⇒m≢o]⇒o<n n o rec)
+∀[m≤n⇒m≢o]⇒n<o : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
+∀[m≤n⇒m≢o]⇒n<o _       zero    m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)
+∀[m≤n⇒m≢o]⇒n<o zero    (suc o) _       = 0<1+n
+∀[m≤n⇒m≢o]⇒n<o (suc n) (suc o) m≤n⇒n≢o = s≤s (∀[m≤n⇒m≢o]⇒n<o n o rec)
   where
   rec : ∀ {m} → m ≤ n → m ≢ o
   rec m≤n refl = m≤n⇒n≢o (s≤s m≤n) refl
 
-∀[m<n⇒m≢o]⇒o≤n : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
-∀[m<n⇒m≢o]⇒o≤n zero    n       _       = z≤n
-∀[m<n⇒m≢o]⇒o≤n (suc n) zero    m<n⇒m≢0 = contradiction refl (m<n⇒m≢0 0<1+n)
-∀[m<n⇒m≢o]⇒o≤n (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒o≤n n o rec)
+∀[m<n⇒m≢o]⇒n≤o : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
+∀[m<n⇒m≢o]⇒n≤o zero    n       _       = z≤n
+∀[m<n⇒m≢o]⇒n≤o (suc n) zero    m<n⇒m≢0 = contradiction refl (m<n⇒m≢0 0<1+n)
+∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
   where
   rec : ∀ {m} → m < n → m ≢ o
   rec x<m refl = m<n⇒m≢o (s≤s x<m) refl
@@ -1520,6 +1520,10 @@ m≮m∸n (suc m) (suc n) = m≮m∸n m n ∘ ≤-trans (n≤1+n (suc m))
 ∸-cancelˡ-≡ {n = suc n} (s≤s _)   z≤n       eq = contradiction (sym eq) (1+m≢m∸n n)
 ∸-cancelˡ-≡ {_}         (s≤s n≤m) (s≤s o≤m) eq = cong suc (∸-cancelˡ-≡ n≤m o≤m eq)
 
+∸-cancelʳ-≡ :  ∀ {m n o} → o ≤ m → o ≤ n → m ∸ o ≡ n ∸ o → m ≡ n
+∸-cancelʳ-≡  z≤n       z≤n      eq = eq
+∸-cancelʳ-≡ (s≤s o≤m) (s≤s o≤n) eq = cong suc (∸-cancelʳ-≡ o≤m o≤n eq)
+
 m∸n≡0⇒m≤n : ∀ {m n} → m ∸ n ≡ 0 → m ≤ n
 m∸n≡0⇒m≤n {zero}  {_}    _   = z≤n
 m∸n≡0⇒m≤n {suc m} {suc n} eq = s≤s (m∸n≡0⇒m≤n eq)
@@ -1798,6 +1802,22 @@ m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)
   suc (⌊ n /2⌋ + ⌊ suc n /2⌋) ≡⟨ cong suc (⌊n/2⌋+⌈n/2⌉≡n n) ⟩
   suc n                       ∎
 
+⌊n/2⌋≤n : ∀ n → ⌊ n /2⌋ ≤ n
+⌊n/2⌋≤n zero          = z≤n
+⌊n/2⌋≤n (suc zero)    = z≤n
+⌊n/2⌋≤n (suc (suc n)) = s≤s (≤-step (⌊n/2⌋≤n n))
+
+⌊n/2⌋<n : ∀ n → ⌊ suc n /2⌋ < suc n
+⌊n/2⌋<n zero    = s≤s z≤n
+⌊n/2⌋<n (suc n) = s≤s (s≤s (⌊n/2⌋≤n n))
+
+⌈n/2⌉≤n : ∀ n → ⌈ n /2⌉ ≤ n
+⌈n/2⌉≤n zero = z≤n
+⌈n/2⌉≤n (suc n) = s≤s (⌊n/2⌋≤n n)
+
+⌈n/2⌉<n : ∀ n → ⌈ suc (suc n) /2⌉ < suc (suc n)
+⌈n/2⌉<n n = s≤s (⌊n/2⌋<n n)
+
 ------------------------------------------------------------------------
 -- Properties of _≤′_ and _<′_
 ------------------------------------------------------------------------
@@ -2234,3 +2254,18 @@ n∸m≤n m n = m∸n≤m n m
 "Warning: n∸m≤n was deprecated in v1.2.
 Please use m∸n≤m instead (note, you will need to switch the argument order)."
 #-}
+
+-- Version 1.3
+
+∀[m≤n⇒m≢o]⇒o<n : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
+∀[m≤n⇒m≢o]⇒o<n = ∀[m≤n⇒m≢o]⇒n<o
+{-# WARNING_ON_USAGE n∸m≤∣n-m∣
+"Warning: ∀[m≤n⇒m≢o]⇒o<n was deprecated in v1.3.
+Please use ∀[m≤n⇒m≢o]⇒n<o instead."
+#-}
+∀[m<n⇒m≢o]⇒o≤n : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
+∀[m<n⇒m≢o]⇒o≤n = ∀[m<n⇒m≢o]⇒n≤o
+{-# WARNING_ON_USAGE n∸m≤∣n-m∣
+"Warning: ∀[m<n⇒m≢o]⇒o≤n was deprecated in v1.3.
+Please use ∀[m<n⇒m≢o]⇒n≤o instead."
+#-}