From 098dc4820ce164591e5d12b6b83c8b21782b1b58 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 19 Jul 2024 10:12:41 +0200 Subject: [PATCH 1/4] =?UTF-8?q?Define=20Data.Nat.=E2=89=B0=E2=87=92?= =?UTF-8?q?=E2=89=A5=20directly=20and=20earlier?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Properties.agda | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index e2d667f3e9..4bc5aa98d5 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -162,6 +162,11 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) -- Properties of _≤_ ------------------------------------------------------------------------ +≰⇒≥ : _≰_ ⇒ _≥_ +≰⇒≥ {m} {zero} m≰n = z≤n +≰⇒≥ {zero} {suc n} m≰n = contradiction z≤n m≰n +≰⇒≥ {suc m} {suc n} m≰n = s≤s (≰⇒≥ (m≰n ∘ s≤s)) + ------------------------------------------------------------------------ -- Relational properties of _≤_ @@ -331,9 +336,6 @@ n≤1⇒n≡0∨n≡1 (s≤s z≤n) = inj₂ refl ≰⇒> {suc m} {zero} _ = z {suc m} {suc n} m≰n = s (m≰n ∘ s≤s)) -≰⇒≥ : _≰_ ⇒ _≥_ -≰⇒≥ = <⇒≤ ∘ ≰⇒> - ≮⇒≥ : _≮_ ⇒ _≥_ ≮⇒≥ {_} {zero} _ = z≤n ≮⇒≥ {zero} {suc j} 1≮j+1 = contradiction z Date: Fri, 19 Jul 2024 10:13:10 +0200 Subject: [PATCH 2/4] =?UTF-8?q?Define=20Data.Nat.=E2=89=A4-total=20in=20te?= =?UTF-8?q?rms=20of=20=5F=E2=89=A4=3F=5F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Properties.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 4bc5aa98d5..e4b04f02be 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -185,11 +185,6 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ≤-trans z≤n _ = z≤n ≤-trans (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o) -≤-total : Total _≤_ -≤-total zero _ = inj₁ z≤n -≤-total _ zero = inj₂ z≤n -≤-total (suc m) (suc n) = Sum.map s≤s s≤s (≤-total m n) - ≤-irrelevant : Irrelevant _≤_ ≤-irrelevant z≤n z≤n = refl ≤-irrelevant (s≤s m≤n₁) (s≤s m≤n₂) = cong s≤s (≤-irrelevant m≤n₁ m≤n₂) @@ -208,6 +203,11 @@ m ≤? n = map′ (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ (T? (m ≤ᵇ n)) _≥?_ : Decidable _≥_ _≥?_ = flip _≤?_ +≤-total : Total _≤_ +≤-total m n with m ≤? n +... | yes m≤n = inj₁ m≤n +... | no m≰n = inj₂ (≰⇒≥ m≰n) + ------------------------------------------------------------------------ -- Structures From d8d20015c6aa64a08de75dac580ee418888fbffb Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 30 Aug 2024 16:17:01 +0200 Subject: [PATCH 3/4] Update changelog --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f16ed00b65..ca3bb98120 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,11 @@ Bug-fixes Non-backwards compatible changes -------------------------------- +* The implementation of `≤-total` in `Data.Nat.Properties` has been altered + to use operations backed by primitives, rather than recursion, making it + significantly faster. However, its reduction behaviour on open terms may have + changed. + Minor improvements ------------------ From a8224d2d2ccf5866278feea1ed3e5ed5397c9f87 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 30 Jan 2025 12:59:59 +0100 Subject: [PATCH 4/4] Be a bit lazier --- src/Data/Nat/Properties.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index e4b04f02be..20428045ea 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -205,8 +205,8 @@ _≥?_ = flip _≤?_ ≤-total : Total _≤_ ≤-total m n with m ≤? n -... | yes m≤n = inj₁ m≤n -... | no m≰n = inj₂ (≰⇒≥ m≰n) +... | true because m≤n = inj₁ (invert m≤n) +... | false because m≰n = inj₂ (≰⇒≥ (invert m≰n)) ------------------------------------------------------------------------ -- Structures