From 97e43f5309081235c91b6f37d9c9f69303ece0f8 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 26 Feb 2025 15:54:24 -0800 Subject: [PATCH 01/14] Multiplication of closed intervals on the rational numbers --- ...closed-intervals-rational-numbers.lagda.md | 169 +++++++++++ .../inequality-integer-fractions.lagda.md | 16 ++ .../inequality-integers.lagda.md | 11 + .../inequality-rational-numbers.lagda.md | 12 + .../integer-fractions.lagda.md | 8 + .../maximum-rational-numbers.lagda.md | 112 ++++++++ .../minimum-rational-numbers.lagda.md | 112 ++++++++ ...on-positive-and-negative-integers.lagda.md | 30 ++ .../negative-integer-fractions.lagda.md | 139 +++++++++ .../negative-rational-numbers.lagda.md | 269 ++++++++++++++++++ .../positive-and-negative-integers.lagda.md | 9 + .../positive-rational-numbers.lagda.md | 122 +++++++- .../decidable-total-orders.lagda.md | 50 ++++ 13 files changed, 1055 insertions(+), 4 deletions(-) create mode 100644 src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/maximum-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/minimum-rational-numbers.lagda.md create mode 100644 src/elementary-number-theory/negative-integer-fractions.lagda.md create mode 100644 src/elementary-number-theory/negative-rational-numbers.lagda.md diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md new file mode 100644 index 0000000000..6426b31bc7 --- /dev/null +++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md @@ -0,0 +1,169 @@ +# Closed intervals of rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.closed-intervals-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.decidable-total-order-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.maximum-rational-numbers +open import elementary-number-theory.minimum-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.negative-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels +``` + +
+ +## Idea + +A [rational number](elementary-number-theory.rational-numbers.md) `p` is in a +{{#concept "closed interval" Disambiguation="rational numbers" WDID=Q78240777 WD="closed interval"}} +`[q , r]` if `q` is +[less than or equal to](elementary-number-theory.inequality-rational-numbers.md) +`p` and `p` is less than or equal to `r`. + +## Definition + +```agda +module _ + (p q : ℚ) + where + + closed-interval-ℚ : subtype lzero ℚ + closed-interval-ℚ r = leq-ℚ-Prop p r ∧ leq-ℚ-Prop r q + + is-in-closed-interval-ℚ : ℚ → UU lzero + is-in-closed-interval-ℚ r = type-Prop (closed-interval-ℚ r) + +unordered-closed-interval-ℚ : ℚ → ℚ → subtype lzero ℚ +unordered-closed-interval-ℚ p q = closed-interval-ℚ (min-ℚ p q) (max-ℚ p q) + +is-in-unordered-closed-interval-ℚ : ℚ → ℚ → ℚ → UU lzero +is-in-unordered-closed-interval-ℚ p q = + is-in-closed-interval-ℚ (min-ℚ p q) (max-ℚ p q) +``` + +## Properties + +### Multiplication of elements in a closed interval + +```agda +abstract + left-mul-closed-interval-ℚ : (p q r s : ℚ) → is-in-closed-interval-ℚ p q r → + is-in-unordered-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s) + left-mul-closed-interval-ℚ p q r s (p≤r , r≤q) = + let + p≤q = transitive-leq-ℚ p r q r≤q p≤r + in + trichotomy-le-ℚ + ( s) + ( zero-ℚ) + ( λ s<0 → + let + s⁻ = s , is-negative-le-zero-ℚ s s<0 + rs≤ps = reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r + qs≤ps = reverses-leq-right-mul-ℚ⁻ s⁻ p q p≤q + qs≤rs = reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q + min=qs = right-leq-left-min-ℚ (p *ℚ s) (q *ℚ s) qs≤ps + max=ps = right-leq-left-max-ℚ (p *ℚ s) (q *ℚ s) qs≤ps + in + inv-tr (λ t → leq-ℚ t (r *ℚ s)) min=qs qs≤rs , + inv-tr (leq-ℚ (r *ℚ s)) max=ps rs≤ps) + ( λ s=0 → + let + ps=0 = ap (p *ℚ_) s=0 ∙ right-zero-law-mul-ℚ p + rs=0 = ap (r *ℚ_) s=0 ∙ right-zero-law-mul-ℚ r + qs=0 = ap (q *ℚ_) s=0 ∙ right-zero-law-mul-ℚ q + min=0 = ap-binary min-ℚ ps=0 qs=0 ∙ idempotent-min-ℚ zero-ℚ + max=0 = ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ + in leq-eq-ℚ _ _ (min=0 ∙ inv rs=0) , leq-eq-ℚ _ _ (rs=0 ∙ inv max=0)) + ( λ 0Imports + +```agda +open import elementary-number-theory.decidable-total-order-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.coproduct-types +open import foundation.identity-types +open import foundation.transport-along-identifications + +open import order-theory.decidable-total-orders +``` + + + +## Idea + +We define the operation of maximum +([least upper bound](order-theory.least-upper-bounds-posets.md)) for the +[rational numbers](elementary-number-theory.rational-numbers.md). + +## Definition + +```agda +max-ℚ : ℚ → ℚ → ℚ +max-ℚ = max-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +## Properties + +### Associativity of `max-ℚ` + +```agda +associative-max-ℚ : (x y z : ℚ) → max-ℚ (max-ℚ x y) z ＝ max-ℚ x (max-ℚ y z) +associative-max-ℚ = + associative-max-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### Commutativity of `max-ℚ` + +```agda +commutative-max-ℚ : (x y : ℚ) → max-ℚ x y ＝ max-ℚ y x +commutative-max-ℚ = + commutative-max-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### `max-ℚ` is idempotent + +```agda +idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x +idempotent-max-ℚ = + idempotent-max-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### The maximum is an upper bound + +```agda +leq-left-max-ℚ : (x y : ℚ) → x ≤-ℚ max-ℚ x y +leq-left-max-ℚ = leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order + +leq-right-max-ℚ : (x y : ℚ) → y ≤-ℚ max-ℚ x y +leq-right-max-ℚ = leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### If `a ≤ b`, `max a b = b` + +```agda +left-leq-right-max-ℚ : (x y : ℚ) → leq-ℚ x y → max-ℚ x y ＝ y +left-leq-right-max-ℚ = + left-leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order + +right-leq-left-max-ℚ : (x y : ℚ) → leq-ℚ y x → max-ℚ x y ＝ x +right-leq-left-max-ℚ = + right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### If both `x` and `y` are less than `z`, so is their maximum + +```agda +le-max-le-both-ℚ : (z x y : ℚ) → le-ℚ x z → le-ℚ y z → le-ℚ (max-ℚ x y) z +le-max-le-both-ℚ z x y xImports + +```agda +open import elementary-number-theory.decidable-total-order-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.coproduct-types +open import foundation.identity-types +open import foundation.transport-along-identifications + +open import order-theory.decidable-total-orders +``` + + + +## Idea + +We define the operation of minimum +([greatest lower bound](order-theory.greatest-lower-bounds-posets.md)) for the +[rational numbers](elementary-number-theory.rational-numbers.md). + +## Definition + +```agda +min-ℚ : ℚ → ℚ → ℚ +min-ℚ = min-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +## Properties + +### Associativity of `min-ℚ` + +```agda +associative-min-ℚ : (x y z : ℚ) → min-ℚ (min-ℚ x y) z ＝ min-ℚ x (min-ℚ y z) +associative-min-ℚ = + associative-min-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### Commutativity of `min-ℚ` + +```agda +commutative-min-ℚ : (x y : ℚ) → min-ℚ x y ＝ min-ℚ y x +commutative-min-ℚ = + commutative-min-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### `min-ℚ` is idempotent + +```agda +idempotent-min-ℚ : (x : ℚ) → min-ℚ x x ＝ x +idempotent-min-ℚ = + idempotent-min-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### The minimum is a lower bound + +```agda +leq-left-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ x +leq-left-min-ℚ = leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order + +leq-right-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ y +leq-right-min-ℚ = leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### If `a ≤ b`, `min a b = a` + +```agda +left-leq-right-min-ℚ : (x y : ℚ) → leq-ℚ x y → min-ℚ x y ＝ x +left-leq-right-min-ℚ = + left-leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order + +right-leq-left-min-ℚ : (x y : ℚ) → leq-ℚ y x → min-ℚ x y ＝ y +right-leq-left-min-ℚ = + right-leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order +``` + +### If `z` is less than both `x` and `y`, it is less than their minimum + +```agda +le-min-le-both-ℚ : (z x y : ℚ) → le-ℚ z x → le-ℚ z y → le-ℚ z (min-ℚ x y) +le-min-le-both-ℚ z x y zImports + +```agda +open import elementary-number-theory.addition-integer-fractions +open import elementary-number-theory.addition-positive-and-negative-integers +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-integer-fractions +open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers +open import elementary-number-theory.negative-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integer-fractions +open import elementary-number-theory.positive-integers +open import elementary-number-theory.reduced-integer-fractions + +open import foundation.identity-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels +``` + + + +## Idea + +An [integer fraction](elementary-number-theory.integer-fractions.md) `x` is said +to be +{{#concept "negative" Disambiguation="integer fraction" Agda=is-negative-fraction-ℤ}} +if its numerator is a +[negative integer](elementary-number-theory.negative-integers.md). + +## Definitions + +### The property of being a negative integer fraction + +```agda +module _ + (x : fraction-ℤ) + where + + is-negative-fraction-ℤ : UU lzero + is-negative-fraction-ℤ = is-negative-ℤ (numerator-fraction-ℤ x) + + is-prop-is-negative-fraction-ℤ : is-prop is-negative-fraction-ℤ + is-prop-is-negative-fraction-ℤ = + is-prop-is-negative-ℤ (numerator-fraction-ℤ x) +``` + +## Properties + +### The negative of a positive integer fraction is negative + +```agda +abstract + is-negative-neg-positive-fraction-ℤ : + (x : fraction-ℤ) → is-positive-fraction-ℤ x → + is-negative-fraction-ℤ (neg-fraction-ℤ x) + is-negative-neg-positive-fraction-ℤ _ = is-negative-neg-is-positive-ℤ +``` + +### The negative of a negative integer fraction is positive + +```agda +abstract + is-positive-neg-negative-fraction-ℤ : + (x : fraction-ℤ) → is-negative-fraction-ℤ x → + is-positive-fraction-ℤ (neg-fraction-ℤ x) + is-positive-neg-negative-fraction-ℤ _ = is-positive-neg-is-negative-ℤ +``` + +### An integer fraction similar to a negative integer fraction is negative + +```agda +is-negative-sim-fraction-ℤ : + (x y : fraction-ℤ) (S : sim-fraction-ℤ x y) → + is-negative-fraction-ℤ x → + is-negative-fraction-ℤ y +is-negative-sim-fraction-ℤ x y S N = + is-negative-right-factor-mul-positive-ℤ + ( is-negative-eq-ℤ + ( S ∙ + commutative-mul-ℤ (numerator-fraction-ℤ y) (denominator-fraction-ℤ x)) + ( is-negative-mul-negative-positive-ℤ + ( N) + ( is-positive-denominator-fraction-ℤ y))) + ( is-positive-denominator-fraction-ℤ x) +``` + +### The reduced fraction of a negative integer fraction is negative + +```agda +is-negative-reduce-fraction-ℤ : + {x : fraction-ℤ} (P : is-negative-fraction-ℤ x) → + is-negative-fraction-ℤ (reduce-fraction-ℤ x) +is-negative-reduce-fraction-ℤ {x} = + is-negative-sim-fraction-ℤ + ( x) + ( reduce-fraction-ℤ x) + ( sim-reduced-fraction-ℤ x) +``` + +### The sum of two negative integer fractions is negative + +```agda +is-negative-add-fraction-ℤ : + {x y : fraction-ℤ} → + is-negative-fraction-ℤ x → + is-negative-fraction-ℤ y → + is-negative-fraction-ℤ (add-fraction-ℤ x y) +is-negative-add-fraction-ℤ {x} {y} P Q = + is-negative-add-ℤ + ( is-negative-mul-negative-positive-ℤ + ( P) + ( is-positive-denominator-fraction-ℤ y)) + ( is-negative-mul-negative-positive-ℤ + ( Q) + ( is-positive-denominator-fraction-ℤ x)) +``` + +### The product of two negative integer fractions is positive + +```agda +is-positive-mul-negative-fraction-ℤ : + {x y : fraction-ℤ} → + is-negative-fraction-ℤ x → + is-negative-fraction-ℤ y → + is-positive-fraction-ℤ (mul-fraction-ℤ x y) +is-positive-mul-negative-fraction-ℤ = is-positive-mul-negative-ℤ +``` diff --git a/src/elementary-number-theory/negative-rational-numbers.lagda.md b/src/elementary-number-theory/negative-rational-numbers.lagda.md new file mode 100644 index 0000000000..8691d5ed71 --- /dev/null +++ b/src/elementary-number-theory/negative-rational-numbers.lagda.md @@ -0,0 +1,269 @@ +# Negative rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.negative-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.negative-integer-fractions +open import elementary-number-theory.negative-integers +open import elementary-number-theory.nonzero-rational-numbers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integer-fractions +open import elementary-number-theory.positive-integers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels +``` + +
+ +## Idea + +A [rational number](elementary-number-theory.rational-numbers.md) `x` is said to +be {{#concept "negative" Disambiguation="rational number" Agda=is-negative-ℚ}} +if its negation is positive. + +Negative rational numbers are a [subsemigroup](group-theory.subsemigroups.md) of +the +[additive monoid of rational numbers](elementary-number-theory.additive-group-of-rational-numbers.md). + +## Definitions + +### The property of being a negative rational number + +```agda +module _ + (q : ℚ) + where + + is-negative-ℚ : UU lzero + is-negative-ℚ = is-positive-ℚ (neg-ℚ q) + + is-prop-is-negative-ℚ : is-prop is-negative-ℚ + is-prop-is-negative-ℚ = is-prop-is-positive-ℚ (neg-ℚ q) + + is-negative-prop-ℚ : Prop lzero + pr1 is-negative-prop-ℚ = is-negative-ℚ + pr2 is-negative-prop-ℚ = is-prop-is-negative-ℚ +``` + +### The type of negative rational numbers + +```agda +negative-ℚ : UU lzero +negative-ℚ = type-subtype is-negative-prop-ℚ + +ℚ⁻ : UU lzero +ℚ⁻ = negative-ℚ + +module _ + (x : negative-ℚ) + where + + rational-ℚ⁻ : ℚ + rational-ℚ⁻ = pr1 x + + fraction-ℚ⁻ : fraction-ℤ + fraction-ℚ⁻ = fraction-ℚ rational-ℚ⁻ + + numerator-ℚ⁻ : ℤ + numerator-ℚ⁻ = numerator-ℚ rational-ℚ⁻ + + denominator-ℚ⁻ : ℤ + denominator-ℚ⁻ = denominator-ℚ rational-ℚ⁻ + + is-negative-rational-ℚ⁻ : is-negative-ℚ rational-ℚ⁻ + is-negative-rational-ℚ⁻ = pr2 x + + is-negative-fraction-ℚ⁻ : is-negative-fraction-ℤ fraction-ℚ⁻ + is-negative-fraction-ℚ⁻ = + tr + ( is-negative-fraction-ℤ) + ( neg-neg-fraction-ℤ fraction-ℚ⁻) + ( is-negative-neg-positive-fraction-ℤ + ( neg-fraction-ℤ fraction-ℚ⁻) + ( is-negative-rational-ℚ⁻)) + + is-negative-numerator-ℚ⁻ : is-negative-ℤ numerator-ℚ⁻ + is-negative-numerator-ℚ⁻ = is-negative-fraction-ℚ⁻ + + is-positive-denominator-ℚ⁻ : is-positive-ℤ denominator-ℚ⁻ + is-positive-denominator-ℚ⁻ = is-positive-denominator-ℚ rational-ℚ⁻ + + neg-ℚ⁻ : ℚ⁺ + neg-ℚ⁻ = (neg-ℚ rational-ℚ⁻) , is-negative-rational-ℚ⁻ + +neg-ℚ⁺ : ℚ⁺ → ℚ⁻ +neg-ℚ⁺ (q , q-is-pos) = neg-ℚ q , inv-tr is-positive-ℚ (neg-neg-ℚ q) q-is-pos + +abstract + eq-ℚ⁻ : {x y : ℚ⁻} → rational-ℚ⁻ x ＝ rational-ℚ⁻ y → x ＝ y + eq-ℚ⁻ {x} {y} = eq-type-subtype is-negative-prop-ℚ +``` + +## Properties + +### The negative rational numbers form a set + +```agda +is-set-ℚ⁻ : is-set ℚ⁻ +is-set-ℚ⁻ = is-set-type-subtype is-negative-prop-ℚ is-set-ℚ +``` + +### The rational image of a negative integer is negative + +```agda +abstract + is-negative-rational-ℤ : + (x : ℤ) → is-negative-ℤ x → is-negative-ℚ (rational-ℤ x) + is-negative-rational-ℤ _ = is-positive-neg-is-negative-ℤ + +negative-rational-negative-ℤ : negative-ℤ → ℚ⁻ +negative-rational-negative-ℤ (x , x-is-neg) = + rational-ℤ x , is-negative-rational-ℤ x x-is-neg +``` + +### The rational image of a negative integer fraction is negative + +```agda +abstract + is-negative-rational-fraction-ℤ : + {x : fraction-ℤ} (P : is-negative-fraction-ℤ x) → + is-negative-ℚ (rational-fraction-ℤ x) + is-negative-rational-fraction-ℤ P = + is-positive-neg-is-negative-ℤ (is-negative-reduce-fraction-ℤ P) +``` + +### A rational number `x` is negative if and only if `x < 0` + +```agda +module _ + (x : ℚ) + where + + abstract + le-zero-is-negative-ℚ : is-negative-ℚ x → le-ℚ x zero-ℚ + le-zero-is-negative-ℚ x-is-neg = + tr + ( λ y → le-ℚ y zero-ℚ) + ( neg-neg-ℚ x) + ( neg-le-ℚ zero-ℚ (neg-ℚ x) (le-zero-is-positive-ℚ (neg-ℚ x) x-is-neg)) + + is-negative-le-zero-ℚ : le-ℚ x zero-ℚ → is-negative-ℚ x + is-negative-le-zero-ℚ x-is-neg = + is-positive-le-zero-ℚ (neg-ℚ x) (neg-le-ℚ x zero-ℚ x-is-neg) + + is-negative-iff-le-zero-ℚ : is-negative-ℚ x ↔ le-ℚ x zero-ℚ + is-negative-iff-le-zero-ℚ = + le-zero-is-negative-ℚ , + is-negative-le-zero-ℚ +``` + +### The difference of a rational number with a greater rational number is negative + +```agda +module _ + (x y : ℚ) (H : le-ℚ x y) + where + + abstract + is-negative-diff-le-ℚ : is-negative-ℚ (x -ℚ y) + is-negative-diff-le-ℚ = + inv-tr + ( is-positive-ℚ) + ( distributive-neg-diff-ℚ x y) + ( is-positive-diff-le-ℚ x y H) + + negative-diff-le-ℚ : ℚ⁻ + negative-diff-le-ℚ = x -ℚ y , is-negative-diff-le-ℚ +``` + +### Negative rational numbers are nonzero + +```agda +abstract + is-nonzero-is-negative-ℚ : {x : ℚ} → is-negative-ℚ x → is-nonzero-ℚ x + is-nonzero-is-negative-ℚ {x} H = + tr + ( is-nonzero-ℚ) + ( neg-neg-ℚ x) + ( is-nonzero-neg-ℚ (is-nonzero-is-positive-ℚ H)) +``` + +### The product of two negative rational numbers is positive + +```agda + is-positive-mul-negative-ℚ : + {x y : ℚ} → is-negative-ℚ x → is-negative-ℚ y → is-positive-ℚ (x *ℚ y) + is-positive-mul-negative-ℚ {x} {y} P Q = + is-positive-reduce-fraction-ℤ + ( is-positive-mul-negative-fraction-ℤ + { fraction-ℚ x} + { fraction-ℚ y} + ( is-negative-fraction-ℚ⁻ (x , P)) + ( is-negative-fraction-ℚ⁻ (y , Q))) +``` + +### Multiplication by a negative rational number reverses inequality + +```agda +module _ + (p : ℚ⁻) + (q r : ℚ) + (H : leq-ℚ q r) + where + + reverses-leq-right-mul-ℚ⁻ : leq-ℚ (r *ℚ rational-ℚ⁻ p) (q *ℚ rational-ℚ⁻ p) + reverses-leq-right-mul-ℚ⁻ = + binary-tr + ( leq-ℚ) + ( negative-law-mul-ℚ r (rational-ℚ⁻ p)) + ( negative-law-mul-ℚ q (rational-ℚ⁻ p)) + ( preserves-leq-right-mul-ℚ⁺ + ( neg-ℚ⁻ p) + ( neg-ℚ r) + ( neg-ℚ q) + ( neg-leq-ℚ q r H)) +``` + +### Multiplication by a negative rational number reverses strict inequality + +```agda +module _ + (p : ℚ⁻) + (q r : ℚ) + (H : le-ℚ q r) + where + + reverses-le-right-mul-ℚ⁻ : le-ℚ (r *ℚ rational-ℚ⁻ p) (q *ℚ rational-ℚ⁻ p) + reverses-le-right-mul-ℚ⁻ = + binary-tr + ( le-ℚ) + ( negative-law-mul-ℚ r (rational-ℚ⁻ p)) + ( negative-law-mul-ℚ q (rational-ℚ⁻ p)) + ( preserves-le-right-mul-ℚ⁺ + ( neg-ℚ⁻ p) + ( neg-ℚ r) + ( neg-ℚ q) + ( neg-le-ℚ q r H)) +``` diff --git a/src/elementary-number-theory/positive-and-negative-integers.lagda.md b/src/elementary-number-theory/positive-and-negative-integers.lagda.md index 844b95a8b8..9f35831163 100644 --- a/src/elementary-number-theory/positive-and-negative-integers.lagda.md +++ b/src/elementary-number-theory/positive-and-negative-integers.lagda.md @@ -51,6 +51,15 @@ is-not-negative-and-positive-ℤ (inl x) (H , K) = K is-not-negative-and-positive-ℤ (inr x) (H , K) = H ``` +### No integer is both nonnegative and negative + +```agda +is-not-negative-and-nonnegative-ℤ : + (x : ℤ) → ¬ (is-negative-ℤ x × is-nonnegative-ℤ x) +is-not-negative-and-nonnegative-ℤ (inl x) (H , K) = K +is-not-negative-and-nonnegative-ℤ (inr x) (H , K) = H +``` + ### Dichotomies #### A nonzero integer is either negative or positive diff --git a/src/elementary-number-theory/positive-rational-numbers.lagda.md b/src/elementary-number-theory/positive-rational-numbers.lagda.md index 63ae446cfa..6ad222c781 100644 --- a/src/elementary-number-theory/positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-rational-numbers.lagda.md @@ -14,11 +14,13 @@ open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.cross-multiplication-difference-integer-fractions open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.inequality-integers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integer-fractions open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.multiplicative-inverses-positive-integer-fractions open import elementary-number-theory.multiplicative-monoid-of-rational-numbers @@ -29,9 +31,11 @@ open import elementary-number-theory.positive-integer-fractions open import elementary-number-theory.positive-integers open import elementary-number-theory.rational-numbers open import elementary-number-theory.reduced-integer-fractions +open import elementary-number-theory.strict-inequality-integers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions +open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.coproduct-types open import foundation.dependent-pair-types @@ -152,8 +156,11 @@ abstract (x : ℤ) → is-positive-ℤ x → is-positive-ℚ (rational-ℤ x) is-positive-rational-ℤ x P = P +positive-rational-positive-ℤ : positive-ℤ → ℚ⁺ +positive-rational-positive-ℤ (z , pos-z) = rational-ℤ z , pos-z + one-ℚ⁺ : ℚ⁺ -one-ℚ⁺ = (one-ℚ , is-positive-int-positive-ℤ one-positive-ℤ) +one-ℚ⁺ = positive-rational-positive-ℤ one-positive-ℤ ``` ### The rational image of a positive integer fraction is positive @@ -453,6 +460,19 @@ is-prop-le-ℚ⁺ : (x y : ℚ⁺) → is-prop (le-ℚ⁺ x y) is-prop-le-ℚ⁺ x y = is-prop-type-Prop (le-prop-ℚ⁺ x y) ``` +### The inequality on positive rational numbers + +```agda +leq-prop-ℚ⁺ : ℚ⁺ → ℚ⁺ → Prop lzero +leq-prop-ℚ⁺ x y = leq-ℚ-Prop (rational-ℚ⁺ x) (rational-ℚ⁺ y) + +leq-ℚ⁺ : ℚ⁺ → ℚ⁺ → UU lzero +leq-ℚ⁺ x y = type-Prop (leq-prop-ℚ⁺ x y) + +is-prop-leq-ℚ⁺ : (x y : ℚ⁺) → is-prop (leq-ℚ⁺ x y) +is-prop-leq-ℚ⁺ x y = is-prop-type-Prop (leq-prop-ℚ⁺ x y) +``` + ### The sum of two positive rational numbers is greater than each of them ```agda @@ -526,6 +546,95 @@ module _ ( left-diff-law-add-ℚ⁺) ``` +### Multiplication by a positive rational number preserves strict inequality + +```agda +preserves-le-left-mul-ℚ⁺ : + (p : ℚ⁺) (q r : ℚ) → le-ℚ q r → le-ℚ (rational-ℚ⁺ p *ℚ q) (rational-ℚ⁺ p *ℚ r) +preserves-le-left-mul-ℚ⁺ + p⁺@((p@(p-num , p-denom , p-denom-pos) , _) , p-num-pos) + q@((q-num , q-denom , _) , _) + r@((r-num , r-denom , _) , _) + q Date: Wed, 26 Feb 2025 15:54:53 -0800 Subject: [PATCH 02/14] make pre-commit --- src/elementary-number-theory.lagda.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 8c83736e27..d57f6dc233 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -32,6 +32,7 @@ open import elementary-number-theory.binomial-theorem-integers public open import elementary-number-theory.binomial-theorem-natural-numbers public open import elementary-number-theory.bounded-sums-arithmetic-functions public open import elementary-number-theory.catalan-numbers public +open import elementary-number-theory.closed-intervals-rational-numbers public open import elementary-number-theory.cofibonacci public open import elementary-number-theory.collatz-bijection public open import elementary-number-theory.collatz-conjecture public @@ -95,10 +96,12 @@ open import elementary-number-theory.kolakoski-sequence public open import elementary-number-theory.legendre-symbol public open import elementary-number-theory.lower-bounds-natural-numbers public open import elementary-number-theory.maximum-natural-numbers public +open import elementary-number-theory.maximum-rational-numbers public open import elementary-number-theory.maximum-standard-finite-types public open import elementary-number-theory.mediant-integer-fractions public open import elementary-number-theory.mersenne-primes public open import elementary-number-theory.minimum-natural-numbers public +open import elementary-number-theory.minimum-rational-numbers public open import elementary-number-theory.minimum-standard-finite-types public open import elementary-number-theory.modular-arithmetic public open import elementary-number-theory.modular-arithmetic-standard-finite-types public @@ -119,7 +122,9 @@ open import elementary-number-theory.multiplicative-units-integers public open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public open import elementary-number-theory.multiset-coefficients public open import elementary-number-theory.natural-numbers public +open import elementary-number-theory.negative-integer-fractions public open import elementary-number-theory.negative-integers public +open import elementary-number-theory.negative-rational-numbers public open import elementary-number-theory.nonnegative-integers public open import elementary-number-theory.nonpositive-integers public open import elementary-number-theory.nonzero-integers public From fa9738ac79bace8da0dd4d3f7d162e6bc053f7c3 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 28 Feb 2025 07:50:58 -0800 Subject: [PATCH 03/14] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- .../closed-intervals-rational-numbers.lagda.md | 2 +- .../maximum-rational-numbers.lagda.md | 10 +++++----- .../minimum-rational-numbers.lagda.md | 10 +++++----- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md index 6426b31bc7..52d17c7750 100644 --- a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md @@ -36,7 +36,7 @@ open import foundation.universe-levels ## Idea A [rational number](elementary-number-theory.rational-numbers.md) `p` is in a -{{#concept "closed interval" Disambiguation="rational numbers" WDID=Q78240777 WD="closed interval"}} +{{#concept "closed interval" Disambiguation="rational numbers" WDID=Q78240777 WD="closed interval" Agda=closed-interval-ℚ}} `[q , r]` if `q` is [less than or equal to](elementary-number-theory.inequality-rational-numbers.md) `p` and `p` is less than or equal to `r`. diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md index 162f9f8f61..550ce9fa47 100644 --- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md @@ -23,7 +23,7 @@ open import order-theory.decidable-total-orders ## Idea -We define the operation of maximum +We define the operation of {{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}} ([least upper bound](order-theory.least-upper-bounds-posets.md)) for the [rational numbers](elementary-number-theory.rational-numbers.md). @@ -36,7 +36,7 @@ max-ℚ = max-Decidable-Total-Order ℚ-Decidable-Total-Order ## Properties -### Associativity of `max-ℚ` +### Associativity of the maximum operation ```agda associative-max-ℚ : (x y z : ℚ) → max-ℚ (max-ℚ x y) z ＝ max-ℚ x (max-ℚ y z) @@ -44,7 +44,7 @@ associative-max-ℚ = associative-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` -### Commutativity of `max-ℚ` +### Commutativity of the maximum operation ```agda commutative-max-ℚ : (x y : ℚ) → max-ℚ x y ＝ max-ℚ y x @@ -52,7 +52,7 @@ commutative-max-ℚ = commutative-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` -### `max-ℚ` is idempotent +### The maximum operation is idempotent ```agda idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x @@ -70,7 +70,7 @@ leq-right-max-ℚ : (x y : ℚ) → y ≤-ℚ max-ℚ x y leq-right-max-ℚ = leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` -### If `a ≤ b`, `max a b = b` +### If `a` is less than or equal to `b`, then the maximum of `a` and `b` is `b` ```agda left-leq-right-max-ℚ : (x y : ℚ) → leq-ℚ x y → max-ℚ x y ＝ y diff --git a/src/elementary-number-theory/minimum-rational-numbers.lagda.md b/src/elementary-number-theory/minimum-rational-numbers.lagda.md index 442fc1e1a8..3a811bb795 100644 --- a/src/elementary-number-theory/minimum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/minimum-rational-numbers.lagda.md @@ -23,7 +23,7 @@ open import order-theory.decidable-total-orders ## Idea -We define the operation of minimum +We define the operation of {{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}} ([greatest lower bound](order-theory.greatest-lower-bounds-posets.md)) for the [rational numbers](elementary-number-theory.rational-numbers.md). @@ -36,7 +36,7 @@ min-ℚ = min-Decidable-Total-Order ℚ-Decidable-Total-Order ## Properties -### Associativity of `min-ℚ` +### Associativity of the minimum operation ```agda associative-min-ℚ : (x y z : ℚ) → min-ℚ (min-ℚ x y) z ＝ min-ℚ x (min-ℚ y z) @@ -44,7 +44,7 @@ associative-min-ℚ = associative-min-Decidable-Total-Order ℚ-Decidable-Total-Order ``` -### Commutativity of `min-ℚ` +### Commutativity of the minimum operation ```agda commutative-min-ℚ : (x y : ℚ) → min-ℚ x y ＝ min-ℚ y x @@ -52,7 +52,7 @@ commutative-min-ℚ = commutative-min-Decidable-Total-Order ℚ-Decidable-Total-Order ``` -### `min-ℚ` is idempotent +### The minimum operation is idempotent ```agda idempotent-min-ℚ : (x : ℚ) → min-ℚ x x ＝ x @@ -70,7 +70,7 @@ leq-right-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ y leq-right-min-ℚ = leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order ``` -### If `a ≤ b`, `min a b = a` +### If `a` is less than or equal to `b`, then the minimum of `a` and `b` is `a` ```agda left-leq-right-min-ℚ : (x y : ℚ) → leq-ℚ x y → min-ℚ x y ＝ x From 995cf33b42a1d68a61c0a15be7fccda650266ee4 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 16 Mar 2025 18:26:12 -0700 Subject: [PATCH 04/14] Fix merge --- .../positive-rational-numbers.lagda.md | 56 +------------------ 1 file changed, 1 insertion(+), 55 deletions(-) diff --git a/src/elementary-number-theory/positive-rational-numbers.lagda.md b/src/elementary-number-theory/positive-rational-numbers.lagda.md index ac26ec97ca..f65d527a96 100644 --- a/src/elementary-number-theory/positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-rational-numbers.lagda.md @@ -161,8 +161,7 @@ positive-rational-positive-ℤ : positive-ℤ → ℚ⁺ positive-rational-positive-ℤ (z , pos-z) = rational-ℤ z , pos-z one-ℚ⁺ : ℚ⁺ -one-ℚ⁺ = (one-ℚ , is-positive-int-po -sitive-ℤ one-positive-ℤ) +one-ℚ⁺ = (one-ℚ , is-positive-int-positive-ℤ one-positive-ℤ) ``` ### The rational image of a positive integer fraction is positive @@ -637,59 +636,6 @@ le-right-mul-less-than-one-ℚ⁺ p p<1 q = ( le-left-mul-less-than-one-ℚ⁺ p p<1 q) ``` -### Multiplication by a positive rational number preserves strict inequality - -```agda -preserves-le-left-mul-ℚ⁺ : - (p : ℚ⁺) (q r : ℚ) → le-ℚ q r → le-ℚ (rational-ℚ⁺ p *ℚ q) (rational-ℚ⁺ p *ℚ r) -preserves-le-left-mul-ℚ⁺ - p⁺@((p@(p-num , p-denom , p-denom-pos) , _) , p-num-pos) - q@((q-num , q-denom , _) , _) - r@((r-num , r-denom , _) , _) - q Date: Sun, 16 Mar 2025 19:02:12 -0700 Subject: [PATCH 05/14] Generalize functoriality of meets and joins --- .../decidable-total-orders.lagda.md | 30 ++------ src/order-theory/join-semilattices.lagda.md | 68 +++++++++++++++++++ src/order-theory/meet-semilattices.lagda.md | 66 ++++++++++++++++++ 3 files changed, 140 insertions(+), 24 deletions(-) diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md index 092fbd34b8..671f8a8d3d 100644 --- a/src/order-theory/decidable-total-orders.lagda.md +++ b/src/order-theory/decidable-total-orders.lagda.md @@ -487,18 +487,9 @@ module _ ( T) ( min-Decidable-Total-Order T a c) ( min-Decidable-Total-Order T b d) - min-leq-leq-Decidable-Total-Order a b c d a≤b c≤d - with is-leq-or-strict-greater-Decidable-Total-Order T a c - ... | inl a≤c = - forward-implication - ( min-is-greatest-binary-lower-bound-Decidable-Total-Order T b d a) - ( a≤b , - transitive-leq-Decidable-Total-Order T a c d c≤d a≤c) - ... | inr c Date: Sun, 16 Mar 2025 19:03:10 -0700 Subject: [PATCH 06/14] make pre-commit --- src/elementary-number-theory/maximum-rational-numbers.lagda.md | 3 ++- src/elementary-number-theory/minimum-rational-numbers.lagda.md | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md index 550ce9fa47..e8adbe5976 100644 --- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md @@ -23,7 +23,8 @@ open import order-theory.decidable-total-orders ## Idea -We define the operation of {{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}} +We define the operation of +{{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}} ([least upper bound](order-theory.least-upper-bounds-posets.md)) for the [rational numbers](elementary-number-theory.rational-numbers.md). diff --git a/src/elementary-number-theory/minimum-rational-numbers.lagda.md b/src/elementary-number-theory/minimum-rational-numbers.lagda.md index 3a811bb795..a60e03e357 100644 --- a/src/elementary-number-theory/minimum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/minimum-rational-numbers.lagda.md @@ -23,7 +23,8 @@ open import order-theory.decidable-total-orders ## Idea -We define the operation of {{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}} +We define the operation of +{{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}} ([greatest lower bound](order-theory.greatest-lower-bounds-posets.md)) for the [rational numbers](elementary-number-theory.rational-numbers.md). From 993f0c17fea593859d585ee97d56ec2085d7c202 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sun, 16 Mar 2025 19:25:22 -0700 Subject: [PATCH 07/14] Fix missing function --- .../positive-rational-numbers.lagda.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/elementary-number-theory/positive-rational-numbers.lagda.md b/src/elementary-number-theory/positive-rational-numbers.lagda.md index f65d527a96..04f5c23411 100644 --- a/src/elementary-number-theory/positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/positive-rational-numbers.lagda.md @@ -164,6 +164,13 @@ one-ℚ⁺ : ℚ⁺ one-ℚ⁺ = (one-ℚ , is-positive-int-positive-ℤ one-positive-ℤ) ``` +### The rational image of a positive natural number is positive + +```agda +positive-rational-ℕ⁺ : ℕ⁺ → ℚ⁺ +positive-rational-ℕ⁺ n = positive-rational-positive-ℤ (positive-int-ℕ⁺ n) +``` + ### The rational image of a positive integer fraction is positive ```agda From dda8a69ba4e7464257cfd272e0b578605c0184f5 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 22 Mar 2025 12:59:23 -0700 Subject: [PATCH 08/14] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- .../maximum-rational-numbers.lagda.md | 5 +---- .../minimum-rational-numbers.lagda.md | 5 +---- src/order-theory/decidable-total-orders.lagda.md | 4 ++-- 3 files changed, 4 insertions(+), 10 deletions(-) diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md index e8adbe5976..85c33d42de 100644 --- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md @@ -23,10 +23,7 @@ open import order-theory.decidable-total-orders ## Idea -We define the operation of -{{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}} -([least upper bound](order-theory.least-upper-bounds-posets.md)) for the -[rational numbers](elementary-number-theory.rational-numbers.md). +The {{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}} of two [rational numbers](elementary-number-theory.rational-numbers.md) is the [greatest](elementary-number-theory.inequality-rational-numbers.md) rational number of the two. This is the [binary least upper bound](order-theory.least-upper-bounds-posets.md) in the [total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md). ## Definition diff --git a/src/elementary-number-theory/minimum-rational-numbers.lagda.md b/src/elementary-number-theory/minimum-rational-numbers.lagda.md index a60e03e357..d2a3112329 100644 --- a/src/elementary-number-theory/minimum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/minimum-rational-numbers.lagda.md @@ -23,10 +23,7 @@ open import order-theory.decidable-total-orders ## Idea -We define the operation of -{{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}} -([greatest lower bound](order-theory.greatest-lower-bounds-posets.md)) for the -[rational numbers](elementary-number-theory.rational-numbers.md). +The {{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}} of two [rational numbers](elementary-number-theory.rational-numbers.md) is the [smallest](elementary-number-theory.inequality-rational-numbers.md) rational number of the two. This is the [binary greatest lower bound](order-theory.greatest-lower-bounds-posets.md) in the [total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md). ## Definition diff --git a/src/order-theory/decidable-total-orders.lagda.md b/src/order-theory/decidable-total-orders.lagda.md index 671f8a8d3d..2d8296df76 100644 --- a/src/order-theory/decidable-total-orders.lagda.md +++ b/src/order-theory/decidable-total-orders.lagda.md @@ -477,7 +477,7 @@ module _ ... | inr y Date: Sat, 22 Mar 2025 13:10:00 -0700 Subject: [PATCH 09/14] Progress --- ...closed-intervals-rational-numbers.lagda.md | 86 ++++++++++--------- 1 file changed, 45 insertions(+), 41 deletions(-) diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md index 52d17c7750..230b6445ed 100644 --- a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md @@ -80,33 +80,43 @@ abstract ( λ s<0 → let s⁻ = s , is-negative-le-zero-ℚ s s<0 - rs≤ps = reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r qs≤ps = reverses-leq-right-mul-ℚ⁻ s⁻ p q p≤q - qs≤rs = reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q - min=qs = right-leq-left-min-ℚ (p *ℚ s) (q *ℚ s) qs≤ps - max=ps = right-leq-left-max-ℚ (p *ℚ s) (q *ℚ s) qs≤ps in - inv-tr (λ t → leq-ℚ t (r *ℚ s)) min=qs qs≤rs , - inv-tr (leq-ℚ (r *ℚ s)) max=ps rs≤ps) + inv-tr + ( λ t → leq-ℚ t (r *ℚ s)) + ( right-leq-left-min-ℚ (p *ℚ s) (q *ℚ s) qs≤ps) + ( reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q) , + inv-tr + ( leq-ℚ (r *ℚ s)) + ( right-leq-left-max-ℚ (p *ℚ s) (q *ℚ s) qs≤ps) + ( reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r)) ( λ s=0 → let ps=0 = ap (p *ℚ_) s=0 ∙ right-zero-law-mul-ℚ p rs=0 = ap (r *ℚ_) s=0 ∙ right-zero-law-mul-ℚ r qs=0 = ap (q *ℚ_) s=0 ∙ right-zero-law-mul-ℚ q - min=0 = ap-binary min-ℚ ps=0 qs=0 ∙ idempotent-min-ℚ zero-ℚ - max=0 = ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ - in leq-eq-ℚ _ _ (min=0 ∙ inv rs=0) , leq-eq-ℚ _ _ (rs=0 ∙ inv max=0)) + in + leq-eq-ℚ + ( _) + ( _) + ( ap-binary min-ℚ ps=0 qs=0 ∙ + idempotent-min-ℚ zero-ℚ ∙ inv rs=0) , + leq-eq-ℚ _ _ + ( rs=0 ∙ + inv (ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ))) ( λ 0 Date: Sun, 23 Mar 2025 10:55:47 -0700 Subject: [PATCH 10/14] make pre-commit --- .../maximum-rational-numbers.lagda.md | 8 +++++++- .../minimum-rational-numbers.lagda.md | 9 ++++++++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md index 85c33d42de..59124d8e82 100644 --- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md @@ -23,7 +23,13 @@ open import order-theory.decidable-total-orders ## Idea -The {{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}} of two [rational numbers](elementary-number-theory.rational-numbers.md) is the [greatest](elementary-number-theory.inequality-rational-numbers.md) rational number of the two. This is the [binary least upper bound](order-theory.least-upper-bounds-posets.md) in the [total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md). +The +{{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}} +of two [rational numbers](elementary-number-theory.rational-numbers.md) is the +[greatest](elementary-number-theory.inequality-rational-numbers.md) rational +number of the two. This is the +[binary least upper bound](order-theory.least-upper-bounds-posets.md) in the +[total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md). ## Definition diff --git a/src/elementary-number-theory/minimum-rational-numbers.lagda.md b/src/elementary-number-theory/minimum-rational-numbers.lagda.md index d2a3112329..a0e9cf67da 100644 --- a/src/elementary-number-theory/minimum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/minimum-rational-numbers.lagda.md @@ -23,7 +23,14 @@ open import order-theory.decidable-total-orders ## Idea -The {{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}} of two [rational numbers](elementary-number-theory.rational-numbers.md) is the [smallest](elementary-number-theory.inequality-rational-numbers.md) rational number of the two. This is the [binary greatest lower bound](order-theory.greatest-lower-bounds-posets.md) in the [total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md). +The +{{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}} +of two [rational numbers](elementary-number-theory.rational-numbers.md) is the +[smallest](elementary-number-theory.inequality-rational-numbers.md) rational +number of the two. This is the +[binary greatest lower bound](order-theory.greatest-lower-bounds-posets.md) in +the +[total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md). ## Definition From c37f6e36c2ddab541c77cbee56f6cc0c775e5331 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Mon, 24 Mar 2025 16:12:00 +0000 Subject: [PATCH 11/14] edits `abstract` --- ...closed-intervals-rational-numbers.lagda.md | 14 ++- .../maximum-rational-numbers.lagda.md | 85 +++++++++--------- .../minimum-rational-numbers.lagda.md | 86 ++++++++++--------- .../negative-rational-numbers.lagda.md | 47 +++++----- 4 files changed, 128 insertions(+), 104 deletions(-) diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md index 230b6445ed..21adaa0ad1 100644 --- a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md @@ -49,7 +49,7 @@ module _ where closed-interval-ℚ : subtype lzero ℚ - closed-interval-ℚ r = leq-ℚ-Prop p r ∧ leq-ℚ-Prop r q + closed-interval-ℚ r = (leq-ℚ-Prop p r) ∧ (leq-ℚ-Prop r q) is-in-closed-interval-ℚ : ℚ → UU lzero is-in-closed-interval-ℚ r = type-Prop (closed-interval-ℚ r) @@ -68,7 +68,9 @@ is-in-unordered-closed-interval-ℚ p q = ```agda abstract - left-mul-closed-interval-ℚ : (p q r s : ℚ) → is-in-closed-interval-ℚ p q r → + left-mul-closed-interval-ℚ : + (p q r s : ℚ) → + is-in-closed-interval-ℚ p q r → is-in-unordered-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s) left-mul-closed-interval-ℚ p q r s (p≤r , r≤q) = let @@ -118,8 +120,10 @@ abstract ( left-leq-right-max-ℚ (p *ℚ s) (q *ℚ s) ps≤qs) ( preserves-leq-right-mul-ℚ⁺ s⁺ r q r≤q)) +abstract right-mul-closed-interval-ℚ : - (p q r s : ℚ) → is-in-closed-interval-ℚ p q r → + (p q r s : ℚ) → + is-in-closed-interval-ℚ p q r → is-in-unordered-closed-interval-ℚ (s *ℚ p) (s *ℚ q) (s *ℚ r) right-mul-closed-interval-ℚ p q r s r∈[p,q] = tr @@ -131,9 +135,11 @@ abstract ( commutative-mul-ℚ q s) ( left-mul-closed-interval-ℚ p q r s r∈[p,q])) +abstract mul-closed-interval-closed-interval-ℚ : (p q r s t u : ℚ) → - is-in-closed-interval-ℚ p q r → is-in-closed-interval-ℚ s t u → + is-in-closed-interval-ℚ p q r → + is-in-closed-interval-ℚ s t u → is-in-closed-interval-ℚ (min-ℚ (min-ℚ (p *ℚ s) (p *ℚ t)) (min-ℚ (q *ℚ s) (q *ℚ t))) (max-ℚ (max-ℚ (p *ℚ s) (p *ℚ t)) (max-ℚ (q *ℚ s) (q *ℚ t))) diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md index 59124d8e82..5861ba5fdb 100644 --- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md @@ -43,74 +43,81 @@ max-ℚ = max-Decidable-Total-Order ℚ-Decidable-Total-Order ### Associativity of the maximum operation ```agda -associative-max-ℚ : (x y z : ℚ) → max-ℚ (max-ℚ x y) z ＝ max-ℚ x (max-ℚ y z) -associative-max-ℚ = - associative-max-Decidable-Total-Order ℚ-Decidable-Total-Order +abstract + associative-max-ℚ : (x y z : ℚ) → max-ℚ (max-ℚ x y) z ＝ max-ℚ x (max-ℚ y z) + associative-max-ℚ = + associative-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` ### Commutativity of the maximum operation ```agda -commutative-max-ℚ : (x y : ℚ) → max-ℚ x y ＝ max-ℚ y x -commutative-max-ℚ = - commutative-max-Decidable-Total-Order ℚ-Decidable-Total-Order +abstract + commutative-max-ℚ : (x y : ℚ) → max-ℚ x y ＝ max-ℚ y x + commutative-max-ℚ = + commutative-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` ### The maximum operation is idempotent ```agda -idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x -idempotent-max-ℚ = - idempotent-max-Decidable-Total-Order ℚ-Decidable-Total-Order +abstract + idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x + idempotent-max-ℚ = + idempotent-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` ### The maximum is an upper bound ```agda -leq-left-max-ℚ : (x y : ℚ) → x ≤-ℚ max-ℚ x y -leq-left-max-ℚ = leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order +abstract + leq-left-max-ℚ : (x y : ℚ) → x ≤-ℚ max-ℚ x y + leq-left-max-ℚ = leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order -leq-right-max-ℚ : (x y : ℚ) → y ≤-ℚ max-ℚ x y -leq-right-max-ℚ = leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order + leq-right-max-ℚ : (x y : ℚ) → y ≤-ℚ max-ℚ x y + leq-right-max-ℚ = leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` ### If `a` is less than or equal to `b`, then the maximum of `a` and `b` is `b` ```agda -left-leq-right-max-ℚ : (x y : ℚ) → leq-ℚ x y → max-ℚ x y ＝ y -left-leq-right-max-ℚ = - left-leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order - -right-leq-left-max-ℚ : (x y : ℚ) → leq-ℚ y x → max-ℚ x y ＝ x -right-leq-left-max-ℚ = - right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order +abstract + left-leq-right-max-ℚ : (x y : ℚ) → leq-ℚ x y → max-ℚ x y ＝ y + left-leq-right-max-ℚ = + left-leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order + + right-leq-left-max-ℚ : (x y : ℚ) → leq-ℚ y x → max-ℚ x y ＝ x + right-leq-left-max-ℚ = + right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order ``` ### If both `x` and `y` are less than `z`, so is their maximum ```agda -le-max-le-both-ℚ : (z x y : ℚ) → le-ℚ x z → le-ℚ y z → le-ℚ (max-ℚ x y) z -le-max-le-both-ℚ z x y x Date: Mon, 24 Mar 2025 16:45:58 +0000 Subject: [PATCH 12/14] pre-commit --- .../maximum-rational-numbers.lagda.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md index 5861ba5fdb..9bb3eab066 100644 --- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md +++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md @@ -109,7 +109,10 @@ abstract ... | inr y≤x = inv-tr ( λ w → le-ℚ w z) - ( right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order x y y≤x) + ( right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order + ( x) + ( y) + ( y≤x)) ( x Date: Mon, 24 Mar 2025 17:54:35 -0700 Subject: [PATCH 13/14] Progress --- ...closed-intervals-rational-numbers.lagda.md | 101 +++++++++++++----- 1 file changed, 73 insertions(+), 28 deletions(-) diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md index 230b6445ed..7729fee535 100644 --- a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md @@ -60,6 +60,41 @@ unordered-closed-interval-ℚ p q = closed-interval-ℚ (min-ℚ p q) (max-ℚ p is-in-unordered-closed-interval-ℚ : ℚ → ℚ → ℚ → UU lzero is-in-unordered-closed-interval-ℚ p q = is-in-closed-interval-ℚ (min-ℚ p q) (max-ℚ p q) + +is-in-unordered-closed-interval-is-in-closed-interval-ℚ : + (p q r : ℚ) → is-in-closed-interval-ℚ p q r → + is-in-unordered-closed-interval-ℚ p q r +is-in-unordered-closed-interval-is-in-closed-interval-ℚ p q r (p≤r , q≤r) = + transitive-leq-ℚ + ( min-ℚ p q) + ( p) + ( r) + ( p≤r) + ( leq-left-min-ℚ p q) , + transitive-leq-ℚ + ( r) + ( q) + ( max-ℚ p q) + ( leq-right-max-ℚ p q) + ( q≤r) + +is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ : + (p q r : ℚ) → is-in-closed-interval-ℚ p q r → + is-in-unordered-closed-interval-ℚ q p r +is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ + p q r (p≤r , q≤r) = + transitive-leq-ℚ + ( min-ℚ q p) + ( p) + ( r) + ( p≤r) + ( leq-right-min-ℚ q p) , + transitive-leq-ℚ + ( r) + ( q) + ( max-ℚ q p) + ( leq-left-max-ℚ q p) + ( q≤r) ``` ## Properties @@ -68,9 +103,29 @@ is-in-unordered-closed-interval-ℚ p q = ```agda abstract + left-mul-negative-closed-interval-ℚ : (p q r s : ℚ) → + is-in-closed-interval-ℚ p q r → is-negative-ℚ s → + is-in-closed-interval-ℚ (q *ℚ s) (p *ℚ s) (r *ℚ s) + left-mul-negative-closed-interval-ℚ p q r s (p≤r , r≤q) neg-s = + let + s⁻ = s , neg-s + in + reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q , + reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r + + left-mul-positive-closed-interval-ℚ : (p q r s : ℚ) → + is-in-closed-interval-ℚ p q r → is-positive-ℚ s → + is-in-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s) + left-mul-positive-closed-interval-ℚ p q r s (p≤r , r≤q) pos-s = + let + s⁺ = s , pos-s + in + preserves-leq-right-mul-ℚ⁺ s⁺ p r p≤r , + preserves-leq-right-mul-ℚ⁺ s⁺ r q r≤q + left-mul-closed-interval-ℚ : (p q r s : ℚ) → is-in-closed-interval-ℚ p q r → is-in-unordered-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s) - left-mul-closed-interval-ℚ p q r s (p≤r , r≤q) = + left-mul-closed-interval-ℚ p q r s H@(p≤r , r≤q) = let p≤q = transitive-leq-ℚ p r q r≤q p≤r in @@ -78,18 +133,12 @@ abstract ( s) ( zero-ℚ) ( λ s<0 → - let - s⁻ = s , is-negative-le-zero-ℚ s s<0 - qs≤ps = reverses-leq-right-mul-ℚ⁻ s⁻ p q p≤q - in - inv-tr - ( λ t → leq-ℚ t (r *ℚ s)) - ( right-leq-left-min-ℚ (p *ℚ s) (q *ℚ s) qs≤ps) - ( reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q) , - inv-tr - ( leq-ℚ (r *ℚ s)) - ( right-leq-left-max-ℚ (p *ℚ s) (q *ℚ s) qs≤ps) - ( reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r)) + is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ + (q *ℚ s) + (p *ℚ s) + (r *ℚ s) + ( left-mul-negative-closed-interval-ℚ p q r s H + ( is-negative-le-zero-ℚ s s<0))) ( λ s=0 → let ps=0 = ap (p *ℚ_) s=0 ∙ right-zero-law-mul-ℚ p @@ -101,22 +150,18 @@ abstract ( _) ( ap-binary min-ℚ ps=0 qs=0 ∙ idempotent-min-ℚ zero-ℚ ∙ inv rs=0) , - leq-eq-ℚ _ _ - ( rs=0 ∙ - inv (ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ))) + leq-eq-ℚ + ( _) + ( _) + ( rs=0 ∙ + inv (ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ))) ( λ 0 Date: Mon, 24 Mar 2025 17:56:35 -0700 Subject: [PATCH 14/14] Progress --- .../closed-intervals-rational-numbers.lagda.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md index c139b411d7..86535643cd 100644 --- a/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md +++ b/src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md @@ -62,7 +62,8 @@ is-in-unordered-closed-interval-ℚ p q = is-in-closed-interval-ℚ (min-ℚ p q) (max-ℚ p q) is-in-unordered-closed-interval-is-in-closed-interval-ℚ : - (p q r : ℚ) → is-in-closed-interval-ℚ p q r → + (p q r : ℚ) → + is-in-closed-interval-ℚ p q r → is-in-unordered-closed-interval-ℚ p q r is-in-unordered-closed-interval-is-in-closed-interval-ℚ p q r (p≤r , q≤r) = transitive-leq-ℚ @@ -103,7 +104,8 @@ is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ ```agda abstract - left-mul-negative-closed-interval-ℚ : (p q r s : ℚ) → + left-mul-negative-closed-interval-ℚ : + (p q r s : ℚ) → is-in-closed-interval-ℚ p q r → is-negative-ℚ s → is-in-closed-interval-ℚ (q *ℚ s) (p *ℚ s) (r *ℚ s) left-mul-negative-closed-interval-ℚ p q r s (p≤r , r≤q) neg-s = @@ -113,7 +115,8 @@ abstract reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q , reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r - left-mul-positive-closed-interval-ℚ : (p q r s : ℚ) → + left-mul-positive-closed-interval-ℚ : + (p q r s : ℚ) → is-in-closed-interval-ℚ p q r → is-positive-ℚ s → is-in-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s) left-mul-positive-closed-interval-ℚ p q r s (p≤r , r≤q) pos-s =