From 84c77536ff3099e4527a68c45cc52775fd388d40 Mon Sep 17 00:00:00 2001 From: Bob Atkey Date: Sat, 17 Apr 2021 03:45:45 +0100 Subject: [PATCH] More properties of absolute value in Data.Rational (#1477) --- CHANGELOG.md | 14 +++++++-- src/Data/Rational/Properties.agda | 19 ++++++++---- .../Rational/Unnormalised/Properties.agda | 30 +++++++++++++++++++ 3 files changed, 56 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7acb73568c..7562b48645 100644 --- 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 index c6923d0f97..b63b6de120 100644 --- 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 index 155b9f6d13..19078094ed 100644 --- 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