From 37d80b8efb1bc01e482c90ff6e2f50fee356fa57 Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Sat, 1 May 2021 23:17:07 +0100 Subject: [PATCH 01/14] Add 2 additional implementations of nat -> binary --- src/Data/Nat/Binary/Base.agda | 27 ++++++++++++++++++++++++++- src/Data/Nat/DivMod.agda | 6 ++++++ 2 files changed, 32 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Binary/Base.agda b/src/Data/Nat/Binary/Base.agda index d15044f30a..1ca73a2873 100644 --- a/src/Data/Nat/Binary/Base.agda +++ b/src/Data/Nat/Binary/Base.agda @@ -13,13 +13,16 @@ module Data.Nat.Binary.Base where open import Algebra.Core using (Op₂) +open import Data.Bool using (if_then_else_) open import Data.Nat.Base as ℕ using (ℕ) +open import Data.Nat.DivMod using (_%_ ; _/_ ; m/n≤m) +open import Data.Nat.Properties using (≤-refl ; ≤-trans) open import Data.Sum.Base using (_⊎_) open import Function.Base using (_on_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality using (_≡_) -open import Relation.Nullary using (¬_) +open import Relation.Nullary using (¬_ ) ------------------------------------------------------------------------ -- Definition @@ -117,6 +120,28 @@ fromℕ : ℕ → ℕᵇ fromℕ 0 = zero fromℕ (ℕ.suc n) = suc (fromℕ n) +fromℕ' : ℕ → ℕᵇ +fromℕ' n = helper n n ≤-refl + where + helper : (n w : ℕ) → n ℕ.≤ w → ℕᵇ + helper 0 _ _ = zero + helper (ℕ.suc n) (ℕ.suc w) (ℕ._≤_.s≤s p) = + if (n % 2 ℕ.≡ᵇ 0) + then 1+[2 helper (n / 2) w (≤-trans (m/n≤m n 2) p) ] + else 2[1+ helper (n / 2) w (≤-trans (m/n≤m n 2) p) ] + +fromℕ″ : ℕ → ℕᵇ +fromℕ″ n = helper n n + where + helper : ℕ → ℕ → ℕᵇ + helper 0 _ = zero + helper (ℕ.suc n) (ℕ.suc w) = + if (n % 2 ℕ.≡ᵇ 0) + then 1+[2 helper (n / 2) w ] + else 2[1+ helper (n / 2) w ] + helper _ 0 = zero -- impossible + + -- An alternative ordering lifted from ℕ infix 4 _<ℕ_ diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index cbe4b9276e..cbbecccf91 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -185,6 +185,12 @@ m/n*n≤m m n@(suc n-1) = begin m % n + (m / n) * n ≡⟨ sym (m≡m%n+[m/n]*n m n-1) ⟩ m ∎ +m/n≤m : ∀ m n {≢0} → (m / n) {≢0} ≤ m +m/n≤m m n@(suc n-1) = *-cancelʳ-≤ (m / n) m n-1 (begin + (m / n) * n ≤⟨ m/n*n≤m m n ⟩ + m ≤⟨ m≤m*n m (s≤s z≤n) ⟩ + m * n ∎) + m/n Date: Mon, 3 May 2021 00:57:00 +0100 Subject: [PATCH 02/14] Refine fromN interface --- src/Data/Nat/Binary/Base.agda | 39 +++++++++++++---------------------- 1 file changed, 14 insertions(+), 25 deletions(-) diff --git a/src/Data/Nat/Binary/Base.agda b/src/Data/Nat/Binary/Base.agda index 1ca73a2873..ea4063a30b 100644 --- a/src/Data/Nat/Binary/Base.agda +++ b/src/Data/Nat/Binary/Base.agda @@ -13,9 +13,9 @@ module Data.Nat.Binary.Base where open import Algebra.Core using (Op₂) -open import Data.Bool using (if_then_else_) +open import Data.Bool.Base using (if_then_else_) open import Data.Nat.Base as ℕ using (ℕ) -open import Data.Nat.DivMod using (_%_ ; _/_ ; m/n≤m) +open import Data.Nat.DivMod using (_%_ ; _/_) open import Data.Nat.Properties using (≤-refl ; ≤-trans) open import Data.Sum.Base using (_⊎_) open import Function.Base using (_on_) @@ -115,32 +115,21 @@ toℕ zero = 0 toℕ 2[1+ x ] = 2 ℕ.* (ℕ.suc (toℕ x)) toℕ 1+[2 x ] = ℕ.suc (2 ℕ.* (toℕ x)) --- Costs O(n), could be improved using `_/_` and `_%_` +fromℕ-helper : ℕ → ℕ → ℕᵇ +fromℕ-helper 0 _ = zero +fromℕ-helper (ℕ.suc n) (ℕ.suc w) = + if (n % 2 ℕ.≡ᵇ 0) + then 1+[2 fromℕ-helper (n / 2) w ] + else 2[1+ fromℕ-helper (n / 2) w ] +fromℕ-helper _ 0 = zero + fromℕ : ℕ → ℕᵇ -fromℕ 0 = zero -fromℕ (ℕ.suc n) = suc (fromℕ n) +fromℕ n = fromℕ-helper n n +-- An alternative slower definition fromℕ' : ℕ → ℕᵇ -fromℕ' n = helper n n ≤-refl - where - helper : (n w : ℕ) → n ℕ.≤ w → ℕᵇ - helper 0 _ _ = zero - helper (ℕ.suc n) (ℕ.suc w) (ℕ._≤_.s≤s p) = - if (n % 2 ℕ.≡ᵇ 0) - then 1+[2 helper (n / 2) w (≤-trans (m/n≤m n 2) p) ] - else 2[1+ helper (n / 2) w (≤-trans (m/n≤m n 2) p) ] - -fromℕ″ : ℕ → ℕᵇ -fromℕ″ n = helper n n - where - helper : ℕ → ℕ → ℕᵇ - helper 0 _ = zero - helper (ℕ.suc n) (ℕ.suc w) = - if (n % 2 ℕ.≡ᵇ 0) - then 1+[2 helper (n / 2) w ] - else 2[1+ helper (n / 2) w ] - helper _ 0 = zero -- impossible - +fromℕ' 0 = zero +fromℕ' (ℕ.suc n) = suc (fromℕ' n) -- An alternative ordering lifted from ℕ From ee8ef0d571e4e4c6f0a1e1400d8b4cb4726d8179 Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Mon, 3 May 2021 01:05:38 +0100 Subject: [PATCH 03/14] Sketch Properties with new fromN impl --- src/Data/Nat/Binary/Properties.agda | 36 ++++++++++++++++++----------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index d8479c4a7e..792fd57871 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -98,15 +98,21 @@ toℕ-pred zero = refl toℕ-pred 2[1+ x ] = cong ℕ.pred $ sym $ ℕₚ.*-distribˡ-+ 2 1 (toℕ x) toℕ-pred 1+[2 x ] = toℕ-double x -toℕ-fromℕ : toℕ ∘ fromℕ ≗ id -toℕ-fromℕ 0 = refl -toℕ-fromℕ (ℕ.suc n) = begin - toℕ (fromℕ (ℕ.suc n)) ≡⟨⟩ - toℕ (suc (fromℕ n)) ≡⟨ toℕ-suc (fromℕ n) ⟩ - ℕ.suc (toℕ (fromℕ n)) ≡⟨ cong ℕ.suc (toℕ-fromℕ n) ⟩ +toℕ-fromℕ' : toℕ ∘ fromℕ' ≗ id +toℕ-fromℕ' 0 = refl +toℕ-fromℕ' (ℕ.suc n) = begin + toℕ (fromℕ' (ℕ.suc n)) ≡⟨⟩ + toℕ (suc (fromℕ' n)) ≡⟨ toℕ-suc (fromℕ' n) ⟩ + ℕ.suc (toℕ (fromℕ' n)) ≡⟨ cong ℕ.suc (toℕ-fromℕ' n) ⟩ ℕ.suc n ∎ where open ≡-Reasoning +fromℕ≡fromℕ' : fromℕ ≗ fromℕ' +fromℕ≡fromℕ' n = {! !} + +toℕ-fromℕ : toℕ ∘ fromℕ ≗ id +toℕ-fromℕ n rewrite fromℕ≡fromℕ' n = toℕ-fromℕ' n + toℕ-injective : Injective _≡_ _≡_ toℕ toℕ-injective {zero} {zero} _ = refl toℕ-injective {2[1+ x ]} {2[1+ y ]} 2[1+xN]≡2[1+yN] = cong 2[1+_] x≡y @@ -654,15 +660,19 @@ suc-+ 1+[2 x ] 1+[2 y ] = refl 1+≗suc : (1ᵇ +_) ≗ suc 1+≗suc = suc-+ zero -fromℕ-homo-+ : ∀ m n → fromℕ (m ℕ.+ n) ≡ fromℕ m + fromℕ n -fromℕ-homo-+ 0 _ = refl -fromℕ-homo-+ (ℕ.suc m) n = begin - fromℕ ((ℕ.suc m) ℕ.+ n) ≡⟨⟩ - suc (fromℕ (m ℕ.+ n)) ≡⟨ cong suc (fromℕ-homo-+ m n) ⟩ +fromℕ'-homo-+ : ∀ m n → fromℕ' (m ℕ.+ n) ≡ fromℕ' m + fromℕ' n +fromℕ'-homo-+ 0 _ = refl +fromℕ'-homo-+ (ℕ.suc m) n = begin + fromℕ' ((ℕ.suc m) ℕ.+ n) ≡⟨⟩ + suc (fromℕ' (m ℕ.+ n)) ≡⟨ cong suc (fromℕ'-homo-+ m n) ⟩ suc (a + b) ≡⟨ sym (suc-+ a b) ⟩ (suc a) + b ≡⟨⟩ - (fromℕ (ℕ.suc m)) + (fromℕ n) ∎ - where open ≡-Reasoning; a = fromℕ m; b = fromℕ n + (fromℕ' (ℕ.suc m)) + (fromℕ' n) ∎ + where open ≡-Reasoning; a = fromℕ' m; b = fromℕ' n + +fromℕ-homo-+ : ∀ m n → fromℕ (m ℕ.+ n) ≡ fromℕ m + fromℕ n +fromℕ-homo-+ m n rewrite fromℕ≡fromℕ' (m ℕ.+ n) | fromℕ≡fromℕ' m | fromℕ≡fromℕ' n = + fromℕ'-homo-+ m n ------------------------------------------------------------------------ -- Algebraic properties of _+_ From 74abf4f936f9b797a615e5ba9f1d1997b999701b Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Mon, 3 May 2021 01:55:32 +0100 Subject: [PATCH 04/14] Add @oisdk's equivalent proof --- src/Data/Nat/Binary/Properties.agda | 55 ++++++++++++++++++++++++++++- 1 file changed, 54 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 792fd57871..bf97be4bb7 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -12,8 +12,12 @@ open import Algebra.Bundles open import Algebra.Morphism.Structures import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism open import Algebra.Consequences.Propositional +open import Data.Bool.Base using (if_then_else_; Bool; true; false) +open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Binary.Base open import Data.Nat as ℕ using (ℕ; z≤n; s≤s) +import Data.Nat.DivMod as ℕ÷ +open import Data.Nat.DivMod.Core using (divₕ-extractAcc) import Data.Nat.Properties as ℕₚ open import Data.Nat.Solver open import Data.Product using (_,_; proj₁; proj₂; ∃) @@ -107,8 +111,57 @@ toℕ-fromℕ' (ℕ.suc n) = begin ℕ.suc n ∎ where open ≡-Reasoning +fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ-helper n w ≡ fromℕ' n +fromℕ-helper≡fromℕ' ℕ.zero w p = refl +fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = + head-tail-cong _ _ + (trans (head-homo' _ _) (sym (head-homo n))) + (trans + (trans + (tail-homo' (n ℕ÷.% 2 ℕ.≡ᵇ 0) _) + (fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w))) + (sym (tail-homo n))) + where + head : ℕᵇ → Maybe Bool + head zero = nothing + head 2[1+ n ] = just false + head 1+[2 n ] = just true + head-suc : ∀ n → head (suc (suc (suc n))) ≡ head (suc n) + head-suc zero = refl + head-suc 2[1+ n ] = refl + head-suc 1+[2 n ] = refl + head-homo : ∀ n → head (suc (fromℕ' n)) ≡ just (n ℕ÷.% 2 ℕ.≡ᵇ 0) + head-homo ℕ.zero = refl + head-homo (ℕ.suc ℕ.zero) = refl + head-homo (ℕ.suc (ℕ.suc n)) = trans (head-suc (fromℕ' n)) (head-homo n) + head-homo' : ∀ x xs → head (if x then (1+[2 xs ]) else (2[1+ xs ])) ≡ just x + head-homo' false xs = refl + head-homo' true xs = refl + tail : ℕᵇ → ℕᵇ + tail zero = zero + tail 2[1+ n ] = n + tail 1+[2 n ] = n + tail-suc : ∀ n → suc (tail (suc n)) ≡ tail (suc (suc (suc n))) + tail-suc zero = refl + tail-suc 2[1+ n ] = refl + tail-suc 1+[2 n ] = refl + tail-homo : ∀ n → tail (suc (fromℕ' n)) ≡ fromℕ' (n ℕ÷./ 2) + tail-homo ℕ.zero = refl + tail-homo (ℕ.suc ℕ.zero) = refl + tail-homo (ℕ.suc (ℕ.suc n)) = + trans + (trans (sym (tail-suc (fromℕ' n))) (cong suc (tail-homo n))) + (cong fromℕ' (sym (divₕ-extractAcc 1 1 n 1))) + tail-homo' : ∀ x xs → tail (if x then (1+[2 xs ]) else (2[1+ xs ])) ≡ xs + tail-homo' false xs = refl + tail-homo' true xs = refl + head-tail-cong : ∀ m n → head m ≡ head n → tail m ≡ tail n → m ≡ n + head-tail-cong zero zero p q = refl + head-tail-cong 2[1+ m ] 2[1+ n ] p q = cong 2[1+_] q + head-tail-cong 1+[2 m ] 1+[2 n ] p q = cong 1+[2_] q + fromℕ≡fromℕ' : fromℕ ≗ fromℕ' -fromℕ≡fromℕ' n = {! !} +fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl toℕ-fromℕ : toℕ ∘ fromℕ ≗ id toℕ-fromℕ n rewrite fromℕ≡fromℕ' n = toℕ-fromℕ' n From bd17ad83f5d045f44bcdab3f65332f720a6f6092 Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Tue, 4 May 2021 21:48:13 +0100 Subject: [PATCH 05/14] Format proofs --- src/Data/Nat/Binary/Properties.agda | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index bf97be4bb7..7b44fb79a8 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -115,13 +115,17 @@ fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ-helper n w ≡ f fromℕ-helper≡fromℕ' ℕ.zero w p = refl fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = head-tail-cong _ _ - (trans (head-homo' _ _) (sym (head-homo n))) - (trans - (trans - (tail-homo' (n ℕ÷.% 2 ℕ.≡ᵇ 0) _) - (fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w))) - (sym (tail-homo n))) + (begin + head (fromℕ-helper (ℕ.suc n) (ℕ.suc w)) ≡⟨ head-homo' _ _ ⟩ + just (n ℕ÷.% 2 ℕ.≡ᵇ 0) ≡˘⟨ head-homo n ⟩ + head (fromℕ' (ℕ.suc n)) ∎) + (begin + tail (fromℕ-helper (ℕ.suc n) (ℕ.suc w)) ≡⟨ tail-homo' (n ℕ÷.% 2 ℕ.≡ᵇ 0) _ ⟩ + fromℕ-helper (n ℕ÷./ 2) w ≡⟨ fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w) ⟩ + fromℕ' (n ℕ÷./ 2) ≡˘⟨ tail-homo n ⟩ + tail (fromℕ' (ℕ.suc n)) ∎) where + open ≡-Reasoning head : ℕᵇ → Maybe Bool head zero = nothing head 2[1+ n ] = just false @@ -148,10 +152,11 @@ fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = tail-homo : ∀ n → tail (suc (fromℕ' n)) ≡ fromℕ' (n ℕ÷./ 2) tail-homo ℕ.zero = refl tail-homo (ℕ.suc ℕ.zero) = refl - tail-homo (ℕ.suc (ℕ.suc n)) = - trans - (trans (sym (tail-suc (fromℕ' n))) (cong suc (tail-homo n))) - (cong fromℕ' (sym (divₕ-extractAcc 1 1 n 1))) + tail-homo (ℕ.suc (ℕ.suc n)) = begin + tail (suc (fromℕ' (ℕ.suc (ℕ.suc n)))) ≡˘⟨ tail-suc (fromℕ' n) ⟩ + suc (tail (suc (fromℕ' n))) ≡⟨ cong suc (tail-homo n) ⟩ + fromℕ' (ℕ.suc (n ℕ÷./ 2)) ≡⟨ cong fromℕ' (sym (divₕ-extractAcc 1 1 n 1)) ⟩ + fromℕ' (ℕ.suc (ℕ.suc n) ℕ÷./ 2) ∎ tail-homo' : ∀ x xs → tail (if x then (1+[2 xs ]) else (2[1+ xs ])) ≡ xs tail-homo' false xs = refl tail-homo' true xs = refl From f284a3b9d8fdd3d3dff1b4ca76a1d9931f1f1f1f Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Tue, 4 May 2021 23:43:50 +0100 Subject: [PATCH 06/14] Refactor head/tail --- src/Data/Nat/Binary/Properties.agda | 51 +++++++++++++---------------- 1 file changed, 22 insertions(+), 29 deletions(-) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 7b44fb79a8..fb5ab41100 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -20,7 +20,8 @@ import Data.Nat.DivMod as ℕ÷ open import Data.Nat.DivMod.Core using (divₕ-extractAcc) import Data.Nat.Properties as ℕₚ open import Data.Nat.Solver -open import Data.Product using (_,_; proj₁; proj₂; ∃) +open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃) +import Data.Product.Properties as Productₚ open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (_∘_; _$_; id) open import Function.Definitions using (Injective) @@ -114,22 +115,28 @@ toℕ-fromℕ' (ℕ.suc n) = begin fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ-helper n w ≡ fromℕ' n fromℕ-helper≡fromℕ' ℕ.zero w p = refl fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = - head-tail-cong _ _ - (begin - head (fromℕ-helper (ℕ.suc n) (ℕ.suc w)) ≡⟨ head-homo' _ _ ⟩ - just (n ℕ÷.% 2 ℕ.≡ᵇ 0) ≡˘⟨ head-homo n ⟩ - head (fromℕ' (ℕ.suc n)) ∎) - (begin - tail (fromℕ-helper (ℕ.suc n) (ℕ.suc w)) ≡⟨ tail-homo' (n ℕ÷.% 2 ℕ.≡ᵇ 0) _ ⟩ - fromℕ-helper (n ℕ÷./ 2) w ≡⟨ fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w) ⟩ - fromℕ' (n ℕ÷./ 2) ≡˘⟨ tail-homo n ⟩ - tail (fromℕ' (ℕ.suc n)) ∎) + split-cong _ _ (begin + split (fromℕ-helper (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ + just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ-helper (n ℕ÷./ 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ + just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ' (n ℕ÷./ 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ + head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩ + split (fromℕ' (ℕ.suc n)) ∎) where open ≡-Reasoning - head : ℕᵇ → Maybe Bool - head zero = nothing - head 2[1+ n ] = just false - head 1+[2 n ] = just true + rec-n/2 = fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w) + split : ℕᵇ → Maybe Bool × ℕᵇ + split zero = nothing , zero + split 2[1+ n ] = just false , n + split 1+[2 n ] = just true , n + head = proj₁ ∘ split + tail = proj₂ ∘ split + split-cong : ∀ m n → split m ≡ split n → m ≡ n + split-cong zero zero refl = refl + split-cong 2[1+ m ] 2[1+ .m ] refl = refl + split-cong 1+[2 m ] 1+[2 .m ] refl = refl + split-if : ∀ x xs → split (if x then 1+[2 xs ] else 2[1+ xs ]) ≡ (just x , xs) + split-if false xs = refl + split-if true xs = refl head-suc : ∀ n → head (suc (suc (suc n))) ≡ head (suc n) head-suc zero = refl head-suc 2[1+ n ] = refl @@ -138,13 +145,6 @@ fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = head-homo ℕ.zero = refl head-homo (ℕ.suc ℕ.zero) = refl head-homo (ℕ.suc (ℕ.suc n)) = trans (head-suc (fromℕ' n)) (head-homo n) - head-homo' : ∀ x xs → head (if x then (1+[2 xs ]) else (2[1+ xs ])) ≡ just x - head-homo' false xs = refl - head-homo' true xs = refl - tail : ℕᵇ → ℕᵇ - tail zero = zero - tail 2[1+ n ] = n - tail 1+[2 n ] = n tail-suc : ∀ n → suc (tail (suc n)) ≡ tail (suc (suc (suc n))) tail-suc zero = refl tail-suc 2[1+ n ] = refl @@ -157,13 +157,6 @@ fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = suc (tail (suc (fromℕ' n))) ≡⟨ cong suc (tail-homo n) ⟩ fromℕ' (ℕ.suc (n ℕ÷./ 2)) ≡⟨ cong fromℕ' (sym (divₕ-extractAcc 1 1 n 1)) ⟩ fromℕ' (ℕ.suc (ℕ.suc n) ℕ÷./ 2) ∎ - tail-homo' : ∀ x xs → tail (if x then (1+[2 xs ]) else (2[1+ xs ])) ≡ xs - tail-homo' false xs = refl - tail-homo' true xs = refl - head-tail-cong : ∀ m n → head m ≡ head n → tail m ≡ tail n → m ≡ n - head-tail-cong zero zero p q = refl - head-tail-cong 2[1+ m ] 2[1+ n ] p q = cong 2[1+_] q - head-tail-cong 1+[2 m ] 1+[2 n ] p q = cong 1+[2_] q fromℕ≡fromℕ' : fromℕ ≗ fromℕ' fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl From 78490f10cddf3195998d7ebbcf03a7b37acfbf2c Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Wed, 5 May 2021 00:22:02 +0100 Subject: [PATCH 07/14] Cleanup --- src/Data/Nat/Binary/Base.agda | 3 +-- src/Data/Nat/Binary/Properties.agda | 2 +- src/Data/Nat/DivMod.agda | 6 ------ 3 files changed, 2 insertions(+), 9 deletions(-) diff --git a/src/Data/Nat/Binary/Base.agda b/src/Data/Nat/Binary/Base.agda index ea4063a30b..c6dc208953 100644 --- a/src/Data/Nat/Binary/Base.agda +++ b/src/Data/Nat/Binary/Base.agda @@ -16,13 +16,12 @@ open import Algebra.Core using (Op₂) open import Data.Bool.Base using (if_then_else_) open import Data.Nat.Base as ℕ using (ℕ) open import Data.Nat.DivMod using (_%_ ; _/_) -open import Data.Nat.Properties using (≤-refl ; ≤-trans) open import Data.Sum.Base using (_⊎_) open import Function.Base using (_on_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality using (_≡_) -open import Relation.Nullary using (¬_ ) +open import Relation.Nullary using (¬_) ------------------------------------------------------------------------ -- Definition diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index fb5ab41100..65bed876d9 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -201,7 +201,7 @@ fromℕ-injective {x} {y} f[x]≡f[y] = begin where open ≡-Reasoning fromℕ-toℕ : fromℕ ∘ toℕ ≗ id -fromℕ-toℕ = toℕ-injective ∘ toℕ-fromℕ ∘ toℕ +fromℕ-toℕ = toℕ-injective ∘ toℕ-fromℕ ∘ toℕ fromℕ-pred : ∀ n → fromℕ (ℕ.pred n) ≡ pred (fromℕ n) fromℕ-pred n = begin diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index cbbecccf91..cbe4b9276e 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -185,12 +185,6 @@ m/n*n≤m m n@(suc n-1) = begin m % n + (m / n) * n ≡⟨ sym (m≡m%n+[m/n]*n m n-1) ⟩ m ∎ -m/n≤m : ∀ m n {≢0} → (m / n) {≢0} ≤ m -m/n≤m m n@(suc n-1) = *-cancelʳ-≤ (m / n) m n-1 (begin - (m / n) * n ≤⟨ m/n*n≤m m n ⟩ - m ≤⟨ m≤m*n m (s≤s z≤n) ⟩ - m * n ∎) - m/n Date: Wed, 5 May 2021 00:33:46 +0100 Subject: [PATCH 08/14] Readd m/n<=m --- src/Data/Nat/DivMod.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index cbe4b9276e..cbbecccf91 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -185,6 +185,12 @@ m/n*n≤m m n@(suc n-1) = begin m % n + (m / n) * n ≡⟨ sym (m≡m%n+[m/n]*n m n-1) ⟩ m ∎ +m/n≤m : ∀ m n {≢0} → (m / n) {≢0} ≤ m +m/n≤m m n@(suc n-1) = *-cancelʳ-≤ (m / n) m n-1 (begin + (m / n) * n ≤⟨ m/n*n≤m m n ⟩ + m ≤⟨ m≤m*n m (s≤s z≤n) ⟩ + m * n ∎) + m/n Date: Wed, 5 May 2021 00:33:56 +0100 Subject: [PATCH 09/14] Update changelog --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8253479648..839fc44501 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,10 @@ Bug-fixes Non-backwards compatible changes -------------------------------- +* Replaced O(n) implementation of `Data.Nat.Binary.fromℕ` with O(log n). The old + implementation is maintained under `Data.Nat.Binary.fromℕ'` and proven to be + equivalent. + Deprecated modules ------------------ From cc6fcd6a9d538c482b570be777f696f2a2651770 Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Wed, 5 May 2021 00:45:14 +0100 Subject: [PATCH 10/14] Add to CHANGELOG --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 839fc44501..acd28d9df7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -65,3 +65,8 @@ Other minor additions respʳ-flip : _≈_ Respectsʳ (flip _≈_) respˡ-flip : _≈_ Respectsˡ (flip _≈_) ``` + +* Added new proof to `Data.Nat.DivMod`: + ```agda + m/n≤m : ∀ m n {≢0} → (m / n) {≢0} ≤ m + ``` From 896298a27118ab0b66f8d3005d1eacd2a440ce39 Mon Sep 17 00:00:00 2001 From: = Date: Thu, 6 May 2021 09:55:32 +0800 Subject: [PATCH 11/14] Make fromN-helper an inner module --- src/Data/Nat/Binary/Base.agda | 19 +++++++------ src/Data/Nat/Binary/Properties.agda | 44 +++++++++++++++++------------ 2 files changed, 36 insertions(+), 27 deletions(-) diff --git a/src/Data/Nat/Binary/Base.agda b/src/Data/Nat/Binary/Base.agda index c6dc208953..e4cd618199 100644 --- a/src/Data/Nat/Binary/Base.agda +++ b/src/Data/Nat/Binary/Base.agda @@ -114,16 +114,17 @@ toℕ zero = 0 toℕ 2[1+ x ] = 2 ℕ.* (ℕ.suc (toℕ x)) toℕ 1+[2 x ] = ℕ.suc (2 ℕ.* (toℕ x)) -fromℕ-helper : ℕ → ℕ → ℕᵇ -fromℕ-helper 0 _ = zero -fromℕ-helper (ℕ.suc n) (ℕ.suc w) = - if (n % 2 ℕ.≡ᵇ 0) - then 1+[2 fromℕ-helper (n / 2) w ] - else 2[1+ fromℕ-helper (n / 2) w ] -fromℕ-helper _ 0 = zero - fromℕ : ℕ → ℕᵇ -fromℕ n = fromℕ-helper n n +fromℕ n = helper n n + module fromℕ where + helper : ℕ → ℕ → ℕᵇ + helper 0 _ = zero + helper (ℕ.suc n) (ℕ.suc w) = + if (n % 2 ℕ.≡ᵇ 0) + then 1+[2 helper (n / 2) w ] + else 2[1+ helper (n / 2) w ] + -- Impossible case + helper _ 0 = zero -- An alternative slower definition fromℕ' : ℕ → ℕᵇ diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 65bed876d9..6b59813049 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -112,43 +112,43 @@ toℕ-fromℕ' (ℕ.suc n) = begin ℕ.suc n ∎ where open ≡-Reasoning -fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ-helper n w ≡ fromℕ' n -fromℕ-helper≡fromℕ' ℕ.zero w p = refl -fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = - split-cong _ _ (begin - split (fromℕ-helper (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ - just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ-helper (n ℕ÷./ 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ - just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ' (n ℕ÷./ 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ - head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩ - split (fromℕ' (ℕ.suc n)) ∎) +fromℕ≡fromℕ' : fromℕ ≗ fromℕ' +fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl where - open ≡-Reasoning - rec-n/2 = fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w) split : ℕᵇ → Maybe Bool × ℕᵇ - split zero = nothing , zero + split zero = nothing , zero split 2[1+ n ] = just false , n split 1+[2 n ] = just true , n + head = proj₁ ∘ split tail = proj₂ ∘ split + split-cong : ∀ m n → split m ≡ split n → m ≡ n split-cong zero zero refl = refl split-cong 2[1+ m ] 2[1+ .m ] refl = refl split-cong 1+[2 m ] 1+[2 .m ] refl = refl + split-if : ∀ x xs → split (if x then 1+[2 xs ] else 2[1+ xs ]) ≡ (just x , xs) split-if false xs = refl split-if true xs = refl + head-suc : ∀ n → head (suc (suc (suc n))) ≡ head (suc n) head-suc zero = refl head-suc 2[1+ n ] = refl head-suc 1+[2 n ] = refl - head-homo : ∀ n → head (suc (fromℕ' n)) ≡ just (n ℕ÷.% 2 ℕ.≡ᵇ 0) - head-homo ℕ.zero = refl - head-homo (ℕ.suc ℕ.zero) = refl - head-homo (ℕ.suc (ℕ.suc n)) = trans (head-suc (fromℕ' n)) (head-homo n) + tail-suc : ∀ n → suc (tail (suc n)) ≡ tail (suc (suc (suc n))) tail-suc zero = refl tail-suc 2[1+ n ] = refl tail-suc 1+[2 n ] = refl + + head-homo : ∀ n → head (suc (fromℕ' n)) ≡ just (n ℕ÷.% 2 ℕ.≡ᵇ 0) + head-homo ℕ.zero = refl + head-homo (ℕ.suc ℕ.zero) = refl + head-homo (ℕ.suc (ℕ.suc n)) = trans (head-suc (fromℕ' n)) (head-homo n) + + open ≡-Reasoning + tail-homo : ∀ n → tail (suc (fromℕ' n)) ≡ fromℕ' (n ℕ÷./ 2) tail-homo ℕ.zero = refl tail-homo (ℕ.suc ℕ.zero) = refl @@ -158,8 +158,16 @@ fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = fromℕ' (ℕ.suc (n ℕ÷./ 2)) ≡⟨ cong fromℕ' (sym (divₕ-extractAcc 1 1 n 1)) ⟩ fromℕ' (ℕ.suc (ℕ.suc n) ℕ÷./ 2) ∎ -fromℕ≡fromℕ' : fromℕ ≗ fromℕ' -fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl + fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ.helper n n w ≡ fromℕ' n + fromℕ-helper≡fromℕ' ℕ.zero w p = refl + fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = + split-cong _ _ (begin + split (fromℕ.helper n (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ + just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ.helper n (n ℕ÷./ 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ + just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ' (n ℕ÷./ 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ + head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩ + split (fromℕ' (ℕ.suc n)) ∎) + where rec-n/2 = fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w) toℕ-fromℕ : toℕ ∘ fromℕ ≗ id toℕ-fromℕ n rewrite fromℕ≡fromℕ' n = toℕ-fromℕ' n From 7bac4543f895022a5baed4b896e31bd5d7ce3f05 Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Fri, 7 May 2021 20:47:42 +0100 Subject: [PATCH 12/14] Use Injective --- src/Data/Nat/Binary/Properties.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 6b59813049..575e849d0d 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -123,10 +123,10 @@ fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl head = proj₁ ∘ split tail = proj₂ ∘ split - split-cong : ∀ m n → split m ≡ split n → m ≡ n - split-cong zero zero refl = refl - split-cong 2[1+ m ] 2[1+ .m ] refl = refl - split-cong 1+[2 m ] 1+[2 .m ] refl = refl + split-injective : Injective _≡_ _≡_ split + split-injective {zero} {zero} refl = refl + split-injective {2[1+ _ ]} {2[1+ _ ]} refl = refl + split-injective {1+[2 _ ]} {1+[2 _ ]} refl = refl split-if : ∀ x xs → split (if x then 1+[2 xs ] else 2[1+ xs ]) ≡ (just x , xs) split-if false xs = refl @@ -161,7 +161,7 @@ fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ.helper n n w ≡ fromℕ' n fromℕ-helper≡fromℕ' ℕ.zero w p = refl fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = - split-cong _ _ (begin + split-injective (begin split (fromℕ.helper n (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ.helper n (n ℕ÷./ 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ' (n ℕ÷./ 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ From 8ce4e9ed7d461acd590baf06ab65d2109e1a9f63 Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Fri, 7 May 2021 21:26:18 +0100 Subject: [PATCH 13/14] Switch divh-extractAcc with +-distrib-/-| and fixup imports --- src/Data/Nat/Binary/Properties.agda | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 575e849d0d..269404e93f 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -16,12 +16,11 @@ open import Data.Bool.Base using (if_then_else_; Bool; true; false) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.Nat.Binary.Base open import Data.Nat as ℕ using (ℕ; z≤n; s≤s) -import Data.Nat.DivMod as ℕ÷ -open import Data.Nat.DivMod.Core using (divₕ-extractAcc) +open import Data.Nat.DivMod using (_%_; _/_; m/n≤m; +-distrib-/-∣ˡ) +open import Data.Nat.Divisibility using (∣-refl) import Data.Nat.Properties as ℕₚ open import Data.Nat.Solver open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃) -import Data.Product.Properties as Productₚ open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Function.Base using (_∘_; _$_; id) open import Function.Definitions using (Injective) @@ -142,32 +141,32 @@ fromℕ≡fromℕ' n = fromℕ-helper≡fromℕ' n n ℕₚ.≤-refl tail-suc 2[1+ n ] = refl tail-suc 1+[2 n ] = refl - head-homo : ∀ n → head (suc (fromℕ' n)) ≡ just (n ℕ÷.% 2 ℕ.≡ᵇ 0) + head-homo : ∀ n → head (suc (fromℕ' n)) ≡ just (n % 2 ℕ.≡ᵇ 0) head-homo ℕ.zero = refl head-homo (ℕ.suc ℕ.zero) = refl head-homo (ℕ.suc (ℕ.suc n)) = trans (head-suc (fromℕ' n)) (head-homo n) open ≡-Reasoning - tail-homo : ∀ n → tail (suc (fromℕ' n)) ≡ fromℕ' (n ℕ÷./ 2) + tail-homo : ∀ n → tail (suc (fromℕ' n)) ≡ fromℕ' (n / 2) tail-homo ℕ.zero = refl tail-homo (ℕ.suc ℕ.zero) = refl tail-homo (ℕ.suc (ℕ.suc n)) = begin tail (suc (fromℕ' (ℕ.suc (ℕ.suc n)))) ≡˘⟨ tail-suc (fromℕ' n) ⟩ suc (tail (suc (fromℕ' n))) ≡⟨ cong suc (tail-homo n) ⟩ - fromℕ' (ℕ.suc (n ℕ÷./ 2)) ≡⟨ cong fromℕ' (sym (divₕ-extractAcc 1 1 n 1)) ⟩ - fromℕ' (ℕ.suc (ℕ.suc n) ℕ÷./ 2) ∎ + fromℕ' (ℕ.suc (n / 2)) ≡˘⟨ cong fromℕ' (+-distrib-/-∣ˡ {2} n ∣-refl) ⟩ + fromℕ' (ℕ.suc (ℕ.suc n) / 2) ∎ fromℕ-helper≡fromℕ' : ∀ n w → n ℕ.≤ w → fromℕ.helper n n w ≡ fromℕ' n fromℕ-helper≡fromℕ' ℕ.zero w p = refl fromℕ-helper≡fromℕ' (ℕ.suc n) (ℕ.suc w) (s≤s n≤w) = split-injective (begin - split (fromℕ.helper n (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ - just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ.helper n (n ℕ÷./ 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ - just (n ℕ÷.% 2 ℕ.≡ᵇ 0) , fromℕ' (n ℕ÷./ 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ - head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩ - split (fromℕ' (ℕ.suc n)) ∎) - where rec-n/2 = fromℕ-helper≡fromℕ' (n ℕ÷./ 2) w (ℕₚ.≤-trans (ℕ÷.m/n≤m n 2) n≤w) + split (fromℕ.helper n (ℕ.suc n) (ℕ.suc w)) ≡⟨ split-if _ _ ⟩ + just (n % 2 ℕ.≡ᵇ 0) , fromℕ.helper n (n / 2) w ≡⟨ cong (_ ,_) rec-n/2 ⟩ + just (n % 2 ℕ.≡ᵇ 0) , fromℕ' (n / 2) ≡˘⟨ cong₂ _,_ (head-homo n) (tail-homo n) ⟩ + head (fromℕ' (ℕ.suc n)) , tail (fromℕ' (ℕ.suc n)) ≡⟨⟩ + split (fromℕ' (ℕ.suc n)) ∎) + where rec-n/2 = fromℕ-helper≡fromℕ' (n / 2) w (ℕₚ.≤-trans (m/n≤m n 2) n≤w) toℕ-fromℕ : toℕ ∘ fromℕ ≗ id toℕ-fromℕ n rewrite fromℕ≡fromℕ' n = toℕ-fromℕ' n From e59b2eadf4878d396a31bde123bfd5f6327a864d Mon Sep 17 00:00:00 2001 From: Jamie Lowenthal Date: Fri, 7 May 2021 21:35:10 +0100 Subject: [PATCH 14/14] Update changelog --- CHANGELOG.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index acd28d9df7..8ab135d39b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -66,6 +66,19 @@ Other minor additions respˡ-flip : _≈_ Respectsˡ (flip _≈_) ``` +* Added new proofs to `Data.Nat.Binary.Properties`: + ```agda + fromℕ≡fromℕ' : fromℕ ≗ fromℕ' + toℕ-fromℕ' : toℕ ∘ fromℕ' ≗ id + fromℕ'-homo-+ : ∀ m n → fromℕ' (m ℕ.+ n) ≡ fromℕ' m + fromℕ' n + ``` + +* Rewrote proofs in `Data.Nat.Binary.Properties` for new implementation of `fromℕ`: + ```agda + toℕ-fromℕ : toℕ ∘ fromℕ ≗ id + fromℕ-homo-+ : ∀ m n → fromℕ (m ℕ.+ n) ≡ fromℕ m + fromℕ n + ``` + * Added new proof to `Data.Nat.DivMod`: ```agda m/n≤m : ∀ m n {≢0} → (m / n) {≢0} ≤ m