More properties of absolute value in Data.Rational (#1477)

agda · Apr 17, 2021 · 84c7753 · 84c7753
1 parent 6dcfb72
commit 84c7753
Show file tree

Hide file tree

Showing 3 changed files with 56 additions and 7 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -789,12 +789,14 @@ Other minor additions
   ∣-∣-nonNeg                 : NonNegative ∣ p ∣
   0≤∣p∣                      : 0ℚ ≤ ∣ p ∣
   0≤p⇒∣p∣≡p                  : 0ℚ ≤ p → ∣ p ∣ ≡ p
+  ∣p∣≡p⇒0≤p                  : ∣ p ∣ ≡ p → 0ℚ ≤ p
   ∣-p∣≡∣p∣                   : ∣ - p ∣ ≡ ∣ p ∣
-  ∣p∣≡p⇒p≡0                  : ∣ p ∣ ≡ 0ℚ → p ≡ 0ℚ
-  ∣p∣≡p⊎∣p∣≡-p               : ∣ p ∣ ≡ p ⊎ ∣ p ∣ ≡ - p
+  ∣p∣≡0⇒p≡0                  : ∣ p ∣ ≡ 0ℚ → p ≡ 0ℚ
+  ∣p∣≡p∨∣p∣≡-p               : ∣ p ∣ ≡ p ⊎ ∣ p ∣ ≡ - p
   ∣p+q∣≤∣p∣+∣q∣              : ∣ p + q ∣ ≤ ∣ p ∣ + ∣ q ∣
   ∣p-q∣≤∣p∣+∣q∣              : ∣ p - q ∣ ≤ ∣ p ∣ + ∣ q ∣
   ∣p*q∣≡∣p∣*∣q∣              : ∣ p * q ∣ ≡ ∣ p ∣ * ∣ q ∣
+  ∣∣p∣∣≡∣p∣                  : ∣ ∣ p ∣ ∣ ≡ ∣ p ∣
   ```
 
 * Add new relations and functions to `Data.Rational.Unnormalised.Base`:
@@ -827,6 +829,9 @@ Other minor additions
   ≤ᵇ⇒≤                      : T (p ≤ᵇ q) → p ≤ q
   ≤⇒≤ᵇ                      : p ≤ q → T (p ≤ᵇ q)
 
+  p+p≃0⇒p≃0                 : p + p ≃ 0ℚᵘ → p ≃ 0ℚᵘ
+  p≃-p⇒p≃0                  : p ≃ - p → p ≃ 0ℚᵘ
+
   neg-cancel-<              : - p < - q → q < p
   neg-cancel-≤-≥            : - p ≤ - q → q ≤ p
 
@@ -986,17 +991,22 @@ Other minor additions
   *-distribʳ-⊓-nonPos       : NonPositive p → (q ⊓ r) * p ≃ (q * p) ⊔ (r * p)
 
   ∣-∣-cong                  : p ≃ q → ∣ p ∣ ≃ ∣ q ∣
+  ∣-∣-nonNeg                : NonNegative ∣ p ∣
+  0≤∣p∣                     : 0 ≤ ∣ p ∣
   ∣p∣≃0⇒p≃0                 : ∣ p ∣ ≃ 0ℚᵘ → p ≃ 0ℚᵘ
   ∣-p∣≡∣p∣                  : ∣ - p ∣ ≡ ∣ p ∣
   ∣-p∣≃∣p∣                  : ∣ - p ∣ ≃ ∣ p ∣
   0≤p⇒∣p∣≡p                 : 0ℚᵘ ≤ p → ∣ p ∣ ≡ p
   0≤p⇒∣p∣≃p                 : 0ℚᵘ ≤ p → ∣ p ∣ ≃ p
   ∣p∣≡p⇒0≤p                 : ∣ p ∣ ≡ p → 0ℚᵘ ≤ p
+  ∣p∣≃p⇒0≤p                 : ∣ p ∣ ≃ p → 0ℚᵘ ≤ p
   ∣p∣≡p∨∣p∣≡-p              : (∣ p ∣ ≡ p) ⊎ (∣ p ∣ ≡ - p)
   ∣p+q∣≤∣p∣+∣q∣             : ∣ p + q ∣ ≤ ∣ p ∣ + ∣ q ∣
   ∣p-q∣≤∣p∣+∣q∣             : ∣ p - q ∣ ≤ ∣ p ∣ + ∣ q ∣
   ∣p*q∣≡∣p∣*∣q∣             : ∣ p * q ∣ ≡ ∣ p ∣ * ∣ q ∣
   ∣p*q∣≃∣p∣*∣q∣             : ∣ p * q ∣ ≃ ∣ p ∣ * ∣ q ∣
+  ∣∣p∣∣≡∣p∣                 : ∣ ∣ p ∣ ∣ ≡ ∣ p ∣
+  ∣∣p∣∣≃∣p∣                 : ∣ ∣ p ∣ ∣ ≃ ∣ p ∣
   ```
 
 * Added new functions and pattern synonyms to `Data.Tree.AVL.Indexed`:

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
@@ -1619,8 +1619,8 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ------------------------------------------------------------------------
 -- Properties
 
-∣p∣≡p⇒p≡0 : ∀ p → ∣ p ∣ ≡ 0ℚ → p ≡ 0ℚ
-∣p∣≡p⇒p≡0 (mkℚ +0 zero _) ∣p∣≡0 = refl
+∣p∣≡0⇒p≡0 : ∀ p → ∣ p ∣ ≡ 0ℚ → p ≡ 0ℚ
+∣p∣≡0⇒p≡0 (mkℚ +0 zero _) ∣p∣≡0 = refl
 
 0≤∣p∣ : ∀ p → 0ℚ ≤ ∣ p ∣
 0≤∣p∣ p = *≤* (begin
@@ -1638,9 +1638,16 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣-p∣≡∣p∣ (mkℚ (+ zero) d-1 _) = refl
 ∣-p∣≡∣p∣ (mkℚ -[1+ n ] d-1 _) = refl
 
-∣p∣≡p⊎∣p∣≡-p : ∀ p → ∣ p ∣ ≡ p ⊎ ∣ p ∣ ≡ - p
-∣p∣≡p⊎∣p∣≡-p (mkℚ (+ n) d-1 _) = inj₁ refl
-∣p∣≡p⊎∣p∣≡-p (mkℚ (-[1+ n ]) d-1 _) = inj₂ refl
+∣p∣≡p⇒0≤p : ∀ {p} → ∣ p ∣ ≡ p → 0ℚ ≤ p
+∣p∣≡p⇒0≤p {p} ∣p∣≡p = toℚᵘ-cancel-≤ (ℚᵘ.∣p∣≃p⇒0≤p (begin-equality
+  ℚᵘ.∣ toℚᵘ p ∣  ≈⟨ ℚᵘ.≃-sym (toℚᵘ-homo-∣-∣ p) ⟩
+  toℚᵘ ∣ p ∣     ≡⟨ cong toℚᵘ ∣p∣≡p ⟩
+  toℚᵘ p         ∎))
+  where open ℚᵘ.≤-Reasoning
+
+∣p∣≡p∨∣p∣≡-p : ∀ p → ∣ p ∣ ≡ p ⊎ ∣ p ∣ ≡ - p
+∣p∣≡p∨∣p∣≡-p (mkℚ (+ n) d-1 _) = inj₁ refl
+∣p∣≡p∨∣p∣≡-p (mkℚ (-[1+ n ]) d-1 _) = inj₂ refl
 
 ∣p+q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p + q ∣ ≤ ∣ p ∣ + ∣ q ∣
 ∣p+q∣≤∣p∣+∣q∣ p q = toℚᵘ-cancel-≤ (begin
@@ -1674,6 +1681,8 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣-∣-nonNeg (mkℚ +0       _ _) = _
 ∣-∣-nonNeg (mkℚ -[1+ _ ] _ _) = _
 
+∣∣p∣∣≡∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≡ ∣ p ∣
+∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p)
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
@@ -717,6 +717,9 @@ nonNeg∧nonPos⇒0 {mkℚᵘ +0 _} _ _ = *≡* refl
   q + r ≈⟨ +-comm q r ⟩
   r + q ∎ where open ≤-Reasoning
 
+p+p≃0⇒p≃0 : ∀ p → p + p ≃ 0ℚᵘ → p ≃ 0ℚᵘ
+p+p≃0⇒p≃0 (mkℚᵘ (ℤ.+ ℕ.zero) _) (*≡* _) = *≡* refl
+
 ------------------------------------------------------------------------
 -- Properties of _+_ and -_
 
@@ -729,6 +732,13 @@ neg-distrib-+ p q = ↥↧≡⇒≡ (begin
   ) refl
   where open ≡-Reasoning
 
+p≃-p⇒p≃0 : ∀ p → p ≃ - p → p ≃ 0ℚᵘ
+p≃-p⇒p≃0 p p≃-p = p+p≃0⇒p≃0 p (begin-equality
+  p + p  ≈⟨ +-congʳ p p≃-p ⟩
+  p - p  ≈⟨ +-inverseʳ p ⟩
+  0ℚᵘ    ∎)
+  where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of _+_ and _≤_
 
@@ -1647,6 +1657,11 @@ neg-distrib-⊓-⊔ = antimono-≤-distrib-⊓ neg-mono-≤
 ∣p∣≃0⇒p≃0 {mkℚᵘ (ℤ.+ n)  d-1} p≃0ℚ = p≃0ℚ
 ∣p∣≃0⇒p≃0 {mkℚᵘ -[1+ n ] d-1} (*≡* ())
 
+0≤∣p∣ : ∀ p → 0ℚᵘ ≤ ∣ p ∣
+0≤∣p∣ (mkℚᵘ ℤ.+0       _) = *≤* (ℤ.+≤+ ℕ.z≤n)
+0≤∣p∣ (mkℚᵘ ℤ.+[1+ _ ] _) = *≤* (ℤ.+≤+ ℕ.z≤n)
+0≤∣p∣ (mkℚᵘ ℤ.-[1+ _ ] _) = *≤* (ℤ.+≤+ ℕ.z≤n)
+
 ∣-p∣≡∣p∣ : ∀ p → ∣ - p ∣ ≡ ∣ p ∣
 ∣-p∣≡∣p∣ (mkℚᵘ +[1+ n ] d) = refl
 ∣-p∣≡∣p∣ (mkℚᵘ +0       d) = refl
@@ -1674,6 +1689,11 @@ neg-distrib-⊓-⊔ = antimono-≤-distrib-⊓ neg-mono-≤
 ∣p∣≡p∨∣p∣≡-p (mkℚᵘ (ℤ.+ n)    d-1) = inj₁ refl
 ∣p∣≡p∨∣p∣≡-p (mkℚᵘ (-[1+ n ]) d-1) = inj₂ refl
 
+∣p∣≃p⇒0≤p : ∀ {p} → ∣ p ∣ ≃ p → 0ℚᵘ ≤ p
+∣p∣≃p⇒0≤p {p} ∣p∣≃p with ∣p∣≡p∨∣p∣≡-p p
+... | inj₁ ∣p∣≡p  = ∣p∣≡p⇒0≤p ∣p∣≡p
+... | inj₂ ∣p∣≡-p rewrite ∣p∣≡-p = ≤-reflexive (≃-sym (p≃-p⇒p≃0 p (≃-sym ∣p∣≃p)))
+
 ∣p+q∣≤∣p∣+∣q∣ : ∀ p q → ∣ p + q ∣ ≤ ∣ p ∣ + ∣ q ∣
 ∣p+q∣≤∣p∣+∣q∣ p q = *≤* (begin
   ↥ ∣ p + q ∣ ℤ.* ↧ (∣ p ∣ + ∣ q ∣)                ≡⟨⟩
@@ -1732,6 +1752,16 @@ neg-distrib-⊓-⊔ = antimono-≤-distrib-⊓ neg-mono-≤
 ∣p*q∣≃∣p∣*∣q∣ : ∀ p q → ∣ p * q ∣ ≃ ∣ p ∣ * ∣ q ∣
 ∣p*q∣≃∣p∣*∣q∣ p q = ≃-reflexive (∣p*q∣≡∣p∣*∣q∣ p q)
 
+∣∣p∣∣≡∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≡ ∣ p ∣
+∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p)
+
+∣∣p∣∣≃∣p∣ : ∀ p → ∣ ∣ p ∣ ∣ ≃ ∣ p ∣
+∣∣p∣∣≃∣p∣ p = ≃-reflexive (∣∣p∣∣≡∣p∣ p)
+
+∣-∣-nonNeg : ∀ p → NonNegative ∣ p ∣
+∣-∣-nonNeg (mkℚᵘ +[1+ _ ] _) = _
+∣-∣-nonNeg (mkℚᵘ +0       _) = _
+∣-∣-nonNeg (mkℚᵘ -[1+ _ ] _) = _
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES