Skip to content

Commit ae33a51

Browse files
MatthewDaggittMatthewDaggitt
authored
Changed _/_ and _%_ to use irrelevant instance arguments for Nat and Integer (#1538)
1 parent 27db795 commit ae33a51

15 files changed

+445
-343
lines changed

‎CHANGELOG.md

+83
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,9 @@ Bug-fixes
2020
rather than a natural. The previous binding was incorrectly assuming that
2121
all exit codes where non-negative.
2222

23+
* In `/-monoˡ-≤` in `Data.Nat.DivMod` the parameter `o` was implicit but not inferrable.
24+
It has been changed to be explicit.
25+
2326
* In `Function.Definitions` the definitions of `Surjection`, `Inverseˡ`,
2427
`Inverseʳ` were not being re-exported correctly and therefore had an unsolved
2528
meta-variable whenever this module was explicitly parameterised. This has
@@ -72,6 +75,86 @@ Non-backwards compatible changes
7275
So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to"
7376
will return "Main.agdai" when it used to be happy to just return "n.agda".
7477

78+
#### Proofs of non-zeroness as instance arguments
79+
80+
* Many numeric operations in the library require their arguments to be non-zero.
81+
The previous way of constructing and passing round these proofs resulted in clunky code.
82+
As described on the [mailing list](https://lists.chalmers.se/pipermail/agda/2021/012693.html)
83+
we have converted the operations to take the proofs of non-zeroness as irrelevant
84+
[instance arguments](https://agda.readthedocs.io/en/latest/language/instance-arguments.html).
85+
See the mailing list for a fuller explanation of the motivation and implementation.
86+
87+
* For example the type signature of division is now:
88+
```
89+
_/_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
90+
```
91+
which means that as long as an instance of `NonZero n` is in scope then you can write
92+
`m / n` without having to explicitly provide a proof as instance search will fill it in
93+
for you. The full list of such operations changed is as follows:
94+
- In `Data.Nat.DivMod`: `_/_`, `_%_`, `_div_`, `_mod_`
95+
- In `Data.Nat.Pseudorandom.LCG`: `Generator`
96+
- In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_`
97+
98+
* At the moment, there are 4 different ways such instance arguments can be provided,
99+
listed in order of convenience and clarity:
100+
1. By default there is always an instance of `NonZero (suc n)` for any `n` which
101+
will be picked up automatically:
102+
```
103+
0/n≡0 : 0 / suc n ≡ 0
104+
```
105+
2. You can take the proof an instance argument as a parameter, e.g.
106+
```
107+
0/n≡0 : {{_ : NonZero n}} → 0 / n ≡ 0
108+
```
109+
3. You can define an instance argument in scope higher-up (or in a `where` clause):
110+
```
111+
instance
112+
n≢0 : NonZero n
113+
n≢0 = ...
114+
115+
0/n≡0 : 0 / n ≡ 0
116+
```
117+
4. You can provide the instance argument explicitly, e.g. `0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0`
118+
```
119+
0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0
120+
```
121+
122+
* Previously one of the hacks used in proofs was to explicitly put everything in the form `suc n`.
123+
This often made the proofs extremely difficult to use if you're term wasn't in that form. These
124+
proofs have now all been updated to use instance arguments instead, e.g.
125+
```
126+
n/n≡1 : ∀ n → suc n / suc n ≡ 1
127+
```
128+
becomes
129+
```
130+
n/n≡1 : ∀ n {{_ : NonZero n}} → n / n ≡ 1
131+
```
132+
This does however mean that if you passed in the value `x` to these proofs before, then you
133+
will now have to pass in `suc x`. The full list of such proofs is below:
134+
- In `Data.Nat.DivMod`:
135+
```agda
136+
m≡m%n+[m/n]*n : ∀ m n → m ≡ m % suc n + (m / suc n) * suc n
137+
m%n≡m∸m/n*n : ∀ m n → m % suc n ≡ m ∸ (m / suc n) * suc n
138+
n%n≡0 : ∀ n → suc n % suc n ≡ 0
139+
m%n%n≡m%n : ∀ m n → m % suc n % suc n ≡ m % suc n
140+
[m+n]%n≡m%n : ∀ m n → (m + suc n) % suc n ≡ m % suc n
141+
[m+kn]%n≡m%n : ∀ m k n → (m + k * (suc n)) % suc n ≡ m % suc n
142+
m*n%n≡0 : ∀ m n → (m * suc n) % suc n ≡ 0
143+
m%n<n : ∀ m n → m % suc n < suc n
144+
m%n≤m : ∀ m n → m % suc n ≤ m
145+
m≤n⇒m%n≡m : ∀ {m n} → m ≤ n → m % suc n ≡ m
146+
```
147+
- In `Data.Nat.Divisibility`
148+
```agda
149+
m%n≡0⇒n∣m : ∀ m n → m % suc n ≡ 0 → suc n ∣ m
150+
n∣m⇒m%n≡0 : ∀ m n → suc n ∣ m → m % suc n ≡ 0
151+
m%n≡0⇔n∣m : ∀ m n → m % suc n ≡ 0 ⇔ suc n ∣ m
152+
```
153+
- In `Data.Nat.GCD`
154+
```
155+
GCD-* : ∀ {m n d c} → GCD (m * suc c) (n * suc c) (d * suc c) → GCD m n d
156+
```
157+
75158
### Strict functions
76159
77160
* The module `Strict` has been deprecated in favour of `Function.Strict`

‎src/Data/Integer/Base.agda

+2-1
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ open import Relation.Binary using (Rel)
2626
open import Relation.Binary.PropositionalEquality.Core
2727
using (_≡_; _≢_; refl)
2828
open import Relation.Nullary using (¬_)
29+
open import Relation.Nullary.Negation using (contradiction)
2930
open import Relation.Unary using (Pred)
3031

3132
infix 8 -_
@@ -148,7 +149,7 @@ NonNegative -[1+ n ] = ⊥
148149

149150
≢-nonZero : ∀ {i} → i ≢ 0ℤ → NonZero i
150151
≢-nonZero { +[1+ n ]} _ = _
151-
≢-nonZero { +0} 0≢0 = 0≢0 refl
152+
≢-nonZero { +0} 0≢0 = contradiction refl 0≢0
152153
≢-nonZero { -[1+ n ]} _ = _
153154

154155
>-nonZero : ∀ {i} → i > 0ℤ → NonZero i

‎src/Data/Integer/DivMod.agda

+82-82
Original file line numberDiff line numberDiff line change
@@ -26,74 +26,74 @@ open import Relation.Binary.PropositionalEquality
2626
-- Definition
2727

2828
infixl 7 _divℕ_ _div_ _modℕ_ _mod_
29-
_divℕ_ : (dividend : ℤ) (divisor : ℕ) {≢0 : False (divisor ℕ.≟ 0)} → ℤ
30-
(+ n divℕ d) {d≠0} = + (n NDM./ d) {d≠0}
31-
(-[1+ n ] divℕ d) {d≠0} with (ℕ.suc n NDM.divMod d) {d≠0}
29+
_divℕ_ : (dividend : ℤ) (divisor : ℕ) .{{_ : ℕ.NonZero divisor}} → ℤ
30+
(+ n divℕ d) = + (n NDM./ d)
31+
(-[1+ n ] divℕ d) with (ℕ.suc n NDM.divMod d)
3232
... | NDM.result q Fin.zero eq = - (+ q)
3333
... | NDM.result q (Fin.suc r) eq = -[1+ q ]
3434

35-
_div_ : (dividend divisor : ℤ) {≢0 : False (∣ divisor ∣ ℕ.≟ 0)} → ℤ
36-
(n div d) {d≢0} = (sign d ◃ 1) ℤ.* (n divℕ ∣ d ∣) {d≢0}
35+
_div_ : (dividend divisor : ℤ) .{{_ : NonZero divisor}} → ℤ
36+
n div d = (sign d ◃ 1) ℤ.* (n divℕ ∣ d ∣)
3737

38-
_modℕ_ : (dividend : ℤ) (divisor : ℕ) {≢0 : False (divisor ℕ.≟ 0)} → ℕ
39-
(+ n modℕ d) {d≠0} = (n NDM.% d) {d≠0}
40-
(-[1+ n ] modℕ d) {d≠0} with (ℕ.suc n NDM.divMod d) {d≠0}
38+
_modℕ_ : (dividend : ℤ) (divisor : ℕ) .{{_ : ℕ.NonZero divisor}} → ℕ
39+
(+ n modℕ d) = n NDM.% d
40+
(-[1+ n ] modℕ d) with ℕ.suc n NDM.divMod d
4141
... | NDM.result q Fin.zero eq = 0
4242
... | NDM.result q (Fin.suc r) eq = d ℕ.∸ ℕ.suc (Fin.toℕ r)
4343

44-
_mod_ : (dividend divisor : ℤ) {≢0 : False (∣ divisor ∣ ℕ.≟ 0)} → ℕ
45-
(n mod d) {d≢0} = (n modℕ ∣ d ∣) {d≢0}
44+
_mod_ : (dividend divisor : ℤ) .{{_ : NonZero divisor}} → ℕ
45+
n mod d = n modℕ ∣ d ∣
4646

4747
------------------------------------------------------------------------
4848
-- Properties
4949

50-
n%ℕd<d : ∀ n d {d≢0} → (n modℕ d) {d≢0} ℕ.< d
51-
n%ℕd<d (+ n) sd@(ℕ.suc d) = NDM.m%n<n n d
52-
n%ℕd<d -[1+ n ] sd@(ℕ.suc d) with ℕ.suc n NDM.divMod sd
50+
n%ℕd<d : ∀ n d .{{_ : ℕ.NonZero d}} → n modℕ d ℕ.< d
51+
n%ℕd<d (+ n) d = NDM.m%n<n n d
52+
n%ℕd<d -[1+ n ] d with ℕ.suc n NDM.divMod d
5353
... | NDM.result q Fin.zero eq = ℕ.s≤s ℕ.z≤n
54-
... | NDM.result q (Fin.suc r) eq = ℕ.s≤s (NProp.m∸n≤m d (Fin.toℕ r))
54+
... | NDM.result q (Fin.suc r) eq = ℕ.s≤s (NProp.m∸n≤m _ (Fin.toℕ r))
5555

56-
n%d<d : ∀ n d {d≢0} → (n mod d) {d≢0} ℕ.< ℤ.∣ d ∣
57-
n%d<d n (+ ℕ.suc d) = n%ℕd<d n (ℕ.suc d)
58-
n%d<d n -[1+ d ] = n%ℕd<d n (ℕ.suc d)
56+
n%d<d : ∀ n d .{{_ : NonZero d}} → n mod d ℕ.< ℤ.∣ d ∣
57+
n%d<d n (+ d) = n%ℕd<d n d
58+
n%d<d n -[1+ d ] = n%ℕd<d n (ℕ.suc d)
5959

60-
a≡a%ℕn+[a/ℕn]*n : ∀ n d {d≢0} → n ≡ + (n modℕ d) {d≢0} + (n divℕ d) {d≢0} * + d
61-
a≡a%ℕn+[a/ℕn]*n (+ n) sd@(ℕ.suc d) = let q = n NDM./ sd; r = n NDM.% sd in begin
60+
a≡a%ℕn+[a/ℕn]*n : ∀ n d .{{_ : ℕ.NonZero d}} → n ≡ + (n modℕ d) + (n divℕ d) * + d
61+
a≡a%ℕn+[a/ℕn]*n (+ n) d = let q = n NDM./ d; r = n NDM.% d in begin
6262
+ n ≡⟨ cong +_ (NDM.m≡m%n+[m/n]*n n d) ⟩
63-
+ (r ℕ.+ q ℕ.* sd) ≡⟨ pos-+-commute r (q ℕ.* sd) ⟩
64-
+ r + + (q ℕ.* sd) ≡⟨ cong (_+_ (+ (+ n modℕ sd))) (sym (pos-distrib-* q sd)) ⟩
65-
+ r + + q * + sd ∎ where open ≡-Reasoning
66-
a≡a%ℕn+[a/ℕn]*n -[1+ n ] sd@(ℕ.suc d) with (ℕ.suc n) NDM.divMod (ℕ.suc d)
63+
+ (r ℕ.+ q ℕ.* d) ≡⟨ pos-+-commute r (q ℕ.* d) ⟩
64+
+ r + + (q ℕ.* d) ≡⟨ cong (_+_ (+ (+ n modℕ d))) (sym (pos-distrib-* q d)) ⟩
65+
+ r + + q * + d ∎ where open ≡-Reasoning
66+
a≡a%ℕn+[a/ℕn]*n -[1+ n ] d with (ℕ.suc n) NDM.divMod d
6767
... | NDM.result q Fin.zero eq = begin
6868
-[1+ n ] ≡⟨ cong (-_ ∘′ +_) eq ⟩
69-
- + (q ℕ.* sd) ≡⟨ cong -_ (sym (pos-distrib-* q sd)) ⟩
70-
- (+ q * + sd) ≡⟨ neg-distribˡ-* (+ q) (+ sd) ⟩
71-
- (+ q) * + sd ≡⟨ sym (+-identityˡ (- (+ q) * + sd)) ⟩
72-
+ 0 + - (+ q) * + sd ∎ where open ≡-Reasoning
69+
- + (q ℕ.* d) ≡⟨ cong -_ (sym (pos-distrib-* q d)) ⟩
70+
- (+ q * + d) ≡⟨ neg-distribˡ-* (+ q) (+ d) ⟩
71+
- (+ q) * + d ≡⟨ sym (+-identityˡ (- (+ q) * + d)) ⟩
72+
+ 0 + - (+ q) * + d ∎ where open ≡-Reasoning
7373
... | NDM.result q (Fin.suc r) eq = begin
74-
let sd = ℕ.suc d; sr = ℕ.suc (Fin.toℕ r); sq = ℕ.suc q in
74+
let sr = ℕ.suc (Fin.toℕ r); sq = ℕ.suc q in
7575
-[1+ n ]
7676
≡⟨ cong (-_ ∘′ +_) eq ⟩
77-
- + (sr ℕ.+ q ℕ.* sd)
78-
≡⟨ cong -_ (pos-+-commute sr (q ℕ.* sd)) ⟩
79-
- (+ sr + + (q ℕ.* sd))
80-
≡⟨ neg-distrib-+ (+ sr) (+ (q ℕ.* sd)) ⟩
81-
- + sr - + (q ℕ.* sd)
82-
≡⟨ cong (_-_ (- + sr)) (sym (pos-distrib-* q sd)) ⟩
83-
- + sr - (+ q) * (+ sd)
77+
- + (sr ℕ.+ q ℕ.* d)
78+
≡⟨ cong -_ (pos-+-commute sr (q ℕ.* d)) ⟩
79+
- (+ sr + + (q ℕ.* d))
80+
≡⟨ neg-distrib-+ (+ sr) (+ (q ℕ.* d)) ⟩
81+
- + sr - + (q ℕ.* d)
82+
≡⟨ cong (_-_ (- + sr)) (sym (pos-distrib-* q d)) ⟩
83+
- + sr - (+ q) * (+ d)
8484
≡⟨⟩
85-
- + sr - pred (+ sq) * (+ sd)
86-
≡⟨ cong (_-_ (- + sr)) (*-distribʳ-+ (+ sd) (- + 1) (+ sq)) ⟩
87-
- + sr - (- (+ 1) * + sd + (+ sq * + sd))
88-
≡⟨ cong (_+_ (- (+ sr))) (neg-distrib-+ (- (+ 1) * + sd) (+ sq * + sd)) ⟩
89-
- + sr + (- (-[1+ 0 ] * + sd) + - (+ sq * + sd))
90-
≡⟨ cong₂ (λ p q → - + sr + (- p + q)) (-1*n≡-n (+ sd))
91-
(neg-distribˡ-* (+ sq) (+ sd)) ⟩
92-
- + sr + ((- - + sd) + -[1+ q ] * + sd)
93-
≡⟨ sym (+-assoc (- + sr) (- - + sd) (-[1+ q ] * + sd)) ⟩
94-
(+ sd - + sr) + -[1+ q ] * + sd
95-
≡⟨ cong (_+ -[1+ q ] * + sd) (fin-inv d r) ⟩
96-
+ (sd ℕ.∸ sr) + -[1+ q ] * + sd
85+
- + sr - pred (+ sq) * (+ d)
86+
≡⟨ cong (_-_ (- + sr)) (*-distribʳ-+ (+ d) (- + 1) (+ sq)) ⟩
87+
- + sr - (- (+ 1) * + d + (+ sq * + d))
88+
≡⟨ cong (_+_ (- (+ sr))) (neg-distrib-+ (- (+ 1) * + d) (+ sq * + d)) ⟩
89+
- + sr + (- (-[1+ 0 ] * + d) + - (+ sq * + d))
90+
≡⟨ cong₂ (λ p q → - + sr + (- p + q)) (-1*n≡-n (+ d))
91+
(neg-distribˡ-* (+ sq) (+ d)) ⟩
92+
- + sr + ((- - + d) + -[1+ q ] * + d)
93+
≡⟨ sym (+-assoc (- + sr) (- - + d) (-[1+ q ] * + d)) ⟩
94+
(+ d - + sr) + -[1+ q ] * + d
95+
≡⟨ cong (_+ -[1+ q ] * + d) (fin-inv _ r) ⟩
96+
+ (d ℕ.∸ sr) + -[1+ q ] * + d
9797
∎ where
9898

9999
open ≡-Reasoning
@@ -104,52 +104,52 @@ a≡a%ℕn+[a/ℕn]*n -[1+ n ] sd@(ℕ.suc d) with (ℕ.suc n) NDM.divMod (ℕ.s
104104
ℕ.suc d ⊖ ℕ.suc (Fin.toℕ k) ≡⟨ ⊖-≥ (ℕ.s≤s (FProp.toℕ≤n k)) ⟩
105105
+ (d ℕ.∸ Fin.toℕ k) ∎ where open ≡-Reasoning
106106

107-
[n/ℕd]*d≤n : ∀ n d {d≢0} → (n divℕ d) {d≢0} ℤ.* ℤ.+ d ℤ.≤ n
107+
[n/ℕd]*d≤n : ∀ n d .{{_ : ℕ.NonZero d}} → (n divℕ d) ℤ.* ℤ.+ d ℤ.≤ n
108108
[n/ℕd]*d≤n n (ℕ.suc d) = let q = n divℕ ℕ.suc d; r = n modℕ ℕ.suc d in begin
109109
q ℤ.* ℤ.+ (ℕ.suc d) ≤⟨ n≤m+n r ⟩
110110
ℤ.+ r ℤ.+ q ℤ.* ℤ.+ (ℕ.suc d) ≡⟨ sym (a≡a%ℕn+[a/ℕn]*n n (ℕ.suc d)) ⟩
111111
n ∎ where open ≤-Reasoning
112112

113-
div-pos-is-divℕ : ∀ n d {d≢0} → (n div + d) {d≢0} ≡ (n divℕ d) {d≢0}
113+
div-pos-is-divℕ : ∀ n d .{{_ : ℕ.NonZero d}} → n div (+ d) ≡ n divℕ d
114114
div-pos-is-divℕ n (ℕ.suc d) = *-identityˡ (n divℕ ℕ.suc d)
115115

116-
div-neg-is-neg-divℕ : ∀ n d {d≢0} {∣d∣≢0} → (n div (- ℤ.+ d)) {∣d∣≢0} ≡ - (n divℕ d) {d≢0}
116+
div-neg-is-neg-divℕ : ∀ n d .{{_ : ℕ.NonZero d}} .{{_ : NonZero (- + d)}} → n div (- + d) ≡ - (n divℕ d)
117117
div-neg-is-neg-divℕ n (ℕ.suc d) = -1*n≡-n (n divℕ ℕ.suc d)
118118

119-
0≤n⇒0≤n/ℕd : ∀ n d {d≢0} → + 0 ℤ.≤ n → + 0 ℤ.≤ (n divℕ d) {d≢0}
119+
0≤n⇒0≤n/ℕd : ∀ n d .{{_ : ℕ.NonZero d}} → +0 ℤ.≤ n → +0 ℤ.≤ (n divℕ d)
120120
0≤n⇒0≤n/ℕd (+ n) d (+≤+ m≤n) = +≤+ ℕ.z≤n
121121

122-
0≤n⇒0≤n/d : ∀ n d {d≢0} → + 0 ℤ.≤ n → + 0 ℤ.≤ d → + 0 ℤ.≤ (n div d) {d≢0}
123-
0≤n⇒0≤n/d n (+ d) {d≢0} 0≤n (+≤+ 0≤d)
124-
rewrite div-pos-is-divℕ n d {d≢0}
125-
= 0≤n⇒0≤n/ℕd n d {d≢0} 0≤n
126-
127-
[n/d]*d≤n : ∀ n d {d≢0} → (n div d) {d≢0} ℤ.* d ℤ.≤ n
128-
[n/d]*d≤n n (+ ℕ.suc d) = begin let sd = ℕ.suc d in
129-
n div + sd * + sd ≡⟨ cong (_* (+ sd)) (div-pos-is-divℕ n sd) ⟩
130-
n divℕ sd * + sd ≤⟨ [n/ℕd]*d≤n n sd ⟩
131-
n ∎ where open ≤-Reasoning
132-
[n/d]*d≤n n -[1+ d ] = begin let sd = ℕ.suc d in
133-
n div (- + sd) * - + sd ≡⟨ cong (_* (- + sd)) (div-neg-is-neg-divℕ n sd) ⟩
134-
- (n divℕ sd) * - + sd ≡⟨ sym (neg-distribˡ-* (n divℕ sd) (- + sd)) ⟩
135-
- (n divℕ sd * - + sd) ≡⟨ neg-distribʳ-* (n divℕ sd) (- + sd) ⟩
136-
n divℕ sd * + sd ≤⟨ [n/ℕd]*d≤n n sd ⟩
137-
n ∎ where open ≤-Reasoning
138-
139-
n<s[n/ℕd]*d : ∀ n d {d≢0} → n ℤ.< suc ((n divℕ d) {d≢0}) ℤ.* ℤ.+ d
140-
n<s[n/ℕd]*d n sd@(ℕ.suc d) = begin-strict
141-
n ≡⟨ a≡a%ℕn+[a/ℕn]*n n sd ⟩
142-
ℤ.+ r ℤ.+ q ℤ.* + sd <⟨ +-monoˡ-< (q ℤ.* + sd) (ℤ.+<+ (n%ℕd<d n sd)) ⟩
143-
+ sd ℤ.+ q ℤ.* + sd ≡⟨ sym (suc-* q (+ sd)) ⟩
144-
suc (n divℕ ℕ.suc d) * + sd ∎ where
145-
open ≤-Reasoning; q = n divℕ sd; r = n modℕ sd
146-
147-
a≡a%n+[a/n]*n : ∀ a n {≢0} → a ≡ + (a mod n) {≢0} + (a div n) {≢0} * n
148-
a≡a%n+[a/n]*n n (+ ℕ.suc d) = begin
149-
let sd = ℕ.suc d; r = n modℕ sd; q = n divℕ sd; qsd = q * + sd in
150-
n ≡⟨ a≡a%ℕn+[a/ℕn]*n n sd ⟩
151-
+ r + qsd ≡⟨ cong (λ p → + r + p * + sd) (sym (div-pos-is-divℕ n sd)) ⟩
152-
+ r + n div + sd * + sd ∎ where open ≡-Reasoning
122+
0≤n⇒0≤n/d : ∀ n d .{{_ : NonZero d}} → +0 ℤ.≤ n → +0 ℤ.≤ d → +0 ℤ.≤ (n div d)
123+
0≤n⇒0≤n/d n (+ d) {{d≢0}} 0≤n (+≤+ 0≤d)
124+
rewrite div-pos-is-divℕ n d {{d≢0}}
125+
= 0≤n⇒0≤n/ℕd n d 0≤n
126+
127+
[n/d]*d≤n : ∀ n d .{{_ : NonZero d}} → (n div d) ℤ.* d ℤ.≤ n
128+
[n/d]*d≤n n (+ d) = begin
129+
n div + d * + d ≡⟨ cong (_* (+ d)) (div-pos-is-divℕ n d) ⟩
130+
n divℕ d * + d ≤⟨ [n/ℕd]*d≤n n d ⟩
131+
n ∎ where open ≤-Reasoning
132+
[n/d]*d≤n n -[1+ d-1 ] = begin let d = ℕ.suc d-1 in
133+
n div (- + d) * - + d ≡⟨ cong (_* (- + d)) (div-neg-is-neg-divℕ n d) ⟩
134+
- (n divℕ d) * - + d ≡⟨ sym (neg-distribˡ-* (n divℕ d) (- + d)) ⟩
135+
- (n divℕ d * - + d) ≡⟨ neg-distribʳ-* (n divℕ d) (- + d) ⟩
136+
n divℕ d * + d ≤⟨ [n/ℕd]*d≤n n d ⟩
137+
n ∎ where open ≤-Reasoning
138+
139+
n<s[n/ℕd]*d : ∀ n d .{{_ : ℕ.NonZero d}} → n ℤ.< suc (n divℕ d) ℤ.* ℤ.+ d
140+
n<s[n/ℕd]*d n d = begin-strict
141+
n ≡⟨ a≡a%ℕn+[a/ℕn]*n n d ⟩
142+
+ r + q * + d <⟨ +-monoˡ-< (q * + d) (ℤ.+<+ (n%ℕd<d n d)) ⟩
143+
+ d + q * + d ≡⟨ sym (suc-* q (+ d)) ⟩
144+
suc (n divℕ d) * + d ∎ where
145+
open ≤-Reasoning; q = n divℕ d; r = n modℕ d
146+
147+
a≡a%n+[a/n]*n : ∀ a n .{{_ : NonZero n}} → a ≡ + (a mod n) + (a div n) * n
148+
a≡a%n+[a/n]*n n (+ d) = begin
149+
let r = n modℕ d; q = n divℕ d; qsd = q * + d in
150+
n ≡⟨ a≡a%ℕn+[a/ℕn]*n n d ⟩
151+
+ r + qsd ≡⟨ cong (λ p → + r + p * + d) (sym (div-pos-is-divℕ n d)) ⟩
152+
+ r + n div + d * + d ∎ where open ≡-Reasoning
153153
a≡a%n+[a/n]*n n -[1+ d ] = begin
154154
let sd = ℕ.suc d; r = n modℕ sd; q = n divℕ sd; qsd = q * + sd in
155155
n ≡⟨ a≡a%ℕn+[a/ℕn]*n n sd ⟩

‎src/Data/Nat/Base.agda

+24-18
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,7 @@
1111

1212
module Data.Nat.Base where
1313

14-
open import Data.Bool.Base using (Bool; true; false)
15-
open import Data.Empty using (⊥)
16-
open import Data.Unit.Base using (⊤; tt)
14+
open import Data.Bool.Base using (Bool; true; false; T; not)
1715
open import Level using (0ℓ)
1816
open import Relation.Binary.Core using (Rel)
1917
open import Relation.Binary.PropositionalEquality.Core
@@ -78,30 +76,38 @@ a ≯ b = ¬ a > b
7876
------------------------------------------------------------------------
7977
-- Simple predicates
8078

81-
-- Defining `NonZero` in terms of `⊤` and `⊥` allows Agda to
82-
-- automatically infer nonZero-ness for any natural of the form
83-
-- `suc n`. Consequently in many circumstances this eliminates the need
84-
-- to explicitly pass a proof when the NonZero argument is either an
85-
-- implicit or an instance argument.
86-
--
87-
-- It could alternatively be defined using a datatype with an instance
88-
-- constructor but then it would not be inferrable when passed as an
89-
-- implicit argument.
79+
-- Defining `NonZero` in terms of `T` and therefore ultimately `⊤` and
80+
-- `⊥` allows Agda to automatically infer nonZero-ness for any natural
81+
-- of the form `suc n`. Consequently in many circumstances this
82+
-- eliminates the need to explicitly pass a proof when the NonZero
83+
-- argument is either an implicit or an instance argument.
9084
--
9185
-- See `Data.Nat.DivMod` for an example.
9286

93-
NonZero : ℕ → Set
94-
NonZero zero = ⊥
95-
NonZero (suc x) = ⊤
87+
record NonZero (n : ℕ) : Set where
88+
field
89+
nonZero : T (not (n ≡ᵇ 0))
90+
91+
instance
92+
nonZero : ∀ {n} → NonZero (suc n)
93+
nonZero = _
9694

9795
-- Constructors
9896

9997
≢-nonZero : ∀ {n} → n ≢ 0 → NonZero n
100-
≢-nonZero {zero} 0≢0 = 0≢0 refl
101-
≢-nonZero {suc n} n≢0 = tt
98+
≢-nonZero {zero} 0≢0 = contradiction refl 0≢0
99+
≢-nonZero {suc n} n≢0 = _
102100

103101
>-nonZero : ∀ {n} → n > 0 → NonZero n
104-
>-nonZero (s≤s 0<n) = tt
102+
>-nonZero (s≤s 0<n) = _
103+
104+
-- Destructors
105+
106+
≢-nonZero⁻¹ : ∀ {n} → .(NonZero n) → n ≢ 0
107+
≢-nonZero⁻¹ {suc n} _ ()
108+
109+
>-nonZero⁻¹ : ∀ {n} → .(NonZero n) → n > 0
110+
>-nonZero⁻¹ {suc n} _ = s≤s z≤n
105111

106112
------------------------------------------------------------------------
107113
-- Arithmetic

0 commit comments

Comments
 (0)