From 11a71a91a97278efda215aa38322ac861b9d01b1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 14:15:27 +0100 Subject: [PATCH 1/8] half of the adjunction --- src/Data/Nat/Properties.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 3d38c77d07..b5f5f45738 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1473,9 +1473,21 @@ pred[m∸n]≡m∸[1+n] (suc m) zero = refl pred[m∸n]≡m∸[1+n] zero (suc n) = refl pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n +------------------------------------------------------------------------ +-- Properties of _∸_ and suc + +m≤n⇒[1+m]m∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m) +m≤n⇒[1+m]m∸n≡1+[m∸n] z≤n = refl +m≤n⇒[1+m]m∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]m∸n≡1+[m∸n] le = refl + ------------------------------------------------------------------------ -- Properties of _∸_ and _≤_/_<_ +m+n≤p⇒m≤p∸n : ∀ m n p → m + n ≤ p → m ≤ p ∸ n +m+n≤p⇒m≤p∸n zero n p le = z≤n +m+n≤p⇒m≤p∸n (suc m) n (suc p) (s≤s le) + rewrite m≤n⇒[1+m]m∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤p⇒m≤p∸n m n p le) + m∸n≤m : ∀ m n → m ∸ n ≤ m m∸n≤m n zero = ≤-refl m∸n≤m zero (suc n) = ≤-refl From 22d9d93008a3fd5e0039fb092687349573598a80 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 22 Apr 2023 17:50:00 +0100 Subject: [PATCH 2/8] other half of the adjunction; NB side condition --- src/Data/Nat/Base.agda | 2 +- src/Data/Nat/Properties.agda | 18 +++++++++++++----- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 1e2db666b8..3c10279aab 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -123,7 +123,7 @@ instance -- Arithmetic open import Agda.Builtin.Nat public - using (_+_; _*_) renaming (_-_ to _∸_) + using (_+_; _*_) renaming (_-_ to _∸_) open import Agda.Builtin.Nat using (div-helper; mod-helper) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index b5f5f45738..347dc69c7f 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1474,11 +1474,15 @@ pred[m∸n]≡m∸[1+n] zero (suc n) = refl pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n ------------------------------------------------------------------------ --- Properties of _∸_ and suc +-- Properties of _∸_ and zero, suc -m≤n⇒[1+m]m∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m) -m≤n⇒[1+m]m∸n≡1+[m∸n] z≤n = refl -m≤n⇒[1+m]m∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]m∸n≡1+[m∸n] le = refl +0∸n≡n : ∀ n → 0 ∸ n ≡ 0 +0∸n≡n zero = refl +0∸n≡n (suc _) = refl + +m≤n⇒[1+m]∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m) +m≤n⇒[1+m]∸n≡1+[m∸n] z≤n = refl +m≤n⇒[1+m]∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] le = refl ------------------------------------------------------------------------ -- Properties of _∸_ and _≤_/_<_ @@ -1486,7 +1490,11 @@ m≤n⇒[1+m]m∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]m∸n≡1+[m∸n] m+n≤p⇒m≤p∸n : ∀ m n p → m + n ≤ p → m ≤ p ∸ n m+n≤p⇒m≤p∸n zero n p le = z≤n m+n≤p⇒m≤p∸n (suc m) n (suc p) (s≤s le) - rewrite m≤n⇒[1+m]m∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤p⇒m≤p∸n m n p le) + rewrite m≤n⇒[1+m]∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤p⇒m≤p∸n m n p le) + +m≤p∸n⇒m+n≤p : ∀ m {n p} (n≤p : n ≤ p) → m ≤ p ∸ n → m + n ≤ p +m≤p∸n⇒m+n≤p m z≤n le rewrite +-identityʳ m = le +m≤p∸n⇒m+n≤p m {suc n} (s≤s n≤p) le rewrite +-suc m n = s≤s (m≤p∸n⇒m+n≤p m n≤p le) m∸n≤m : ∀ m n → m ∸ n ≤ m m∸n≤m n zero = ≤-refl From 74c43738940700b0f7f4b3f863d96ee20a9148e4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 23 Apr 2023 10:00:16 +0100 Subject: [PATCH 3/8] `CHANGELOG` --- CHANGELOG.md | 4 ++++ src/Data/Nat/Properties.agda | 15 ++++----------- 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 76ca38cd42..44c565b327 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2044,6 +2044,10 @@ Other minor changes <⇒<′ : m < n → m <′ n <′⇒< : m <′ n → m < n + m≤n⇒[1+m]∸n≡1+[m∸n] : m ≤ n → suc n ∸ m ≡ suc (n ∸ m) + m+n≤p⇒m≤p∸n : m + n ≤ p → m ≤ p ∸ n + m≤p∸n⇒m+n≤p : n ≤ p → m ≤ p ∸ n → m + n ≤ p + 1≤n! : 1 ≤ n ! _!≢0 : NonZero (n !) _!*_!≢0 : NonZero (m ! * n !) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 347dc69c7f..47d8ab04ab 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1464,6 +1464,10 @@ n∸n≡0 : ∀ n → n ∸ n ≡ 0 n∸n≡0 zero = refl n∸n≡0 (suc n) = n∸n≡0 n +m≤n⇒[1+m]∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m) +m≤n⇒[1+m]∸n≡1+[m∸n] z≤n = refl +m≤n⇒[1+m]∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] le = refl + ------------------------------------------------------------------------ -- Properties of _∸_ and pred @@ -1473,17 +1477,6 @@ pred[m∸n]≡m∸[1+n] (suc m) zero = refl pred[m∸n]≡m∸[1+n] zero (suc n) = refl pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n ------------------------------------------------------------------------- --- Properties of _∸_ and zero, suc - -0∸n≡n : ∀ n → 0 ∸ n ≡ 0 -0∸n≡n zero = refl -0∸n≡n (suc _) = refl - -m≤n⇒[1+m]∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m) -m≤n⇒[1+m]∸n≡1+[m∸n] z≤n = refl -m≤n⇒[1+m]∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] le = refl - ------------------------------------------------------------------------ -- Properties of _∸_ and _≤_/_<_ From 097d6b6633e6f58a722c95bc65bb74afec9d949d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 23 Apr 2023 19:58:19 +0100 Subject: [PATCH 4/8] fix whitespace --- src/Data/Nat/Base.agda | 2 +- src/Data/Nat/Properties.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 3c10279aab..1e2db666b8 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -123,7 +123,7 @@ instance -- Arithmetic open import Agda.Builtin.Nat public - using (_+_; _*_) renaming (_-_ to _∸_) + using (_+_; _*_) renaming (_-_ to _∸_) open import Agda.Builtin.Nat using (div-helper; mod-helper) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 47d8ab04ab..e6d1c24a74 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1481,7 +1481,7 @@ pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n -- Properties of _∸_ and _≤_/_<_ m+n≤p⇒m≤p∸n : ∀ m n p → m + n ≤ p → m ≤ p ∸ n -m+n≤p⇒m≤p∸n zero n p le = z≤n +m+n≤p⇒m≤p∸n zero n p le = z≤n m+n≤p⇒m≤p∸n (suc m) n (suc p) (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤p⇒m≤p∸n m n p le) From 08596f97221aab29182b5885f4a5c30051ce794d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 23 Apr 2023 20:00:36 +0100 Subject: [PATCH 5/8] more whitespace fixes --- 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 e6d1c24a74..a164931e7c 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1465,7 +1465,7 @@ n∸n≡0 zero = refl n∸n≡0 (suc n) = n∸n≡0 n m≤n⇒[1+m]∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m) -m≤n⇒[1+m]∸n≡1+[m∸n] z≤n = refl +m≤n⇒[1+m]∸n≡1+[m∸n] z≤n = refl m≤n⇒[1+m]∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] le = refl ------------------------------------------------------------------------ @@ -1481,7 +1481,7 @@ pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n -- Properties of _∸_ and _≤_/_<_ m+n≤p⇒m≤p∸n : ∀ m n p → m + n ≤ p → m ≤ p ∸ n -m+n≤p⇒m≤p∸n zero n p le = z≤n +m+n≤p⇒m≤p∸n zero n p le = z≤n m+n≤p⇒m≤p∸n (suc m) n (suc p) (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤p⇒m≤p∸n m n p le) From 4816b2099321a3f2f7275ddd45cc5d1d3efc1963 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 24 Apr 2023 08:18:10 +0100 Subject: [PATCH 6/8] corrected `p` -> `o` --- src/Data/Nat/Properties.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index a164931e7c..93c8712eb5 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1480,14 +1480,14 @@ pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n ------------------------------------------------------------------------ -- Properties of _∸_ and _≤_/_<_ -m+n≤p⇒m≤p∸n : ∀ m n p → m + n ≤ p → m ≤ p ∸ n -m+n≤p⇒m≤p∸n zero n p le = z≤n -m+n≤p⇒m≤p∸n (suc m) n (suc p) (s≤s le) - rewrite m≤n⇒[1+m]∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤p⇒m≤p∸n m n p le) - -m≤p∸n⇒m+n≤p : ∀ m {n p} (n≤p : n ≤ p) → m ≤ p ∸ n → m + n ≤ p -m≤p∸n⇒m+n≤p m z≤n le rewrite +-identityʳ m = le -m≤p∸n⇒m+n≤p m {suc n} (s≤s n≤p) le rewrite +-suc m n = s≤s (m≤p∸n⇒m+n≤p m n≤p le) +m+n≤o⇒m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n +m+n≤o⇒m≤o∸n zero n o le = z≤n +m+n≤o⇒m≤o∸n (suc m) n (suc o) (s≤s le) + rewrite m≤n⇒[1+m]∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m n o le) + +m≤o∸n⇒m+n≤o : ∀ m {n o} (n≤o : n ≤ o) → m ≤ o ∸ n → m + n ≤ o +m≤o∸n⇒m+n≤o m z≤n le rewrite +-identityʳ m = le +m≤o∸n⇒m+n≤o m {suc n} (s≤s n≤o) le rewrite +-suc m n = s≤s (m≤o∸n⇒m+n≤o m n≤o le) m∸n≤m : ∀ m n → m ∸ n ≤ m m∸n≤m n zero = ≤-refl From 0dfa127abe6ef525833a65de299ab33d0d75a6d2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 24 Apr 2023 11:08:49 +0100 Subject: [PATCH 7/8] removed redudant additional lemma; relocated adjointness proofs --- src/Data/Nat/Properties.agda | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 93c8712eb5..6ff1b1f38b 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1464,10 +1464,6 @@ n∸n≡0 : ∀ n → n ∸ n ≡ 0 n∸n≡0 zero = refl n∸n≡0 (suc n) = n∸n≡0 n -m≤n⇒[1+m]∸n≡1+[m∸n] : ∀ {m n} → m ≤ n → suc n ∸ m ≡ suc (n ∸ m) -m≤n⇒[1+m]∸n≡1+[m∸n] z≤n = refl -m≤n⇒[1+m]∸n≡1+[m∸n] (s≤s le) rewrite m≤n⇒[1+m]∸n≡1+[m∸n] le = refl - ------------------------------------------------------------------------ -- Properties of _∸_ and pred @@ -1480,15 +1476,6 @@ pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n ------------------------------------------------------------------------ -- Properties of _∸_ and _≤_/_<_ -m+n≤o⇒m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n -m+n≤o⇒m≤o∸n zero n o le = z≤n -m+n≤o⇒m≤o∸n (suc m) n (suc o) (s≤s le) - rewrite m≤n⇒[1+m]∸n≡1+[m∸n] (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m n o le) - -m≤o∸n⇒m+n≤o : ∀ m {n o} (n≤o : n ≤ o) → m ≤ o ∸ n → m + n ≤ o -m≤o∸n⇒m+n≤o m z≤n le rewrite +-identityʳ m = le -m≤o∸n⇒m+n≤o m {suc n} (s≤s n≤o) le rewrite +-suc m n = s≤s (m≤o∸n⇒m+n≤o m n≤o le) - m∸n≤m : ∀ m n → m ∸ n ≤ m m∸n≤m n zero = ≤-refl m∸n≤m zero (suc n) = ≤-refl @@ -1586,6 +1573,15 @@ m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n) (m + n) ∸ o ≡⟨ +-∸-assoc m o≤n ⟩ m + (n ∸ o) ∎ +m+n≤o⇒m≤o∸n : ∀ m n o → m + n ≤ o → m ≤ o ∸ n +m+n≤o⇒m≤o∸n zero n o le = z≤n +m+n≤o⇒m≤o∸n (suc m) n (suc o) (s≤s le) + rewrite +-∸-assoc 1 (m+n≤o⇒n≤o m le) = s≤s (m+n≤o⇒m≤o∸n m n o le) + +m≤o∸n⇒m+n≤o : ∀ m {n o} (n≤o : n ≤ o) → m ≤ o ∸ n → m + n ≤ o +m≤o∸n⇒m+n≤o m z≤n le rewrite +-identityʳ m = le +m≤o∸n⇒m+n≤o m {suc n} (s≤s n≤o) le rewrite +-suc m n = s≤s (m≤o∸n⇒m+n≤o m n≤o le) + m≤n+m∸n : ∀ m n → m ≤ n + (m ∸ n) m≤n+m∸n zero n = z≤n m≤n+m∸n (suc m) zero = ≤-refl From b240ce341e3e838c1962da675b234c5bd00b7c4e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 24 Apr 2023 11:22:21 +0100 Subject: [PATCH 8/8] `CHANGELOG` --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 44c565b327..957ea761d7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2044,7 +2044,6 @@ Other minor changes <⇒<′ : m < n → m <′ n <′⇒< : m <′ n → m < n - m≤n⇒[1+m]∸n≡1+[m∸n] : m ≤ n → suc n ∸ m ≡ suc (n ∸ m) m+n≤p⇒m≤p∸n : m + n ≤ p → m ≤ p ∸ n m≤p∸n⇒m+n≤p : n ≤ p → m ≤ p ∸ n → m + n ≤ p