diff --git a/CHANGELOG.md b/CHANGELOG.md index 875f65cce7..ac2612d467 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,9 @@ Bug-fixes rather than a natural. The previous binding was incorrectly assuming that all exit codes where non-negative. +* In `/-monoˡ-≤` in `Data.Nat.DivMod` the parameter `o` was implicit but not inferrable. + It has been changed to be explicit. + * In `Function.Definitions` the definitions of `Surjection`, `Inverseˡ`, `Inverseʳ` were not being re-exported correctly and therefore had an unsolved meta-variable whenever this module was explicitly parameterised. This has @@ -72,6 +75,86 @@ Non-backwards compatible changes So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to" will return "Main.agdai" when it used to be happy to just return "n.agda". +#### Proofs of non-zeroness as instance arguments + +* Many numeric operations in the library require their arguments to be non-zero. + The previous way of constructing and passing round these proofs resulted in clunky code. + As described on the [mailing list](https://lists.chalmers.se/pipermail/agda/2021/012693.html) + we have converted the operations to take the proofs of non-zeroness as irrelevant + [instance arguments](https://agda.readthedocs.io/en/latest/language/instance-arguments.html). + See the mailing list for a fuller explanation of the motivation and implementation. + +* For example the type signature of division is now: + ``` + _/_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ + ``` + which means that as long as an instance of `NonZero n` is in scope then you can write + `m / n` without having to explicitly provide a proof as instance search will fill it in + for you. The full list of such operations changed is as follows: + - In `Data.Nat.DivMod`: `_/_`, `_%_`, `_div_`, `_mod_` + - In `Data.Nat.Pseudorandom.LCG`: `Generator` + - In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_` + +* At the moment, there are 4 different ways such instance arguments can be provided, + listed in order of convenience and clarity: + 1. By default there is always an instance of `NonZero (suc n)` for any `n` which + will be picked up automatically: + ``` + 0/n≡0 : 0 / suc n ≡ 0 + ``` + 2. You can take the proof an instance argument as a parameter, e.g. + ``` + 0/n≡0 : {{_ : NonZero n}} → 0 / n ≡ 0 + ``` + 3. You can define an instance argument in scope higher-up (or in a `where` clause): + ``` + instance + n≢0 : NonZero n + n≢0 = ... + + 0/n≡0 : 0 / n ≡ 0 + ``` + 4. You can provide the instance argument explicitly, e.g. `0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0` + ``` + 0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0 + ``` + +* Previously one of the hacks used in proofs was to explicitly put everything in the form `suc n`. + This often made the proofs extremely difficult to use if you're term wasn't in that form. These + proofs have now all been updated to use instance arguments instead, e.g. + ``` + n/n≡1 : ∀ n → suc n / suc n ≡ 1 + ``` + becomes + ``` + n/n≡1 : ∀ n {{_ : NonZero n}} → n / n ≡ 1 + ``` + This does however mean that if you passed in the value `x` to these proofs before, then you + will now have to pass in `suc x`. The full list of such proofs is below: + - In `Data.Nat.DivMod`: + ```agda + m≡m%n+[m/n]*n : ∀ m n → m ≡ m % suc n + (m / suc n) * suc n + m%n≡m∸m/n*n : ∀ m n → m % suc n ≡ m ∸ (m / suc n) * suc n + n%n≡0 : ∀ n → suc n % suc n ≡ 0 + m%n%n≡m%n : ∀ m n → m % suc n % suc n ≡ m % suc n + [m+n]%n≡m%n : ∀ m n → (m + suc n) % suc n ≡ m % suc n + [m+kn]%n≡m%n : ∀ m k n → (m + k * (suc n)) % suc n ≡ m % suc n + m*n%n≡0 : ∀ m n → (m * suc n) % suc n ≡ 0 + m%n-nonZero : ∀ {i} → i > 0ℤ → NonZero i diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda index 27c23b4a5f..96f5b9bacf 100644 --- a/src/Data/Integer/DivMod.agda +++ b/src/Data/Integer/DivMod.agda @@ -26,74 +26,74 @@ open import Relation.Binary.PropositionalEquality -- Definition infixl 7 _divℕ_ _div_ _modℕ_ _mod_ -_divℕ_ : (dividend : ℤ) (divisor : ℕ) {≢0 : False (divisor ℕ.≟ 0)} → ℤ -(+ n divℕ d) {d≠0} = + (n NDM./ d) {d≠0} -(-[1+ n ] divℕ d) {d≠0} with (ℕ.suc n NDM.divMod d) {d≠0} +_divℕ_ : (dividend : ℤ) (divisor : ℕ) .{{_ : ℕ.NonZero divisor}} → ℤ +(+ n divℕ d) = + (n NDM./ d) +(-[1+ n ] divℕ d) with (ℕ.suc n NDM.divMod d) ... | NDM.result q Fin.zero eq = - (+ q) ... | NDM.result q (Fin.suc r) eq = -[1+ q ] -_div_ : (dividend divisor : ℤ) {≢0 : False (∣ divisor ∣ ℕ.≟ 0)} → ℤ -(n div d) {d≢0} = (sign d ◃ 1) ℤ.* (n divℕ ∣ d ∣) {d≢0} +_div_ : (dividend divisor : ℤ) .{{_ : NonZero divisor}} → ℤ +n div d = (sign d ◃ 1) ℤ.* (n divℕ ∣ d ∣) -_modℕ_ : (dividend : ℤ) (divisor : ℕ) {≢0 : False (divisor ℕ.≟ 0)} → ℕ -(+ n modℕ d) {d≠0} = (n NDM.% d) {d≠0} -(-[1+ n ] modℕ d) {d≠0} with (ℕ.suc n NDM.divMod d) {d≠0} +_modℕ_ : (dividend : ℤ) (divisor : ℕ) .{{_ : ℕ.NonZero divisor}} → ℕ +(+ n modℕ d) = n NDM.% d +(-[1+ n ] modℕ d) with ℕ.suc n NDM.divMod d ... | NDM.result q Fin.zero eq = 0 ... | NDM.result q (Fin.suc r) eq = d ℕ.∸ ℕ.suc (Fin.toℕ r) -_mod_ : (dividend divisor : ℤ) {≢0 : False (∣ divisor ∣ ℕ.≟ 0)} → ℕ -(n mod d) {d≢0} = (n modℕ ∣ d ∣) {d≢0} +_mod_ : (dividend divisor : ℤ) .{{_ : NonZero divisor}} → ℕ +n mod d = n modℕ ∣ d ∣ ------------------------------------------------------------------------ -- Properties -n%ℕd b ------------------------------------------------------------------------ -- Simple predicates --- Defining `NonZero` in terms of `⊤` and `⊥` allows Agda to --- automatically infer nonZero-ness for any natural of the form --- `suc n`. Consequently in many circumstances this eliminates the need --- to explicitly pass a proof when the NonZero argument is either an --- implicit or an instance argument. --- --- It could alternatively be defined using a datatype with an instance --- constructor but then it would not be inferrable when passed as an --- implicit argument. +-- Defining `NonZero` in terms of `T` and therefore ultimately `⊤` and +-- `⊥` allows Agda to automatically infer nonZero-ness for any natural +-- of the form `suc n`. Consequently in many circumstances this +-- eliminates the need to explicitly pass a proof when the NonZero +-- argument is either an implicit or an instance argument. -- -- See `Data.Nat.DivMod` for an example. -NonZero : ℕ → Set -NonZero zero = ⊥ -NonZero (suc x) = ⊤ +record NonZero (n : ℕ) : Set where + field + nonZero : T (not (n ≡ᵇ 0)) + +instance + nonZero : ∀ {n} → NonZero (suc n) + nonZero = _ -- Constructors ≢-nonZero : ∀ {n} → n ≢ 0 → NonZero n -≢-nonZero {zero} 0≢0 = 0≢0 refl -≢-nonZero {suc n} n≢0 = tt +≢-nonZero {zero} 0≢0 = contradiction refl 0≢0 +≢-nonZero {suc n} n≢0 = _ >-nonZero : ∀ {n} → n > 0 → NonZero n ->-nonZero (s≤s 0-nonZero (s≤s 0-nonZero⁻¹ : ∀ {n} → .(NonZero n) → n > 0 +>-nonZero⁻¹ {suc n} _ = s≤s z≤n ------------------------------------------------------------------------ -- Arithmetic diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index dedeeb08c7..72ba60fc68 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -57,9 +57,9 @@ coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime) gcd≡1⇒coprime : ∀ {m n} → gcd m n ≡ 1 → Coprime m n gcd≡1⇒coprime gcd≡1 = GCD≡1⇒coprime (subst (GCD _ _) gcd≡1 (gcd-GCD _ _)) -coprime-/gcd : ∀ m n {gcd≢0} → - Coprime ((m / gcd m n) {gcd≢0}) ((n / gcd m n) {gcd≢0}) -coprime-/gcd m n {gcd≢0} = GCD≡1⇒coprime (GCD-/gcd m n {gcd≢0}) +coprime-/gcd : ∀ m n .{{_ : NonZero (gcd m n)}} → + Coprime (m / gcd m n) (n / gcd m n) +coprime-/gcd m n = GCD≡1⇒coprime (GCD-/gcd m n) ------------------------------------------------------------------------ -- Relational properties of Coprime diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index cbbecccf91..56d3e1ad7f 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -30,7 +30,7 @@ open ≤-Reasoning -- The division and modulus operations are only defined when the divisor -- is non-zero. The proof of non-zero-ness is provided as an irrelevant --- implicit argument which is defined in terms of `⊤` and `⊥`. This +-- instance argument which is defined in terms of `⊤` and `⊥`. This -- allows it to be automatically inferred when the divisor is of the -- form `suc n`, and hence minimises the number of these proofs that -- need be passed around. You can therefore write `m / suc n` without @@ -40,26 +40,26 @@ infixl 7 _/_ _%_ -- Natural division -_/_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ +_/_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ m / (suc n) = div-helper 0 n m n -- Natural remainder/modulus -_%_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ +_%_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ m % (suc n) = mod-helper 0 n m n ------------------------------------------------------------------------ -- Relationship between _%_ and _div_ -m≡m%n+[m/n]*n : ∀ m n → m ≡ m % suc n + (m / suc n) * suc n -m≡m%n+[m/n]*n m n = div-mod-lemma 0 0 m n +m≡m%n+[m/n]*n : ∀ m n .{{_ : NonZero n}} → m ≡ m % n + (m / n) * n +m≡m%n+[m/n]*n m (suc n) = div-mod-lemma 0 0 m n -m%n≡m∸m/n*n : ∀ m n → m % suc n ≡ m ∸ (m / suc n) * suc n -m%n≡m∸m/n*n m n-1 = begin-equality +m%n≡m∸m/n*n : ∀ m n .{{_ : NonZero n}} → m % n ≡ m ∸ (m / n) * n +m%n≡m∸m/n*n m n = begin-equality m % n ≡˘⟨ m+n∸n≡m (m % n) m/n*n ⟩ - m % n + m/n*n ∸ m/n*n ≡˘⟨ cong (_∸ m/n*n) (m≡m%n+[m/n]*n m n-1) ⟩ + m % n + m/n*n ∸ m/n*n ≡˘⟨ cong (_∸ m/n*n) (m≡m%n+[m/n]*n m n) ⟩ m ∸ m/n*n ∎ - where n = suc n-1; m/n*n = (m / n) * n + where m/n*n = (m / n) * n ------------------------------------------------------------------------ -- Properties of _%_ @@ -67,71 +67,70 @@ m%n≡m∸m/n*n m n-1 = begin-equality n%1≡0 : ∀ n → n % 1 ≡ 0 n%1≡0 = a[modₕ]1≡0 -n%n≡0 : ∀ n → suc n % suc n ≡ 0 -n%n≡0 n = n[modₕ]n≡0 0 n +n%n≡0 : ∀ n .{{_ : NonZero n}} → n % n ≡ 0 +n%n≡0 (suc n-1) = n[modₕ]n≡0 0 n-1 -m%n%n≡m%n : ∀ m n → m % suc n % suc n ≡ m % suc n -m%n%n≡m%n m n = modₕ-idem 0 m n +m%n%n≡m%n : ∀ m n .{{_ : NonZero n}} → m % n % n ≡ m % n +m%n%n≡m%n m (suc n-1) = modₕ-idem 0 m n-1 -[m+n]%n≡m%n : ∀ m n → (m + suc n) % suc n ≡ m % suc n -[m+n]%n≡m%n m n = a+n[modₕ]n≡a[modₕ]n 0 m n +[m+n]%n≡m%n : ∀ m n .{{_ : NonZero n}} → (m + n) % n ≡ m % n +[m+n]%n≡m%n m (suc n-1) = a+n[modₕ]n≡a[modₕ]n 0 m n-1 -[m+kn]%n≡m%n : ∀ m k n → (m + k * (suc n)) % suc n ≡ m % suc n -[m+kn]%n≡m%n m zero n-1 = cong (_% suc n-1) (+-identityʳ m) -[m+kn]%n≡m%n m (suc k) n-1 = begin-equality +[m+kn]%n≡m%n : ∀ m k n .{{_ : NonZero n}} → (m + k * n) % n ≡ m % n +[m+kn]%n≡m%n m zero n = cong (_% n) (+-identityʳ m) +[m+kn]%n≡m%n m (suc k) n = begin-equality (m + (n + k * n)) % n ≡⟨ cong (_% n) (sym (+-assoc m n (k * n))) ⟩ - (m + n + k * n) % n ≡⟨ [m+kn]%n≡m%n (m + n) k n-1 ⟩ - (m + n) % n ≡⟨ [m+n]%n≡m%n m n-1 ⟩ + (m + n + k * n) % n ≡⟨ [m+kn]%n≡m%n (m + n) k n ⟩ + (m + n) % n ≡⟨ [m+n]%n≡m%n m n ⟩ m % n ∎ - where n = suc n-1 -m*n%n≡0 : ∀ m n → (m * suc n) % suc n ≡ 0 -m*n%n≡0 = [m+kn]%n≡m%n 0 +m*n%n≡0 : ∀ m n .{{_ : NonZero n}} → (m * n) % n ≡ 0 +m*n%n≡0 m (suc n-1) = [m+kn]%n≡m%n 0 m (suc n-1) -m%n0 : ∀ {m n n≢0} → m ≥ n → (m / n) {n≢0} > 0 -m≥n⇒m/n>0 {m@(suc m-1)} {n@(suc n-1)} m≥n = begin +m≥n⇒m/n>0 : ∀ {m n} .{{_ : NonZero n}} → m ≥ n → m / n > 0 +m≥n⇒m/n>0 {m@(suc _)} {n@(suc _)} m≥n = begin 1 ≡⟨ sym (n/n≡1 m) ⟩ m / m ≤⟨ /-monoʳ-≤ m m≥n ⟩ m / n ∎ -+-distrib-/ : ∀ m n {d} {≢0} → (m % d) {≢0} + (n % d) {≢0} < d → - ((m + n) / d) {≢0} ≡ (m / d) {≢0} + (n / d) {≢0} ++-distrib-/ : ∀ m n {d} .{{_ : NonZero d}} → m % d + n % d < d → + (m + n) / d ≡ m / d + n / d +-distrib-/ m n {suc d-1} leq = +-distrib-divₕ 0 0 m n d-1 leq -+-distrib-/-∣ˡ : ∀ {m} n {d} {≢0} → d ∣ m → - ((m + n) / d) {≢0} ≡ (m / d) {≢0} + (n / d) {≢0} -+-distrib-/-∣ˡ {m} n {d@(suc d-1)} (divides p refl) = +-distrib-/ m n (begin-strict - p * d % d + n % d ≡⟨ cong (_+ n % d) (m*n%n≡0 p d-1) ⟩ - n % d <⟨ m%n0 (toWitnessFalse o≢0)) (≮⇒≥ n≮o) + where n∸o0 (≢-nonZero⁻¹ o≢0)) (≮⇒≥ n≮o) -*-/-assoc : ∀ m {n d} {≢0} → d ∣ n → (m * n / d) {≢0} ≡ m * ((n / d) {≢0}) +*-/-assoc : ∀ m {n d} .{{_ : NonZero d}} → d ∣ n → m * n / d ≡ m * (n / d) *-/-assoc zero {_} {d@(suc _)} d∣n = 0/n≡0 (suc d) *-/-assoc (suc m) {n} {d@(suc _)} d∣n = begin-equality (n + m * n) / d ≡⟨ +-distrib-/-∣ˡ _ d∣n ⟩ n / d + (m * n) / d ≡⟨ cong (n / d +_) (*-/-assoc m d∣n) ⟩ n / d + m * (n / d) ∎ -/-*-interchange : ∀ {m n o p op≢0 o≢0 p≢0} → o ∣ m → p ∣ n → - ((m * n) / (o * p)) {op≢0} ≡ (m / o) {o≢0} * (n / p) {p≢0} +/-*-interchange : ∀ {m n o p} .{{_ : NonZero o}} .{{_ : NonZero p}} .{{_ : NonZero (o * p)}} → + o ∣ m → p ∣ n → (m * n) / (o * p) ≡ (m / o) * (n / p) /-*-interchange {m} {n} {o@(suc _)} {p@(suc _)} o∣m p∣n = *-cancelˡ-≡ (pred (o * p)) (begin-equality (o * p) * ((m * n) / (o * p)) ≡⟨ m*[n/m]≡n (*-pres-∣ o∣m p∣n) ⟩ m * n ≡˘⟨ cong₂ _*_ (m*[n/m]≡n o∣m) (m*[n/m]≡n p∣n) ⟩ @@ -293,18 +296,18 @@ record DivMod (dividend divisor : ℕ) : Set where infixl 7 _div_ _mod_ _divMod_ -_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ +_div_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ _div_ = _/_ -_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor -m mod (suc n) = fromℕ< (m%n0 {n} {gcd m n} {gcd≢0} (gcd[m,n]≤n m n-1)) +n/gcd[m,n]≢0 : ∀ m n .{{_ : NonZero n}} .{{_ : NonZero (gcd m n)}} → n / gcd m n ≢ 0 +n/gcd[m,n]≢0 m n@(suc n-1) = m0 {n} {gcd m n} (gcd[m,n]≤n m n-1)) -m/gcd[m,n]≢0 : ∀ m n {m≢0 : Dec.False (m ≟ 0)} {gcd≢0} → (m / gcd m n) {gcd≢0} ≢ 0 +m/gcd[m,n]≢0 : ∀ m n .{{_ : NonZero m}} .{{_ : NonZero (gcd m n)}} → m / gcd m n ≢ 0 m/gcd[m,n]≢0 m@(suc _) n rewrite gcd-comm m n = n/gcd[m,n]≢0 n m ------------------------------------------------------------------------ @@ -221,20 +221,20 @@ gcd? m n d = Dec.map′ (λ { P.refl → gcd-GCD m n }) (GCD.unique (gcd-GCD m n)) (gcd m n ≟ d) -GCD-* : ∀ {m n d c} → GCD (m * suc c) (n * suc c) (d * suc c) → GCD m n d -GCD-* (GCD.is (dc∣nc , dc∣mc) dc-greatest) = +GCD-* : ∀ {m n d c} .{{_ : NonZero c}} → GCD (m * c) (n * c) (d * c) → GCD m n d +GCD-* {c = suc _} (GCD.is (dc∣nc , dc∣mc) dc-greatest) = GCD.is (*-cancelʳ-∣ _ dc∣nc , *-cancelʳ-∣ _ dc∣mc) λ {_} → *-cancelʳ-∣ _ ∘ dc-greatest ∘ map (*-monoˡ-∣ _) (*-monoˡ-∣ _) -GCD-/ : ∀ {m n d c} {≢0} → c ∣ m → c ∣ n → c ∣ d → - GCD m n d → GCD ((m / c) {≢0}) ((n / c) {≢0}) ((d / c) {≢0}) -GCD-/ {m} {n} {d} {c@(suc c-1)} +GCD-/ : ∀ {m n d c} .{{_ : NonZero c}} → c ∣ m → c ∣ n → c ∣ d → + GCD m n d → GCD (m / c) (n / c) (d / c) +GCD-/ {m} {n} {d} {c} {{x}} (divides p P.refl) (divides q P.refl) (divides r P.refl) gcd - rewrite m*n/n≡m p c {_} | m*n/n≡m q c {_} | m*n/n≡m r c {_} = GCD-* gcd + rewrite m*n/n≡m p c {{x}} | m*n/n≡m q c {{x}} | m*n/n≡m r c {{x}} = GCD-* gcd -GCD-/gcd : ∀ m n {≢0} → GCD ((m / gcd m n) {≢0}) ((n / gcd m n) {≢0}) 1 -GCD-/gcd m n {≢0} rewrite P.sym (n/n≡1 (gcd m n) {≢0}) = - GCD-/ {≢0 = ≢0} (gcd[m,n]∣m m n) (gcd[m,n]∣n m n) ∣-refl (gcd-GCD m n) +GCD-/gcd : ∀ m n .{{_ : NonZero (gcd m n)}} → GCD (m / gcd m n) (n / gcd m n) 1 +GCD-/gcd m n rewrite P.sym (n/n≡1 (gcd m n)) = + GCD-/ (gcd[m,n]∣m m n) (gcd[m,n]∣n m n) ∣-refl (gcd-GCD m n) ------------------------------------------------------------------------ -- Calculating the gcd @@ -325,13 +325,13 @@ module Bézout where P (m , n) = Lemma m n gcd″ : ∀ p → (<′-Rec ⊗ <′-Rec) P p → P p - gcd″ (zero , n ) rec = Lemma.base n - gcd″ (suc m , zero ) rec = Lemma.sym (Lemma.base (suc m)) - gcd″ (suc m , suc n ) rec with compare m n - ... | equal .m = Lemma.refl (suc m) - ... | less .m k = Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m) + gcd″ (zero , n) rec = Lemma.base n + gcd″ (suc m , zero) rec = Lemma.sym (Lemma.base (suc m)) + gcd″ (suc m , suc n) rec with compare m n + ... | equal m = Lemma.refl (suc m) + ... | less m k = Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m) -- "gcd (suc m) (suc k)" - ... | greater .n k = Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n) + ... | greater n k = Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n) -- "gcd (suc k) (suc n)" -- Bézout's identity can be recovered from the GCD. diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda index 4d2d3b1f2a..2969a984e6 100644 --- a/src/Data/Nat/LCM.agda +++ b/src/Data/Nat/LCM.agda @@ -14,7 +14,6 @@ open import Data.Nat.Coprimality using (Coprime) open import Data.Nat.Divisibility open import Data.Nat.DivMod open import Data.Nat.Properties -open import Data.Nat.Solver open import Data.Nat.GCD open import Data.Product open import Data.Sum.Base using (_⊎_; inj₁; inj₂) @@ -24,54 +23,58 @@ open import Relation.Binary.PropositionalEquality as P open import Relation.Binary open import Relation.Nullary.Decidable using (False; fromWitnessFalse) -open +-*-Solver - private - gcd≢0′ : ∀ m n → False (gcd (suc m) n ≟ 0) - gcd≢0′ m n = fromWitnessFalse (gcd[m,n]≢0 (suc m) n (inj₁ (λ()))) + -- instance + gcd≢0ˡ : ∀ {m n} {{_ : NonZero m}} → NonZero (gcd m n) + gcd≢0ˡ {m@(suc _)} {n} = ≢-nonZero (gcd[m,n]≢0 m n (inj₁ λ())) ------------------------------------------------------------------------ -- Definition lcm : ℕ → ℕ → ℕ lcm zero n = zero -lcm m@(suc m-1) n = m * (n / gcd m n) {gcd≢0′ m-1 n} +lcm m@(suc m-1) n = m * (n / gcd m n) + where instance _ = gcd≢0ˡ {m} {n} ------------------------------------------------------------------------ -- Core properties private - rearrange : ∀ m-1 n → lcm (suc m-1) n ≡ ((suc m-1) * n / gcd (suc m-1) n) {gcd≢0′ m-1 n} - rearrange m-1 n = sym (*-/-assoc m {n} {gcd m n} {gcd≢0′ m-1 n} (gcd[m,n]∣n m n)) - where m = suc m-1 + rearrange : ∀ m n .{{_ : NonZero m}} → + lcm m n ≡ (m * n / gcd m n) {{gcd≢0ˡ {m} {n}}} + rearrange m@(suc _) n = sym (*-/-assoc m {{gcd≢0ˡ {m} {n}}} (gcd[m,n]∣n m n)) m∣lcm[m,n] : ∀ m n → m ∣ lcm m n m∣lcm[m,n] zero n = 0 ∣0 m∣lcm[m,n] m@(suc _) n = m∣m*n (n / gcd m n) + where instance _ = gcd≢0ˡ {m} {n} n∣lcm[m,n] : ∀ m n → n ∣ lcm m n n∣lcm[m,n] zero n = n ∣0 n∣lcm[m,n] m@(suc m-1) n = begin - n ∣⟨ m∣m*n (m / gcd m n) ⟩ - n * (m / gcd m n) ≡⟨ sym (*-/-assoc n {≢0 = gcd≢0′ m-1 n} (gcd[m,n]∣m m n)) ⟩ - n * m / gcd m n ≡⟨ cong (λ v → (v / gcd m n) {gcd≢0′ m-1 n}) (*-comm n m) ⟩ - m * n / gcd m n ≡⟨ sym (rearrange m-1 n) ⟩ + n ∣⟨ m∣m*n (m / gcd m n) ⟩ + n * (m / gcd m n) ≡˘⟨ *-/-assoc n (gcd[m,n]∣m m n) ⟩ + n * m / gcd m n ≡⟨ cong (_/ gcd m n) (*-comm n m) ⟩ + m * n / gcd m n ≡˘⟨ rearrange m n ⟩ m * (n / gcd m n) ∎ - where open ∣-Reasoning + where open ∣-Reasoning; instance _ = gcd≢0ˡ {m} {n} + lcm-least : ∀ {m n c} → m ∣ c → n ∣ c → lcm m n ∣ c -lcm-least {zero} {n} {c} 0∣c _ = 0∣c -lcm-least {m@(suc m-1)} {n} {c} m∣c n∣c = P.subst (_∣ c) (sym (rearrange m-1 n)) - (m∣n*o⇒m/n∣o {n≢0 = gcd≢0′ m-1 n} gcd[m,n]∣m*n mn∣c*gcd) +lcm-least {zero} {n} {c} 0∣c _ = 0∣c +lcm-least {m@(suc _)} {n} {c} m∣c n∣c = P.subst (_∣ c) (sym (rearrange m n)) + (m∣n*o⇒m/n∣o gcd[m,n]∣m*n mn∣c*gcd) where + instance _ = gcd≢0ˡ {m} {n} + open ∣-Reasoning gcd[m,n]∣m*n : gcd m n ∣ m * n gcd[m,n]∣m*n = ∣-trans (gcd[m,n]∣m m n) (m∣m*n n) mn∣c*gcd : m * n ∣ c * gcd m n mn∣c*gcd = begin - m * n ∣⟨ gcd-greatest (P.subst (_∣ c * m) (*-comm n m) (*-monoˡ-∣ m n∣c)) (*-monoˡ-∣ n m∣c) ⟩ - gcd (c * m) (c * n) ≡⟨ sym (c*gcd[m,n]≡gcd[cm,cn] c m n) ⟩ + m * n ∣⟨ gcd-greatest (P.subst (_∣ c * m) (*-comm n m) (*-monoˡ-∣ m n∣c)) (*-monoˡ-∣ n m∣c) ⟩ + gcd (c * m) (c * n) ≡˘⟨ c*gcd[m,n]≡gcd[cm,cn] c m n ⟩ c * gcd m n ∎ ------------------------------------------------------------------------ @@ -82,11 +85,11 @@ lcm-least {m@(suc m-1)} {n} {c} m∣c n∣c = P.subst (_∣ c) (sym (rearrange m gcd*lcm : ∀ m n → gcd m n * lcm m n ≡ m * n gcd*lcm zero n = *-zeroʳ (gcd 0 n) -gcd*lcm m@(suc m-1) n = trans (cong (gcd m n *_) (rearrange m-1 n)) (m*[n/m]≡n {gcd m n} (begin +gcd*lcm m@(suc m-1) n = trans (cong (gcd m n *_) (rearrange m n)) (m*[n/m]≡n (begin gcd m n ∣⟨ gcd[m,n]∣m m n ⟩ m ∣⟨ m∣m*n n ⟩ m * n ∎)) - where open ∣-Reasoning + where open ∣-Reasoning; instance gcd≢0 = gcd≢0ˡ {m} {n} lcm[0,n]≡0 : ∀ n → lcm 0 n ≡ 0 lcm[0,n]≡0 n = 0∣⇒≡0 (m∣lcm[m,n] 0 n) diff --git a/src/Data/Nat/PseudoRandom/LCG.agda b/src/Data/Nat/PseudoRandom/LCG.agda index fe6f531757..83dd279842 100644 --- a/src/Data/Nat/PseudoRandom/LCG.agda +++ b/src/Data/Nat/PseudoRandom/LCG.agda @@ -9,24 +9,23 @@ module Data.Nat.PseudoRandom.LCG where -open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _≟_) +open import Data.Nat.Base open import Data.Nat.DivMod using (_%_) open import Data.List.Base using (List; []; _∷_) -open import Relation.Nullary.Decidable using (False) ------------------------------------------------------------------------ -- Type and generator record Generator : Set where - field multiplier : ℕ - increment : ℕ - modulus : ℕ - {modulus≢0} : False (modulus ≟ 0) + field multiplier : ℕ + increment : ℕ + modulus : ℕ + .{{modulus≢0}} : NonZero modulus step : Generator → ℕ → ℕ step gen x = let open Generator gen in - ((multiplier * x + increment) % modulus) {modulus≢0} + ((multiplier * x + increment) % modulus) list : ℕ → Generator → ℕ → List ℕ list zero gen x = [] diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda index b34ef95460..0320df655a 100644 --- a/src/Data/Rational/Base.agda +++ b/src/Data/Rational/Base.agda @@ -122,11 +122,11 @@ p ≤ᵇ q = (↥ p ℤ.* ↧ q) ℤ.≤ᵇ (↥ q ℤ.* ↧ p) -- and returns them in a normalized form, e.g. say 2 and 7 normalize : ∀ (m n : ℕ) {n≢0 : n ≢0} → ℚ -normalize m n {n≢0} = mkℚ+ (m ℕ./ gcd m n) (n ℕ./ gcd m n) - {n/g≢0} (coprime-/gcd m n {g≢0}) +normalize m n {n≢0} = mkℚ+ ((m ℕ./ gcd m n) {{g≢0}}) ((n ℕ./ gcd m n) {{g≢0}}) + {n/g≢0} (coprime-/gcd m n {{g≢0}}) where - g≢0 = fromWitnessFalse (gcd[m,n]≢0 m n (inj₂ (toWitnessFalse n≢0))) - n/g≢0 = fromWitnessFalse (n/gcd[m,n]≢0 m n {n≢0} {g≢0}) + g≢0 = ℕ.≢-nonZero (gcd[m,n]≢0 m n (inj₂ (toWitnessFalse n≢0))) + n/g≢0 = fromWitnessFalse (n/gcd[m,n]≢0 m n {{ℕ.≢-nonZero (toWitnessFalse n≢0)}} {{g≢0}}) -- A constructor for ℚ that (unlike mkℚ) automatically normalises it's -- arguments. See the constants section below for how to use this operator. @@ -184,8 +184,8 @@ NonNegative p = ℚᵘ.NonNegative (toℚᵘ p) ≢-nonZero : ∀ {p} → p ≢ 0ℚ → NonZero p ≢-nonZero {mkℚ -[1+ _ ] _ _} _ = _ ≢-nonZero {mkℚ +[1+ _ ] _ _} _ = _ -≢-nonZero {mkℚ +0 zero _} p≢0 = p≢0 refl -≢-nonZero {mkℚ +0 (suc d) c} p≢0 = ¬0-coprimeTo-2+ (C.recompute c) +≢-nonZero {mkℚ +0 zero _} p≢0 = contradiction refl p≢0 +≢-nonZero {mkℚ +0 (suc d) c} p≢0 = contradiction (λ {i} → C.recompute c {i}) ¬0-coprimeTo-2+ >-nonZero : ∀ {p} → p > 0ℚ → NonZero p >-nonZero {p} (*<* p-nonZero {toℚᵘ p} (ℚᵘ.*<* p-nonZero : ∀ {p} → p > 0ℚᵘ → NonZero p >-nonZero {mkℚᵘ +0 _} (*<* (+<+ ())) diff --git a/src/System/Clock.agda b/src/System/Clock.agda index 916e6786e1..97891c020c 100644 --- a/src/System/Clock.agda +++ b/src/System/Clock.agda @@ -11,9 +11,9 @@ module System.Clock where open import Level using (Level; 0ℓ; Lift; lower) open import Data.Bool.Base using (if_then_else_) open import Data.Fin.Base using (Fin; toℕ) -open import Data.Nat.Base using (ℕ; zero; suc; _+_; _∸_; _^_; _<ᵇ_) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _∸_; _^_; _<ᵇ_) import Data.Nat.Show as ℕ -open import Data.Nat.DivMod using (_div_) +open import Data.Nat.DivMod using (_/_) import Data.Nat.Properties as ℕₚ open import Data.String.Base using (String; _++_; padLeft) @@ -105,8 +105,8 @@ show (mkTime s ns) prec = secs ++ "s" ++ padLeft '0' decimals nsecs where decimals = toℕ prec secs = ℕ.show s - exp-nz : ∀ x n {x≠0 : False (x ℕₚ.≟ 0)} → False (x ^ n ℕₚ.≟ 0) - exp-nz x n {x≠0} = fromWitnessFalse (toWitnessFalse x≠0 ∘′ ℕₚ.m^n≡0⇒m≡0 x n) + exp-nz : ∀ x n {x≠0 : ℕ.NonZero x} → ℕ.NonZero (x ^ n) + exp-nz x n {x≠0} = ℕ.≢-nonZero (ℕ.≢-nonZero⁻¹ x≠0 ∘′ ℕₚ.m^n≡0⇒m≡0 x n) prf = exp-nz 10 (9 ∸ decimals) - nsecs = ℕ.show ((ns div (10 ^ (9 ∸ decimals))) {prf}) + nsecs = ℕ.show ((ns / (10 ^ (9 ∸ decimals))) {{prf}})