From c50af11d0fee3b09eba2d479d7adcf9b3e9a178a Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 20 Jan 2025 15:18:26 -0800 Subject: [PATCH 01/17] Define the theorem to prove --- .../strict-inequality-rational-numbers.lagda.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index f15fb7085d..0388bb8b9e 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -445,3 +445,10 @@ located-le-ℚ x y z H = ( λ p → concatenate-leq-le-ℚ x y z p H) ( decide-le-leq-ℚ y x)) ``` + +### Negation reverses the ordering of strict inequality on the rational numbers + +```agda +neg-le-ℚ : + (x y : ℚ) → le-ℚ x y → le-ℚ (neg-ℚ y) (neg-ℚ x) +``` From 8384f315bd2e4ed9ed025f61577a0f3c5efebf94 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 20 Jan 2025 15:20:41 -0800 Subject: [PATCH 02/17] Define the theorem on integer fractions --- .../strict-inequality-integer-fractions.lagda.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md index 5afdad1e89..40eae18afe 100644 --- a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md @@ -339,3 +339,15 @@ module _ ( numerator-fraction-ℤ x) ( denominator-fraction-ℤ y)))) ``` + +### Negation reverses the order of strict inequality on rational numbers + +```agda +module _ + (x y : fraction-ℤ) (H : le-fraction-ℤ x y) + where + + neg-le-fraction-ℤ : + le-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ y) + +``` From fd7c61390077dba499b0812cbe41ffad56d551ea Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 20 Jan 2025 15:34:35 -0800 Subject: [PATCH 03/17] Prove the theorem on integers --- .../strict-inequality-integers.lagda.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index 2989ad4e5d..3afa9dec3f 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integers.lagda.md @@ -268,3 +268,19 @@ module _ ( le-zero-is-negative-ℤ y H) ( I)) ``` + +### Negation reverses the order of strict inequality of integers + +```agda +module _ + (x y : ℤ) (I : le-ℤ x y) + where + + neg-le-ℤ : le-ℤ (neg-ℤ y) (neg-ℤ x) + neg-le-ℤ = + tr + is-positive-ℤ + (ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙ + commutative-add-ℤ (neg-ℤ (neg-ℤ y)) (neg-ℤ x)) + I +``` From e0ed494c6876da9226ced4a53b149203f0009cef Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Mon, 20 Jan 2025 16:04:33 -0800 Subject: [PATCH 04/17] Prove the theorem on rationals --- ...rict-inequality-integer-fractions.lagda.md | 19 +++++++++++-------- ...trict-inequality-rational-numbers.lagda.md | 1 + 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md index 40eae18afe..3c96b0fd89 100644 --- a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md @@ -26,6 +26,7 @@ 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.binary-transport open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.coproduct-types @@ -340,14 +341,16 @@ module _ ( denominator-fraction-ℤ y)))) ``` -### Negation reverses the order of strict inequality on rational numbers +### Negation reverses the order of strict inequality on integer fractions ```agda -module _ - (x y : fraction-ℤ) (H : le-fraction-ℤ x y) - where - - neg-le-fraction-ℤ : - le-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ y) - +neg-le-fraction-ℤ : + (x y : fraction-ℤ) → + le-fraction-ℤ x y → + le-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ x) +neg-le-fraction-ℤ (m , n , p) (m' , n' , p') H = + binary-tr le-ℤ + (inv (left-negative-law-mul-ℤ m' n)) + (inv (left-negative-law-mul-ℤ m n')) + (neg-le-ℤ (m *ℤ n') (m' *ℤ n) H) ``` diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index 0388bb8b9e..8d93ddef7c 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -451,4 +451,5 @@ located-le-ℚ x y z H = ```agda neg-le-ℚ : (x y : ℚ) → le-ℚ x y → le-ℚ (neg-ℚ y) (neg-ℚ x) +neg-le-ℚ x y = neg-le-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) ``` From d3cea33402d7d41cadbe5af8e8be7c86408fdd72 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 29 Jan 2025 09:48:57 -0800 Subject: [PATCH 05/17] Add lowasser to CONTRIBUTORS.toml --- CONTRIBUTORS.toml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CONTRIBUTORS.toml b/CONTRIBUTORS.toml index 34027f6812..e895ae5ed3 100644 --- a/CONTRIBUTORS.toml +++ b/CONTRIBUTORS.toml @@ -252,3 +252,8 @@ github = "djspacewhale" displayName = "Job Petrovčič" usernames = [ "Job Petrovčič", "JobPetrovcic" ] github = "JobPetrovcic" + +[[contributors]] +displayName = "Louis Wasserman" +usernames = [ "Louis Wasserman" ] +github = "lowasser" From e292096c2524375c398e9b92a0af4d2750f4b24d Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 29 Jan 2025 10:08:40 -0800 Subject: [PATCH 06/17] Define the negation of a real number, and prove it is itself real. --- ...rict-inequality-integer-fractions.lagda.md | 15 ++ .../strict-inequality-integers.lagda.md | 16 ++ ...trict-inequality-rational-numbers.lagda.md | 8 + .../negation-real-numbers.lagda.md | 155 ++++++++++++++++++ 4 files changed, 194 insertions(+) create mode 100644 src/real-numbers/negation-real-numbers.lagda.md diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md index 5afdad1e89..3c96b0fd89 100644 --- a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md @@ -26,6 +26,7 @@ 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.binary-transport open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.coproduct-types @@ -339,3 +340,17 @@ module _ ( numerator-fraction-ℤ x) ( denominator-fraction-ℤ y)))) ``` + +### Negation reverses the order of strict inequality on integer fractions + +```agda +neg-le-fraction-ℤ : + (x y : fraction-ℤ) → + le-fraction-ℤ x y → + le-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ x) +neg-le-fraction-ℤ (m , n , p) (m' , n' , p') H = + binary-tr le-ℤ + (inv (left-negative-law-mul-ℤ m' n)) + (inv (left-negative-law-mul-ℤ m n')) + (neg-le-ℤ (m *ℤ n') (m' *ℤ n) H) +``` diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index 2989ad4e5d..3afa9dec3f 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integers.lagda.md @@ -268,3 +268,19 @@ module _ ( le-zero-is-negative-ℤ y H) ( I)) ``` + +### Negation reverses the order of strict inequality of integers + +```agda +module _ + (x y : ℤ) (I : le-ℤ x y) + where + + neg-le-ℤ : le-ℤ (neg-ℤ y) (neg-ℤ x) + neg-le-ℤ = + tr + is-positive-ℤ + (ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙ + commutative-add-ℤ (neg-ℤ (neg-ℤ y)) (neg-ℤ x)) + I +``` diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index f15fb7085d..8d93ddef7c 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -445,3 +445,11 @@ located-le-ℚ x y z H = ( λ p → concatenate-leq-le-ℚ x y z p H) ( decide-le-leq-ℚ y x)) ``` + +### Negation reverses the ordering of strict inequality on the rational numbers + +```agda +neg-le-ℚ : + (x y : ℚ) → le-ℚ x y → le-ℚ (neg-ℚ y) (neg-ℚ x) +neg-le-ℚ x y = neg-le-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) +``` diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md new file mode 100644 index 0000000000..664e578fe3 --- /dev/null +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -0,0 +1,155 @@ +# Signs of real numbers + +```agda +module real-numbers.negation-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +``` + +
+ +## Idea + +The negation of a Dedekind real number with cuts `L, U` has lower cut equal to +the negation of elements of `U`, and upper cut equal to the negation of elements +in `L`. + +```agda +module _ + {l : Level} (x : ℝ l) + where + + lower-cut-neg-ℝ : subtype l ℚ + lower-cut-neg-ℝ q = upper-cut-ℝ x (neg-ℚ q) + + upper-cut-neg-ℝ : subtype l ℚ + upper-cut-neg-ℝ q = lower-cut-ℝ x (neg-ℚ q) + + inhabited-lower-cut-neg-ℝ : exists ℚ lower-cut-neg-ℝ + inhabited-lower-cut-neg-ℝ = + elim-exists + (∃ ℚ lower-cut-neg-ℝ) + (λ q q-in-upper → + intro-exists + (neg-ℚ q) + (tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ q)) q-in-upper)) + (is-inhabited-upper-cut-ℝ x) + + inhabited-upper-cut-neg-ℝ : exists ℚ upper-cut-neg-ℝ + inhabited-upper-cut-neg-ℝ = + elim-exists + (∃ ℚ upper-cut-neg-ℝ) + (λ q q-in-lower → + intro-exists + (neg-ℚ q) + (tr (is-in-lower-cut-ℝ x) (inv (neg-neg-ℚ q)) q-in-lower)) + (is-inhabited-lower-cut-ℝ x) + + is-rounded-lower-cut-neg-ℝ : + (q : ℚ) → + is-in-subtype lower-cut-neg-ℝ q ↔ + exists ℚ (λ r → (le-ℚ-Prop q r) ∧ (lower-cut-neg-ℝ r)) + pr1 (is-rounded-lower-cut-neg-ℝ q) in-neg-lower = + elim-exists + (∃ ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-neg-ℝ r)) + (λ r (r<-q , in-upper-r) → + intro-exists + (neg-ℚ r) + (tr + (λ x → le-ℚ x (neg-ℚ r)) + (neg-neg-ℚ q) + (neg-le-ℚ r (neg-ℚ q) r<-q) , + tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ r)) in-upper-r)) + (forward-implication (is-rounded-upper-cut-ℝ x (neg-ℚ q)) in-neg-lower) + pr2 (is-rounded-lower-cut-neg-ℝ q) exists-r = + backward-implication + (is-rounded-upper-cut-ℝ x (neg-ℚ q)) + (elim-exists + (∃ ℚ (λ r → le-ℚ-Prop r (neg-ℚ q) ∧ upper-cut-ℝ x r)) + (λ r (q Date: Wed, 29 Jan 2025 10:10:33 -0800 Subject: [PATCH 07/17] Make naming slightly more consistent with precedent. --- src/real-numbers/negation-real-numbers.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index 664e578fe3..f7e75ae16b 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -49,7 +49,7 @@ module _ upper-cut-neg-ℝ : subtype l ℚ upper-cut-neg-ℝ q = lower-cut-ℝ x (neg-ℚ q) - inhabited-lower-cut-neg-ℝ : exists ℚ lower-cut-neg-ℝ + is-inhabited-lower-cut-neg-ℝ : exists ℚ lower-cut-neg-ℝ inhabited-lower-cut-neg-ℝ = elim-exists (∃ ℚ lower-cut-neg-ℝ) @@ -59,8 +59,8 @@ module _ (tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ q)) q-in-upper)) (is-inhabited-upper-cut-ℝ x) - inhabited-upper-cut-neg-ℝ : exists ℚ upper-cut-neg-ℝ - inhabited-upper-cut-neg-ℝ = + is-inhabited-upper-cut-neg-ℝ : exists ℚ upper-cut-neg-ℝ + is-inhabited-upper-cut-neg-ℝ = elim-exists (∃ ℚ upper-cut-neg-ℝ) (λ q q-in-lower → @@ -137,7 +137,7 @@ module _ real-dedekind-cut lower-cut-neg-ℝ upper-cut-neg-ℝ - ((inhabited-lower-cut-neg-ℝ , inhabited-upper-cut-neg-ℝ) , + ((is-inhabited-lower-cut-neg-ℝ , is-inhabited-upper-cut-neg-ℝ) , (is-rounded-lower-cut-neg-ℝ , is-rounded-upper-cut-neg-ℝ) , is-disjoint-cut-neg-ℝ , is-located-lower-upper-cut-neg-ℝ) From a40d503765ecc5328cef53d89fea3385b18845aa Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Wed, 29 Jan 2025 20:47:23 -0800 Subject: [PATCH 08/17] Typo fix --- src/real-numbers/negation-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index f7e75ae16b..08b8f6eeb2 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -50,7 +50,7 @@ module _ upper-cut-neg-ℝ q = lower-cut-ℝ x (neg-ℚ q) is-inhabited-lower-cut-neg-ℝ : exists ℚ lower-cut-neg-ℝ - inhabited-lower-cut-neg-ℝ = + is-inhabited-lower-cut-neg-ℝ = elim-exists (∃ ℚ lower-cut-neg-ℝ) (λ q q-in-upper → From 1f46e1a315030979e5703a4a6c2d5923eed79f1b Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Thu, 30 Jan 2025 13:32:54 -0800 Subject: [PATCH 09/17] Fix file header --- src/real-numbers/negation-real-numbers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index 08b8f6eeb2..bade41ed90 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -1,4 +1,4 @@ -# Signs of real numbers +# Negation of real numbers ```agda module real-numbers.negation-real-numbers where From 7b3207894451ecec9c45914d56ea59e881656907 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 31 Jan 2025 08:55:58 -0800 Subject: [PATCH 10/17] make pre-commit updates --- src/real-numbers.lagda.md | 1 + src/real-numbers/negation-real-numbers.lagda.md | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index a4f057db42..e6d7266ffc 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -7,5 +7,6 @@ module real-numbers where open import real-numbers.dedekind-real-numbers public open import real-numbers.metric-space-of-real-numbers public +open import real-numbers.negation-real-numbers public open import real-numbers.rational-real-numbers public ``` diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index bade41ed90..b76bf4a281 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -83,7 +83,7 @@ module _ (λ x → le-ℚ x (neg-ℚ r)) (neg-neg-ℚ q) (neg-le-ℚ r (neg-ℚ q) r<-q) , - tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ r)) in-upper-r)) + tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ r)) in-upper-r)) (forward-implication (is-rounded-upper-cut-ℝ x (neg-ℚ q)) in-neg-lower) pr2 (is-rounded-lower-cut-neg-ℝ q) exists-r = backward-implication From c1092af3de3e6e2304972423c11949d57b6261cc Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 31 Jan 2025 10:38:44 -0800 Subject: [PATCH 11/17] Fix indentation style --- .../strict-inequality-integer-fractions.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md index 3c96b0fd89..cb04a49b11 100644 --- a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md @@ -350,7 +350,7 @@ neg-le-fraction-ℤ : le-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ x) neg-le-fraction-ℤ (m , n , p) (m' , n' , p') H = binary-tr le-ℤ - (inv (left-negative-law-mul-ℤ m' n)) - (inv (left-negative-law-mul-ℤ m n')) - (neg-le-ℤ (m *ℤ n') (m' *ℤ n) H) + ( inv (left-negative-law-mul-ℤ m' n)) + ( inv (left-negative-law-mul-ℤ m n')) + ( neg-le-ℤ (m *ℤ n') (m' *ℤ n) H) ``` From 41586183c53214f7a1faffd49b8657844f271e2e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 31 Jan 2025 10:40:27 -0800 Subject: [PATCH 12/17] Fix more indentatino --- .../strict-inequality-integers.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index 3afa9dec3f..7187b86618 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integers.lagda.md @@ -279,8 +279,8 @@ module _ neg-le-ℤ : le-ℤ (neg-ℤ y) (neg-ℤ x) neg-le-ℤ = tr - is-positive-ℤ - (ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙ + ( is-positive-ℤ) + ( ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙ commutative-add-ℤ (neg-ℤ (neg-ℤ y)) (neg-ℤ x)) I ``` From 201c3a4f5a34d761d96f4bbbeca3ff0e9bd6538e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Fri, 31 Jan 2025 10:44:17 -0800 Subject: [PATCH 13/17] Attempt to fix indentation --- .../negation-real-numbers.lagda.md | 83 ++++++++++--------- 1 file changed, 42 insertions(+), 41 deletions(-) diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index b76bf4a281..087ff569f7 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -52,22 +52,22 @@ module _ is-inhabited-lower-cut-neg-ℝ : exists ℚ lower-cut-neg-ℝ is-inhabited-lower-cut-neg-ℝ = elim-exists - (∃ ℚ lower-cut-neg-ℝ) - (λ q q-in-upper → + ( ∃ ℚ lower-cut-neg-ℝ) + ( λ q q-in-upper → intro-exists (neg-ℚ q) (tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ q)) q-in-upper)) - (is-inhabited-upper-cut-ℝ x) + ( is-inhabited-upper-cut-ℝ x) is-inhabited-upper-cut-neg-ℝ : exists ℚ upper-cut-neg-ℝ is-inhabited-upper-cut-neg-ℝ = elim-exists - (∃ ℚ upper-cut-neg-ℝ) - (λ q q-in-lower → + ( ∃ ℚ upper-cut-neg-ℝ) + ( λ q q-in-lower → intro-exists (neg-ℚ q) (tr (is-in-lower-cut-ℝ x) (inv (neg-neg-ℚ q)) q-in-lower)) - (is-inhabited-lower-cut-ℝ x) + ( is-inhabited-lower-cut-ℝ x) is-rounded-lower-cut-neg-ℝ : (q : ℚ) → @@ -75,24 +75,24 @@ module _ exists ℚ (λ r → (le-ℚ-Prop q r) ∧ (lower-cut-neg-ℝ r)) pr1 (is-rounded-lower-cut-neg-ℝ q) in-neg-lower = elim-exists - (∃ ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-neg-ℝ r)) - (λ r (r<-q , in-upper-r) → + ( ∃ ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-neg-ℝ r)) + ( λ r (r<-q , in-upper-r) → intro-exists - (neg-ℚ r) - (tr - (λ x → le-ℚ x (neg-ℚ r)) - (neg-neg-ℚ q) - (neg-le-ℚ r (neg-ℚ q) r<-q) , + ( neg-ℚ r) + ( tr + ( λ x → le-ℚ x (neg-ℚ r)) + ( neg-neg-ℚ q) + ( neg-le-ℚ r (neg-ℚ q) r<-q) , tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ r)) in-upper-r)) - (forward-implication (is-rounded-upper-cut-ℝ x (neg-ℚ q)) in-neg-lower) + ( forward-implication (is-rounded-upper-cut-ℝ x (neg-ℚ q)) in-neg-lower) pr2 (is-rounded-lower-cut-neg-ℝ q) exists-r = backward-implication - (is-rounded-upper-cut-ℝ x (neg-ℚ q)) - (elim-exists - (∃ ℚ (λ r → le-ℚ-Prop r (neg-ℚ q) ∧ upper-cut-ℝ x r)) - (λ r (q Date: Fri, 31 Jan 2025 10:50:05 -0800 Subject: [PATCH 14/17] Fix missed indentation --- src/real-numbers/negation-real-numbers.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index 087ff569f7..679cb36dae 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -100,13 +100,13 @@ module _ exists ℚ (λ q → (le-ℚ-Prop q r) ∧ (upper-cut-neg-ℝ q)) pr1 (is-rounded-upper-cut-neg-ℝ r) in-neg-upper = elim-exists - (∃ ℚ (λ q → le-ℚ-Prop q r ∧ upper-cut-neg-ℝ q)) - (λ q (-r Date: Fri, 31 Jan 2025 16:57:05 -0800 Subject: [PATCH 15/17] Apply suggestions from code review Co-authored-by: Fredrik Bakke Co-authored-by: Egbert Rijke --- .../strict-inequality-integers.lagda.md | 17 ++++++----------- .../strict-inequality-rational-numbers.lagda.md | 3 +-- src/real-numbers/negation-real-numbers.lagda.md | 6 +++--- 3 files changed, 10 insertions(+), 16 deletions(-) diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index 7187b86618..9c434f9ec8 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integers.lagda.md @@ -272,15 +272,10 @@ module _ ### Negation reverses the order of strict inequality of integers ```agda -module _ - (x y : ℤ) (I : le-ℤ x y) - where - - neg-le-ℤ : le-ℤ (neg-ℤ y) (neg-ℤ x) - neg-le-ℤ = - tr - ( is-positive-ℤ) - ( ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙ - commutative-add-ℤ (neg-ℤ (neg-ℤ y)) (neg-ℤ x)) - I +neg-le-ℤ : (x y : ℤ) → le-ℤ x y → le-ℤ (neg-ℤ y) (neg-ℤ x) +neg-le-ℤ x y = + tr + ( is-positive-ℤ) + ( ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙ + commutative-add-ℤ (neg-ℤ (neg-ℤ y)) (neg-ℤ 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 index 8d93ddef7c..91d98033f3 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md @@ -449,7 +449,6 @@ located-le-ℚ x y z H = ### Negation reverses the ordering of strict inequality on the rational numbers ```agda -neg-le-ℚ : - (x y : ℚ) → le-ℚ x y → le-ℚ (neg-ℚ y) (neg-ℚ x) +neg-le-ℚ : (x y : ℚ) → le-ℚ x y → le-ℚ (neg-ℚ y) (neg-ℚ x) neg-le-ℚ x y = neg-le-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) ``` diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index 679cb36dae..9f95642814 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -34,7 +34,7 @@ open import real-numbers.dedekind-real-numbers ## Idea -The negation of a Dedekind real number with cuts `L, U` has lower cut equal to +The {{#concept "negation" Disambiguation="Dedekind real number" Agda=neg-ℝ}} of a [Dedekind real number](real-numbers.dedekind-real-numbers.md) with cuts `(L, U)` has lower cut equal to the negation of elements of `U`, and upper cut equal to the negation of elements in `L`. @@ -118,13 +118,13 @@ module _ is-disjoint-cut-neg-ℝ : (q : ℚ) → - ¬ (is-in-subtype lower-cut-neg-ℝ q × is-in-subtype upper-cut-neg-ℝ q) + ¬ (is-in-subtype lower-cut-neg-ℝ q × is-in-subtype upper-cut-neg-ℝ q) is-disjoint-cut-neg-ℝ q (in-lower-neg , in-upper-neg) = is-disjoint-cut-ℝ x (neg-ℚ q) (in-upper-neg , in-lower-neg) is-located-lower-upper-cut-neg-ℝ : (q r : ℚ) → le-ℚ q r → - type-disjunction-Prop (lower-cut-neg-ℝ q) (upper-cut-neg-ℝ r) + type-disjunction-Prop (lower-cut-neg-ℝ q) (upper-cut-neg-ℝ r) is-located-lower-upper-cut-neg-ℝ q r q Date: Tue, 4 Feb 2025 14:28:51 -0800 Subject: [PATCH 16/17] Fix merge --- .../strict-inequality-integers.lagda.md | 1 - src/real-numbers/negation-real-numbers.lagda.md | 2 ++ 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index 6e967e7cde..107592ee5c 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/src/elementary-number-theory/strict-inequality-integers.lagda.md @@ -258,7 +258,6 @@ module _ module _ (x y : ℤ) (I : le-ℤ x y) where -(l : Level) → ℝ l abstract is-negative-le-negative-ℤ : is-negative-ℤ y → is-negative-ℤ x is-negative-le-negative-ℤ H = diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index 9f95642814..dcb4fccd86 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -1,6 +1,8 @@ # Negation of real numbers ```agda +{-# OPTIONS --lossy-unification #-} + module real-numbers.negation-real-numbers where ``` From 7291c8239983a2afbcca3a7b5737497c3e6c6ac3 Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Tue, 4 Feb 2025 14:29:41 -0800 Subject: [PATCH 17/17] make pre-commit formatting --- src/real-numbers/negation-real-numbers.lagda.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/real-numbers/negation-real-numbers.lagda.md b/src/real-numbers/negation-real-numbers.lagda.md index dcb4fccd86..dfe6575734 100644 --- a/src/real-numbers/negation-real-numbers.lagda.md +++ b/src/real-numbers/negation-real-numbers.lagda.md @@ -36,9 +36,10 @@ open import real-numbers.dedekind-real-numbers ## Idea -The {{#concept "negation" Disambiguation="Dedekind real number" Agda=neg-ℝ}} of a [Dedekind real number](real-numbers.dedekind-real-numbers.md) with cuts `(L, U)` has lower cut equal to -the negation of elements of `U`, and upper cut equal to the negation of elements -in `L`. +The {{#concept "negation" Disambiguation="Dedekind real number" Agda=neg-ℝ}} of +a [Dedekind real number](real-numbers.dedekind-real-numbers.md) with cuts +`(L, U)` has lower cut equal to the negation of elements of `U`, and upper cut +equal to the negation of elements in `L`. ```agda module _