diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 8548212757..dbf5dd22d6 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -10,6 +10,7 @@ open import elementary-number-theory.ackermann-function public open import elementary-number-theory.addition-integer-fractions public open import elementary-number-theory.addition-integers public open import elementary-number-theory.addition-natural-numbers public +open import elementary-number-theory.addition-positive-and-negative-integers public open import elementary-number-theory.addition-rational-numbers public open import elementary-number-theory.arithmetic-functions public open import elementary-number-theory.based-induction-natural-numbers public @@ -30,7 +31,9 @@ open import elementary-number-theory.congruence-natural-numbers public open import elementary-number-theory.cross-multiplication-difference-integer-fractions public open import elementary-number-theory.cubes-natural-numbers public open import elementary-number-theory.decidable-dependent-function-types public +open import elementary-number-theory.decidable-total-order-integers public open import elementary-number-theory.decidable-total-order-natural-numbers public +open import elementary-number-theory.decidable-total-order-rational-numbers public open import elementary-number-theory.decidable-total-order-standard-finite-types public open import elementary-number-theory.decidable-types public open import elementary-number-theory.difference-integers public @@ -86,12 +89,16 @@ open import elementary-number-theory.multiplication-integer-fractions public open import elementary-number-theory.multiplication-integers public open import elementary-number-theory.multiplication-lists-of-natural-numbers public open import elementary-number-theory.multiplication-natural-numbers public +open import elementary-number-theory.multiplication-positive-and-negative-integers public open import elementary-number-theory.multiplication-rational-numbers public open import elementary-number-theory.multiplicative-monoid-of-natural-numbers public 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-integers 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 open import elementary-number-theory.nonzero-natural-numbers public open import elementary-number-theory.ordinal-induction-natural-numbers public @@ -99,6 +106,8 @@ open import elementary-number-theory.parity-natural-numbers public open import elementary-number-theory.peano-arithmetic public open import elementary-number-theory.pisano-periods public open import elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility public +open import elementary-number-theory.positive-and-negative-integers public +open import elementary-number-theory.positive-integers public open import elementary-number-theory.powers-integers public open import elementary-number-theory.powers-of-two public open import elementary-number-theory.prime-numbers public @@ -120,7 +129,10 @@ open import elementary-number-theory.squares-natural-numbers public open import elementary-number-theory.standard-cyclic-groups public open import elementary-number-theory.standard-cyclic-rings public open import elementary-number-theory.stirling-numbers-of-the-second-kind public +open import elementary-number-theory.strict-inequality-integer-fractions public +open import elementary-number-theory.strict-inequality-integers public open import elementary-number-theory.strict-inequality-natural-numbers public +open import elementary-number-theory.strict-inequality-rational-numbers public open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public open import elementary-number-theory.strong-induction-natural-numbers public open import elementary-number-theory.sums-of-natural-numbers public diff --git a/src/elementary-number-theory/absolute-value-integers.lagda.md b/src/elementary-number-theory/absolute-value-integers.lagda.md index 8d812cedac..63a02a8915 100644 --- a/src/elementary-number-theory/absolute-value-integers.lagda.md +++ b/src/elementary-number-theory/absolute-value-integers.lagda.md @@ -14,6 +14,8 @@ open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-functions open import foundation.coproduct-types diff --git a/src/elementary-number-theory/addition-integer-fractions.lagda.md b/src/elementary-number-theory/addition-integer-fractions.lagda.md index 7593f46214..adfbc5841a 100644 --- a/src/elementary-number-theory/addition-integer-fractions.lagda.md +++ b/src/elementary-number-theory/addition-integer-fractions.lagda.md @@ -10,6 +10,7 @@ module elementary-number-theory.addition-integer-fractions where open import elementary-number-theory.addition-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import foundation.action-on-identifications-binary-functions open import foundation.dependent-pair-types diff --git a/src/elementary-number-theory/addition-integers.lagda.md b/src/elementary-number-theory/addition-integers.lagda.md index 8b93313e77..0e17c532a8 100644 --- a/src/elementary-number-theory/addition-integers.lagda.md +++ b/src/elementary-number-theory/addition-integers.lagda.md @@ -10,6 +10,9 @@ module elementary-number-theory.addition-integers where open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions @@ -30,9 +33,9 @@ open import foundation.unit-type ## Idea -We introduce addition on the integers and derive its basic properties with -respect to `succ-ℤ` and `neg-ℤ`. Properties of addition with respect to -inequality are derived in `inequality-integers`. +We introduce {{#concept "addition" Disambiguation="integers" Agda=add-ℤ}} on the +[integers](elementary-number-theory.integers.md) and derive its basic properties +with respect to `succ-ℤ` and `neg-ℤ`. ## Definition @@ -506,52 +509,6 @@ distributive-neg-add-ℤ (inr (inr (succ-ℕ n))) l = by ap pred-ℤ (distributive-neg-add-ℤ (inr (inr n)) l) ``` -### Addition of nonnegative integers is nonnegative - -```agda -is-nonnegative-add-ℤ : - (k l : ℤ) → - is-nonnegative-ℤ k → is-nonnegative-ℤ l → is-nonnegative-ℤ (k +ℤ l) -is-nonnegative-add-ℤ (inr (inl star)) (inr (inl star)) p q = star -is-nonnegative-add-ℤ (inr (inl star)) (inr (inr n)) p q = star -is-nonnegative-add-ℤ (inr (inr zero-ℕ)) (inr (inl star)) p q = star -is-nonnegative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inl star)) star star = - is-nonnegative-succ-ℤ - ( (inr (inr n)) +ℤ (inr (inl star))) - ( is-nonnegative-add-ℤ (inr (inr n)) (inr (inl star)) star star) -is-nonnegative-add-ℤ (inr (inr zero-ℕ)) (inr (inr m)) star star = star -is-nonnegative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inr m)) star star = - is-nonnegative-succ-ℤ - ( (inr (inr n)) +ℤ (inr (inr m))) - ( is-nonnegative-add-ℤ (inr (inr n)) (inr (inr m)) star star) -``` - -### Addition of positive integers is positive - -```agda -is-positive-add-ℤ : - {x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) -is-positive-add-ℤ {inr (inr zero-ℕ)} {inr (inr y)} H K = star -is-positive-add-ℤ {inr (inr (succ-ℕ x))} {inr (inr y)} H K = - is-positive-succ-ℤ - ( is-nonnegative-is-positive-ℤ - ( is-positive-add-ℤ {inr (inr x)} {inr (inr y)} star star)) - -is-positive-add-nonnegative-positive-ℤ : - {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) -is-positive-add-nonnegative-positive-ℤ {inr (inl x)} {y} H H' = - is-positive-eq-ℤ refl H' -is-positive-add-nonnegative-positive-ℤ {inr (inr x)} {y} H H' = - is-positive-add-ℤ {inr (inr x)} {y} H H' - -is-positive-add-positive-nonnegative-ℤ : - {x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-positive-ℤ (x +ℤ y) -is-positive-add-positive-nonnegative-ℤ {x} {y} H H' = - is-positive-eq-ℤ - ( commutative-add-ℤ y x) - ( is-positive-add-nonnegative-positive-ℤ H' H) -``` - ### The inclusion of ℕ into ℤ preserves addition ```agda @@ -595,17 +552,14 @@ is-zero-right-add-ℤ x y H = is-zero-left-add-ℤ y x (commutative-add-ℤ y x ∙ H) ``` -### Adding negatives results in a negative - -```agda -negatives-add-ℤ : - (x y : ℕ) → in-neg x +ℤ in-neg y ＝ in-neg (succ-ℕ (x +ℕ y)) -negatives-add-ℤ zero-ℕ y = ap (inl ∘ succ-ℕ) (inv (left-unit-law-add-ℕ y)) -negatives-add-ℤ (succ-ℕ x) y = - equational-reasoning - pred-ℤ (in-neg x +ℤ in-neg y) - ＝ pred-ℤ (in-neg (succ-ℕ (x +ℕ y))) - by ap pred-ℤ (negatives-add-ℤ x y) - ＝ (inl ∘ succ-ℕ) ((succ-ℕ x) +ℕ y) - by ap (inl ∘ succ-ℕ) (inv (left-successor-law-add-ℕ x y)) -``` +## See also + +- Properties of addition with respect to positivity, nonnegativity, negativity + and nonnpositivity are derived in + [`addition-positive-and-negative-integers`](elementary-number-theory.addition-positive-and-negative-integers.md) +- Properties of addition with respect to the standard ordering on the integers + are derived in + [`inequality-integers`](elementary-number-theory.inequality-integers.md) +- Properties of addition with respect to the standard strict ordering on the + integers are derived in + [`strict-inequality-integers`](elementary-number-theory.strict-inequality-integers.md) diff --git a/src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md b/src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md new file mode 100644 index 0000000000..ae0daa642c --- /dev/null +++ b/src/elementary-number-theory/addition-positive-and-negative-integers.lagda.md @@ -0,0 +1,193 @@ +# Addition of positive, negative, nonnegative and nonpositive integers + +```agda +module elementary-number-theory.addition-positive-and-negative-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.negative-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers + +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.unit-type +``` + +
+ +## Idea + +When we have information about the sign of the summands, we can in many cases +deduce the sign of their sum too. The table below tabulates all such cases and +displays the corresponding Agda definition. + +| `p` | `q` | `p +ℤ q` | operation | +| :---------: | :---------: | :---------: | ------------------- | +| positive | positive | positive | `add-positive-ℤ` | +| positive | nonnegative | positive | | +| positive | negative | | | +| positive | nonpositive | | | +| nonnegative | positive | positive | | +| nonnegative | nonnegative | nonnegative | `add-nonnegative-ℤ` | +| nonnegative | negative | | | +| nonnegative | nonpositive | | | +| negative | positive | | | +| negative | nonnegative | | | +| negative | negative | negative | `add-negative-ℤ` | +| negative | nonpositive | negative | | +| nonpositive | positive | | | +| nonpositive | nonnegative | | | +| nonpositive | negative | negative | | +| nonpositive | nonpositive | nonpositive | `add-nonpositive-ℤ` | + +## Lemmas + +### The sum of two positive integers is positive + +```agda +is-positive-add-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) +is-positive-add-ℤ {inr (inr zero-ℕ)} {y} H K = + is-positive-succ-is-positive-ℤ K +is-positive-add-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-positive-succ-is-positive-ℤ + ( is-positive-add-ℤ {inr (inr x)} H K) +``` + +### The sum of a positive and a nonnegative integer is positive + +```agda +is-positive-add-positive-nonnegative-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-positive-ℤ (x +ℤ y) +is-positive-add-positive-nonnegative-ℤ {inr (inr zero-ℕ)} {y} H K = + is-positive-succ-is-nonnegative-ℤ K +is-positive-add-positive-nonnegative-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-positive-succ-is-positive-ℤ + ( is-positive-add-positive-nonnegative-ℤ {inr (inr x)} H K) +``` + +### The sum of a nonnegative and a positive integer is positive + +```agda +is-positive-add-nonnegative-positive-ℤ : + {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y) +is-positive-add-nonnegative-positive-ℤ {x} {y} H K = + is-positive-eq-ℤ + ( commutative-add-ℤ y x) + ( is-positive-add-positive-nonnegative-ℤ K H) +``` + +### The sum of two nonnegative integers is nonnegative + +```agda +is-nonnegative-add-ℤ : + {x y : ℤ} → + is-nonnegative-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x +ℤ y) +is-nonnegative-add-ℤ {inr (inl x)} {y} H K = K +is-nonnegative-add-ℤ {inr (inr zero-ℕ)} {y} H K = + is-nonnegative-succ-is-nonnegative-ℤ K +is-nonnegative-add-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-nonnegative-succ-is-nonnegative-ℤ + ( is-nonnegative-add-ℤ {inr (inr x)} star K) +``` + +### The sum of two negative integers is negative + +```agda +is-negative-add-ℤ : + {x y : ℤ} → is-negative-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y) +is-negative-add-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( neg-neg-ℤ (x +ℤ y)) + ( is-negative-neg-is-positive-ℤ + ( is-positive-eq-ℤ + ( inv (distributive-neg-add-ℤ x y)) + ( is-positive-add-ℤ + ( is-positive-neg-is-negative-ℤ H) + ( is-positive-neg-is-negative-ℤ K)))) +``` + +### The sum of a negative and a nonpositive integer is negative + +```agda +is-negative-add-negative-nonnegative-ℤ : + {x y : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ y → is-negative-ℤ (x +ℤ y) +is-negative-add-negative-nonnegative-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( neg-neg-ℤ (x +ℤ y)) + ( is-negative-neg-is-positive-ℤ + ( is-positive-eq-ℤ + ( inv (distributive-neg-add-ℤ x y)) + ( is-positive-add-positive-nonnegative-ℤ + ( is-positive-neg-is-negative-ℤ H) + ( is-nonnegative-neg-is-nonpositive-ℤ K)))) +``` + +### The sum of a nonpositive and a negative integer is negative + +```agda +is-negative-add-nonpositive-negative-ℤ : + {x y : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ y → is-negative-ℤ (x +ℤ y) +is-negative-add-nonpositive-negative-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( commutative-add-ℤ y x) + ( is-negative-add-negative-nonnegative-ℤ K H) +``` + +### The sum of two nonpositive integers is nonpositive + +```agda +is-nonpositive-add-ℤ : + {x y : ℤ} → + is-nonpositive-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x +ℤ y) +is-nonpositive-add-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( neg-neg-ℤ (x +ℤ y)) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( is-nonnegative-eq-ℤ + ( inv (distributive-neg-add-ℤ x y)) + ( is-nonnegative-add-ℤ + ( is-nonnegative-neg-is-nonpositive-ℤ H) + ( is-nonnegative-neg-is-nonpositive-ℤ K)))) +``` + +## Definitions + +### Addition of positive integers + +```agda +add-positive-ℤ : positive-ℤ → positive-ℤ → positive-ℤ +add-positive-ℤ (x , H) (y , K) = (add-ℤ x y , is-positive-add-ℤ H K) +``` + +### Addition of nonnegative integers + +```agda +add-nonnegative-ℤ : nonnegative-ℤ → nonnegative-ℤ → nonnegative-ℤ +add-nonnegative-ℤ (x , H) (y , K) = (add-ℤ x y , is-nonnegative-add-ℤ H K) +``` + +### Addition of negative integers + +```agda +add-negative-ℤ : negative-ℤ → negative-ℤ → negative-ℤ +add-negative-ℤ (x , H) (y , K) = (add-ℤ x y , is-negative-add-ℤ H K) +``` + +### Addition of nonpositive integers + +```agda +add-nonpositive-ℤ : nonpositive-ℤ → nonpositive-ℤ → nonpositive-ℤ +add-nonpositive-ℤ (x , H) (y , K) = (add-ℤ x y , is-nonpositive-add-ℤ H K) +``` diff --git a/src/elementary-number-theory/addition-rational-numbers.lagda.md b/src/elementary-number-theory/addition-rational-numbers.lagda.md index 3f0c47f1a5..f653c99ef3 100644 --- a/src/elementary-number-theory/addition-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-rational-numbers.lagda.md @@ -51,7 +51,7 @@ ap-add-ℚ p q = ap-binary add-ℚ p q ```agda left-unit-law-add-ℚ : (x : ℚ) → zero-ℚ +ℚ x ＝ x left-unit-law-add-ℚ (x , p) = - eq-ℚ-sim-fractions-ℤ + eq-ℚ-sim-fraction-ℤ ( add-fraction-ℤ zero-fraction-ℤ x) ( x) ( left-unit-law-add-fraction-ℤ x) ∙ @@ -59,7 +59,7 @@ left-unit-law-add-ℚ (x , p) = right-unit-law-add-ℚ : (x : ℚ) → x +ℚ zero-ℚ ＝ x right-unit-law-add-ℚ (x , p) = - eq-ℚ-sim-fractions-ℤ + eq-ℚ-sim-fraction-ℤ ( add-fraction-ℤ x zero-fraction-ℤ) ( x) ( right-unit-law-add-fraction-ℤ x) ∙ @@ -76,16 +76,16 @@ associative-add-ℚ (x , px) (y , py) (z , pz) = equational-reasoning in-fraction-ℤ (add-fraction-ℤ (pr1 (in-fraction-ℤ (add-fraction-ℤ x y))) z) ＝ in-fraction-ℤ (add-fraction-ℤ (add-fraction-ℤ x y) z) - by eq-ℚ-sim-fractions-ℤ _ _ + by eq-ℚ-sim-fraction-ℤ _ _ ( sim-fraction-add-fraction-ℤ ( symmetric-sim-fraction-ℤ _ _ ( sim-reduced-fraction-ℤ (add-fraction-ℤ x y))) ( refl-sim-fraction-ℤ z)) ＝ in-fraction-ℤ (add-fraction-ℤ x (add-fraction-ℤ y z)) - by eq-ℚ-sim-fractions-ℤ _ _ (associative-add-fraction-ℤ x y z) + by eq-ℚ-sim-fraction-ℤ _ _ (associative-add-fraction-ℤ x y z) ＝ in-fraction-ℤ ( add-fraction-ℤ x (pr1 (in-fraction-ℤ (add-fraction-ℤ y z)))) - by eq-ℚ-sim-fractions-ℤ _ _ + by eq-ℚ-sim-fraction-ℤ _ _ ( sim-fraction-add-fraction-ℤ ( refl-sim-fraction-ℤ x) ( sim-reduced-fraction-ℤ (add-fraction-ℤ y z))) @@ -98,7 +98,7 @@ commutative-add-ℚ : (x y : ℚ) → x +ℚ y ＝ y +ℚ x commutative-add-ℚ (x , px) (y , py) = - eq-ℚ-sim-fractions-ℤ + eq-ℚ-sim-fraction-ℤ ( add-fraction-ℤ x y) ( add-fraction-ℤ y x) ( commutative-add-fraction-ℤ x y) diff --git a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md index cb14d6fcfd..8bab982a09 100644 --- a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md +++ b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md @@ -21,7 +21,11 @@ open import elementary-number-theory.greatest-common-divisor-natural-numbers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-functions open import foundation.coproduct-types @@ -194,10 +198,11 @@ bezouts-lemma-refactor-hypotheses x y H K = x-product-nonneg : is-nonnegative-ℤ ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P) *ℤ x) - x-product-nonneg = is-nonnegative-mul-ℤ - (is-nonnegative-int-ℕ - ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P)) - (is-nonnegative-is-positive-ℤ H) + x-product-nonneg = + is-nonnegative-mul-ℤ + ( is-nonnegative-int-ℕ + ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P)) + ( is-nonnegative-is-positive-ℤ H) y-product-nonneg : is-nonnegative-ℤ ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) P) *ℤ y) @@ -212,7 +217,7 @@ bezouts-lemma-pos-ints : Σ ℤ (λ s → Σ ℤ (λ t → (s *ℤ x) +ℤ (t *ℤ y) ＝ gcd-ℤ x y)) bezouts-lemma-pos-ints x y H K = sx-ty-nonneg-case-split - ( decide-is-nonnegative-ℤ {(s *ℤ x) -ℤ (t *ℤ y)}) + ( decide-is-nonnegative-is-nonnegative-neg-ℤ {(s *ℤ x) -ℤ (t *ℤ y)}) where s : ℤ s = int-ℕ (minimal-positive-distance-x-coeff diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md index a1ea80e7c2..2817097de3 100755 --- a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md +++ b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md @@ -25,7 +25,10 @@ open import elementary-number-theory.lower-bounds-natural-numbers open import elementary-number-theory.modular-arithmetic open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.strict-inequality-natural-numbers open import elementary-number-theory.well-ordering-principle-natural-numbers @@ -311,7 +314,7 @@ is-distance-between-multiples-div-mod-ℕ : (x y z : ℕ) → div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z) → is-distance-between-multiples-ℕ x y z is-distance-between-multiples-div-mod-ℕ zero-ℕ y z (u , p) = - u-nonneg-case-split (decide-is-nonnegative-ℤ {u}) + u-nonneg-case-split (decide-is-nonnegative-is-nonnegative-neg-ℤ {u}) where u-nonneg-case-split : (is-nonnegative-ℤ u + is-nonnegative-ℤ (neg-ℤ u)) → @@ -331,7 +334,6 @@ is-distance-between-multiples-div-mod-ℕ zero-ℕ y z (u , p) = is-injective-int-ℕ ( inv ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ - ( int-ℕ z) ( is-nonnegative-int-ℕ z) ( tr ( is-nonnegative-ℤ) @@ -339,7 +341,7 @@ is-distance-between-multiples-div-mod-ℕ zero-ℕ y z (u , p) = ( is-nonnegative-mul-ℤ neg (is-nonnegative-int-ℕ y)))))) is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) = - uy-z-case-split (decide-is-nonnegative-ℤ + uy-z-case-split (decide-is-nonnegative-is-nonnegative-neg-ℤ { ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z))}) where a : ℤ @@ -714,31 +716,38 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) = ＝ z by abs-int-ℕ z)) where neg-a-is-nonnegative-ℤ : is-nonnegative-ℤ (neg-ℤ a) - neg-a-is-nonnegative-ℤ = (is-nonnegative-left-factor-mul-ℤ - (tr is-nonnegative-ℤ - (equational-reasoning - neg-ℤ (((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ - (neg-ℤ (int-ℕ z))) - ＝ (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ - (neg-ℤ (neg-ℤ (int-ℕ z))) - by (distributive-neg-add-ℤ - ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) - (neg-ℤ (int-ℕ z))) - ＝ (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ - (int-ℕ z) - by ap ((neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ_) - (neg-neg-ℤ (int-ℕ z)) - ＝ add-ℤ (int-ℕ z) - (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) - by commutative-add-ℤ - (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) - (int-ℕ z) - ＝ (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)) - by inv (pr2 - (symmetric-cong-ℤ (int-ℕ (succ-ℕ x)) - ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) (int-ℕ z) - (cong-div-mod-ℤ (succ-ℕ x) y z (u , p))))) - z-uy) (is-nonnegative-int-ℕ (succ-ℕ x))) + neg-a-is-nonnegative-ℤ = + is-nonnegative-left-factor-mul-ℤ + ( tr is-nonnegative-ℤ + ( equational-reasoning + ( neg-ℤ (((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ + ( neg-ℤ (int-ℕ z)))) + ＝ ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ + ( neg-ℤ (neg-ℤ (int-ℕ z))) + by + ( distributive-neg-add-ℤ + ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) + ( neg-ℤ (int-ℕ z))) + ＝ ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ + ( int-ℕ z) + by + ap + ( (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ_) + ( neg-neg-ℤ (int-ℕ z)) + ＝ add-ℤ + ( int-ℕ z) + ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) + by + commutative-add-ℤ + ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) + ( int-ℕ z) + ＝ (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)) + by inv (pr2 + ( symmetric-cong-ℤ (int-ℕ (succ-ℕ x)) + ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) (int-ℕ z) + ( cong-div-mod-ℤ (succ-ℕ x) y z (u , p))))) + ( z-uy)) + ( is-nonnegative-int-ℕ (succ-ℕ x)) ``` ### The type `is-distance-between-multiples-ℕ x y z` is decidable @@ -1700,13 +1709,13 @@ remainder-min-dist-succ-x-is-distance x y = (int-ℕ s)) (neg-ℤ one-ℤ))) (succ-ℕ x)) -remainder-min-dist-succ-x-not-is-nonzero : +remainder-min-dist-succ-x-is-not-nonzero : (x y : ℕ) → ¬ ( is-nonzero-ℕ ( remainder-euclidean-division-ℕ ( minimal-positive-distance (succ-ℕ x) y) ( succ-ℕ x))) -remainder-min-dist-succ-x-not-is-nonzero x y nonzero = +remainder-min-dist-succ-x-is-not-nonzero x y nonzero = contradiction-le-ℕ ( remainder-euclidean-division-ℕ ( minimal-positive-distance (succ-ℕ x) y) @@ -1762,8 +1771,8 @@ remainder-min-dist-succ-x-is-zero x y = ( remainder-euclidean-division-ℕ (minimal-positive-distance (succ-ℕ x) y) (succ-ℕ x)) is-zero-case-split (inl z) = z - is-zero-case-split (inr nz) = ex-falso - (remainder-min-dist-succ-x-not-is-nonzero x y nz) + is-zero-case-split (inr nz) = + ex-falso (remainder-min-dist-succ-x-is-not-nonzero x y nz) minimal-positive-distance-div-fst : (x y : ℕ) → div-ℕ (minimal-positive-distance x y) x diff --git a/src/elementary-number-theory/decidable-total-order-integers.lagda.md b/src/elementary-number-theory/decidable-total-order-integers.lagda.md new file mode 100644 index 0000000000..f4e2772ec7 --- /dev/null +++ b/src/elementary-number-theory/decidable-total-order-integers.lagda.md @@ -0,0 +1,43 @@ +# The decidable total order of integers + +```agda +module elementary-number-theory.decidable-total-order-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-integers + +open import foundation.dependent-pair-types +open import foundation.propositional-truncations +open import foundation.universe-levels + +open import order-theory.decidable-total-orders +open import order-theory.total-orders +``` + +
+ +## Idea + +The type of [integers](elementary-number-theory.integers.md) +[equipped](foundation.structure.md) with its +[standard ordering relation](elementary-number-theory.inequality-integers.md) +forms a [decidable total order](order-theory.decidable-total-orders.md). + +## Definition + +```agda +is-total-leq-ℤ : is-total-Poset ℤ-Poset +is-total-leq-ℤ x y = unit-trunc-Prop (linear-leq-ℤ x y) + +ℤ-Total-Order : Total-Order lzero lzero +pr1 ℤ-Total-Order = ℤ-Poset +pr2 ℤ-Total-Order = is-total-leq-ℤ + +ℤ-Decidable-Total-Order : Decidable-Total-Order lzero lzero +pr1 ℤ-Decidable-Total-Order = ℤ-Poset +pr1 (pr2 ℤ-Decidable-Total-Order) = is-total-leq-ℤ +pr2 (pr2 ℤ-Decidable-Total-Order) = is-decidable-leq-ℤ +``` diff --git a/src/elementary-number-theory/decidable-total-order-rational-numbers.lagda.md b/src/elementary-number-theory/decidable-total-order-rational-numbers.lagda.md new file mode 100644 index 0000000000..3a1b901c63 --- /dev/null +++ b/src/elementary-number-theory/decidable-total-order-rational-numbers.lagda.md @@ -0,0 +1,43 @@ +# The decidable total order of rational numbers + +```agda +module elementary-number-theory.decidable-total-order-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.inequality-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.propositional-truncations +open import foundation.universe-levels + +open import order-theory.decidable-total-orders +open import order-theory.total-orders +``` + +
+ +## Idea + +The type of [rational numbers](elementary-number-theory.rational-numbers.md) +[equipped](foundation.structure.md) with its +[standard ordering relation](elementary-number-theory.inequality-rational-numbers.md) +forms a [decidable total order](order-theory.decidable-total-orders.md). + +## Definition + +```agda +is-total-leq-ℚ : is-total-Poset ℚ-Poset +is-total-leq-ℚ x y = unit-trunc-Prop (linear-leq-ℚ x y) + +ℚ-Total-Order : Total-Order lzero lzero +pr1 ℚ-Total-Order = ℚ-Poset +pr2 ℚ-Total-Order = is-total-leq-ℚ + +ℚ-Decidable-Total-Order : Decidable-Total-Order lzero lzero +pr1 ℚ-Decidable-Total-Order = ℚ-Poset +pr1 (pr2 ℚ-Decidable-Total-Order) = is-total-leq-ℚ +pr2 (pr2 ℚ-Decidable-Total-Order) = is-decidable-leq-ℚ +``` diff --git a/src/elementary-number-theory/distance-integers.lagda.md b/src/elementary-number-theory/distance-integers.lagda.md index 7c6976af5a..ee659aed25 100644 --- a/src/elementary-number-theory/distance-integers.lagda.md +++ b/src/elementary-number-theory/distance-integers.lagda.md @@ -12,6 +12,9 @@ open import elementary-number-theory.difference-integers open import elementary-number-theory.distance-natural-numbers open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions diff --git a/src/elementary-number-theory/divisibility-integers.lagda.md b/src/elementary-number-theory/divisibility-integers.lagda.md index 144135cf62..877056479c 100644 --- a/src/elementary-number-theory/divisibility-integers.lagda.md +++ b/src/elementary-number-theory/divisibility-integers.lagda.md @@ -13,8 +13,12 @@ open import elementary-number-theory.divisibility-natural-numbers open import elementary-number-theory.equality-integers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers open import elementary-number-theory.nonzero-integers +open import elementary-number-theory.positive-and-negative-integers open import foundation.action-on-identifications-functions open import foundation.binary-relations @@ -657,23 +661,14 @@ is-plus-or-minus-sim-unit-ℤ {x} {y} H | inr nz | inr p = ```agda eq-sim-unit-is-nonnegative-ℤ : {a b : ℤ} → is-nonnegative-ℤ a → is-nonnegative-ℤ b → sim-unit-ℤ a b → a ＝ b -eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K - with is-plus-or-minus-sim-unit-ℤ K -eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inl pos = pos -eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg - with is-decidable-is-zero-ℤ a -eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg | inl z = - equational-reasoning - a - ＝ zero-ℤ - by z - ＝ neg-ℤ a - by inv (ap neg-ℤ z) - ＝ b - by neg -eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K | inr neg | inr nz = - ex-falso - ( nz - ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ - a H (tr is-nonnegative-ℤ (inv neg) H'))) +eq-sim-unit-is-nonnegative-ℤ {a} {b} H H' K = + rec-coproduct + ( id) + ( λ K' → + eq-is-zero-ℤ + ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ H + ( is-nonnegative-eq-ℤ (inv K') H')) + ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ H' + ( is-nonnegative-eq-ℤ (inv (neg-neg-ℤ a) ∙ ap neg-ℤ K') H))) + ( is-plus-or-minus-sim-unit-ℤ K) ``` diff --git a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md index e5035b277b..8a6883a877 100644 --- a/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md +++ b/src/elementary-number-theory/greatest-common-divisor-integers.lagda.md @@ -14,6 +14,9 @@ open import elementary-number-theory.equality-integers open import elementary-number-theory.greatest-common-divisor-natural-numbers open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types @@ -234,7 +237,7 @@ div-gcd-is-common-divisor-ℤ x y k H = is-positive-gcd-is-positive-left-ℤ : (x y : ℤ) → is-positive-ℤ x → is-positive-ℤ (gcd-ℤ x y) is-positive-gcd-is-positive-left-ℤ x y H = - is-positive-int-ℕ + is-positive-int-is-nonzero-ℕ ( gcd-ℕ (abs-ℤ x) (abs-ℤ y)) ( is-nonzero-gcd-ℕ ( abs-ℤ x) @@ -247,7 +250,7 @@ is-positive-gcd-is-positive-left-ℤ x y H = is-positive-gcd-is-positive-right-ℤ : (x y : ℤ) → is-positive-ℤ y → is-positive-ℤ (gcd-ℤ x y) is-positive-gcd-is-positive-right-ℤ x y H = - is-positive-int-ℕ + is-positive-int-is-nonzero-ℕ ( gcd-ℕ (abs-ℤ x) (abs-ℤ y)) ( is-nonzero-gcd-ℕ ( abs-ℤ x) diff --git a/src/elementary-number-theory/inequality-integer-fractions.lagda.md b/src/elementary-number-theory/inequality-integer-fractions.lagda.md index 72408db7b4..60660edfed 100644 --- a/src/elementary-number-theory/inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/inequality-integer-fractions.lagda.md @@ -8,17 +8,24 @@ module elementary-number-theory.inequality-integer-fractions where ```agda open import elementary-number-theory.addition-integers +open import elementary-number-theory.addition-positive-and-negative-integers open import elementary-number-theory.cross-multiplication-difference-integer-fractions open import elementary-number-theory.difference-integers open import elementary-number-theory.inequality-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers -open import elementary-number-theory.mediant-integer-fractions open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers +open import elementary-number-theory.strict-inequality-integers open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types open import foundation.coproduct-types +open import foundation.decidable-propositions open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types @@ -32,12 +39,15 @@ open import foundation.universe-levels ## Idea -A fraction `m/n` is less (or equal) to a fraction `m'/n'` iff `m * n'` is less -(or equal) to `m' * n`. +An [integer fraction](elementary-number-theory.integer-fractions.md) `m/n` is +{{#concept "less or equal" Disambiguation="integer fracion" Agda=leq-fraction-ℤ}} +to a fraction `m'/n'` if the +[integer product](elementary-number-theory.multiplication-integers.md) `m * n'` +is [less or equal](elementary-number-theory.inequality-integers.md) to `m' * n`. ## Definition -### Inequality of integer fractions +### Inequality on integer fractions ```agda leq-fraction-ℤ-Prop : fraction-ℤ → fraction-ℤ → Prop lzero @@ -51,22 +61,25 @@ is-prop-leq-fraction-ℤ : (x y : fraction-ℤ) → is-prop (leq-fraction-ℤ x is-prop-leq-fraction-ℤ x y = is-prop-type-Prop (leq-fraction-ℤ-Prop x y) ``` -### Strict inequality of integer fractions - -```agda -le-fraction-ℤ-Prop : fraction-ℤ → fraction-ℤ → Prop lzero -le-fraction-ℤ-Prop (m , n , p) (m' , n' , p') = - le-ℤ-Prop (m *ℤ n') (m' *ℤ n) +## Properties -le-fraction-ℤ : fraction-ℤ → fraction-ℤ → UU lzero -le-fraction-ℤ x y = type-Prop (le-fraction-ℤ-Prop x y) +### Inequality on integer fractions is decidable -is-prop-le-fraction-ℤ : (x y : fraction-ℤ) → is-prop (le-fraction-ℤ x y) -is-prop-le-fraction-ℤ x y = is-prop-type-Prop (le-fraction-ℤ-Prop x y) +```agda +is-decidable-leq-fraction-ℤ : + (x y : fraction-ℤ) → (leq-fraction-ℤ x y) + ¬ (leq-fraction-ℤ x y) +is-decidable-leq-fraction-ℤ x y = + is-decidable-leq-ℤ + ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y) + ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x) + +leq-fraction-ℤ-Decidable-Prop : (x y : fraction-ℤ) → Decidable-Prop lzero +leq-fraction-ℤ-Decidable-Prop x y = + ( leq-fraction-ℤ x y , + is-prop-leq-fraction-ℤ x y , + is-decidable-leq-fraction-ℤ x y) ``` -## Properties - ### Inequality on integer fractions is antisymmetric with respect to the similarity relation ```agda @@ -80,30 +93,12 @@ module _ sim-fraction-ℤ x y is-sim-antisymmetric-leq-fraction-ℤ H H' = sim-is-zero-coss-mul-diff-fraction-ℤ x y - ( is-zero-is-nonnegative-ℤ + ( is-zero-is-nonnegative-is-nonpositive-ℤ ( H) - ( is-nonnegative-eq-ℤ - ( inv ( skew-commutative-cross-mul-diff-fraction-ℤ x y)) - ( H'))) -``` - -### Strict inequality on integer fractions is asymmetric - -```agda -module _ - (x y : fraction-ℤ) - where - - asymmetric-le-fraction-ℤ : - le-fraction-ℤ x y → ¬ (le-fraction-ℤ y x) - asymmetric-le-fraction-ℤ = - asymmetric-le-ℤ - ( mul-ℤ - ( numerator-fraction-ℤ x) - ( denominator-fraction-ℤ y)) - ( mul-ℤ - ( numerator-fraction-ℤ y) - ( denominator-fraction-ℤ x)) + ( is-nonpositive-eq-ℤ + ( skew-commutative-cross-mul-diff-fraction-ℤ y x) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( H')))) ``` ### Inequality on integer fractions is transitive @@ -111,165 +106,21 @@ module _ ```agda transitive-leq-fraction-ℤ : (p q r : fraction-ℤ) → - leq-fraction-ℤ p q → leq-fraction-ℤ q r → + leq-fraction-ℤ p q → leq-fraction-ℤ p r transitive-leq-fraction-ℤ p q r H H' = is-nonnegative-right-factor-mul-ℤ ( is-nonnegative-eq-ℤ ( lemma-add-cross-mul-diff-fraction-ℤ p q r) - (is-nonnegative-add-ℤ - ( denominator-fraction-ℤ p *ℤ cross-mul-diff-fraction-ℤ q r) - ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q) + ( is-nonnegative-add-ℤ ( is-nonnegative-mul-ℤ ( is-nonnegative-is-positive-ℤ ( is-positive-denominator-fraction-ℤ p)) - ( H')) + ( H)) ( is-nonnegative-mul-ℤ ( is-nonnegative-is-positive-ℤ ( is-positive-denominator-fraction-ℤ r)) - ( H)))) + ( H')))) ( is-positive-denominator-fraction-ℤ q) ``` - -### Strict inequality on integer fractions is transitive - -```agda -transitive-le-fraction-ℤ : - (p q r : fraction-ℤ) → - le-fraction-ℤ p q → - le-fraction-ℤ q r → - le-fraction-ℤ p r -transitive-le-fraction-ℤ p q r H H' = - is-positive-right-factor-mul-ℤ - ( is-positive-eq-ℤ - ( lemma-add-cross-mul-diff-fraction-ℤ p q r) - ( is-positive-add-ℤ - ( is-positive-mul-ℤ - ( is-positive-denominator-fraction-ℤ p) - ( H')) - ( is-positive-mul-ℤ - ( is-positive-denominator-fraction-ℤ r) - ( H)))) - ( is-positive-denominator-fraction-ℤ q) -``` - -### Chaining rules for inequality and strict inequality on integer fractions - -```agda -module _ - (p q r : fraction-ℤ) - where - - concatenate-le-leq-fraction-ℤ : - le-fraction-ℤ p q → - leq-fraction-ℤ q r → - le-fraction-ℤ p r - concatenate-le-leq-fraction-ℤ H H' = - is-positive-right-factor-mul-ℤ - ( is-positive-eq-ℤ - ( lemma-add-cross-mul-diff-fraction-ℤ p q r) - ( is-positive-add-nonnegative-positive-ℤ - ( is-nonnegative-mul-ℤ - ( is-nonnegative-is-positive-ℤ - ( is-positive-denominator-fraction-ℤ p)) - ( H')) - ( is-positive-mul-ℤ - ( is-positive-denominator-fraction-ℤ r) - ( H)))) - ( is-positive-denominator-fraction-ℤ q) - - concatenate-leq-le-fraction-ℤ : - leq-fraction-ℤ p q → - le-fraction-ℤ q r → - le-fraction-ℤ p r - concatenate-leq-le-fraction-ℤ H H' = - is-positive-right-factor-mul-ℤ - ( is-positive-eq-ℤ - ( lemma-add-cross-mul-diff-fraction-ℤ p q r) - ( is-positive-add-positive-nonnegative-ℤ - ( is-positive-mul-ℤ - ( is-positive-denominator-fraction-ℤ p) - ( H')) - ( is-nonnegative-mul-ℤ - ( is-nonnegative-is-positive-ℤ - ( is-positive-denominator-fraction-ℤ r)) - ( H)))) - ( is-positive-denominator-fraction-ℤ q) -``` - -### Chaining rules for similarity and strict inequality on integer fractions - -```agda -module _ - (p q r : fraction-ℤ) - where - - concatenate-sim-le-fraction-ℤ : - sim-fraction-ℤ p q → - le-fraction-ℤ q r → - le-fraction-ℤ p r - concatenate-sim-le-fraction-ℤ H H' = - is-positive-right-factor-mul-ℤ - ( is-positive-eq-ℤ - ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H) - ( is-positive-mul-ℤ - ( is-positive-denominator-fraction-ℤ p) H')) - ( is-positive-denominator-fraction-ℤ q) - - concatenate-le-sim-fraction-ℤ : - le-fraction-ℤ p q → - sim-fraction-ℤ q r → - le-fraction-ℤ p r - concatenate-le-sim-fraction-ℤ H H' = - is-positive-right-factor-mul-ℤ - ( is-positive-eq-ℤ - ( inv ( lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H')) - ( is-positive-mul-ℤ (is-positive-denominator-fraction-ℤ r) H)) - ( is-positive-denominator-fraction-ℤ q) -``` - -### Fractions with equal denominator compare the same as their numerators - -```agda -module _ - (x y : fraction-ℤ) (H : denominator-fraction-ℤ x ＝ denominator-fraction-ℤ y) - where - - le-fraction-le-numerator-fraction-ℤ : - le-ℤ (numerator-fraction-ℤ x) (numerator-fraction-ℤ y) → - le-fraction-ℤ x y - le-fraction-le-numerator-fraction-ℤ H' = - tr - ( λ (k : ℤ) → - le-ℤ - ( numerator-fraction-ℤ x *ℤ k) - ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)) - ( H) - ( preserves-strict-order-mul-positive-ℤ' - { numerator-fraction-ℤ x} - { numerator-fraction-ℤ y} - ( denominator-fraction-ℤ x) - ( is-positive-denominator-fraction-ℤ x) - ( H')) -``` - -### The mediant of two fractions is between them - -```agda -module _ - (x y : fraction-ℤ) - where - - le-left-mediant-fraction-ℤ : - le-fraction-ℤ x y → - le-fraction-ℤ x (mediant-fraction-ℤ x y) - le-left-mediant-fraction-ℤ = - is-positive-eq-ℤ (cross-mul-diff-left-mediant-fraction-ℤ x y) - - le-right-mediant-fraction-ℤ : - le-fraction-ℤ x y → - le-fraction-ℤ (mediant-fraction-ℤ x y) y - le-right-mediant-fraction-ℤ = - is-positive-eq-ℤ (cross-mul-diff-right-mediant-fraction-ℤ x y) -``` diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md index 3eb990d983..58ca328611 100644 --- a/src/elementary-number-theory/inequality-integers.lagda.md +++ b/src/elementary-number-theory/inequality-integers.lagda.md @@ -8,13 +8,21 @@ module elementary-number-theory.inequality-integers where ```agda open import elementary-number-theory.addition-integers +open import elementary-number-theory.addition-positive-and-negative-integers open import elementary-number-theory.difference-integers open import elementary-number-theory.inequality-natural-numbers open import elementary-number-theory.integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.negative-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-functions open import foundation.coproduct-types +open import foundation.decidable-propositions +open import foundation.dependent-pair-types open import foundation.function-types open import foundation.functoriality-coproduct-types open import foundation.identity-types @@ -24,15 +32,30 @@ open import foundation.propositions open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels + +open import order-theory.posets +open import order-theory.preorders ``` +## Idea + +An [integer](elementary-number-theory.integers.md) `x` is _less than or equal_ +to the integer `y` if the +[difference](elementary-number-theory.difference-integers.md) `y - x` is +[nonnegative](elementary-number-theory.nonnegative-integers.md). This relation +defines the +{{#concept "standard ordering" Disambiguation="integers" Agda=leq-ℤ}} on the +integers. + ## Definition +### Inequality on the integers + ```agda leq-ℤ-Prop : ℤ → ℤ → Prop lzero -leq-ℤ-Prop x y = is-nonnegative-ℤ-Prop (y -ℤ x) +leq-ℤ-Prop x y = subtype-nonnegative-ℤ (y -ℤ x) leq-ℤ : ℤ → ℤ → UU lzero leq-ℤ x y = type-Prop (leq-ℤ-Prop x y) @@ -46,6 +69,8 @@ _≤-ℤ_ = leq-ℤ ## Properties +### Inequality on the integers is reflexive, antisymmetric and transitive + ```agda refl-leq-ℤ : (k : ℤ) → leq-ℤ k k refl-leq-ℤ k = tr is-nonnegative-ℤ (inv (right-inverse-law-add-ℤ k)) star @@ -53,27 +78,47 @@ refl-leq-ℤ k = tr is-nonnegative-ℤ (inv (right-inverse-law-add-ℤ k)) star antisymmetric-leq-ℤ : {x y : ℤ} → leq-ℤ x y → leq-ℤ y x → x ＝ y antisymmetric-leq-ℤ {x} {y} H K = eq-diff-ℤ - ( is-zero-is-nonnegative-ℤ K + ( is-zero-is-nonnegative-neg-is-nonnegative-ℤ K ( is-nonnegative-eq-ℤ (inv (distributive-neg-diff-ℤ x y)) H)) -transitive-leq-ℤ : (k l m : ℤ) → leq-ℤ k l → leq-ℤ l m → leq-ℤ k m -transitive-leq-ℤ k l m p q = - tr is-nonnegative-ℤ +transitive-leq-ℤ : (k l m : ℤ) → leq-ℤ l m → leq-ℤ k l → leq-ℤ k m +transitive-leq-ℤ k l m H K = + is-nonnegative-eq-ℤ ( triangle-diff-ℤ m l k) - ( is-nonnegative-add-ℤ - ( m +ℤ (neg-ℤ l)) - ( l +ℤ (neg-ℤ k)) - ( q) - ( p)) - -decide-leq-ℤ : - {x y : ℤ} → (leq-ℤ x y) + (leq-ℤ y x) -decide-leq-ℤ {x} {y} = + ( is-nonnegative-add-ℤ H K) +``` + +### Inequality on the integers is decidable + +```agda +is-decidable-leq-ℤ : (x y : ℤ) → (leq-ℤ x y) + ¬ (leq-ℤ x y) +is-decidable-leq-ℤ x y = is-decidable-is-nonnegative-ℤ (y -ℤ x) + +leq-ℤ-Decidable-Prop : (x y : ℤ) → Decidable-Prop lzero +leq-ℤ-Decidable-Prop x y = + ( leq-ℤ x y , + is-prop-leq-ℤ x y , + is-decidable-leq-ℤ x y) +``` + +### Inequality on the integers is linear + +```agda +linear-leq-ℤ : (x y : ℤ) → (leq-ℤ x y) + (leq-ℤ y x) +linear-leq-ℤ x y = map-coproduct + ( λ H → + is-nonnegative-is-positive-ℤ + ( is-positive-eq-ℤ + ( distributive-neg-diff-ℤ x y) + ( is-positive-neg-is-negative-ℤ H))) ( id) - ( is-nonnegative-eq-ℤ (distributive-neg-diff-ℤ y x)) - ( decide-is-nonnegative-ℤ {y -ℤ x}) + ( decide-is-negative-is-nonnegative-ℤ) +``` + +### An integer is lesser than its successor +```agda succ-leq-ℤ : (k : ℤ) → leq-ℤ k (succ-ℤ k) succ-leq-ℤ k = is-nonnegative-eq-ℤ @@ -83,8 +128,12 @@ succ-leq-ℤ k = ( star) leq-ℤ-succ-leq-ℤ : (k l : ℤ) → leq-ℤ k l → leq-ℤ k (succ-ℤ l) -leq-ℤ-succ-leq-ℤ k l p = transitive-leq-ℤ k l (succ-ℤ l) p (succ-leq-ℤ l) +leq-ℤ-succ-leq-ℤ k l = transitive-leq-ℤ k l (succ-ℤ l) (succ-leq-ℤ l) +``` +### Chaining rules for equality and inequality + +```agda concatenate-eq-leq-eq-ℤ : {x' x y y' : ℤ} → x' ＝ x → leq-ℤ x y → y ＝ y' → leq-ℤ x' y' concatenate-eq-leq-eq-ℤ refl H refl = H @@ -98,71 +147,17 @@ concatenate-eq-leq-ℤ : concatenate-eq-leq-ℤ y refl H = H ``` -### The strict ordering on ℤ - -```agda -le-ℤ-Prop : ℤ → ℤ → Prop lzero -le-ℤ-Prop x y = is-positive-ℤ-Prop (y -ℤ x) - -le-ℤ : ℤ → ℤ → UU lzero -le-ℤ x y = type-Prop (le-ℤ-Prop x y) - -is-prop-le-ℤ : (x y : ℤ) → is-prop (le-ℤ x y) -is-prop-le-ℤ x y = is-prop-type-Prop (le-ℤ-Prop x y) -``` - -## Properties +### Addition on the integers preserves inequality ```agda -transitive-le-ℤ : (k l m : ℤ) → le-ℤ k l → le-ℤ l m → le-ℤ k m -transitive-le-ℤ k l m p q = - tr is-positive-ℤ - ( triangle-diff-ℤ m l k) - ( is-positive-add-ℤ q p) - -asymmetric-le-ℤ : (x y : ℤ) → le-ℤ x y → ¬ (le-ℤ y x) -asymmetric-le-ℤ x y p q = - not-is-nonpositive-is-positive-ℤ - ( y -ℤ x) - ( p) - ( is-nonnegative-is-positive-ℤ - ( is-positive-eq-ℤ - ( inv ( distributive-neg-diff-ℤ y x)) - ( q))) - -connected-le-ℤ : (x y : ℤ) → x ≠ y → le-ℤ x y + le-ℤ y x -connected-le-ℤ x y H = - map-coproduct - ( id) - ( is-positive-eq-ℤ ( distributive-neg-diff-ℤ y x)) - ( decide-is-positive-is-nonzero-ℤ (y -ℤ x) (H ∘ inv ∘ eq-diff-ℤ)) - -le-pred-ℤ : (x : ℤ) → le-ℤ (pred-ℤ x) x -le-pred-ℤ x = - is-positive-eq-ℤ - ( inv - ( right-predecessor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x))) - ( is-positive-one-ℤ) - -le-succ-ℤ : (x : ℤ) → le-ℤ x (succ-ℤ x) -le-succ-ℤ x = - is-positive-eq-ℤ - ( inv - ( left-successor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x))) - ( is-positive-one-ℤ) -``` - -### ℤ is an ordered ring - -```agda -preserves-order-add-ℤ' : - {x y : ℤ} (z : ℤ) → leq-ℤ x y → leq-ℤ (x +ℤ z) (y +ℤ z) -preserves-order-add-ℤ' {x} {y} z = +preserves-leq-left-add-ℤ : + (z x y : ℤ) → leq-ℤ x y → leq-ℤ (x +ℤ z) (y +ℤ z) +preserves-leq-left-add-ℤ z x y = is-nonnegative-eq-ℤ (inv (right-translation-diff-ℤ y x z)) -preserves-order-add-ℤ : - {x y : ℤ} (z : ℤ) → leq-ℤ x y → leq-ℤ (z +ℤ x) (z +ℤ y) -preserves-order-add-ℤ {x} {y} z = +preserves-leq-right-add-ℤ : + (z x y : ℤ) → leq-ℤ x y → leq-ℤ (z +ℤ x) (z +ℤ y) +preserves-leq-right-add-ℤ z x y = is-nonnegative-eq-ℤ (inv (left-translation-diff-ℤ y x z)) preserves-leq-add-ℤ : @@ -172,55 +167,25 @@ preserves-leq-add-ℤ {a} {b} {c} {d} H K = ( a +ℤ c) ( b +ℤ c) ( b +ℤ d) - ( preserves-order-add-ℤ' {a} {b} c H) - ( preserves-order-add-ℤ b K) - -reflects-order-add-ℤ' : - {x y z : ℤ} → leq-ℤ (x +ℤ z) (y +ℤ z) → leq-ℤ x y -reflects-order-add-ℤ' {x} {y} {z} = - is-nonnegative-eq-ℤ (right-translation-diff-ℤ y x z) - -reflects-order-add-ℤ : - {x y z : ℤ} → leq-ℤ (z +ℤ x) (z +ℤ y) → leq-ℤ x y -reflects-order-add-ℤ {x} {y} {z} = - is-nonnegative-eq-ℤ (left-translation-diff-ℤ y x z) + ( preserves-leq-right-add-ℤ b c d K) + ( preserves-leq-left-add-ℤ c a b H) ``` -### Addition on the integers preserves and reflects the strict ordering +### Addition on the integers reflects inequality ```agda -preserves-strict-order-add-ℤ' : - {x y : ℤ} (z : ℤ) → le-ℤ x y → le-ℤ (x +ℤ z) (y +ℤ z) -preserves-strict-order-add-ℤ' {x} {y} z = - is-positive-eq-ℤ (inv (right-translation-diff-ℤ y x z)) - -preserves-strict-order-add-ℤ : - {x y : ℤ} (z : ℤ) → le-ℤ x y → le-ℤ (z +ℤ x) (z +ℤ y) -preserves-strict-order-add-ℤ {x} {y} z = - is-positive-eq-ℤ (inv (left-translation-diff-ℤ y x z)) - -preserves-le-add-ℤ : - {a b c d : ℤ} → le-ℤ a b → le-ℤ c d → le-ℤ (a +ℤ c) (b +ℤ d) -preserves-le-add-ℤ {a} {b} {c} {d} H K = - transitive-le-ℤ - ( a +ℤ c) - ( b +ℤ c) - ( b +ℤ d) - ( preserves-strict-order-add-ℤ' {a} {b} c H) - ( preserves-strict-order-add-ℤ b K) - -reflects-strict-order-add-ℤ' : - {x y z : ℤ} → le-ℤ (x +ℤ z) (y +ℤ z) → le-ℤ x y -reflects-strict-order-add-ℤ' {x} {y} {z} = - is-positive-eq-ℤ (right-translation-diff-ℤ y x z) - -reflects-strict-order-add-ℤ : - {x y z : ℤ} → le-ℤ (z +ℤ x) (z +ℤ y) → le-ℤ x y -reflects-strict-order-add-ℤ {x} {y} {z} = - is-positive-eq-ℤ (left-translation-diff-ℤ y x z) +reflects-leq-left-add-ℤ : + (z x y : ℤ) → leq-ℤ (x +ℤ z) (y +ℤ z) → leq-ℤ x y +reflects-leq-left-add-ℤ z x y = + is-nonnegative-eq-ℤ (right-translation-diff-ℤ y x z) + +reflects-leq-right-add-ℤ : + (z x y : ℤ) → leq-ℤ (z +ℤ x) (z +ℤ y) → leq-ℤ x y +reflects-leq-right-add-ℤ z x y = + is-nonnegative-eq-ℤ (left-translation-diff-ℤ y x z) ``` -### Inclusion of ℕ into ℤ preserves order +### The inclusion of ℕ into ℤ preserves inequality ```agda leq-int-ℕ : (x y : ℕ) → leq-ℕ x y → leq-ℤ (int-ℕ x) (int-ℕ y) @@ -233,5 +198,23 @@ leq-int-ℕ (succ-ℕ x) (succ-ℕ y) H = tr (is-nonnegative-ℤ) ( inv (diff-succ-ℤ (int-ℕ y) (int-ℕ x)) ∙ ( ap (_-ℤ (succ-ℤ (int-ℕ x))) (succ-int-ℕ y) ∙ ap ((int-ℕ (succ-ℕ y)) -ℤ_) (succ-int-ℕ x))) - (leq-int-ℕ x y H) + ( leq-int-ℕ x y H) ``` + +### The partially ordered set of integers ordered by inequality + +```agda +ℤ-Preorder : Preorder lzero lzero +ℤ-Preorder = + (ℤ , leq-ℤ-Prop , refl-leq-ℤ , transitive-leq-ℤ) + +ℤ-Poset : Poset lzero lzero +ℤ-Poset = (ℤ-Preorder , λ x y → antisymmetric-leq-ℤ) +``` + +## See also + +- The decidable total order on the integers is defined in + [`decidable-total-order-integers`](elementary-number-theory.decidable-total-order-integers.md) +- Strict inequality on the integers is defined in + [`strict-inequality-integers`](elementary-number-theory.strict-inequality-integers.md) diff --git a/src/elementary-number-theory/inequality-natural-numbers.lagda.md b/src/elementary-number-theory/inequality-natural-numbers.lagda.md index ec0f031359..c2d8117480 100644 --- a/src/elementary-number-theory/inequality-natural-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-natural-numbers.lagda.md @@ -40,7 +40,7 @@ less than any natural number, and such that `m+1 ≤ n+1` is equivalent to ## Definitions -### The partial ordering on ℕ +### Inequality on the natural numbers ```agda leq-ℕ : ℕ → ℕ → UU lzero @@ -52,7 +52,7 @@ infix 30 _≤-ℕ_ _≤-ℕ_ = leq-ℕ ``` -### Alternative definition of the partial ordering on ℕ +### Alternative definition of the inequality on the natural numbers ```agda data leq-ℕ' : ℕ → ℕ → UU lzero where @@ -62,7 +62,7 @@ data leq-ℕ' : ℕ → ℕ → UU lzero where ## Properties -### Inequality on ℕ is a proposition +### Inequality on the natural numbers is a proposition ```agda is-prop-leq-ℕ : @@ -77,7 +77,7 @@ pr1 (leq-ℕ-Prop m n) = leq-ℕ m n pr2 (leq-ℕ-Prop m n) = is-prop-leq-ℕ m n ``` -### The partial ordering on the natural numbers is decidable +### Inequality on the natural numbers is decidable ```agda is-decidable-leq-ℕ : @@ -88,7 +88,7 @@ is-decidable-leq-ℕ (succ-ℕ m) zero-ℕ = inr id is-decidable-leq-ℕ (succ-ℕ m) (succ-ℕ n) = is-decidable-leq-ℕ m n ``` -### The partial ordering on ℕ is a congruence +### Inequality on the natural numbers is a congruence ```agda concatenate-eq-leq-eq-ℕ : @@ -104,7 +104,7 @@ concatenate-eq-leq-ℕ : concatenate-eq-leq-ℕ n refl H = H ``` -### Reflexivity +### Inequality on the natural numbers is reflexive ```agda refl-leq-ℕ : (n : ℕ) → n ≤-ℕ n @@ -115,7 +115,7 @@ leq-eq-ℕ : (m n : ℕ) → m ＝ n → m ≤-ℕ n leq-eq-ℕ m .m refl = refl-leq-ℕ m ``` -### Transitivity +### Inequality on the natural numbers is transitive ```agda transitive-leq-ℕ : is-transitive leq-ℕ @@ -124,7 +124,7 @@ transitive-leq-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q = transitive-leq-ℕ n m l p q ``` -### Antisymmetry +### Inequality on the natural numbers is antisymmetric ```agda antisymmetric-leq-ℕ : (m n : ℕ) → m ≤-ℕ n → n ≤-ℕ m → m ＝ n @@ -133,7 +133,7 @@ antisymmetric-leq-ℕ (succ-ℕ m) (succ-ℕ n) p q = ap succ-ℕ (antisymmetric-leq-ℕ m n p q) ``` -### The poset of natural numbers +### The partially ordered set of natural numbers ordered by inequality ```agda ℕ-Preorder : Preorder lzero lzero @@ -229,7 +229,7 @@ succ-leq-ℕ zero-ℕ = star succ-leq-ℕ (succ-ℕ n) = succ-leq-ℕ n ``` -### An natural number less than `n+1` is either less than `n` or it is `n+1` +### Any natural number less than or equal to `n+1` is either less than or equal to `n` or it is `n+1` ```agda decide-leq-succ-ℕ : @@ -287,19 +287,19 @@ contradiction-leq-ℕ' : (m n : ℕ) → (succ-ℕ n) ≤-ℕ m → ¬ (m ≤- contradiction-leq-ℕ' m n K H = contradiction-leq-ℕ m n H K ``` -### Addition preserves inequality +### Addition preserves inequality of natural numbers ```agda -left-law-leq-add-ℕ : +preserves-leq-left-add-ℕ : (k m n : ℕ) → m ≤-ℕ n → (m +ℕ k) ≤-ℕ (n +ℕ k) -left-law-leq-add-ℕ zero-ℕ m n = id -left-law-leq-add-ℕ (succ-ℕ k) m n H = left-law-leq-add-ℕ k m n H +preserves-leq-left-add-ℕ zero-ℕ m n = id +preserves-leq-left-add-ℕ (succ-ℕ k) m n H = preserves-leq-left-add-ℕ k m n H -right-law-leq-add-ℕ : (k m n : ℕ) → m ≤-ℕ n → (k +ℕ m) ≤-ℕ (k +ℕ n) -right-law-leq-add-ℕ k m n H = +preserves-leq-right-add-ℕ : (k m n : ℕ) → m ≤-ℕ n → (k +ℕ m) ≤-ℕ (k +ℕ n) +preserves-leq-right-add-ℕ k m n H = concatenate-eq-leq-eq-ℕ ( commutative-add-ℕ k m) - ( left-law-leq-add-ℕ k m n H) + ( preserves-leq-left-add-ℕ k m n H) ( commutative-add-ℕ n k) preserves-leq-add-ℕ : @@ -309,22 +309,22 @@ preserves-leq-add-ℕ {m} {m'} {n} {n'} H K = ( m +ℕ n) ( m' +ℕ n) ( m' +ℕ n') - ( right-law-leq-add-ℕ m' n n' K) - ( left-law-leq-add-ℕ n m m' H) + ( preserves-leq-right-add-ℕ m' n n' K) + ( preserves-leq-left-add-ℕ n m m' H) ``` -### Addition reflects the ordering on ℕ +### Addition reflects inequality of natural numbers ```agda -reflects-order-add-ℕ : +reflects-leq-left-add-ℕ : (k m n : ℕ) → (m +ℕ k) ≤-ℕ (n +ℕ k) → m ≤-ℕ n -reflects-order-add-ℕ zero-ℕ m n = id -reflects-order-add-ℕ (succ-ℕ k) m n = reflects-order-add-ℕ k m n +reflects-leq-left-add-ℕ zero-ℕ m n = id +reflects-leq-left-add-ℕ (succ-ℕ k) m n = reflects-leq-left-add-ℕ k m n -reflects-order-add-ℕ' : +reflects-leq-right-add-ℕ : (k m n : ℕ) → (k +ℕ m) ≤-ℕ (k +ℕ n) → m ≤-ℕ n -reflects-order-add-ℕ' k m n H = - reflects-order-add-ℕ k m n +reflects-leq-right-add-ℕ k m n H = + reflects-leq-left-add-ℕ k m n ( concatenate-eq-leq-eq-ℕ ( commutative-add-ℕ m k) ( H) @@ -365,30 +365,26 @@ leq-subtraction-ℕ (succ-ℕ n) (succ-ℕ m) l p = leq-subtraction-ℕ n m l (is-injective-succ-ℕ p) ``` -### Multiplication preserves the ordering on ℕ +### Multiplication preserves inequality of natural numbers ```agda -preserves-order-mul-ℕ : +preserves-leq-left-mul-ℕ : (k m n : ℕ) → m ≤-ℕ n → (m *ℕ k) ≤-ℕ (n *ℕ k) -preserves-order-mul-ℕ k zero-ℕ n p = star -preserves-order-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p = - left-law-leq-add-ℕ k +preserves-leq-left-mul-ℕ k zero-ℕ n p = star +preserves-leq-left-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p = + preserves-leq-left-add-ℕ k ( m *ℕ k) ( n *ℕ k) - ( preserves-order-mul-ℕ k m n p) + ( preserves-leq-left-mul-ℕ k m n p) -preserves-order-mul-ℕ' : +preserves-leq-right-mul-ℕ : (k m n : ℕ) → m ≤-ℕ n → (k *ℕ m) ≤-ℕ (k *ℕ n) -preserves-order-mul-ℕ' k m n H = +preserves-leq-right-mul-ℕ k m n H = concatenate-eq-leq-eq-ℕ ( commutative-mul-ℕ k m) - ( preserves-order-mul-ℕ k m n H) + ( preserves-leq-left-mul-ℕ k m n H) ( commutative-mul-ℕ n k) -``` - -### Multiplication preserves inequality -```agda preserves-leq-mul-ℕ : (m m' n n' : ℕ) → m ≤-ℕ m' → n ≤-ℕ n' → (m *ℕ n) ≤-ℕ (m' *ℕ n') preserves-leq-mul-ℕ m m' n n' H K = @@ -396,11 +392,11 @@ preserves-leq-mul-ℕ m m' n n' H K = ( m *ℕ n) ( m' *ℕ n) ( m' *ℕ n') - ( preserves-order-mul-ℕ' m' n n' K) - ( preserves-order-mul-ℕ n m m' H) + ( preserves-leq-right-mul-ℕ m' n n' K) + ( preserves-leq-left-mul-ℕ n m m' H) ``` -### Multiplication by a nonzero element reflects the ordering on ℕ +### Multiplication by a nonzero natural number reflects inequality of natural numbers ```agda reflects-order-mul-ℕ : @@ -408,7 +404,7 @@ reflects-order-mul-ℕ : reflects-order-mul-ℕ k zero-ℕ n p = star reflects-order-mul-ℕ k (succ-ℕ m) (succ-ℕ n) p = reflects-order-mul-ℕ k m n - ( reflects-order-add-ℕ + ( reflects-leq-left-add-ℕ ( succ-ℕ k) ( m *ℕ (succ-ℕ k)) ( n *ℕ (succ-ℕ k)) @@ -433,7 +429,7 @@ leq-mul-ℕ k x = concatenate-eq-leq-ℕ ( x *ℕ (succ-ℕ k)) ( inv (right-unit-law-mul-ℕ x)) - ( preserves-order-mul-ℕ' x 1 (succ-ℕ k) (leq-zero-ℕ k)) + ( preserves-leq-right-mul-ℕ x 1 (succ-ℕ k) (leq-zero-ℕ k)) leq-mul-ℕ' : (k x : ℕ) → x ≤-ℕ ((succ-ℕ k) *ℕ x) diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md index 12c55dad2c..0919f81e72 100644 --- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md @@ -8,37 +8,47 @@ module elementary-number-theory.inequality-rational-numbers where ```agda open import elementary-number-theory.cross-multiplication-difference-integer-fractions +open import elementary-number-theory.difference-integers open import elementary-number-theory.inequality-integer-fractions open import elementary-number-theory.inequality-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers -open import elementary-number-theory.mediant-integer-fractions open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import elementary-number-theory.rational-numbers -open import elementary-number-theory.reduced-integer-fractions -open import foundation.binary-relations open import foundation.cartesian-product-types open import foundation.coproduct-types +open import foundation.decidable-propositions open import foundation.dependent-pair-types -open import foundation.disjunction -open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-coproduct-types open import foundation.identity-types open import foundation.negation -open import foundation.propositional-truncations open import foundation.propositions open import foundation.universe-levels + +open import order-theory.posets +open import order-theory.preorders ``` ## Idea -A rational number `x` is less (or equal) to a rational number `y` if and only if -the underlying fraction of `x` is less (or equal) than the underlying fraction -of `y`. +The +{{#concept "standard ordering" Disambiguation="rational numbers" Agda=leq-ℚ}} on +the [rational numbers](elementary-number-theory.rational-numbers.md) is +inherited from the +[standard ordering](elementary-number-theory.inequality-integer-fractions.md) on +[integer fractions](elementary-number-theory.integer-fractions.md): the rational +number `m / n` is _less than or equal to_ `m' / n'` if the +[integer product](elementary-number-theory.multiplication-integers.md) `m * n'` +is [less than or equal](elementary-number-theory.inequality-integers.md) to +`m' * n`. ## Definition @@ -58,22 +68,23 @@ infix 30 _≤-ℚ_ _≤-ℚ_ = leq-ℚ ``` -### Strict inequality on the rational numbers - -```agda -le-ℚ-Prop : ℚ → ℚ → Prop lzero -le-ℚ-Prop (x , px) (y , py) = le-fraction-ℤ-Prop x y +## Properties -le-ℚ : ℚ → ℚ → UU lzero -le-ℚ x y = type-Prop (le-ℚ-Prop x y) +### Inequality on the rational numbers is decidable -is-prop-le-ℚ : (x y : ℚ) → is-prop (le-ℚ x y) -is-prop-le-ℚ x y = is-prop-type-Prop (le-ℚ-Prop x y) +```agda +is-decidable-leq-ℚ : (x y : ℚ) → (leq-ℚ x y) + ¬ (leq-ℚ x y) +is-decidable-leq-ℚ x y = + is-decidable-leq-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) + +leq-ℚ-Decidable-Prop : (x y : ℚ) → Decidable-Prop lzero +leq-ℚ-Decidable-Prop x y = + ( leq-ℚ x y , + is-prop-leq-ℚ x y , + is-decidable-leq-ℚ x y) ``` -## Properties - -### Inequality on rational numbers is reflexive +### Inequality on the rational numbers is reflexive ```agda refl-leq-ℚ : (x : ℚ) → leq-ℚ x x @@ -81,13 +92,13 @@ refl-leq-ℚ x = refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x) ``` -### Inequality on rational numbers is antisymmetric +### Inequality on the rational numbers is antisymmetric ```agda antisymmetric-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ y x → x ＝ y antisymmetric-leq-ℚ x y H H' = ( inv (in-fraction-fraction-ℚ x)) ∙ - ( eq-ℚ-sim-fractions-ℤ + ( eq-ℚ-sim-fraction-ℤ ( fraction-ℚ x) ( fraction-ℚ y) ( is-sim-antisymmetric-leq-fraction-ℤ @@ -98,198 +109,50 @@ antisymmetric-leq-ℚ x y H H' = ( in-fraction-fraction-ℚ y) ``` -### Strict inequality on rationals is asymmetric +### Inequality on the rational numbers is linear ```agda -asymmetric-le-ℚ : (x y : ℚ) → le-ℚ x y → ¬ (le-ℚ y x) -asymmetric-le-ℚ x y = - asymmetric-le-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - -irreflexive-le-ℚ : (x : ℚ) → ¬ (le-ℚ x x) -irreflexive-le-ℚ = - is-irreflexive-is-asymmetric le-ℚ asymmetric-le-ℚ +linear-leq-ℚ : (x y : ℚ) → (leq-ℚ x y) + (leq-ℚ y x) +linear-leq-ℚ x y = + map-coproduct + ( id) + ( is-nonnegative-eq-ℤ + (distributive-neg-diff-ℤ + ( numerator-ℚ y *ℤ denominator-ℚ x) + ( numerator-ℚ x *ℤ denominator-ℚ y))) + ( decide-is-nonnegative-is-nonnegative-neg-ℤ + { cross-mul-diff-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)}) ``` -### Transitivity properties +### Inequality on the rational numbers is transitive ```agda module _ (x y z : ℚ) where - transitive-leq-ℚ : leq-ℚ x y → leq-ℚ y z → leq-ℚ x z + transitive-leq-ℚ : leq-ℚ y z → leq-ℚ x y → leq-ℚ x z transitive-leq-ℚ = transitive-leq-fraction-ℤ ( fraction-ℚ x) ( fraction-ℚ y) ( fraction-ℚ z) - - transitive-le-ℚ : le-ℚ x y → le-ℚ y z → le-ℚ x z - transitive-le-ℚ = - transitive-le-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - ( fraction-ℚ z) - - concatenate-le-leq-ℚ : le-ℚ x y → leq-ℚ y z → le-ℚ x z - concatenate-le-leq-ℚ = - concatenate-le-leq-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - ( fraction-ℚ z) - - concatenate-leq-le-ℚ : leq-ℚ x y → le-ℚ y z → le-ℚ x z - concatenate-leq-le-ℚ = - concatenate-leq-le-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y) - ( fraction-ℚ z) ``` -### Strict inequality on the rational numbers reflects strict inequality on the underlying fractions +### The partially ordered set of rational numbers ordered by inequality ```agda -module _ - (x : ℚ) (p : fraction-ℤ) - where +ℚ-Preorder : Preorder lzero lzero +ℚ-Preorder = + (ℚ , leq-ℚ-Prop , refl-leq-ℚ , transitive-leq-ℚ) - right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : - le-fraction-ℤ (fraction-ℚ x) p → - le-ℚ x (in-fraction-ℤ p) - right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ H = - concatenate-le-sim-fraction-ℤ - ( fraction-ℚ x) - ( p) - ( fraction-ℚ ( in-fraction-ℤ p)) - ( H) - ( sim-reduced-fraction-ℤ p) - - left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : - le-fraction-ℤ p (fraction-ℚ x) → - le-ℚ (in-fraction-ℤ p) x - left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ = - concatenate-sim-le-fraction-ℤ - ( fraction-ℚ ( in-fraction-ℤ p)) - ( p) - ( fraction-ℚ x) - ( symmetric-sim-fraction-ℤ - ( p) - ( fraction-ℚ ( in-fraction-ℤ p)) - ( sim-reduced-fraction-ℤ p)) +ℚ-Poset : Poset lzero lzero +ℚ-Poset = (ℚ-Preorder , antisymmetric-leq-ℚ) ``` -### The rational numbers have no lower or upper bound +## See also -```agda -module _ - (x : ℚ) - where - - left-∃-le-ℚ : ∃ ℚ (λ q → le-ℚ q x) - left-∃-le-ℚ = intro-∃ - ( in-fraction-ℤ frac) - ( left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac - ( le-fraction-le-numerator-fraction-ℤ - ( frac) - ( fraction-ℚ x) - ( refl) - ( le-pred-ℤ (numerator-ℚ x)))) - where - frac : fraction-ℤ - frac = pred-ℤ (numerator-ℚ x) , positive-denominator-ℚ x - - right-∃-le-ℚ : ∃ ℚ (λ r → le-ℚ x r) - right-∃-le-ℚ = intro-∃ - ( in-fraction-ℤ frac) - ( right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac - ( le-fraction-le-numerator-fraction-ℤ - ( fraction-ℚ x) - ( frac) - ( refl) - ( le-succ-ℤ (numerator-ℚ x)))) - where - frac : fraction-ℤ - frac = succ-ℤ (numerator-ℚ x) , positive-denominator-ℚ x -``` - -### Decidability of strict inequality on the rationals - -```agda -decide-le-leq-ℚ : (x y : ℚ) → le-ℚ x y + leq-ℚ y x -decide-le-leq-ℚ x y = - map-coproduct - ( id) - ( is-nonnegative-eq-ℤ - ( skew-commutative-cross-mul-diff-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y))) - ( decide-is-positive-ℤ - { cross-mul-diff-fraction-ℤ - ( fraction-ℚ x) - ( fraction-ℚ y)}) -``` - -It remains to fully formalize that strict inequality is decidable. - -### Trichotomy on the rationals - -```agda -trichotomy-le-ℚ : - {l : Level} {A : UU l} (x y : ℚ) → - ( le-ℚ x y → A) → - ( Id x y → A) → - ( le-ℚ y x → A) → - A -trichotomy-le-ℚ x y left eq right with decide-le-leq-ℚ x y | decide-le-leq-ℚ y x -... | inl I | _ = left I -... | inr I | inl I' = right I' -... | inr I | inr I' = eq (antisymmetric-leq-ℚ x y I' I) -``` - -### The mediant of two rationals is between them - -```agda -module _ - (x y : ℚ) (H : le-ℚ x y) - where - - le-left-mediant-ℚ : le-ℚ x (mediant-ℚ x y) - le-left-mediant-ℚ = - right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x - ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) - ( le-left-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) - - le-right-mediant-ℚ : le-ℚ (mediant-ℚ x y) y - le-right-mediant-ℚ = - left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ y - ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) - ( le-right-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) -``` - -### Strict inequality on the rationals is dense - -```agda -module _ - (x y : ℚ) (H : le-ℚ x y) - where - - dense-le-ℚ : ∃ ℚ (λ r → le-ℚ x r × le-ℚ r y) - dense-le-ℚ = - intro-∃ - ( mediant-ℚ x y) - ( le-left-mediant-ℚ x y H , le-right-mediant-ℚ x y H) -``` - -### The strict order on the rationals is located - -```agda -located-le-ℚ : (x y z : ℚ) → le-ℚ y z → (le-ℚ-Prop y x) ∨ (le-ℚ-Prop x z) -located-le-ℚ x y z H = - unit-trunc-Prop - ( map-coproduct - ( id) - ( λ p → concatenate-leq-le-ℚ x y z p H) - ( decide-le-leq-ℚ y x)) -``` +- The decidable total order on the rational numbers is defined in + [`decidable-total-order-rational-numbers](elementary-number-theory.decidable-total-order-rational-numbers.md) +- The strict ordering on the rational numbers is defined in + [`strict-inequality-rational-numbers`](elementary-number-theory.strict-inequality-rational-numbers.md) diff --git a/src/elementary-number-theory/integer-fractions.lagda.md b/src/elementary-number-theory/integer-fractions.lagda.md index f7c60ffceb..86be352c6c 100644 --- a/src/elementary-number-theory/integer-fractions.lagda.md +++ b/src/elementary-number-theory/integer-fractions.lagda.md @@ -11,6 +11,8 @@ open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers open import elementary-number-theory.nonzero-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-functions open import foundation.binary-relations @@ -103,9 +105,7 @@ is-one-fraction-ℤ x = (x ＝ one-fraction-ℤ) is-nonzero-denominator-fraction-ℤ : (x : fraction-ℤ) → is-nonzero-ℤ (denominator-fraction-ℤ x) is-nonzero-denominator-fraction-ℤ x = - is-nonzero-is-positive-ℤ - ( denominator-fraction-ℤ x) - ( is-positive-denominator-fraction-ℤ x) + is-nonzero-is-positive-ℤ (is-positive-denominator-fraction-ℤ x) ``` ### The type of fractions is a set @@ -207,7 +207,5 @@ is-nonzero-gcd-numerator-denominator-fraction-ℤ : (x : fraction-ℤ) → is-nonzero-ℤ (gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) is-nonzero-gcd-numerator-denominator-fraction-ℤ x = - is-nonzero-is-positive-ℤ - ( gcd-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ x)) - ( is-positive-gcd-numerator-denominator-fraction-ℤ x) + is-nonzero-is-positive-ℤ (is-positive-gcd-numerator-denominator-fraction-ℤ x) ``` diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md index 9c8b2a6150..47e3948e0f 100644 --- a/src/elementary-number-theory/integers.lagda.md +++ b/src/elementary-number-theory/integers.lagda.md @@ -72,6 +72,9 @@ zero-ℤ = inr (inl star) is-zero-ℤ : ℤ → UU lzero is-zero-ℤ x = (x ＝ zero-ℤ) + +eq-is-zero-ℤ : {a b : ℤ} → is-zero-ℤ a → is-zero-ℤ b → a ＝ b +eq-is-zero-ℤ {a} {b} H K = H ∙ inv K ``` ### Inclusion of the positive integers @@ -260,221 +263,14 @@ pred-neg-ℤ (inr (inl star)) = refl pred-neg-ℤ (inr (inr x)) = refl ``` -### Nonnegative integers - -```agda -is-nonnegative-ℤ : ℤ → UU lzero -is-nonnegative-ℤ (inl x) = empty -is-nonnegative-ℤ (inr k) = unit - -is-nonnegative-eq-ℤ : - {x y : ℤ} → x ＝ y → is-nonnegative-ℤ x → is-nonnegative-ℤ y -is-nonnegative-eq-ℤ refl = id - -is-zero-is-nonnegative-ℤ : - {x : ℤ} → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x -is-zero-is-nonnegative-ℤ {inr (inl star)} H K = refl - -is-nonnegative-succ-ℤ : - (k : ℤ) → is-nonnegative-ℤ k → is-nonnegative-ℤ (succ-ℤ k) -is-nonnegative-succ-ℤ (inr (inl star)) p = star -is-nonnegative-succ-ℤ (inr (inr x)) p = star - -is-prop-is-nonnegative-ℤ : (x : ℤ) → is-prop (is-nonnegative-ℤ x) -is-prop-is-nonnegative-ℤ (inl x) = is-prop-empty -is-prop-is-nonnegative-ℤ (inr x) = is-prop-unit - -is-nonnegative-ℤ-Prop : ℤ → Prop lzero -pr1 (is-nonnegative-ℤ-Prop x) = is-nonnegative-ℤ x -pr2 (is-nonnegative-ℤ-Prop x) = is-prop-is-nonnegative-ℤ x -``` - -### The positive integers - -```agda -is-positive-ℤ : ℤ → UU lzero -is-positive-ℤ (inl x) = empty -is-positive-ℤ (inr (inl x)) = empty -is-positive-ℤ (inr (inr x)) = unit - -is-prop-is-positive-ℤ : (x : ℤ) → is-prop (is-positive-ℤ x) -is-prop-is-positive-ℤ (inl x) = is-prop-empty -is-prop-is-positive-ℤ (inr (inl x)) = is-prop-empty -is-prop-is-positive-ℤ (inr (inr x)) = is-prop-unit - -is-positive-ℤ-Prop : ℤ → Prop lzero -pr1 (is-positive-ℤ-Prop x) = is-positive-ℤ x -pr2 (is-positive-ℤ-Prop x) = is-prop-is-positive-ℤ x - -is-set-is-positive-ℤ : (x : ℤ) → is-set (is-positive-ℤ x) -is-set-is-positive-ℤ (inl x) = is-set-empty -is-set-is-positive-ℤ (inr (inl x)) = is-set-empty -is-set-is-positive-ℤ (inr (inr x)) = is-set-unit - -is-positive-ℤ-Set : ℤ → Set lzero -pr1 (is-positive-ℤ-Set z) = is-positive-ℤ z -pr2 (is-positive-ℤ-Set z) = is-set-is-positive-ℤ z - -positive-ℤ : UU lzero -positive-ℤ = Σ ℤ is-positive-ℤ - -is-set-positive-ℤ : is-set positive-ℤ -is-set-positive-ℤ = is-set-Σ is-set-ℤ is-set-is-positive-ℤ - -positive-ℤ-Set : Set lzero -pr1 positive-ℤ-Set = positive-ℤ -pr2 positive-ℤ-Set = is-set-positive-ℤ - -int-positive-ℤ : positive-ℤ → ℤ -int-positive-ℤ = pr1 - -is-positive-int-positive-ℤ : - (x : positive-ℤ) → is-positive-ℤ (int-positive-ℤ x) -is-positive-int-positive-ℤ = pr2 - -is-nonnegative-is-positive-ℤ : {x : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ x -is-nonnegative-is-positive-ℤ {inr (inr x)} H = H - -is-positive-eq-ℤ : {x y : ℤ} → x ＝ y → is-positive-ℤ x → is-positive-ℤ y -is-positive-eq-ℤ {x} refl = id - -is-positive-one-ℤ : is-positive-ℤ one-ℤ -is-positive-one-ℤ = star - -one-positive-ℤ : positive-ℤ -pr1 one-positive-ℤ = one-ℤ -pr2 one-positive-ℤ = is-positive-one-ℤ - -is-positive-succ-ℤ : {x : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ (succ-ℤ x) -is-positive-succ-ℤ {inr (inl star)} H = is-positive-one-ℤ -is-positive-succ-ℤ {inr (inr x)} H = star - -is-positive-int-ℕ : - (x : ℕ) → is-nonzero-ℕ x → is-positive-ℤ (int-ℕ x) -is-positive-int-ℕ zero-ℕ H = ex-falso (H refl) -is-positive-int-ℕ (succ-ℕ x) H = star -``` - -### Properties of nonnegative integers - -```agda -nonnegative-ℤ : UU lzero -nonnegative-ℤ = Σ ℤ is-nonnegative-ℤ - -int-nonnegative-ℤ : nonnegative-ℤ → ℤ -int-nonnegative-ℤ = pr1 - -is-nonnegative-int-nonnegative-ℤ : - (x : nonnegative-ℤ) → is-nonnegative-ℤ (int-nonnegative-ℤ x) -is-nonnegative-int-nonnegative-ℤ = pr2 - -is-injective-int-nonnegative-ℤ : is-injective int-nonnegative-ℤ -is-injective-int-nonnegative-ℤ {pair (inr x) star} {pair (inr .x) star} refl = - refl - -is-nonnegative-int-ℕ : (n : ℕ) → is-nonnegative-ℤ (int-ℕ n) -is-nonnegative-int-ℕ zero-ℕ = star -is-nonnegative-int-ℕ (succ-ℕ n) = star - -nonnegative-int-ℕ : ℕ → nonnegative-ℤ -pr1 (nonnegative-int-ℕ n) = int-ℕ n -pr2 (nonnegative-int-ℕ n) = is-nonnegative-int-ℕ n - -nat-nonnegative-ℤ : nonnegative-ℤ → ℕ -nat-nonnegative-ℤ (pair (inr (inl x)) H) = zero-ℕ -nat-nonnegative-ℤ (pair (inr (inr x)) H) = succ-ℕ x - -is-section-nat-nonnegative-ℤ : - (x : nonnegative-ℤ) → nonnegative-int-ℕ (nat-nonnegative-ℤ x) ＝ x -is-section-nat-nonnegative-ℤ (pair (inr (inl star)) star) = refl -is-section-nat-nonnegative-ℤ (pair (inr (inr x)) star) = refl - -is-retraction-nat-nonnegative-ℤ : - (n : ℕ) → nat-nonnegative-ℤ (nonnegative-int-ℕ n) ＝ n -is-retraction-nat-nonnegative-ℤ zero-ℕ = refl -is-retraction-nat-nonnegative-ℤ (succ-ℕ n) = refl - -is-equiv-nat-nonnegative-ℤ : is-equiv nat-nonnegative-ℤ -pr1 (pr1 is-equiv-nat-nonnegative-ℤ) = nonnegative-int-ℕ -pr2 (pr1 is-equiv-nat-nonnegative-ℤ) = is-retraction-nat-nonnegative-ℤ -pr1 (pr2 is-equiv-nat-nonnegative-ℤ) = nonnegative-int-ℕ -pr2 (pr2 is-equiv-nat-nonnegative-ℤ) = is-section-nat-nonnegative-ℤ - -is-equiv-nonnegative-int-ℕ : is-equiv nonnegative-int-ℕ -pr1 (pr1 is-equiv-nonnegative-int-ℕ) = nat-nonnegative-ℤ -pr2 (pr1 is-equiv-nonnegative-int-ℕ) = is-section-nat-nonnegative-ℤ -pr1 (pr2 is-equiv-nonnegative-int-ℕ) = nat-nonnegative-ℤ -pr2 (pr2 is-equiv-nonnegative-int-ℕ) = is-retraction-nat-nonnegative-ℤ - -equiv-nonnegative-int-ℕ : ℕ ≃ nonnegative-ℤ -pr1 equiv-nonnegative-int-ℕ = nonnegative-int-ℕ -pr2 equiv-nonnegative-int-ℕ = is-equiv-nonnegative-int-ℕ - -is-injective-nonnegative-int-ℕ : is-injective nonnegative-int-ℕ -is-injective-nonnegative-int-ℕ {x} {y} p = - ( inv (is-retraction-nat-nonnegative-ℤ x)) ∙ - ( ap nat-nonnegative-ℤ p) ∙ - ( is-retraction-nat-nonnegative-ℤ y) - -decide-is-nonnegative-ℤ : - {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x)) -decide-is-nonnegative-ℤ {inl x} = inr star -decide-is-nonnegative-ℤ {inr x} = inl star - -is-zero-is-nonnegative-neg-is-nonnegative-ℤ : - (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x -is-zero-is-nonnegative-neg-is-nonnegative-ℤ (inr (inl star)) nonneg nonpos = - refl -``` - -### Properties of positive integers - -#### The positivity predicate on integers is decidable - -```agda -decide-is-positive-ℤ : {x : ℤ} → (is-positive-ℤ x) + is-nonnegative-ℤ (neg-ℤ x) -decide-is-positive-ℤ {inl x} = inr star -decide-is-positive-ℤ {inr (inl x)} = inr star -decide-is-positive-ℤ {inr (inr x)} = inl star - -decide-is-positive-is-nonzero-ℤ : - (x : ℤ) → (x ≠ zero-ℤ) → - (is-positive-ℤ x) + is-positive-ℤ (neg-ℤ x) -decide-is-positive-is-nonzero-ℤ (inl x) H = inr star -decide-is-positive-is-nonzero-ℤ (inr (inl x)) H = ex-falso (H refl) -decide-is-positive-is-nonzero-ℤ (inr (inr x)) H = inl star -``` - -This remains to be fully formalized. - -### The nonpositive integers - -```agda -is-nonpositive-ℤ : ℤ → UU lzero -is-nonpositive-ℤ x = is-nonnegative-ℤ (neg-ℤ x) -``` - -#### Positive integers are not nonpositive +### The negative function is injective ```agda -not-is-nonpositive-is-positive-ℤ : - (x : ℤ) → is-positive-ℤ x → ¬ (is-nonpositive-ℤ x) -not-is-nonpositive-is-positive-ℤ (inr (inl x)) x-is-pos _ = x-is-pos -not-is-nonpositive-is-positive-ℤ (inr (inr x)) x-is-pos neg-x-is-nonneg = - neg-x-is-nonneg -``` - -#### An integer that is not positive is nonpositive - -```agda -is-nonpositive-not-is-positive-ℤ : - (x : ℤ) → ¬ (is-positive-ℤ x) → is-nonpositive-ℤ x -is-nonpositive-not-is-positive-ℤ x H with decide-is-positive-ℤ {x} -... | inl K = ex-falso (H K) -... | inr K = K +is-injective-neg-ℤ : is-injective neg-ℤ +is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y ``` -#### Relation between successors of natural numbers and integers +### The integer successor of a natural number is the successor of the natural number ```agda succ-int-ℕ : (x : ℕ) → succ-ℤ (int-ℕ x) ＝ int-ℕ (succ-ℕ x) @@ -482,14 +278,7 @@ succ-int-ℕ zero-ℕ = refl succ-int-ℕ (succ-ℕ x) = refl ``` -#### The negative function is injective - -```agda -is-injective-neg-ℤ : is-injective neg-ℤ -is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y -``` - -#### An integer is zero if its negative is zero +### An integer is zero if its negative is zero ```agda is-zero-is-zero-neg-ℤ : (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x diff --git a/src/elementary-number-theory/mediant-integer-fractions.lagda.md b/src/elementary-number-theory/mediant-integer-fractions.lagda.md index 56ee67d080..96adcb2df1 100644 --- a/src/elementary-number-theory/mediant-integer-fractions.lagda.md +++ b/src/elementary-number-theory/mediant-integer-fractions.lagda.md @@ -8,6 +8,7 @@ module elementary-number-theory.mediant-integer-fractions where ```agda open import elementary-number-theory.addition-integers +open import elementary-number-theory.addition-positive-and-negative-integers open import elementary-number-theory.cross-multiplication-difference-integer-fractions open import elementary-number-theory.difference-integers open import elementary-number-theory.integer-fractions @@ -32,8 +33,7 @@ denominators. ```agda mediant-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ -mediant-fraction-ℤ (a , b , p) (c , d , q) = - (a +ℤ c , b +ℤ d , is-positive-add-ℤ p q) +mediant-fraction-ℤ (a , b) (c , d) = (add-ℤ a c , add-positive-ℤ b d) ``` ## Properties diff --git a/src/elementary-number-theory/modular-arithmetic.lagda.md b/src/elementary-number-theory/modular-arithmetic.lagda.md index c68a033c92..981409d4a8 100644 --- a/src/elementary-number-theory/modular-arithmetic.lagda.md +++ b/src/elementary-number-theory/modular-arithmetic.lagda.md @@ -19,6 +19,7 @@ open import elementary-number-theory.modular-arithmetic-standard-finite-types open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions @@ -154,12 +155,12 @@ int-ℤ-Mod-bounded : (k : ℕ) → (x : ℤ-Mod (succ-ℕ k)) → leq-ℤ (int-ℤ-Mod (succ-ℕ k) x) (int-ℕ (succ-ℕ k)) int-ℤ-Mod-bounded zero-ℕ (inr x) = star -int-ℤ-Mod-bounded (succ-ℕ k) (inl x) = is-nonnegative-succ-ℤ - ((inr (inr k)) +ℤ - (neg-ℤ (int-ℕ (nat-Fin (succ-ℕ k) x)))) (int-ℤ-Mod-bounded k x) -int-ℤ-Mod-bounded (succ-ℕ k) (inr x) = is-nonnegative-succ-ℤ - ((inr (inr k)) +ℤ (inl k)) - (is-nonnegative-eq-ℤ (inv (left-inverse-law-add-ℤ (inl k))) star) +int-ℤ-Mod-bounded (succ-ℕ k) (inl x) = + is-nonnegative-succ-is-nonnegative-ℤ + ( int-ℤ-Mod-bounded k x) +int-ℤ-Mod-bounded (succ-ℕ k) (inr x) = + is-nonnegative-succ-is-nonnegative-ℤ + ( is-nonnegative-eq-ℤ (inv (left-inverse-law-add-ℤ (inl k))) star) ``` ## The successor and predecessor functions on the integers modulo `k` diff --git a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md index 42856beaa7..2667c5256a 100644 --- a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md +++ b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md @@ -9,6 +9,7 @@ module elementary-number-theory.multiplication-integer-fractions where ```agda open import elementary-number-theory.integer-fractions open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import foundation.action-on-identifications-binary-functions open import foundation.dependent-pair-types diff --git a/src/elementary-number-theory/multiplication-integers.lagda.md b/src/elementary-number-theory/multiplication-integers.lagda.md index e9b7690aa8..9e2f167eb2 100644 --- a/src/elementary-number-theory/multiplication-integers.lagda.md +++ b/src/elementary-number-theory/multiplication-integers.lagda.md @@ -9,13 +9,16 @@ module elementary-number-theory.multiplication-integers where ```agda open import elementary-number-theory.addition-integers open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.addition-positive-and-negative-integers open import elementary-number-theory.difference-integers open import elementary-number-theory.equality-integers open import elementary-number-theory.inequality-integers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers open import elementary-number-theory.nonzero-integers +open import elementary-number-theory.positive-integers open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions @@ -26,6 +29,7 @@ open import foundation.function-types open import foundation.identity-types open import foundation.injective-maps open import foundation.interchange-law +open import foundation.transport-along-identifications open import foundation.type-arithmetic-empty-type open import foundation.unit-type open import foundation.universe-levels @@ -33,6 +37,13 @@ open import foundation.universe-levels +## Idea + +We introduce the +{{#concept "multiplication" Disambiguation="integers" Agda=mul-ℤ}} of integers +and derive its basic properties with respect to `succ-ℤ`, `pred-ℤ`, `neg-ℤ` and +`add-ℤ`. + ## Definitions ### The standard definition of multiplication on ℤ @@ -328,17 +339,6 @@ double-negative-law-mul-ℤ k l = by neg-neg-ℤ (k *ℤ l) ``` -### Positivity of multiplication - -```agda -is-positive-mul-ℤ : - {x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x *ℤ y) -is-positive-mul-ℤ {inr (inr zero-ℕ)} {inr (inr y)} H K = star -is-positive-mul-ℤ {inr (inr (succ-ℕ x))} {inr (inr y)} H K = - is-positive-add-ℤ {inr (inr y)} K - ( is-positive-mul-ℤ {inr (inr x)} {inr (inr y)} H K) -``` - ### Computing multiplication of integers that come from natural numbers ```agda @@ -475,79 +475,8 @@ is-emb-right-mul-ℤ x f = is-emb-is-injective is-set-ℤ (is-injective-right-mul-ℤ x f) ``` -```agda -is-positive-left-factor-mul-ℤ : - {x y : ℤ} → is-positive-ℤ (x *ℤ y) → is-positive-ℤ y → is-positive-ℤ x -is-positive-left-factor-mul-ℤ {inl x} {inr (inr y)} H K = - is-positive-eq-ℤ (compute-mul-ℤ (inl x) (inr (inr y))) H -is-positive-left-factor-mul-ℤ {inr (inl star)} {inr (inr y)} H K = - is-positive-eq-ℤ (compute-mul-ℤ zero-ℤ (inr (inr y))) H -is-positive-left-factor-mul-ℤ {inr (inr x)} {inr (inr y)} H K = star - -is-positive-right-factor-mul-ℤ : - {x y : ℤ} → is-positive-ℤ (x *ℤ y) → is-positive-ℤ x → is-positive-ℤ y -is-positive-right-factor-mul-ℤ {x} {y} H = - is-positive-left-factor-mul-ℤ (is-positive-eq-ℤ (commutative-mul-ℤ x y) H) -``` - -### Lemmas about nonnegative integers +## See also -```agda -is-nonnegative-mul-ℤ : - {x y : ℤ} → is-nonnegative-ℤ x → is-nonnegative-ℤ y → - is-nonnegative-ℤ (x *ℤ y) -is-nonnegative-mul-ℤ {inr (inl star)} {y} H K = star -is-nonnegative-mul-ℤ {inr (inr x)} {inr (inl star)} H K = - is-nonnegative-eq-ℤ (inv (right-zero-law-mul-ℤ (inr (inr x)))) star -is-nonnegative-mul-ℤ {inr (inr x)} {inr (inr y)} H K = - is-nonnegative-eq-ℤ (inv (compute-mul-ℤ (inr (inr x)) (inr (inr y)))) star - -is-nonnegative-left-factor-mul-ℤ : - {x y : ℤ} → - is-nonnegative-ℤ (x *ℤ y) → is-positive-ℤ y → is-nonnegative-ℤ x -is-nonnegative-left-factor-mul-ℤ {inl x} {inr (inr y)} H K = - ex-falso (is-nonnegative-eq-ℤ (compute-mul-ℤ (inl x) (inr (inr y))) H) -is-nonnegative-left-factor-mul-ℤ {inr x} {inr y} H K = star - -is-nonnegative-right-factor-mul-ℤ : - {x y : ℤ} → - is-nonnegative-ℤ (x *ℤ y) → is-positive-ℤ x → is-nonnegative-ℤ y -is-nonnegative-right-factor-mul-ℤ {x} {y} H = - is-nonnegative-left-factor-mul-ℤ - ( is-nonnegative-eq-ℤ (commutative-mul-ℤ x y) H) -``` - -```agda -preserves-leq-left-mul-ℤ : - (x y z : ℤ) → is-nonnegative-ℤ z → leq-ℤ x y → leq-ℤ (z *ℤ x) (z *ℤ y) -preserves-leq-left-mul-ℤ x y (inr (inl star)) star K = star -preserves-leq-left-mul-ℤ x y (inr (inr zero-ℕ)) star K = K -preserves-leq-left-mul-ℤ x y (inr (inr (succ-ℕ n))) star K = - preserves-leq-add-ℤ {x} {y} - { (inr (inr n)) *ℤ x} - { (inr (inr n)) *ℤ y} - ( K) - ( preserves-leq-left-mul-ℤ x y (inr (inr n)) star K) - -preserves-leq-right-mul-ℤ : - (x y z : ℤ) → is-nonnegative-ℤ z → leq-ℤ x y → leq-ℤ (x *ℤ z) (y *ℤ z) -preserves-leq-right-mul-ℤ x y z H K = - concatenate-eq-leq-eq-ℤ - ( commutative-mul-ℤ x z) - ( preserves-leq-left-mul-ℤ x y z H K) - ( commutative-mul-ℤ z y) - -preserves-strict-order-mul-positive-ℤ' : - {x y : ℤ} (z : ℤ) → is-positive-ℤ z → le-ℤ x y → le-ℤ (x *ℤ z) (y *ℤ z) -preserves-strict-order-mul-positive-ℤ' {x} {y} z H p = - is-positive-eq-ℤ - ( inv ( linear-diff-right-mul-ℤ y x z)) - ( is-positive-mul-ℤ p H) - -preserves-strict-order-mul-positive-ℤ : - {x y : ℤ} (z : ℤ) → is-positive-ℤ z → le-ℤ x y → le-ℤ (z *ℤ x) (z *ℤ y) -preserves-strict-order-mul-positive-ℤ {x} {y} z H p = - is-positive-eq-ℤ - ( inv ( linear-diff-left-mul-ℤ z y x)) - ( is-positive-mul-ℤ H p) -``` +- Properties of multiplication with respect to inequality and positivity, + nonnegativity, negativity and nonnpositivity of integers are derived in + [`multiplication-positive-and-negative-integers`](elementary-number-theory.multiplication-positive-and-negative-integers.md) diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md new file mode 100644 index 0000000000..ed5eaf8aa0 --- /dev/null +++ b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md @@ -0,0 +1,426 @@ +# Multiplication of positive, negative, nonnegative and nonpositive integers + +```agda +module elementary-number-theory.multiplication-positive-and-negative-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-and-negative-integers +open import elementary-number-theory.inequality-integers +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.negative-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers +open import elementary-number-theory.strict-inequality-integers + +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.identity-types +open import foundation.unit-type +``` + +
+ +## Idea + +When we have information about the sign of the factors of an +[integer product](elementary-number-theory.multiplication-integers.md), we can +deduce the sign of their product too. The table below tabulates every case and +displays the corresponding Agda definition. + +| `p` | `q` | `p *ℤ q` | operation | +| :---------: | :---------: | :---------: | ------------------- | +| positive | positive | positive | `mul-positive-ℤ` | +| positive | nonnegative | nonnegative | | +| positive | negative | negative | | +| positive | nonpositive | nonpositive | | +| nonnegative | positive | nonnegative | | +| nonnegative | nonnegative | nonnegative | `mul-nonnegative-ℤ` | +| nonnegative | negative | nonpositive | | +| nonnegative | nonpositive | nonpositive | | +| negative | positive | negative | | +| negative | nonnegative | nonpositive | | +| negative | negative | positive | `mul-negative-ℤ` | +| negative | nonpositive | nonnegative | | +| nonpositive | positive | nonpositive | | +| nonpositive | nonnegative | nonpositive | | +| nonpositive | negative | nonpositive | | +| nonpositive | nonpositive | nonnegative | `mul-nonpositive-ℤ` | + +As a consequence, multiplication by a positive integer preserves and reflects +strict inequality and multiplication by a nonpositive integer preserves +inequality. + +## Lemmas + +### The product of two positive integers is positive + +```agda +is-positive-mul-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-positive-ℤ y → is-positive-ℤ (x *ℤ y) +is-positive-mul-ℤ {inr (inr zero-ℕ)} {y} H K = K +is-positive-mul-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-positive-add-ℤ K (is-positive-mul-ℤ {inr (inr x)} H K) +``` + +### The product of a positive and a nonnegative integer is nonnegative + +```agda +is-nonnegative-mul-positive-nonnegative-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x *ℤ y) +is-nonnegative-mul-positive-nonnegative-ℤ {inr (inr zero-ℕ)} {y} H K = K +is-nonnegative-mul-positive-nonnegative-ℤ {inr (inr (succ-ℕ x))} {y} H K = + is-nonnegative-add-ℤ K + ( is-nonnegative-mul-positive-nonnegative-ℤ {inr (inr x)} H K) +``` + +### The product of a positive and a negative integer is negative + +```agda +is-negative-mul-positive-negative-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-negative-ℤ y → is-negative-ℤ (x *ℤ y) +is-negative-mul-positive-negative-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( neg-neg-ℤ (x *ℤ y)) + ( is-negative-neg-is-positive-ℤ + ( is-positive-eq-ℤ + ( right-negative-law-mul-ℤ x y) + ( is-positive-mul-ℤ H (is-positive-neg-is-negative-ℤ K)))) +``` + +### The product of a positive and a nonpositive integer is nonpositive + +```agda +is-nonpositive-mul-positive-nonpositive-ℤ : + {x y : ℤ} → is-positive-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x *ℤ y) +is-nonpositive-mul-positive-nonpositive-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( neg-neg-ℤ (x *ℤ y)) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( is-nonnegative-eq-ℤ + ( right-negative-law-mul-ℤ x y) + ( is-nonnegative-mul-positive-nonnegative-ℤ H + ( is-nonnegative-neg-is-nonpositive-ℤ K)))) +``` + +### The product of a nonnegative integer and a positive integer is nonnegative + +```agda +is-nonnegative-mul-nonnegative-positive-ℤ : + {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-nonnegative-ℤ (x *ℤ y) +is-nonnegative-mul-nonnegative-positive-ℤ {x} {y} H K = + is-nonnegative-eq-ℤ + ( commutative-mul-ℤ y x) + ( is-nonnegative-mul-positive-nonnegative-ℤ K H) +``` + +### The product of two nonnegative integers is nonnegative + +```agda +is-nonnegative-mul-ℤ : + {x y : ℤ} → + is-nonnegative-ℤ x → is-nonnegative-ℤ y → is-nonnegative-ℤ (x *ℤ y) +is-nonnegative-mul-ℤ {inr (inl star)} {y} H K = star +is-nonnegative-mul-ℤ {inr (inr x)} {inr (inl star)} H K = + is-nonnegative-eq-ℤ (inv (right-zero-law-mul-ℤ (inr (inr x)))) star +is-nonnegative-mul-ℤ {inr (inr x)} {inr (inr y)} H K = + is-nonnegative-eq-ℤ (inv (compute-mul-ℤ (inr (inr x)) (inr (inr y)))) star +``` + +### The product of a nonnegative and a negative integer is nonpositive + +```agda +is-nonpositive-mul-nonnegative-negative-ℤ : + {x y : ℤ} → is-nonnegative-ℤ x → is-negative-ℤ y → is-nonpositive-ℤ (x *ℤ y) +is-nonpositive-mul-nonnegative-negative-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( neg-neg-ℤ (x *ℤ y)) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( is-nonnegative-eq-ℤ + ( right-negative-law-mul-ℤ x y) + ( is-nonnegative-mul-nonnegative-positive-ℤ H + ( is-positive-neg-is-negative-ℤ K)))) +``` + +### The product of a nonnegative and a nonpositive integer is nonpositive + +```agda +is-nonpositive-mul-nonnegative-nonpositive-ℤ : + {x y : ℤ} → + is-nonnegative-ℤ x → is-nonpositive-ℤ y → is-nonpositive-ℤ (x *ℤ y) +is-nonpositive-mul-nonnegative-nonpositive-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( neg-neg-ℤ (x *ℤ y)) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( is-nonnegative-eq-ℤ + ( right-negative-law-mul-ℤ x y) + ( is-nonnegative-mul-ℤ H + ( is-nonnegative-neg-is-nonpositive-ℤ K)))) +``` + +### The product of a negative and a positive integer is negative + +```agda +is-negative-mul-negative-positive-ℤ : + {x y : ℤ} → is-negative-ℤ x → is-positive-ℤ y → is-negative-ℤ (x *ℤ y) +is-negative-mul-negative-positive-ℤ {x} {y} H K = + is-negative-eq-ℤ + ( commutative-mul-ℤ y x) + ( is-negative-mul-positive-negative-ℤ K H) +``` + +### The product of a negative and a nonnegative integer is nonpositive + +```agda +is-nonpositive-mul-negative-nonnegative-ℤ : + {x y : ℤ} → is-negative-ℤ x → is-nonnegative-ℤ y → is-nonpositive-ℤ (x *ℤ y) +is-nonpositive-mul-negative-nonnegative-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( commutative-mul-ℤ y x) + ( is-nonpositive-mul-nonnegative-negative-ℤ K H) +``` + +### The product of two negative integers 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} H K = + is-positive-eq-ℤ + ( double-negative-law-mul-ℤ x y) + ( is-positive-mul-ℤ + ( is-positive-neg-is-negative-ℤ H) + ( is-positive-neg-is-negative-ℤ K)) +``` + +### The product of a negative and a nonpositive integer is nonnegative + +```agda +is-nonnegative-mul-negative-nonpositive-ℤ : + {x y : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ y → is-nonnegative-ℤ (x *ℤ y) +is-nonnegative-mul-negative-nonpositive-ℤ {x} {y} H K = + is-nonnegative-eq-ℤ + ( double-negative-law-mul-ℤ x y) + ( is-nonnegative-mul-positive-nonnegative-ℤ + ( is-positive-neg-is-negative-ℤ H) + ( is-nonnegative-neg-is-nonpositive-ℤ K)) +``` + +### The product of a nonpositive and a positive integer is nonpositive + +```agda +is-nonpositive-mul-nonpositive-positive-ℤ : + {x y : ℤ} → is-nonpositive-ℤ x → is-positive-ℤ y → is-nonpositive-ℤ (x *ℤ y) +is-nonpositive-mul-nonpositive-positive-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( commutative-mul-ℤ y x) + ( is-nonpositive-mul-positive-nonpositive-ℤ K H) +``` + +### The product of a nonpositive and a nonnegative integer is nonpositive + +```agda +is-nonpositive-mul-nonpositive-nonnegative-ℤ : + {x y : ℤ} → + is-nonpositive-ℤ x → is-nonnegative-ℤ y → is-nonpositive-ℤ (x *ℤ y) +is-nonpositive-mul-nonpositive-nonnegative-ℤ {x} {y} H K = + is-nonpositive-eq-ℤ + ( commutative-mul-ℤ y x) + ( is-nonpositive-mul-nonnegative-nonpositive-ℤ K H) +``` + +### The product of a nonpositive integer and a negative integer is nonnegative + +```agda +is-nonnegative-mul-nonpositive-negative-ℤ : + { x y : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ y → is-nonnegative-ℤ (x *ℤ y) +is-nonnegative-mul-nonpositive-negative-ℤ {x} {y} H K = + is-nonnegative-eq-ℤ + ( commutative-mul-ℤ y x) + ( is-nonnegative-mul-negative-nonpositive-ℤ K H) +``` + +### The product of two nonpositive integers is nonnegative + +```agda +is-nonnegative-mul-nonpositive-ℤ : + {x y : ℤ} → + is-nonpositive-ℤ x → is-nonpositive-ℤ y → is-nonnegative-ℤ (x *ℤ y) +is-nonnegative-mul-nonpositive-ℤ {x} {y} H K = + is-nonnegative-eq-ℤ + ( double-negative-law-mul-ℤ x y) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-neg-is-nonpositive-ℤ H) + ( is-nonnegative-neg-is-nonpositive-ℤ K)) +``` + +### The left factor of a positive product with a positive right factor is positive + +```agda +is-positive-left-factor-mul-ℤ : + {x y : ℤ} → is-positive-ℤ (x *ℤ y) → is-positive-ℤ y → is-positive-ℤ x +is-positive-left-factor-mul-ℤ {inl x} {inr (inr y)} H K = + is-positive-eq-ℤ (compute-mul-ℤ (inl x) (inr (inr y))) H +is-positive-left-factor-mul-ℤ {inr (inl star)} {inr (inr y)} H K = + is-positive-eq-ℤ (compute-mul-ℤ zero-ℤ (inr (inr y))) H +is-positive-left-factor-mul-ℤ {inr (inr x)} {inr (inr y)} H K = star +``` + +### The right factor of a positive product with a positive left factor is positive + +```agda +is-positive-right-factor-mul-ℤ : + {x y : ℤ} → is-positive-ℤ (x *ℤ y) → is-positive-ℤ x → is-positive-ℤ y +is-positive-right-factor-mul-ℤ {x} {y} H = + is-positive-left-factor-mul-ℤ (is-positive-eq-ℤ (commutative-mul-ℤ x y) H) +``` + +### The left factor of a nonnegative product with a positive right factor is nonnegative + +```agda +is-nonnegative-left-factor-mul-ℤ : + {x y : ℤ} → is-nonnegative-ℤ (x *ℤ y) → is-positive-ℤ y → is-nonnegative-ℤ x +is-nonnegative-left-factor-mul-ℤ {inl x} {inr (inr y)} H K = + ex-falso (is-nonnegative-eq-ℤ (compute-mul-ℤ (inl x) (inr (inr y))) H) +is-nonnegative-left-factor-mul-ℤ {inr x} {inr y} H K = star +``` + +### The right factor of a nonnegative product with a positive left factor is nonnegative + +```agda +is-nonnegative-right-factor-mul-ℤ : + {x y : ℤ} → is-nonnegative-ℤ (x *ℤ y) → is-positive-ℤ x → is-nonnegative-ℤ y +is-nonnegative-right-factor-mul-ℤ {x} {y} H = + is-nonnegative-left-factor-mul-ℤ + ( is-nonnegative-eq-ℤ (commutative-mul-ℤ x y) H) +``` + +## Definitions + +### Multiplication by a signed integer + +```agda +int-mul-positive-ℤ : positive-ℤ → ℤ → ℤ +int-mul-positive-ℤ x y = int-positive-ℤ x *ℤ y + +int-mul-positive-ℤ' : positive-ℤ → ℤ → ℤ +int-mul-positive-ℤ' x y = y *ℤ int-positive-ℤ x + +int-mul-nonnegative-ℤ : nonnegative-ℤ → ℤ → ℤ +int-mul-nonnegative-ℤ x y = int-nonnegative-ℤ x *ℤ y + +int-mul-nonnegative-ℤ' : nonnegative-ℤ → ℤ → ℤ +int-mul-nonnegative-ℤ' x y = y *ℤ int-nonnegative-ℤ x + +int-mul-negative-ℤ : negative-ℤ → ℤ → ℤ +int-mul-negative-ℤ x y = int-negative-ℤ x *ℤ y + +int-mul-negative-ℤ' : negative-ℤ → ℤ → ℤ +int-mul-negative-ℤ' x y = y *ℤ int-negative-ℤ x + +int-mul-nonpositive-ℤ : nonpositive-ℤ → ℤ → ℤ +int-mul-nonpositive-ℤ x y = int-nonpositive-ℤ x *ℤ y + +int-mul-nonpositive-ℤ' : nonpositive-ℤ → ℤ → ℤ +int-mul-nonpositive-ℤ' x y = y *ℤ int-nonpositive-ℤ x +``` + +### Multiplication of positive integers + +```agda +mul-positive-ℤ : positive-ℤ → positive-ℤ → positive-ℤ +mul-positive-ℤ (x , H) (y , K) = mul-ℤ x y , is-positive-mul-ℤ H K +``` + +### Multiplication of nonnegative integers + +```agda +mul-nonnegative-ℤ : nonnegative-ℤ → nonnegative-ℤ → nonnegative-ℤ +mul-nonnegative-ℤ (x , H) (y , K) = mul-ℤ x y , is-nonnegative-mul-ℤ H K +``` + +### Multiplication of negative integers + +```agda +mul-negative-ℤ : negative-ℤ → negative-ℤ → positive-ℤ +mul-negative-ℤ (x , H) (y , K) = mul-ℤ x y , is-positive-mul-negative-ℤ H K +``` + +### Multiplication of nonpositive integers + +```agda +mul-nonpositive-ℤ : nonpositive-ℤ → nonpositive-ℤ → nonnegative-ℤ +mul-nonpositive-ℤ (x , H) (y , K) = + mul-ℤ x y , is-nonnegative-mul-nonpositive-ℤ H K +``` + +## Properties + +### Multiplication by a positive integer preserves and reflects the strict ordering + +```agda +module _ + (z : positive-ℤ) (x y : ℤ) + where + + preserves-le-right-mul-positive-ℤ : + le-ℤ x y → le-ℤ (int-mul-positive-ℤ z x) (int-mul-positive-ℤ z y) + preserves-le-right-mul-positive-ℤ K = + is-positive-eq-ℤ + ( inv (linear-diff-left-mul-ℤ (int-positive-ℤ z) y x)) + ( is-positive-mul-ℤ (is-positive-int-positive-ℤ z) K) + + preserves-le-left-mul-positive-ℤ : + le-ℤ x y → le-ℤ (int-mul-positive-ℤ' z x) (int-mul-positive-ℤ' z y) + preserves-le-left-mul-positive-ℤ K = + is-positive-eq-ℤ + ( inv (linear-diff-right-mul-ℤ y x (int-positive-ℤ z))) + ( is-positive-mul-ℤ K (is-positive-int-positive-ℤ z)) + + reflects-le-right-mul-positive-ℤ : + le-ℤ (int-mul-positive-ℤ z x) (int-mul-positive-ℤ z y) → le-ℤ x y + reflects-le-right-mul-positive-ℤ K = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( linear-diff-left-mul-ℤ (int-positive-ℤ z) y x) + ( K)) + ( is-positive-int-positive-ℤ z) + + reflects-le-left-mul-positive-ℤ : + le-ℤ (int-mul-positive-ℤ' z x) (int-mul-positive-ℤ' z y) → le-ℤ x y + reflects-le-left-mul-positive-ℤ K = + is-positive-left-factor-mul-ℤ + ( is-positive-eq-ℤ + ( linear-diff-right-mul-ℤ y x (int-positive-ℤ z)) + ( K)) + ( is-positive-int-positive-ℤ z) +``` + +### Multiplication by a nonnegative integer preserves inequality + +```agda +module _ + (z : nonnegative-ℤ) (x y : ℤ) + where + + preserves-leq-right-mul-nonnegative-ℤ : + leq-ℤ x y → leq-ℤ (int-mul-nonnegative-ℤ z x) (int-mul-nonnegative-ℤ z y) + preserves-leq-right-mul-nonnegative-ℤ K = + is-nonnegative-eq-ℤ + ( inv (linear-diff-left-mul-ℤ (int-nonnegative-ℤ z) y x)) + ( is-nonnegative-mul-ℤ (is-nonnegative-int-nonnegative-ℤ z) K) + + preserves-leq-left-mul-nonnegative-ℤ : + leq-ℤ x y → leq-ℤ (int-mul-nonnegative-ℤ' z x) (int-mul-nonnegative-ℤ' z y) + preserves-leq-left-mul-nonnegative-ℤ K = + is-nonnegative-eq-ℤ + ( inv (linear-diff-right-mul-ℤ y x (int-nonnegative-ℤ z))) + ( is-nonnegative-mul-ℤ K (is-nonnegative-int-nonnegative-ℤ z)) +``` diff --git a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md index 360a331b17..f220975b16 100644 --- a/src/elementary-number-theory/multiplication-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-rational-numbers.lagda.md @@ -45,7 +45,7 @@ _*ℚ_ = mul-ℚ ```agda left-unit-law-mul-ℚ : (x : ℚ) → one-ℚ *ℚ x ＝ x left-unit-law-mul-ℚ x = - ( eq-ℚ-sim-fractions-ℤ + ( eq-ℚ-sim-fraction-ℤ ( mul-fraction-ℤ one-fraction-ℤ (fraction-ℚ x)) ( fraction-ℚ x) ( left-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙ @@ -53,7 +53,7 @@ left-unit-law-mul-ℚ x = right-unit-law-mul-ℚ : (x : ℚ) → x *ℚ one-ℚ ＝ x right-unit-law-mul-ℚ x = - ( eq-ℚ-sim-fractions-ℤ + ( eq-ℚ-sim-fraction-ℤ ( mul-fraction-ℤ (fraction-ℚ x) one-fraction-ℤ) ( fraction-ℚ x) ( right-unit-law-mul-fraction-ℤ (fraction-ℚ x))) ∙ diff --git a/src/elementary-number-theory/negative-integers.lagda.md b/src/elementary-number-theory/negative-integers.lagda.md new file mode 100644 index 0000000000..e99dfc6a58 --- /dev/null +++ b/src/elementary-number-theory/negative-integers.lagda.md @@ -0,0 +1,170 @@ +# The negative integers + +```agda +module elementary-number-theory.negative-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.decidable-subtypes +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +The [integers](elementary-number-theory.integers.md) are defined as a +[disjoint sum](foundation-core.coproduct-types.md) of three components. A single +element component containing the integer _zero_, and two copies of the +[natural numbers](elementary-number-theory.natural-numbers.md), one copy for the +_negative integers_ and one copy for the +[positive integers](elementary-number-theory.positive-integers.md). Arranged on +a number line, we have + +```text + ⋯ -4 -3 -2 -1 0 1 2 3 4 ⋯ + <---+---+---+---] | [---+---+---+---> +``` + +We say an integer is +{{#concept "negative" Disambiguation="integer" Agda=is-negative-ℤ}} if it is an +element of the negative component of the integers. + +## Definitions + +### Negative integers + +```agda +is-negative-ℤ : ℤ → UU lzero +is-negative-ℤ (inl k) = unit +is-negative-ℤ (inr k) = empty + +is-prop-is-negative-ℤ : (x : ℤ) → is-prop (is-negative-ℤ x) +is-prop-is-negative-ℤ (inl x) = is-prop-unit +is-prop-is-negative-ℤ (inr x) = is-prop-empty + +subtype-negative-ℤ : subtype lzero ℤ +subtype-negative-ℤ x = (is-negative-ℤ x , is-prop-is-negative-ℤ x) + +negative-ℤ : UU lzero +negative-ℤ = type-subtype subtype-negative-ℤ + +is-negative-eq-ℤ : {x y : ℤ} → x ＝ y → is-negative-ℤ x → is-negative-ℤ y +is-negative-eq-ℤ = tr is-negative-ℤ + +module _ + (p : negative-ℤ) + where + + int-negative-ℤ : ℤ + int-negative-ℤ = pr1 p + + is-negative-int-negative-ℤ : is-negative-ℤ int-negative-ℤ + is-negative-int-negative-ℤ = pr2 p +``` + +### Negative constants + +```agda +neg-one-negative-ℤ : negative-ℤ +neg-one-negative-ℤ = (neg-one-ℤ , star) +``` + +## Properties + +### Negativity is decidable + +```agda +is-decidable-is-negative-ℤ : is-decidable-fam is-negative-ℤ +is-decidable-is-negative-ℤ (inl x) = inl star +is-decidable-is-negative-ℤ (inr x) = inr id + +decidable-subtype-negative-ℤ : decidable-subtype lzero ℤ +decidable-subtype-negative-ℤ x = + ( is-negative-ℤ x , + is-prop-is-negative-ℤ x , + is-decidable-is-negative-ℤ x) +``` + +### The negative integers form a set + +```agda +is-set-negative-ℤ : is-set negative-ℤ +is-set-negative-ℤ = + is-set-type-subtype (subtype-negative-ℤ) (is-set-ℤ) +``` + +### The predecessor of a negative integer is negative + +```agda +is-negative-pred-is-negative-ℤ : + {x : ℤ} → is-negative-ℤ x → is-negative-ℤ (pred-ℤ x) +is-negative-pred-is-negative-ℤ {inl x} H = H + +pred-negative-ℤ : negative-ℤ → negative-ℤ +pred-negative-ℤ (x , H) = (pred-ℤ x , is-negative-pred-is-negative-ℤ H) +``` + +### The canonical equivalence between natural numbers and negative integers + +```agda +negative-int-ℕ : ℕ → negative-ℤ +negative-int-ℕ = rec-ℕ neg-one-negative-ℤ (λ _ → pred-negative-ℤ) + +nat-negative-ℤ : negative-ℤ → ℕ +nat-negative-ℤ (inl x , H) = x + +eq-nat-negative-pred-negative-ℤ : + (x : negative-ℤ) → + nat-negative-ℤ (pred-negative-ℤ x) ＝ succ-ℕ (nat-negative-ℤ x) +eq-nat-negative-pred-negative-ℤ (inl x , H) = refl + +is-section-nat-negative-ℤ : + (x : negative-ℤ) → negative-int-ℕ (nat-negative-ℤ x) ＝ x +is-section-nat-negative-ℤ (inl zero-ℕ , H) = refl +is-section-nat-negative-ℤ (inl (succ-ℕ x) , H) = + ap pred-negative-ℤ (is-section-nat-negative-ℤ (inl x , H)) + +is-retraction-nat-negative-ℤ : + (n : ℕ) → nat-negative-ℤ (negative-int-ℕ n) ＝ n +is-retraction-nat-negative-ℤ zero-ℕ = refl +is-retraction-nat-negative-ℤ (succ-ℕ n) = + eq-nat-negative-pred-negative-ℤ (negative-int-ℕ n) ∙ + ap succ-ℕ (is-retraction-nat-negative-ℤ n) + +is-equiv-negative-int-ℕ : is-equiv negative-int-ℕ +pr1 (pr1 is-equiv-negative-int-ℕ) = nat-negative-ℤ +pr2 (pr1 is-equiv-negative-int-ℕ) = is-section-nat-negative-ℤ +pr1 (pr2 is-equiv-negative-int-ℕ) = nat-negative-ℤ +pr2 (pr2 is-equiv-negative-int-ℕ) = is-retraction-nat-negative-ℤ + +equiv-negative-int-ℕ : ℕ ≃ negative-ℤ +pr1 equiv-negative-int-ℕ = negative-int-ℕ +pr2 equiv-negative-int-ℕ = is-equiv-negative-int-ℕ +``` + +## See also + +- Relations between negative and positive, nonnegative and nonnpositive integers + are derived in + [`positive-and-negative-integers`](elementary-number-theory.positive-and-negative-integers.md) diff --git a/src/elementary-number-theory/nonnegative-integers.lagda.md b/src/elementary-number-theory/nonnegative-integers.lagda.md new file mode 100644 index 0000000000..6f9d446eca --- /dev/null +++ b/src/elementary-number-theory/nonnegative-integers.lagda.md @@ -0,0 +1,198 @@ +# The nonnegative integers + +```agda +module elementary-number-theory.nonnegative-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.decidable-subtypes +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +The [integers](elementary-number-theory.integers.md) are defined as a +[disjoint sum](foundation-core.coproduct-types.md) of three components. A single +element component containing the integer _zero_, and two copies of the +[natural numbers](elementary-number-theory.natural-numbers.md), one copy for the +[negative integers](elementary-number-theory.negative-integers.md) and one copy +for the [positive integers](elementary-number-theory.positive-integers.md). +Arranged on a number line, we have + +```text + ⋯ -4 -3 -2 -1 0 1 2 3 4 ⋯ + <---+---+---+---] | [---+---+---+---> +``` + +The {{#concept "nonnegative" Disambiguation="integer" Agda=is-nonnegative-ℤ}} +integers are `zero-ℤ` and the positive component of the integers. + +## Definitions + +### Nonnegative integers + +```agda +is-nonnegative-ℤ : ℤ → UU lzero +is-nonnegative-ℤ (inl x) = empty +is-nonnegative-ℤ (inr x) = unit + +is-prop-is-nonnegative-ℤ : (x : ℤ) → is-prop (is-nonnegative-ℤ x) +is-prop-is-nonnegative-ℤ (inl x) = is-prop-empty +is-prop-is-nonnegative-ℤ (inr x) = is-prop-unit + +subtype-nonnegative-ℤ : subtype lzero ℤ +subtype-nonnegative-ℤ x = (is-nonnegative-ℤ x , is-prop-is-nonnegative-ℤ x) + +nonnegative-ℤ : UU lzero +nonnegative-ℤ = type-subtype subtype-nonnegative-ℤ + +is-nonnegative-eq-ℤ : + {x y : ℤ} → x ＝ y → is-nonnegative-ℤ x → is-nonnegative-ℤ y +is-nonnegative-eq-ℤ = tr is-nonnegative-ℤ + +module _ + (p : nonnegative-ℤ) + where + + int-nonnegative-ℤ : ℤ + int-nonnegative-ℤ = pr1 p + + is-nonnegative-int-nonnegative-ℤ : is-nonnegative-ℤ int-nonnegative-ℤ + is-nonnegative-int-nonnegative-ℤ = pr2 p +``` + +### Nonnegative integer constants + +```agda +zero-nonnegative-ℤ : nonnegative-ℤ +zero-nonnegative-ℤ = (zero-ℤ , star) + +one-nonnegative-ℤ : nonnegative-ℤ +one-nonnegative-ℤ = (one-ℤ , star) +``` + +## Properties + +### Nonnegativity is decidable + +```agda +is-decidable-is-nonnegative-ℤ : is-decidable-fam is-nonnegative-ℤ +is-decidable-is-nonnegative-ℤ (inl x) = inr id +is-decidable-is-nonnegative-ℤ (inr x) = inl star + +decidable-subtype-nonnegative-ℤ : decidable-subtype lzero ℤ +decidable-subtype-nonnegative-ℤ x = + ( is-nonnegative-ℤ x , + is-prop-is-nonnegative-ℤ x , + is-decidable-is-nonnegative-ℤ x) +``` + +### The nonnegative integers form a set + +```agda +is-set-nonnegative-ℤ : is-set nonnegative-ℤ +is-set-nonnegative-ℤ = + is-set-emb + ( emb-subtype subtype-nonnegative-ℤ) + ( is-set-ℤ) +``` + +### The only nonnegative integer with a nonnegative negative is zero + +```agda +is-zero-is-nonnegative-neg-is-nonnegative-ℤ : + {x : ℤ} → is-nonnegative-ℤ x → is-nonnegative-ℤ (neg-ℤ x) → is-zero-ℤ x +is-zero-is-nonnegative-neg-is-nonnegative-ℤ {inr (inl star)} nonneg nonpos = + refl +``` + +### The successor of a nonnegative integer is nonnegative + +```agda +is-nonnegative-succ-is-nonnegative-ℤ : + {x : ℤ} → is-nonnegative-ℤ x → is-nonnegative-ℤ (succ-ℤ x) +is-nonnegative-succ-is-nonnegative-ℤ {inr (inl x)} H = H +is-nonnegative-succ-is-nonnegative-ℤ {inr (inr x)} H = H + +succ-nonnegative-ℤ : nonnegative-ℤ → nonnegative-ℤ +succ-nonnegative-ℤ (x , H) = succ-ℤ x , is-nonnegative-succ-is-nonnegative-ℤ H +``` + +### The integer image of a natural number is nonnegative + +```agda +is-nonnegative-int-ℕ : (n : ℕ) → is-nonnegative-ℤ (int-ℕ n) +is-nonnegative-int-ℕ zero-ℕ = star +is-nonnegative-int-ℕ (succ-ℕ n) = star +``` + +### The canonical equivalence between natural numbers and nonnegative integers + +```agda +nonnegative-int-ℕ : ℕ → nonnegative-ℤ +nonnegative-int-ℕ n = int-ℕ n , is-nonnegative-int-ℕ n + +nat-nonnegative-ℤ : nonnegative-ℤ → ℕ +nat-nonnegative-ℤ (inr (inl x) , H) = zero-ℕ +nat-nonnegative-ℤ (inr (inr x) , H) = succ-ℕ x + +eq-nat-nonnegative-succ-nonnnegative-ℤ : + (x : nonnegative-ℤ) → + nat-nonnegative-ℤ (succ-nonnegative-ℤ x) ＝ succ-ℕ (nat-nonnegative-ℤ x) +eq-nat-nonnegative-succ-nonnnegative-ℤ (inr (inl x) , H) = refl +eq-nat-nonnegative-succ-nonnnegative-ℤ (inr (inr x) , H) = refl + +is-section-nat-nonnegative-ℤ : + (x : nonnegative-ℤ) → nonnegative-int-ℕ (nat-nonnegative-ℤ x) ＝ x +is-section-nat-nonnegative-ℤ ((inr (inl star)) , H) = refl +is-section-nat-nonnegative-ℤ ((inr (inr x)) , H) = refl + +is-retraction-nat-nonnegative-ℤ : + (n : ℕ) → nat-nonnegative-ℤ (nonnegative-int-ℕ n) ＝ n +is-retraction-nat-nonnegative-ℤ zero-ℕ = refl +is-retraction-nat-nonnegative-ℤ (succ-ℕ n) = refl + +is-equiv-nat-nonnegative-ℤ : is-equiv nat-nonnegative-ℤ +pr1 (pr1 is-equiv-nat-nonnegative-ℤ) = nonnegative-int-ℕ +pr2 (pr1 is-equiv-nat-nonnegative-ℤ) = is-retraction-nat-nonnegative-ℤ +pr1 (pr2 is-equiv-nat-nonnegative-ℤ) = nonnegative-int-ℕ +pr2 (pr2 is-equiv-nat-nonnegative-ℤ) = is-section-nat-nonnegative-ℤ + +is-equiv-nonnegative-int-ℕ : is-equiv nonnegative-int-ℕ +pr1 (pr1 is-equiv-nonnegative-int-ℕ) = nat-nonnegative-ℤ +pr2 (pr1 is-equiv-nonnegative-int-ℕ) = is-section-nat-nonnegative-ℤ +pr1 (pr2 is-equiv-nonnegative-int-ℕ) = nat-nonnegative-ℤ +pr2 (pr2 is-equiv-nonnegative-int-ℕ) = is-retraction-nat-nonnegative-ℤ + +equiv-nonnegative-int-ℕ : ℕ ≃ nonnegative-ℤ +pr1 equiv-nonnegative-int-ℕ = nonnegative-int-ℕ +pr2 equiv-nonnegative-int-ℕ = is-equiv-nonnegative-int-ℕ +``` + +## See also + +- The relations between nonnegative and positive, negative and nonpositive + integers are derived in + [`positive-and-negative-integers`](elementary-number-theory.positive-and-negative-integers.md) diff --git a/src/elementary-number-theory/nonpositive-integers.lagda.md b/src/elementary-number-theory/nonpositive-integers.lagda.md new file mode 100644 index 0000000000..423216dbe2 --- /dev/null +++ b/src/elementary-number-theory/nonpositive-integers.lagda.md @@ -0,0 +1,191 @@ +# The nonpositive integers + +```agda +module elementary-number-theory.nonpositive-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.decidable-subtypes +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +The [integers](elementary-number-theory.integers.md) are defined as a +[disjoint sum](foundation-core.coproduct-types.md) of three components. A single +element component containing the integer _zero_, and two copies of the +[natural numbers](elementary-number-theory.natural-numbers.md), one copy for the +[negative integers](elementary-number-theory.negative-integers.md) and one copy +for the [positive integers](elementary-number-theory.positive-integers.md). +Arranged on a number line, we have + +```text + ⋯ -4 -3 -2 -1 0 1 2 3 4 ⋯ + <---+---+---+---] | [---+---+---+---> +``` + +The {{#concept "nonpositive" Disambiguation="integer" Agda=is-nonpositive-ℤ}} +integers are `zero-ℤ` and the negative component of the integers. + +## Definitions + +### Nonnpositive integers + +```agda +is-nonpositive-ℤ : ℤ → UU lzero +is-nonpositive-ℤ (inl k) = unit +is-nonpositive-ℤ (inr (inl x)) = unit +is-nonpositive-ℤ (inr (inr x)) = empty + +is-prop-is-nonpositive-ℤ : (x : ℤ) → is-prop (is-nonpositive-ℤ x) +is-prop-is-nonpositive-ℤ (inl x) = is-prop-unit +is-prop-is-nonpositive-ℤ (inr (inl x)) = is-prop-unit +is-prop-is-nonpositive-ℤ (inr (inr x)) = is-prop-empty + +subtype-nonpositive-ℤ : subtype lzero ℤ +subtype-nonpositive-ℤ x = (is-nonpositive-ℤ x , is-prop-is-nonpositive-ℤ x) + +nonpositive-ℤ : UU lzero +nonpositive-ℤ = type-subtype subtype-nonpositive-ℤ + +is-nonpositive-eq-ℤ : + {x y : ℤ} → x ＝ y → is-nonpositive-ℤ x → is-nonpositive-ℤ y +is-nonpositive-eq-ℤ = tr is-nonpositive-ℤ + +module _ + (p : nonpositive-ℤ) + where + + int-nonpositive-ℤ : ℤ + int-nonpositive-ℤ = pr1 p + + is-nonpositive-int-nonpositive-ℤ : is-nonpositive-ℤ int-nonpositive-ℤ + is-nonpositive-int-nonpositive-ℤ = pr2 p +``` + +### Nonpositive constants + +```agda +zero-nonpositive-ℤ : nonpositive-ℤ +zero-nonpositive-ℤ = (zero-ℤ , star) + +neg-one-nonpositive-ℤ : nonpositive-ℤ +neg-one-nonpositive-ℤ = (neg-one-ℤ , star) +``` + +## Properties + +### Nonpositivity is decidable + +```agda +is-decidable-is-nonpositive-ℤ : is-decidable-fam is-nonpositive-ℤ +is-decidable-is-nonpositive-ℤ (inl x) = inl star +is-decidable-is-nonpositive-ℤ (inr (inl x)) = inl star +is-decidable-is-nonpositive-ℤ (inr (inr x)) = inr id + +decidable-subtype-nonpositive-ℤ : decidable-subtype lzero ℤ +decidable-subtype-nonpositive-ℤ x = + ( is-nonpositive-ℤ x , + is-prop-is-nonpositive-ℤ x , + is-decidable-is-nonpositive-ℤ x) +``` + +### The nonpositive integers form a set + +```agda +is-set-nonpositive-ℤ : is-set nonpositive-ℤ +is-set-nonpositive-ℤ = + is-set-emb + ( emb-subtype subtype-nonpositive-ℤ) + ( is-set-ℤ) +``` + +### The only nonpositive integer with a nonpositive negative is zero + +```agda +is-zero-is-nonpositive-neg-is-nonpositive-ℤ : + {x : ℤ} → is-nonpositive-ℤ x → is-nonpositive-ℤ (neg-ℤ x) → is-zero-ℤ x +is-zero-is-nonpositive-neg-is-nonpositive-ℤ {inr (inl star)} nonneg nonpos = + refl +``` + +### The predecessor of a nonpositive integer is nonpositive + +```agda +is-nonpositive-pred-is-nonpositive-ℤ : + {x : ℤ} → is-nonpositive-ℤ x → is-nonpositive-ℤ (pred-ℤ x) +is-nonpositive-pred-is-nonpositive-ℤ {inl x} H = H +is-nonpositive-pred-is-nonpositive-ℤ {inr (inl x)} H = H + +pred-nonpositive-ℤ : nonpositive-ℤ → nonpositive-ℤ +pred-nonpositive-ℤ (x , H) = pred-ℤ x , is-nonpositive-pred-is-nonpositive-ℤ H +``` + +### The canonical equivalence between natural numbers and positive integers + +```agda +nonpositive-int-ℕ : ℕ → nonpositive-ℤ +nonpositive-int-ℕ = rec-ℕ zero-nonpositive-ℤ (λ _ → pred-nonpositive-ℤ) + +nat-nonpositive-ℤ : nonpositive-ℤ → ℕ +nat-nonpositive-ℤ (inl x , H) = succ-ℕ x +nat-nonpositive-ℤ (inr x , H) = zero-ℕ + +eq-nat-nonpositive-pred-nonpositive-ℤ : + (x : nonpositive-ℤ) → + nat-nonpositive-ℤ (pred-nonpositive-ℤ x) ＝ succ-ℕ (nat-nonpositive-ℤ x) +eq-nat-nonpositive-pred-nonpositive-ℤ (inl x , H) = refl +eq-nat-nonpositive-pred-nonpositive-ℤ (inr (inl x) , H) = refl + +is-section-nat-nonpositive-ℤ : + (x : nonpositive-ℤ) → nonpositive-int-ℕ (nat-nonpositive-ℤ x) ＝ x +is-section-nat-nonpositive-ℤ (inl zero-ℕ , H) = refl +is-section-nat-nonpositive-ℤ (inl (succ-ℕ x) , H) = + ap pred-nonpositive-ℤ (is-section-nat-nonpositive-ℤ (inl x , H)) +is-section-nat-nonpositive-ℤ (inr (inl x) , H) = refl + +is-retraction-nat-nonpositive-ℤ : + (n : ℕ) → nat-nonpositive-ℤ (nonpositive-int-ℕ n) ＝ n +is-retraction-nat-nonpositive-ℤ zero-ℕ = refl +is-retraction-nat-nonpositive-ℤ (succ-ℕ n) = + eq-nat-nonpositive-pred-nonpositive-ℤ (nonpositive-int-ℕ n) ∙ + ap succ-ℕ (is-retraction-nat-nonpositive-ℤ n) + +is-equiv-nonpositive-int-ℕ : is-equiv nonpositive-int-ℕ +pr1 (pr1 is-equiv-nonpositive-int-ℕ) = nat-nonpositive-ℤ +pr2 (pr1 is-equiv-nonpositive-int-ℕ) = is-section-nat-nonpositive-ℤ +pr1 (pr2 is-equiv-nonpositive-int-ℕ) = nat-nonpositive-ℤ +pr2 (pr2 is-equiv-nonpositive-int-ℕ) = is-retraction-nat-nonpositive-ℤ + +equiv-nonpositive-int-ℕ : ℕ ≃ nonpositive-ℤ +pr1 equiv-nonpositive-int-ℕ = nonpositive-int-ℕ +pr2 equiv-nonpositive-int-ℕ = is-equiv-nonpositive-int-ℕ +``` + +## See also + +- The relations between nonpositive and positive, nonnegative and negative + integers are derived in + [`positive-and-negative-integers`](elementary-number-theory.positive-and-negative-integers.md) diff --git a/src/elementary-number-theory/nonzero-integers.lagda.md b/src/elementary-number-theory/nonzero-integers.lagda.md index 568ade3bb9..1c9fac8416 100644 --- a/src/elementary-number-theory/nonzero-integers.lagda.md +++ b/src/elementary-number-theory/nonzero-integers.lagda.md @@ -77,16 +77,9 @@ pr2 one-nonzero-ℤ = is-nonzero-one-ℤ ## Properties -### The inclusion of natural numbers into integers maps nonzero natural numbers to nonzero integers +### The integer image of a nonzero natural number is nonzero ```agda is-nonzero-int-ℕ : (n : ℕ) → is-nonzero-ℕ n → is-nonzero-ℤ (int-ℕ n) is-nonzero-int-ℕ zero-ℕ H p = H refl ``` - -### Positive integers are nonzero - -```agda -is-nonzero-is-positive-ℤ : (x : ℤ) → is-positive-ℤ x → is-nonzero-ℤ x -is-nonzero-is-positive-ℤ (inr (inr x)) 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 new file mode 100644 index 0000000000..82a5630d33 --- /dev/null +++ b/src/elementary-number-theory/positive-and-negative-integers.lagda.md @@ -0,0 +1,253 @@ +# The positive, negative, nonnegative and nonpositive integers + +```agda +module elementary-number-theory.positive-and-negative-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.negative-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.nonzero-integers +open import elementary-number-theory.positive-integers + +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.negated-equality +open import foundation.negation +open import foundation.unit-type +``` + +
+ +## Idea + +In this file, we outline basic relations between negative, nonpositive, +nonnegative, and positive integers. + +## Properties + +### The only nonnegative and nonpositive integer is zero + +```agda +is-zero-is-nonnegative-is-nonpositive-ℤ : + {x : ℤ} → is-nonnegative-ℤ x → is-nonpositive-ℤ x → is-zero-ℤ x +is-zero-is-nonnegative-is-nonpositive-ℤ {inr (inl x)} H K = refl +``` + +### Positive integers are nonzero + +```agda +is-nonzero-is-positive-ℤ : {x : ℤ} → is-positive-ℤ x → is-nonzero-ℤ x +is-nonzero-is-positive-ℤ {inr (inr x)} H () +``` + +### Negative integers are nonzero + +```agda +is-nonzero-is-negative-ℤ : {x : ℤ} → is-negative-ℤ x → is-nonzero-ℤ x +is-nonzero-is-negative-ℤ {inl x} H () +``` + +### Dichotomies + +#### A nonzero integer is either negative or positive + +```agda +decide-sign-nonzero-ℤ : + {x : ℤ} → x ≠ zero-ℤ → is-negative-ℤ x + is-positive-ℤ x +decide-sign-nonzero-ℤ {inl x} H = inl star +decide-sign-nonzero-ℤ {inr (inl x)} H = ex-falso (H refl) +decide-sign-nonzero-ℤ {inr (inr x)} H = inr star +``` + +#### An integer is either positive or nonpositive + +```agda +decide-is-positive-is-nonpositive-ℤ : + {x : ℤ} → is-positive-ℤ x + is-nonpositive-ℤ x +decide-is-positive-is-nonpositive-ℤ {inl x} = inr star +decide-is-positive-is-nonpositive-ℤ {inr (inl x)} = inr star +decide-is-positive-is-nonpositive-ℤ {inr (inr x)} = inl star +``` + +#### An integer is either negative or nonnegative + +```agda +decide-is-negative-is-nonnegative-ℤ : + {x : ℤ} → is-negative-ℤ x + is-nonnegative-ℤ x +decide-is-negative-is-nonnegative-ℤ {inl x} = inl star +decide-is-negative-is-nonnegative-ℤ {inr x} = inr star +``` + +#### An integer or its negative is nonnegative + +```agda +decide-is-nonnegative-is-nonnegative-neg-ℤ : + {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x)) +decide-is-nonnegative-is-nonnegative-neg-ℤ {inl x} = inr star +decide-is-nonnegative-is-nonnegative-neg-ℤ {inr x} = inl star +``` + +#### An integer or its negative is nonpositive + +```agda +decide-is-nonpositive-is-nonpositive-neg-ℤ : + {x : ℤ} → (is-nonpositive-ℤ x) + (is-nonpositive-ℤ (neg-ℤ x)) +decide-is-nonpositive-is-nonpositive-neg-ℤ {inl x} = inl star +decide-is-nonpositive-is-nonpositive-neg-ℤ {inr (inl x)} = inl star +decide-is-nonpositive-is-nonpositive-neg-ℤ {inr (inr x)} = inr star +``` + +### Positive integers are nonnegative + +```agda +is-nonnegative-is-positive-ℤ : {x : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ x +is-nonnegative-is-positive-ℤ {inr (inr x)} H = H + +nonnegative-positive-ℤ : positive-ℤ → nonnegative-ℤ +nonnegative-positive-ℤ (x , H) = (x , is-nonnegative-is-positive-ℤ H) +``` + +### Negative integers are nonpositive + +```agda +is-nonpositive-is-negative-ℤ : {x : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ x +is-nonpositive-is-negative-ℤ {inl x} H = H + +nonpositive-negative-ℤ : negative-ℤ → nonpositive-ℤ +nonpositive-negative-ℤ (x , H) = (x , is-nonpositive-is-negative-ℤ H) +``` + +### Determining the sign of the successor of an integer + +#### The successor of a nonnegative integer is positive + +```agda +is-positive-succ-is-nonnegative-ℤ : + {x : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ (succ-ℤ x) +is-positive-succ-is-nonnegative-ℤ {inr (inl x)} H = H +is-positive-succ-is-nonnegative-ℤ {inr (inr x)} H = H +``` + +#### The successor of a negative integer is nonpositive + +```agda +is-nonpositive-succ-is-negative-ℤ : + {x : ℤ} → is-negative-ℤ x → is-nonpositive-ℤ (succ-ℤ x) +is-nonpositive-succ-is-negative-ℤ {inl zero-ℕ} H = H +is-nonpositive-succ-is-negative-ℤ {inl (succ-ℕ x)} H = H +``` + +### Determining the sign of the predecessor of an integer + +#### The predecessor of a positive integer is nonnegative + +```agda +is-nonnegative-pred-is-positive-ℤ : + {x : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ (pred-ℤ x) +is-nonnegative-pred-is-positive-ℤ {inr (inr zero-ℕ)} H = H +is-nonnegative-pred-is-positive-ℤ {inr (inr (succ-ℕ x))} H = H +``` + +#### The predecessor of a nonpositive integer is negative + +```agda +is-negative-pred-is-nonpositive-ℤ : + {x : ℤ} → is-nonpositive-ℤ x → is-negative-ℤ (pred-ℤ x) +is-negative-pred-is-nonpositive-ℤ {inl x} H = H +is-negative-pred-is-nonpositive-ℤ {inr (inl x)} H = H +``` + +### Determining the sign of the negative of an integer + +#### The negative of a nonnegative integer is nonpositive + +```agda +is-nonpositive-neg-is-nonnegative-ℤ : + {x : ℤ} → is-nonnegative-ℤ x → is-nonpositive-ℤ (neg-ℤ x) +is-nonpositive-neg-is-nonnegative-ℤ {inr (inl x)} H = H +is-nonpositive-neg-is-nonnegative-ℤ {inr (inr x)} H = H + +neg-nonnegative-ℤ : nonnegative-ℤ → nonpositive-ℤ +neg-nonnegative-ℤ (x , H) = neg-ℤ x , is-nonpositive-neg-is-nonnegative-ℤ H +``` + +#### The negative of a nonpositive integer is nonnegative + +```agda +is-nonnegative-neg-is-nonpositive-ℤ : + {x : ℤ} → is-nonpositive-ℤ x → is-nonnegative-ℤ (neg-ℤ x) +is-nonnegative-neg-is-nonpositive-ℤ {inl x} H = H +is-nonnegative-neg-is-nonpositive-ℤ {inr (inl x)} H = H + +neg-nonpositive-ℤ : nonpositive-ℤ → nonnegative-ℤ +neg-nonpositive-ℤ (x , H) = neg-ℤ x , is-nonnegative-neg-is-nonpositive-ℤ H +``` + +#### The negative of a positive integer is negative + +```agda +is-negative-neg-is-positive-ℤ : + {x : ℤ} → is-positive-ℤ x → is-negative-ℤ (neg-ℤ x) +is-negative-neg-is-positive-ℤ {inr (inr x)} H = H + +neg-positive-ℤ : positive-ℤ → negative-ℤ +neg-positive-ℤ (x , H) = (neg-ℤ x , is-negative-neg-is-positive-ℤ H) +``` + +#### The negative of a negative integer is positive + +```agda +is-positive-neg-is-negative-ℤ : + {x : ℤ} → is-negative-ℤ x → is-positive-ℤ (neg-ℤ x) +is-positive-neg-is-negative-ℤ {inl x} H = H + +neg-negative-ℤ : negative-ℤ → positive-ℤ +neg-negative-ℤ (x , H) = (neg-ℤ x , is-positive-neg-is-negative-ℤ H) +``` + +### Negated properties + +#### Nonpositivity is negated positivity + +```agda +is-not-positive-is-nonpositive-ℤ : + {x : ℤ} → is-nonpositive-ℤ x → ¬ (is-positive-ℤ x) +is-not-positive-is-nonpositive-ℤ {inr (inl x)} _ q = q +is-not-positive-is-nonpositive-ℤ {inr (inr x)} p _ = p + +is-nonpositive-is-not-positive-ℤ : + {x : ℤ} → ¬ (is-positive-ℤ x) → is-nonpositive-ℤ x +is-nonpositive-is-not-positive-ℤ {x} H = + rec-coproduct + ( λ K → ex-falso (H K)) + ( id) + ( decide-is-positive-is-nonpositive-ℤ) +``` + +#### Nonnegativity is negated negativity + +```agda +is-not-negative-is-nonnegative-ℤ : + {x : ℤ} → is-nonnegative-ℤ x → ¬ (is-negative-ℤ x) +is-not-negative-is-nonnegative-ℤ {x} H K = + is-not-positive-is-nonpositive-ℤ + ( is-nonpositive-neg-is-nonnegative-ℤ H) + ( is-positive-neg-is-negative-ℤ K) + +is-nonnegative-is-not-negative-ℤ : + {x : ℤ} → ¬ (is-negative-ℤ x) → is-nonnegative-ℤ x +is-nonnegative-is-not-negative-ℤ {x} H = + rec-coproduct + ( λ K → ex-falso (H K)) + ( id) + ( decide-is-negative-is-nonnegative-ℤ) +``` diff --git a/src/elementary-number-theory/positive-integers.lagda.md b/src/elementary-number-theory/positive-integers.lagda.md new file mode 100644 index 0000000000..1732ac0bc6 --- /dev/null +++ b/src/elementary-number-theory/positive-integers.lagda.md @@ -0,0 +1,181 @@ +# The positive integers + +```agda +module elementary-number-theory.positive-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.decidable-subtypes +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +The [integers](elementary-number-theory.integers.md) are defined as a +[disjoint sum](foundation-core.coproduct-types.md) of three components. A single +element component containing the integer _zero_, and two copies of the +[natural numbers](elementary-number-theory.natural-numbers.md), one copy for the +[negative integers](elementary-number-theory.negative-integers.md) and one copy +for the _positive integers_. Arranged on a number line, we have + +```text + ⋯ -4 -3 -2 -1 0 1 2 3 4 ⋯ + <---+---+---+---] | [---+---+---+---> +``` + +We say an integer is +{{#concept "positive" Disambiguation="integer" Agda=is-positive-ℤ}} if it is an +element of the positive component of the integers. + +## Definitions + +### Positive integers + +```agda +is-positive-ℤ : ℤ → UU lzero +is-positive-ℤ (inl x) = empty +is-positive-ℤ (inr (inl x)) = empty +is-positive-ℤ (inr (inr x)) = unit + +is-prop-is-positive-ℤ : (x : ℤ) → is-prop (is-positive-ℤ x) +is-prop-is-positive-ℤ (inl x) = is-prop-empty +is-prop-is-positive-ℤ (inr (inl x)) = is-prop-empty +is-prop-is-positive-ℤ (inr (inr x)) = is-prop-unit + +subtype-positive-ℤ : subtype lzero ℤ +subtype-positive-ℤ x = (is-positive-ℤ x , is-prop-is-positive-ℤ x) + +positive-ℤ : UU lzero +positive-ℤ = type-subtype subtype-positive-ℤ + +is-positive-eq-ℤ : {x y : ℤ} → x ＝ y → is-positive-ℤ x → is-positive-ℤ y +is-positive-eq-ℤ = tr is-positive-ℤ + +module _ + (p : positive-ℤ) + where + + int-positive-ℤ : ℤ + int-positive-ℤ = pr1 p + + is-positive-int-positive-ℤ : is-positive-ℤ int-positive-ℤ + is-positive-int-positive-ℤ = pr2 p +``` + +### Positive constants + +```agda +one-positive-ℤ : positive-ℤ +one-positive-ℤ = (one-ℤ , star) +``` + +## Properties + +### Positivity is decidable + +```agda +is-decidable-is-positive-ℤ : is-decidable-fam is-positive-ℤ +is-decidable-is-positive-ℤ (inl x) = inr id +is-decidable-is-positive-ℤ (inr (inl x)) = inr id +is-decidable-is-positive-ℤ (inr (inr x)) = inl star + +decidable-subtype-positive-ℤ : decidable-subtype lzero ℤ +decidable-subtype-positive-ℤ x = + ( is-positive-ℤ x , + is-prop-is-positive-ℤ x , + is-decidable-is-positive-ℤ x) +``` + +### The positive integers form a set + +```agda +is-set-positive-ℤ : is-set positive-ℤ +is-set-positive-ℤ = + is-set-type-subtype subtype-positive-ℤ is-set-ℤ +``` + +### The successor of a positive integer is positive + +```agda +is-positive-succ-is-positive-ℤ : + {x : ℤ} → is-positive-ℤ x → is-positive-ℤ (succ-ℤ x) +is-positive-succ-is-positive-ℤ {inr (inr x)} H = H + +succ-positive-ℤ : positive-ℤ → positive-ℤ +succ-positive-ℤ (x , H) = (succ-ℤ x , is-positive-succ-is-positive-ℤ H) +``` + +### The integer image of a nonzero natural number is positive + +```agda +is-positive-int-is-nonzero-ℕ : + (x : ℕ) → is-nonzero-ℕ x → is-positive-ℤ (int-ℕ x) +is-positive-int-is-nonzero-ℕ zero-ℕ H = ex-falso (H refl) +is-positive-int-is-nonzero-ℕ (succ-ℕ x) H = star +``` + +### The canonical equivalence between natural numbers and positive integers + +```agda +positive-int-ℕ : ℕ → positive-ℤ +positive-int-ℕ = rec-ℕ one-positive-ℤ (λ _ → succ-positive-ℤ) + +nat-positive-ℤ : positive-ℤ → ℕ +nat-positive-ℤ (inr (inr x) , H) = x + +eq-nat-positive-succ-positive-ℤ : + (x : positive-ℤ) → + nat-positive-ℤ (succ-positive-ℤ x) ＝ succ-ℕ (nat-positive-ℤ x) +eq-nat-positive-succ-positive-ℤ (inr (inr x) , H) = refl + +is-section-nat-positive-ℤ : + (x : positive-ℤ) → positive-int-ℕ (nat-positive-ℤ x) ＝ x +is-section-nat-positive-ℤ (inr (inr zero-ℕ) , H) = refl +is-section-nat-positive-ℤ (inr (inr (succ-ℕ x)) , H) = + ap succ-positive-ℤ (is-section-nat-positive-ℤ ( inr (inr x) , H)) + +is-retraction-nat-positive-ℤ : + (n : ℕ) → nat-positive-ℤ (positive-int-ℕ n) ＝ n +is-retraction-nat-positive-ℤ zero-ℕ = refl +is-retraction-nat-positive-ℤ (succ-ℕ n) = + eq-nat-positive-succ-positive-ℤ (positive-int-ℕ n) ∙ + ap succ-ℕ (is-retraction-nat-positive-ℤ n) + +is-equiv-positive-int-ℕ : is-equiv positive-int-ℕ +pr1 (pr1 is-equiv-positive-int-ℕ) = nat-positive-ℤ +pr2 (pr1 is-equiv-positive-int-ℕ) = is-section-nat-positive-ℤ +pr1 (pr2 is-equiv-positive-int-ℕ) = nat-positive-ℤ +pr2 (pr2 is-equiv-positive-int-ℕ) = is-retraction-nat-positive-ℤ + +equiv-positive-int-ℕ : ℕ ≃ positive-ℤ +pr1 equiv-positive-int-ℕ = positive-int-ℕ +pr2 equiv-positive-int-ℕ = is-equiv-positive-int-ℕ +``` + +## See also + +- The relations between positive and nonnegative, negative and nonnpositive + integers are derived in + [`positive-and-negative-integers`](elementary-number-theory.positive-and-negative-integers.md) diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md index b04a7d7592..cd01f83dcf 100644 --- a/src/elementary-number-theory/rational-numbers.lagda.md +++ b/src/elementary-number-theory/rational-numbers.lagda.md @@ -12,6 +12,8 @@ open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers open import elementary-number-theory.mediant-integer-fractions +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import elementary-number-theory.reduced-integer-fractions open import foundation.dependent-pair-types @@ -22,6 +24,7 @@ open import foundation.negation open import foundation.propositions open import foundation.reflecting-maps-equivalence-relations open import foundation.sets +open import foundation.subtypes open import foundation.universe-levels ``` @@ -116,13 +119,13 @@ mediant-ℚ x y = ## Properties -### If two fractions are related by `sim-fraction-ℤ`, then their embeddings into `ℚ` are equal +### The rational images of two similar integer fractions are equal ```agda -eq-ℚ-sim-fractions-ℤ : +eq-ℚ-sim-fraction-ℤ : (x y : fraction-ℤ) → (H : sim-fraction-ℤ x y) → in-fraction-ℤ x ＝ in-fraction-ℤ y -eq-ℚ-sim-fractions-ℤ x y H = +eq-ℚ-sim-fraction-ℤ x y H = eq-pair-Σ' ( pair ( unique-reduce-fraction-ℤ x y H) @@ -159,5 +162,5 @@ in-fraction-fraction-ℚ (pair (pair m (pair n n-pos)) p) = reflecting-map-sim-fraction : reflecting-map-equivalence-relation equivalence-relation-sim-fraction-ℤ ℚ pr1 reflecting-map-sim-fraction = in-fraction-ℤ -pr2 reflecting-map-sim-fraction {x} {y} H = eq-ℚ-sim-fractions-ℤ x y H +pr2 reflecting-map-sim-fraction {x} {y} H = eq-ℚ-sim-fraction-ℤ x y H ``` diff --git a/src/elementary-number-theory/reduced-integer-fractions.lagda.md b/src/elementary-number-theory/reduced-integer-fractions.lagda.md index 06aa1843e5..291af5d0c0 100644 --- a/src/elementary-number-theory/reduced-integer-fractions.lagda.md +++ b/src/elementary-number-theory/reduced-integer-fractions.lagda.md @@ -14,7 +14,10 @@ open import elementary-number-theory.greatest-common-divisor-integers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import elementary-number-theory.relatively-prime-integers open import foundation.action-on-identifications-functions @@ -26,6 +29,7 @@ open import foundation.equality-dependent-pair-types open import foundation.identity-types open import foundation.negation open import foundation.propositions +open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels ``` @@ -127,9 +131,10 @@ is-reduced-reduce-fraction-ℤ : (x : fraction-ℤ) → is-reduced-fraction-ℤ (reduce-fraction-ℤ x) is-reduced-reduce-fraction-ℤ x = is-zero-gcd-case-split - (is-decidable-is-zero-ℤ - (gcd-ℤ ( numerator-fraction-ℤ (reduce-fraction-ℤ x)) - (denominator-fraction-ℤ (reduce-fraction-ℤ x)))) + ( is-decidable-is-zero-ℤ + ( gcd-ℤ + ( numerator-fraction-ℤ (reduce-fraction-ℤ x)) + ( denominator-fraction-ℤ (reduce-fraction-ℤ x)))) where is-zero-gcd-case-split : ( is-zero-ℤ @@ -555,7 +560,7 @@ unique-reduce-fraction-ℤ x y H = ( unique-numerator-reduce-fraction-ℤ x y H) ( eq-pair-Σ' ( pair - (unique-denominator-reduce-fraction-ℤ x y H) - (eq-is-prop + ( unique-denominator-reduce-fraction-ℤ x y H) + ( eq-is-prop ( is-prop-is-positive-ℤ (int-reduce-denominator-fraction-ℤ y)))))) ``` diff --git a/src/elementary-number-theory/squares-integers.lagda.md b/src/elementary-number-theory/squares-integers.lagda.md index a48fe7a26d..2497b17b33 100644 --- a/src/elementary-number-theory/squares-integers.lagda.md +++ b/src/elementary-number-theory/squares-integers.lagda.md @@ -10,7 +10,11 @@ module elementary-number-theory.squares-integers where open import elementary-number-theory.absolute-value-integers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers open import elementary-number-theory.squares-natural-numbers open import foundation.action-on-identifications-functions @@ -49,20 +53,12 @@ square-root-ℤ _ (root , _) = root ### Squares in ℤ are nonnegative ```agda -is-decidable-is-nonnegative-square-ℤ : - (a : ℤ) → - (is-nonnegative-ℤ a) + (is-nonnegative-ℤ (neg-ℤ a)) → - is-nonnegative-ℤ (square-ℤ a) -is-decidable-is-nonnegative-square-ℤ _ (inl x) = is-nonnegative-mul-ℤ x x -is-decidable-is-nonnegative-square-ℤ a (inr x) = - tr - ( is-nonnegative-ℤ) - ( double-negative-law-mul-ℤ a a) - ( is-nonnegative-mul-ℤ x x) - is-nonnegative-square-ℤ : (a : ℤ) → is-nonnegative-ℤ (square-ℤ a) is-nonnegative-square-ℤ a = - is-decidable-is-nonnegative-square-ℤ a decide-is-nonnegative-ℤ + rec-coproduct + ( λ H → is-nonnegative-is-positive-ℤ (is-positive-mul-negative-ℤ H H)) + ( λ H → is-nonnegative-mul-ℤ H H) + ( decide-is-negative-is-nonnegative-ℤ {a}) ``` ### The squares in ℤ are exactly the squares in ℕ diff --git a/src/elementary-number-theory/squares-natural-numbers.lagda.md b/src/elementary-number-theory/squares-natural-numbers.lagda.md index ce63c24575..f8afd7063e 100644 --- a/src/elementary-number-theory/squares-natural-numbers.lagda.md +++ b/src/elementary-number-theory/squares-natural-numbers.lagda.md @@ -104,7 +104,7 @@ contradiction by squaring both sides of the inequality greater-than-square-root-ℕ : (n root : ℕ) → ¬ ((n +ℕ 2 ≤-ℕ root) × (n +ℕ 2 ＝ square-ℕ root)) greater-than-square-root-ℕ n root (pf-leq , pf-eq) = - reflects-order-add-ℕ + reflects-leq-left-add-ℕ ( square-ℕ root) ( square-ℕ n +ℕ 2 *ℕ n +ℕ n +ℕ 2) ( 0) diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md new file mode 100644 index 0000000000..c943654ab8 --- /dev/null +++ b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md @@ -0,0 +1,303 @@ +# Strict inequality on the integer fractions + +```agda +module elementary-number-theory.strict-inequality-integer-fractions where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.addition-positive-and-negative-integers +open import elementary-number-theory.cross-multiplication-difference-integer-fractions +open import elementary-number-theory.difference-integers +open import elementary-number-theory.inequality-integer-fractions +open import elementary-number-theory.inequality-integers +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.mediant-integer-fractions +open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers +open import elementary-number-theory.strict-inequality-integers + +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.coproduct-types +open import foundation.decidable-propositions +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.transport-along-identifications +open import foundation.universe-levels +``` + +
+ +## Idea + +An [integer fraction](elementary-number-theory.integer-fractions.md) `m/n` is +_strictly less than_ the fraction `m'/n'` if the +[integer product](elementary-number-theory.multiplication-integers.md) `m * n'` +is [strictly less](elementary-number-theory.strict-inequality-integers.md) than +`m' * n`. + +## Definition + +### Strict inequality on the integer fractions + +```agda +le-fraction-ℤ-Prop : fraction-ℤ → fraction-ℤ → Prop lzero +le-fraction-ℤ-Prop (m , n , p) (m' , n' , p') = + le-ℤ-Prop (m *ℤ n') (m' *ℤ n) + +le-fraction-ℤ : fraction-ℤ → fraction-ℤ → UU lzero +le-fraction-ℤ x y = type-Prop (le-fraction-ℤ-Prop x y) + +is-prop-le-fraction-ℤ : (x y : fraction-ℤ) → is-prop (le-fraction-ℤ x y) +is-prop-le-fraction-ℤ x y = is-prop-type-Prop (le-fraction-ℤ-Prop x y) +``` + +## Properties + +### Strict inequality on the integer fractions is decidable + +```agda +is-decidable-le-fraction-ℤ : + (x y : fraction-ℤ) → (le-fraction-ℤ x y) + ¬ (le-fraction-ℤ x y) +is-decidable-le-fraction-ℤ x y = + is-decidable-le-ℤ + ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y) + ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x) + +le-fraction-ℤ-Decidable-Prop : (x y : fraction-ℤ) → Decidable-Prop lzero +le-fraction-ℤ-Decidable-Prop x y = + ( le-fraction-ℤ x y , + is-prop-le-fraction-ℤ x y , + is-decidable-le-fraction-ℤ x y) + +decide-le-leq-fraction-ℤ : + (x y : fraction-ℤ) → le-fraction-ℤ x y + leq-fraction-ℤ y x +decide-le-leq-fraction-ℤ x y = + map-coproduct + ( id) + ( λ H → + is-nonnegative-eq-ℤ + ( skew-commutative-cross-mul-diff-fraction-ℤ x y) + ( is-nonnegative-neg-is-nonpositive-ℤ H)) + ( decide-is-positive-is-nonpositive-ℤ) +``` + +### Strict inequality on the integer fractions implies inequality + +```agda +leq-le-fraction-ℤ : {x y : fraction-ℤ} → le-fraction-ℤ x y → leq-fraction-ℤ x y +leq-le-fraction-ℤ {x} {y} = + leq-le-ℤ + { mul-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ y)} + { mul-ℤ (numerator-fraction-ℤ y) (denominator-fraction-ℤ x)} +``` + +### Strict inequality on the integer fractions is asymmetric + +```agda +module _ + (x y : fraction-ℤ) + where + + asymmetric-le-fraction-ℤ : + le-fraction-ℤ x y → ¬ (le-fraction-ℤ y x) + asymmetric-le-fraction-ℤ = + asymmetric-le-ℤ + ( mul-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ y)) + ( mul-ℤ + ( numerator-fraction-ℤ y) + ( denominator-fraction-ℤ x)) +``` + +### Strict inequality on the integer fractions is transitive + +```agda +transitive-le-fraction-ℤ : + (p q r : fraction-ℤ) → + le-fraction-ℤ q r → + le-fraction-ℤ p q → + le-fraction-ℤ p r +transitive-le-fraction-ℤ p q r H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + ( is-positive-add-ℤ + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ p) + ( H)) + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ r) + ( H')))) + ( is-positive-denominator-fraction-ℤ q) +``` + +### Chaining rules for inequality and strict inequality on the integer fractions + +```agda +module _ + (p q r : fraction-ℤ) + where + + concatenate-le-leq-fraction-ℤ : + le-fraction-ℤ p q → + leq-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-le-leq-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + ( is-positive-add-nonnegative-positive-ℤ + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ p)) + ( H')) + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ r) + ( H)))) + ( is-positive-denominator-fraction-ℤ q) + + concatenate-leq-le-fraction-ℤ : + leq-fraction-ℤ p q → + le-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-leq-le-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + ( is-positive-add-positive-nonnegative-ℤ + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ p) + ( H')) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ r)) + ( H)))) + ( is-positive-denominator-fraction-ℤ q) +``` + +### Chaining rules for similarity and strict inequality on the integer fractions + +```agda +module _ + (p q r : fraction-ℤ) + where + + concatenate-sim-le-fraction-ℤ : + sim-fraction-ℤ p q → + le-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-sim-le-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H) + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ p) + ( H'))) + ( is-positive-denominator-fraction-ℤ q) + + concatenate-le-sim-fraction-ℤ : + le-fraction-ℤ p q → + sim-fraction-ℤ q r → + le-fraction-ℤ p r + concatenate-le-sim-fraction-ℤ H H' = + is-positive-right-factor-mul-ℤ + ( is-positive-eq-ℤ + ( inv ( lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H')) + ( is-positive-mul-ℤ + ( is-positive-denominator-fraction-ℤ r) + ( H))) + ( is-positive-denominator-fraction-ℤ q) +``` + +### Fractions with equal denominator compare the same as their numerators + +```agda +module _ + (x y : fraction-ℤ) (H : denominator-fraction-ℤ x ＝ denominator-fraction-ℤ y) + where + + le-fraction-le-numerator-fraction-ℤ : + le-ℤ (numerator-fraction-ℤ x) (numerator-fraction-ℤ y) → + le-fraction-ℤ x y + le-fraction-le-numerator-fraction-ℤ H' = + tr + ( λ (k : ℤ) → + le-ℤ + ( numerator-fraction-ℤ x *ℤ k) + ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)) + ( H) + ( preserves-le-left-mul-positive-ℤ + ( positive-denominator-fraction-ℤ x) + ( numerator-fraction-ℤ x) + ( numerator-fraction-ℤ y) + ( H')) +``` + +### The mediant of two distinct fractions lies strictly between them + +```agda +module _ + (x y : fraction-ℤ) + where + + le-left-mediant-fraction-ℤ : + le-fraction-ℤ x y → + le-fraction-ℤ x (mediant-fraction-ℤ x y) + le-left-mediant-fraction-ℤ = + is-positive-eq-ℤ (cross-mul-diff-left-mediant-fraction-ℤ x y) + + le-right-mediant-fraction-ℤ : + le-fraction-ℤ x y → + le-fraction-ℤ (mediant-fraction-ℤ x y) y + le-right-mediant-fraction-ℤ = + is-positive-eq-ℤ (cross-mul-diff-right-mediant-fraction-ℤ x y) +``` + +### Strict inequality on the integer fractions is dense + +```agda +module _ + (x y : fraction-ℤ) (H : le-fraction-ℤ x y) + where + + dense-le-fraction-ℤ : + ∃ fraction-ℤ (λ r → le-fraction-ℤ x r × le-fraction-ℤ r y) + dense-le-fraction-ℤ = + intro-∃ + ( mediant-fraction-ℤ x y) + ( le-left-mediant-fraction-ℤ x y H , le-right-mediant-fraction-ℤ x y H) +``` + +### Strict inequality on the integer fractions is located + +```agda +module _ + (x y z : fraction-ℤ) + where + + located-le-fraction-ℤ : + le-fraction-ℤ y z → (le-fraction-ℤ-Prop y x) ∨ (le-fraction-ℤ-Prop x z) + located-le-fraction-ℤ H = + unit-trunc-Prop + ( map-coproduct + ( id) + ( λ p → concatenate-leq-le-fraction-ℤ x y z p H) + ( decide-le-leq-fraction-ℤ y x)) +``` diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md new file mode 100644 index 0000000000..20bc5040ac --- /dev/null +++ b/src/elementary-number-theory/strict-inequality-integers.lagda.md @@ -0,0 +1,181 @@ +# Strict inequality on the integers + +```agda +module elementary-number-theory.strict-inequality-integers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.addition-positive-and-negative-integers +open import elementary-number-theory.difference-integers +open import elementary-number-theory.inequality-integers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.negative-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +open import elementary-number-theory.positive-integers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.decidable-propositions +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.negated-equality +open import foundation.negation +open import foundation.propositions +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels + +open import order-theory.posets +open import order-theory.preorders +``` + +
+ +## Idea + +An [integer](elementary-number-theory.integers.md) `x` is _strictly less than_ +the integer `y` if the +[difference](elementary-number-theory.difference-integers.md) `y - x` is +[positive](elementary-number-theory.positive-integers.md). This relation defines +the {{#concept "standard strict ordering" Disambiguation="integers" Agda=leq-ℤ}} +on the integers. + +## Definition + +### Strict inequality on the integers + +```agda +le-ℤ-Prop : ℤ → ℤ → Prop lzero +le-ℤ-Prop x y = subtype-positive-ℤ (y -ℤ x) + +le-ℤ : ℤ → ℤ → UU lzero +le-ℤ x y = type-Prop (le-ℤ-Prop x y) + +is-prop-le-ℤ : (x y : ℤ) → is-prop (le-ℤ x y) +is-prop-le-ℤ x y = is-prop-type-Prop (le-ℤ-Prop x y) +``` + +## Properties + +### Strict inequality on the integers implies inequality + +```agda +leq-le-ℤ : {x y : ℤ} → le-ℤ x y → leq-ℤ x y +leq-le-ℤ {x} {y} = is-nonnegative-is-positive-ℤ +``` + +### Strict inequality on the integers is decidable + +```agda +is-decidable-le-ℤ : (x y : ℤ) → (le-ℤ x y) + ¬ (le-ℤ x y) +is-decidable-le-ℤ x y = is-decidable-is-positive-ℤ (y -ℤ x) + +le-ℤ-Decidable-Prop : (x y : ℤ) → Decidable-Prop lzero +le-ℤ-Decidable-Prop x y = + ( le-ℤ x y , + is-prop-le-ℤ x y , + is-decidable-le-ℤ x y) +``` + +### Strict inequality on the integers is transitive + +```agda +transitive-le-ℤ : (k l m : ℤ) → le-ℤ l m → le-ℤ k l → le-ℤ k m +transitive-le-ℤ k l m H K = + is-positive-eq-ℤ + ( triangle-diff-ℤ m l k) + ( is-positive-add-ℤ H K) +``` + +### Strict inequality on the integers is asymmetric + +```agda +asymmetric-le-ℤ : (x y : ℤ) → le-ℤ x y → ¬ (le-ℤ y x) +asymmetric-le-ℤ x y p = + is-not-positive-is-nonpositive-ℤ + ( is-nonpositive-eq-ℤ + ( distributive-neg-diff-ℤ y x) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( is-nonnegative-is-positive-ℤ p))) +``` + +### Strict inequality on the integers is connected + +```agda +connected-le-ℤ : (x y : ℤ) → x ≠ y → le-ℤ x y + le-ℤ y x +connected-le-ℤ x y H = + map-coproduct + ( λ K → + is-positive-eq-ℤ + ( distributive-neg-diff-ℤ x y) + ( is-positive-neg-is-negative-ℤ K)) + ( id) + ( decide-sign-nonzero-ℤ (H ∘ eq-diff-ℤ)) +``` + +### Any integer is strictly greater than its predecessor + +```agda +le-pred-ℤ : (x : ℤ) → le-ℤ (pred-ℤ x) x +le-pred-ℤ x = + is-positive-eq-ℤ + ( inv (right-predecessor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x))) + ( is-positive-int-positive-ℤ one-positive-ℤ) +``` + +### Any integer is strictly lesser than its successor + +```agda +le-succ-ℤ : (x : ℤ) → le-ℤ x (succ-ℤ x) +le-succ-ℤ x = + is-positive-eq-ℤ + ( inv (left-successor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x))) + ( is-positive-int-positive-ℤ one-positive-ℤ) +``` + +### Addition on the integers preserves strict inequality + +```agda +preserves-le-left-add-ℤ : + (z x y : ℤ) → le-ℤ x y → le-ℤ (x +ℤ z) (y +ℤ z) +preserves-le-left-add-ℤ z x y = + is-positive-eq-ℤ (inv (right-translation-diff-ℤ y x z)) + +preserves-le-right-add-ℤ : + (z x y : ℤ) → le-ℤ x y → le-ℤ (z +ℤ x) (z +ℤ y) +preserves-le-right-add-ℤ z x y = + is-positive-eq-ℤ (inv (left-translation-diff-ℤ y x z)) + +preserves-le-add-ℤ : + {a b c d : ℤ} → le-ℤ a b → le-ℤ c d → le-ℤ (a +ℤ c) (b +ℤ d) +preserves-le-add-ℤ {a} {b} {c} {d} H K = + transitive-le-ℤ + ( a +ℤ c) + ( b +ℤ c) + ( b +ℤ d) + ( preserves-le-right-add-ℤ b c d K) + ( preserves-le-left-add-ℤ c a b H) +``` + +### Addition on the integers reflects strict inequality + +```agda +reflects-le-left-add-ℤ : + (z x y : ℤ) → le-ℤ (x +ℤ z) (y +ℤ z) → le-ℤ x y +reflects-le-left-add-ℤ z x y = + is-positive-eq-ℤ (right-translation-diff-ℤ y x z) + +reflects-le-right-add-ℤ : + (z x y : ℤ) → le-ℤ (z +ℤ x) (z +ℤ y) → le-ℤ x y +reflects-le-right-add-ℤ z x y = + is-positive-eq-ℤ (left-translation-diff-ℤ y x z) +``` diff --git a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md index 86954ce090..4c61b7d554 100644 --- a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md @@ -1,4 +1,4 @@ -# Strict inequality natural numbers +# Strict inequality on the natural numbers ```agda module elementary-number-theory.strict-inequality-natural-numbers where @@ -32,7 +32,7 @@ open import foundation.universe-levels ## Definition -### The strict ordering of the natural numbers +### The standard strict inequality on the natural numbers ```agda le-ℕ-Prop : ℕ → ℕ → Prop lzero @@ -68,7 +68,7 @@ concatenate-le-eq-ℕ : concatenate-le-eq-ℕ p refl = p ``` -### Strict inequality is decidable +### Strict inequality on the natural numbers is decidable ```agda is-decidable-le-ℕ : @@ -112,7 +112,7 @@ contradiction-le-one-ℕ zero-ℕ () contradiction-le-one-ℕ (succ-ℕ n) () ``` -### The strict ordering of the natural numbers is anti-reflexive +### The strict inequality on the natural numbers is anti-reflexive ```agda anti-reflexive-le-ℕ : (n : ℕ) → ¬ (n <-ℕ n) @@ -128,7 +128,7 @@ neq-le-ℕ {zero-ℕ} {succ-ℕ y} H = is-nonzero-succ-ℕ y ∘ inv neq-le-ℕ {succ-ℕ x} {succ-ℕ y} H p = neq-le-ℕ H (is-injective-succ-ℕ p) ``` -### Strict inequality is antisymmetric +### The strict inequality on the natural numbers is antisymmetric ```agda antisymmetric-le-ℕ : (m n : ℕ) → le-ℕ m n → le-ℕ n m → m ＝ n @@ -136,7 +136,7 @@ antisymmetric-le-ℕ (succ-ℕ m) (succ-ℕ n) p q = ap succ-ℕ (antisymmetric-le-ℕ m n p q) ``` -### The strict ordering of the natural numbers is transitive +### The strict inequality on the natural numbers is transitive ```agda transitive-le-ℕ : (n m l : ℕ) → (le-ℕ n m) → (le-ℕ m l) → (le-ℕ n l) @@ -161,7 +161,7 @@ transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) (succ-ℕ m) t s = transitive-le-ℕ' k l m t s ``` -### Strict inequality is linear +### The strict inequality on the natural numbers is linear ```agda linear-le-ℕ : (x y : ℕ) → (le-ℕ x y) + ((x ＝ y) + (le-ℕ y x)) diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md new file mode 100644 index 0000000000..6bbdc58319 --- /dev/null +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -0,0 +1,289 @@ +# Strict inequality on the rational numbers + +```agda +module elementary-number-theory.strict-inequality-rational-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.cross-multiplication-difference-integer-fractions +open import elementary-number-theory.difference-integers +open import elementary-number-theory.inequality-integer-fractions +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.mediant-integer-fractions +open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.nonnegative-integers +open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.positive-and-negative-integers +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-integer-fractions +open import elementary-number-theory.strict-inequality-integers + +open import foundation.binary-relations +open import foundation.cartesian-product-types +open import foundation.coproduct-types +open import foundation.decidable-propositions +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.universe-levels +``` + +
+ +## Idea + +The +{{#concept "standard strict ordering" Disambiguation="rational numbers" Agda=le-ℚ}} +on the [rational numbers](elementary-number-theory.rational-numbers.md) is +inherited from the +[standard strict ordering](elementary-number-theory.strict-inequality-integer-fractions.md) +on [integer fractions](elementary-number-theory.integer-fractions.md): the +rational number `m / n` is _strictly less than_ `m' / n'` if the +[integer product](elementary-number-theory.multiplication-integers.md) `m * n'` +is [strictly less](elementary-number-theory.strict-inequality-integers.md) than +`m' * n`. + +## Definition + +### The standard strict inequality on the rational numbers + +```agda +le-ℚ-Prop : ℚ → ℚ → Prop lzero +le-ℚ-Prop (x , px) (y , py) = le-fraction-ℤ-Prop x y + +le-ℚ : ℚ → ℚ → UU lzero +le-ℚ x y = type-Prop (le-ℚ-Prop x y) + +is-prop-le-ℚ : (x y : ℚ) → is-prop (le-ℚ x y) +is-prop-le-ℚ x y = is-prop-type-Prop (le-ℚ-Prop x y) +``` + +## Properties + +### Strict inequality on the rational numbers is decidable + +```agda +is-decidable-le-ℚ : (x y : ℚ) → (le-ℚ x y) + ¬ (le-ℚ x y) +is-decidable-le-ℚ x y = + is-decidable-le-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) + +le-ℚ-Decidable-Prop : (x y : ℚ) → Decidable-Prop lzero +le-ℚ-Decidable-Prop x y = + ( le-ℚ x y , + is-prop-le-ℚ x y , + is-decidable-le-ℚ x y) +``` + +### Strict inequality on the rational numbers implies inequality + +```agda +leq-le-ℚ : {x y : ℚ} → le-ℚ x y → leq-ℚ x y +leq-le-ℚ {x} {y} = leq-le-fraction-ℤ {fraction-ℚ x} {fraction-ℚ y} +``` + +### Strict inequality on the rationals is asymmetric + +```agda +asymmetric-le-ℚ : (x y : ℚ) → le-ℚ x y → ¬ (le-ℚ y x) +asymmetric-le-ℚ x y = + asymmetric-le-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + +irreflexive-le-ℚ : (x : ℚ) → ¬ (le-ℚ x x) +irreflexive-le-ℚ = + is-irreflexive-is-asymmetric le-ℚ asymmetric-le-ℚ +``` + +### Strict inequality on the rationals is transitive + +```agda +module _ + (x y z : ℚ) + where + + transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z + transitive-le-ℚ = + transitive-le-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) +``` + +### Concatenation rules for inequality and strict inequality on the rational numbers + +```agda +module _ + (x y z : ℚ) + where + + concatenate-le-leq-ℚ : le-ℚ x y → leq-ℚ y z → le-ℚ x z + concatenate-le-leq-ℚ = + concatenate-le-leq-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) + + concatenate-leq-le-ℚ : leq-ℚ x y → le-ℚ y z → le-ℚ x z + concatenate-leq-le-ℚ = + concatenate-leq-le-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y) + ( fraction-ℚ z) +``` + +### Strict inequality on the rational numbers reflects the strict inequality of their underlying fractions + +```agda +module _ + (x : ℚ) (p : fraction-ℤ) + where + + right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : + le-fraction-ℤ (fraction-ℚ x) p → + le-ℚ x (in-fraction-ℤ p) + right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ H = + concatenate-le-sim-fraction-ℤ + ( fraction-ℚ x) + ( p) + ( fraction-ℚ ( in-fraction-ℤ p)) + ( H) + ( sim-reduced-fraction-ℤ p) + + left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ : + le-fraction-ℤ p (fraction-ℚ x) → + le-ℚ (in-fraction-ℤ p) x + left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ = + concatenate-sim-le-fraction-ℤ + ( fraction-ℚ ( in-fraction-ℤ p)) + ( p) + ( fraction-ℚ x) + ( symmetric-sim-fraction-ℤ + ( p) + ( fraction-ℚ ( in-fraction-ℤ p)) + ( sim-reduced-fraction-ℤ p)) +``` + +### The rational numbers have no lower or upper bound + +```agda +module _ + (x : ℚ) + where + + left-∃-le-ℚ : ∃ ℚ (λ q → le-ℚ q x) + left-∃-le-ℚ = intro-∃ + ( in-fraction-ℤ frac) + ( left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac + ( le-fraction-le-numerator-fraction-ℤ + ( frac) + ( fraction-ℚ x) + ( refl) + ( le-pred-ℤ (numerator-ℚ x)))) + where + frac : fraction-ℤ + frac = (pred-ℤ (numerator-ℚ x) , positive-denominator-ℚ x) + + right-∃-le-ℚ : ∃ ℚ (λ r → le-ℚ x r) + right-∃-le-ℚ = intro-∃ + ( in-fraction-ℤ frac) + ( right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac + ( le-fraction-le-numerator-fraction-ℤ + ( fraction-ℚ x) + ( frac) + ( refl) + ( le-succ-ℤ (numerator-ℚ x)))) + where + frac : fraction-ℤ + frac = (succ-ℤ (numerator-ℚ x) , positive-denominator-ℚ x) +``` + +### For any two rational numbers `x` and `y`, either `x < y` or `y ≤ x` + +```agda +decide-le-leq-ℚ : (x y : ℚ) → le-ℚ x y + leq-ℚ y x +decide-le-leq-ℚ x y = + map-coproduct + ( id) + ( λ H → + is-nonnegative-eq-ℤ + ( skew-commutative-cross-mul-diff-fraction-ℤ + ( fraction-ℚ x) + ( fraction-ℚ y)) + ( is-nonnegative-neg-is-nonpositive-ℤ H)) + ( decide-is-positive-is-nonpositive-ℤ) +``` + +### Trichotomy on the rationals + +```agda +trichotomy-le-ℚ : + {l : Level} {A : UU l} (x y : ℚ) → + ( le-ℚ x y → A) → + ( Id x y → A) → + ( le-ℚ y x → A) → + A +trichotomy-le-ℚ x y left eq right with decide-le-leq-ℚ x y | decide-le-leq-ℚ y x +... | inl I | _ = left I +... | inr I | inl I' = right I' +... | inr I | inr I' = eq (antisymmetric-leq-ℚ x y I' I) +``` + +### The mediant of two distinct rationals is strictly between them + +```agda +module _ + (x y : ℚ) (H : le-ℚ x y) + where + + le-left-mediant-ℚ : le-ℚ x (mediant-ℚ x y) + le-left-mediant-ℚ = + right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x + ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( le-left-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) + + le-right-mediant-ℚ : le-ℚ (mediant-ℚ x y) y + le-right-mediant-ℚ = + left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ y + ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)) + ( le-right-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H) +``` + +### Strict inequality on the rational numbers is dense + +```agda +module _ + (x y : ℚ) (H : le-ℚ x y) + where + + dense-le-ℚ : ∃ ℚ (λ r → le-ℚ x r × le-ℚ r y) + dense-le-ℚ = + intro-∃ + ( mediant-ℚ x y) + ( le-left-mediant-ℚ x y H , le-right-mediant-ℚ x y H) +``` + +### Strict inequality on the rational numbers is located + +```agda +located-le-ℚ : (x y z : ℚ) → le-ℚ y z → (le-ℚ-Prop y x) ∨ (le-ℚ-Prop x z) +located-le-ℚ x y z H = + unit-trunc-Prop + ( map-coproduct + ( id) + ( λ p → concatenate-leq-le-ℚ x y z p H) + ( decide-le-leq-ℚ y x)) +``` diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md index 69022e3f2e..599a3c4926 100644 --- a/src/real-numbers/dedekind-real-numbers.lagda.md +++ b/src/real-numbers/dedekind-real-numbers.lagda.md @@ -9,6 +9,7 @@ module real-numbers.dedekind-real-numbers where ```agda 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.binary-transport open import foundation.cartesian-product-types diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index 878b9e33fc..b76bbfaf7b 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -9,6 +9,7 @@ module real-numbers.rational-real-numbers where ```agda 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.action-on-identifications-functions open import foundation.cartesian-product-types @@ -61,13 +62,13 @@ is-dedekind-cut-le-ℚ x = elim-exists-Prop ( λ r → product-Prop ( le-ℚ-Prop q r) ( le-ℚ-Prop r x)) ( le-ℚ-Prop q x) - ( λ r (H , H') → transitive-le-ℚ q r x H H')) , + ( λ r (H , H') → transitive-le-ℚ q r x H' H)) , ( λ (r : ℚ) → α x r ∘ dense-le-ℚ x r , elim-exists-Prop ( λ q → product-Prop ( le-ℚ-Prop q r) ( le-ℚ-Prop x q)) ( le-ℚ-Prop x r) - ( λ q (H , H') → transitive-le-ℚ x q r H' H))) , + ( λ q (H , H') → transitive-le-ℚ x q r H H'))) , ( λ (q : ℚ) (H , H') → asymmetric-le-ℚ q x H H') , ( located-le-ℚ x) where