From f2fb18c97beecf1effb848de4e72d8ed6bb46aca Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 14 Oct 2024 10:10:59 +0200 Subject: [PATCH 1/3] Add lemmas relating Positive etc to addition for rationals --- CHANGELOG.md | 12 ++++++++++++ src/Data/Rational/Properties.agda | 24 ++++++++++++++++++++++++ 2 files changed, 36 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ea407ce874..fd01a4fde4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -316,6 +316,18 @@ Additions to existing modules m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n ``` +* New lemmas in `Data.Rational.Properties`: + ```agda + nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q) + nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q) + pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q) + nonNeg+pos⇒pos : ∀ p .{{_ : NonNegative p}} q .{{_ : Positive q}} → Positive (p + q) + pos+pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p + q) + neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q) + nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q) + neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q) + ``` + * New lemma in `Data.Vec.Properties`: ```agda map-concat : map f (concat xss) ≡ concat (map (map f) xss) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index fb186be08d..da28fc602e 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -1012,6 +1012,12 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ +-monoʳ-≤ : ∀ r → (_+_ r) Preserves _≤_ ⟶ _≤_ +-monoʳ-≤ r p≤q = +-mono-≤ (≤-refl {r}) p≤q +nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q) +nonNeg+nonNeg⇒nonNeg p q = nonNegative $ +-mono-≤ (nonNegative⁻¹ p) (nonNegative⁻¹ q) + +nonPos+nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonPositive (p + q) +nonPos+nonPos⇒nonPos p q = nonPositive $ +-mono-≤ (nonPositive⁻¹ p) (nonPositive⁻¹ q) + ------------------------------------------------------------------------ -- Properties of _+_ and _<_ @@ -1035,6 +1041,24 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ +-monoʳ-< : ∀ r → (_+_ r) Preserves _<_ ⟶ _<_ +-monoʳ-< r p Date: Mon, 14 Oct 2024 10:34:40 +0200 Subject: [PATCH 2/3] Add lemmas relating Positive etc to multiplication for rationals --- CHANGELOG.md | 8 +++++ src/Data/Rational/Properties.agda | 56 +++++++++++++++++++++++++++++++ 2 files changed, 64 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index fd01a4fde4..0e62daa5ac 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -326,6 +326,14 @@ Additions to existing modules neg+nonPos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : NonPositive q}} → Negative (p + q) nonPos+neg⇒neg : ∀ p .{{_ : NonPositive p}} q .{{_ : Negative q}} → Negative (p + q) neg+neg⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Negative (p + q) + nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q) + nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q) + nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q) + nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q) + pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q) + neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q) + pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q) + neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q) ``` * New lemma in `Data.Vec.Properties`: diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index da28fc602e..c4a7c6c26e 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -1364,6 +1364,34 @@ module _ where *-cancelˡ-≤-neg : ∀ r .{{_ : Negative r}} → r * p ≤ r * q → p ≥ q *-cancelˡ-≤-neg {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-neg r +nonNeg*nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p * q) +nonNeg*nonNeg⇒nonNeg p q = nonNegative $ begin + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ ≤⟨ *-monoˡ-≤-nonNeg p (nonNegative⁻¹ q) ⟩ + p * q ∎ + where open ≤-Reasoning + +nonPos*nonNeg⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonNegative q}} → NonPositive (p * q) +nonPos*nonNeg⇒nonPos p q = nonPositive $ begin + p * q ≤⟨ *-monoˡ-≤-nonPos p (nonNegative⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +nonNeg*nonPos⇒nonPos : ∀ p .{{_ : NonNegative p}} q .{{_ : NonPositive q}} → NonPositive (p * q) +nonNeg*nonPos⇒nonPos p q = nonPositive $ begin + p * q ≤⟨ *-monoˡ-≤-nonNeg p (nonPositive⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q) +nonPos*nonPos⇒nonPos p q = nonNegative $ begin + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ ≤⟨ *-monoˡ-≤-nonPos p (nonPositive⁻¹ q) ⟩ + p * q ∎ + where open ≤-Reasoning + ------------------------------------------------------------------------ -- Properties of _*_ and _<_ @@ -1411,6 +1439,34 @@ module _ where *-cancelʳ-<-nonPos : ∀ r .{{_ : NonPositive r}} → p * r < q * r → p > q *-cancelʳ-<-nonPos {p} {q} r rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonPos r +pos*pos⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : Positive q}} → Positive (p * q) +pos*pos⇒pos p q = positive $ begin-strict + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ <⟨ *-monoʳ-<-pos p (positive⁻¹ q) ⟩ + p * q ∎ + where open ≤-Reasoning + +neg*pos⇒neg : ∀ p .{{_ : Negative p}} q .{{_ : Positive q}} → Negative (p * q) +neg*pos⇒neg p q = negative $ begin-strict + p * q <⟨ *-monoʳ-<-neg p (positive⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +pos*neg⇒neg : ∀ p .{{_ : Positive p}} q .{{_ : Negative q}} → Negative (p * q) +pos*neg⇒neg p q = negative $ begin-strict + p * q <⟨ *-monoʳ-<-pos p (negative⁻¹ q) ⟩ + p * 0ℚ ≡⟨ *-zeroʳ p ⟩ + 0ℚ ∎ + where open ≤-Reasoning + +neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q) +neg*neg⇒pos p q = positive $ begin-strict + 0ℚ ≡⟨ *-zeroʳ p ⟨ + p * 0ℚ <⟨ {!*-monoʳ-<-neg p (negative⁻¹ q)!} ⟩ + p * q ∎ + where open ≤-Reasoning + ------------------------------------------------------------------------ -- Properties of _⊓_ ------------------------------------------------------------------------ From a2d078122ebf9f84c0fdb2a7e93ea6131b0f21b3 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 14 Oct 2024 10:49:14 +0200 Subject: [PATCH 3/3] Actually save filling last hole Whoops --- src/Data/Rational/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index c4a7c6c26e..0341f53c45 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -1463,7 +1463,7 @@ pos*neg⇒neg p q = negative $ begin-strict neg*neg⇒pos : ∀ p .{{_ : Negative p}} q .{{_ : Negative q}} → Positive (p * q) neg*neg⇒pos p q = positive $ begin-strict 0ℚ ≡⟨ *-zeroʳ p ⟨ - p * 0ℚ <⟨ {!*-monoʳ-<-neg p (negative⁻¹ q)!} ⟩ + p * 0ℚ <⟨ *-monoʳ-<-neg p (negative⁻¹ q) ⟩ p * q ∎ where open ≤-Reasoning