1
------------------------------------------------------------------------
2
-- A bunch of properties about natural number operations
3
------------------------------------------------------------------------
5
-- See README.Nat for some examples showing how this module can be
8
module Data.Nat.Properties where
10
open import Data.Nat as Nat
12
renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩'_)
13
open import Relation.Binary
14
open DecTotalOrder Nat.decTotalOrder using () renaming (refl to ≤-refl)
15
open import Data.Function
17
open import Algebra.Structures
18
open import Relation.Nullary
19
open import Relation.Binary.PropositionalEquality as PropEq
20
using (_≡_; _≢_; refl; sym; cong; cong₂)
21
open PropEq.≡-Reasoning
22
import Algebra.FunctionProperties as P; open P _≡_
23
open import Data.Product
25
------------------------------------------------------------------------
26
-- (ℕ, +, *, 0, 1) is a commutative semiring
30
+-assoc : Associative _+_
31
+-assoc zero _ _ = refl
32
+-assoc (suc m) n o = cong suc $ +-assoc m n o
34
+-identity : Identity 0 _+_
35
+-identity = (λ _ → refl) , n+0≡n
37
n+0≡n : RightIdentity 0 _+_
39
n+0≡n (suc n) = cong suc $ n+0≡n n
41
m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
42
m+1+n≡1+m+n zero n = refl
43
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)
45
+-comm : Commutative _+_
46
+-comm zero n = sym $ proj₂ +-identity n
52
≡⟨ cong suc (+-comm m n) ⟩
54
≡⟨ sym (m+1+n≡1+m+n n m) ⟩
58
m*1+n≡m+mn : ∀ m n → m * suc n ≡ m + m * n
59
m*1+n≡m+mn zero n = refl
60
m*1+n≡m+mn (suc m) n =
65
≡⟨ cong (λ x → suc n + x) (m*1+n≡m+mn m n) ⟩
69
≡⟨ cong suc (sym $ +-assoc n m (m * n)) ⟩
71
≡⟨ cong (λ x → suc (x + m * n)) (+-comm n m) ⟩
73
≡⟨ cong suc (+-assoc m n (m * n)) ⟩
80
*-zero = (λ _ → refl) , n*0≡0
82
n*0≡0 : RightZero 0 _*_
84
n*0≡0 (suc n) = n*0≡0 n
86
*-comm : Commutative _*_
87
*-comm zero n = sym $ proj₂ *-zero n
93
≡⟨ cong (λ x → n + x) (*-comm m n) ⟩
95
≡⟨ sym (m*1+n≡m+mn n m) ⟩
99
distrib-*-+ : _*_ DistributesOver _+_
100
distrib-*-+ = distˡ , distʳ
102
distˡ : _*_ DistributesOverˡ _+_
103
distˡ zero n o = refl
108
(n + o) + m * (n + o)
109
≡⟨ cong (λ x → (n + o) + x) (distˡ m n o) ⟩
110
(n + o) + (m * n + m * o)
111
≡⟨ sym $ +-assoc (n + o) (m * n) (m * o) ⟩
112
((n + o) + m * n) + m * o
113
≡⟨ cong (λ x → x + (m * o)) $ +-assoc n o (m * n) ⟩
114
(n + (o + m * n)) + m * o
115
≡⟨ cong (λ x → (n + x) + m * o) $ +-comm o (m * n) ⟩
116
(n + (m * n + o)) + m * o
117
≡⟨ cong (λ x → x + (m * o)) $ sym $ +-assoc n (m * n) o ⟩
118
((n + m * n) + o) + m * o
119
≡⟨ +-assoc (n + m * n) o (m * o) ⟩
120
(n + m * n) + (o + m * o)
122
suc m * n + suc m * o
125
distʳ : _*_ DistributesOverʳ _+_
129
≡⟨ *-comm (n + o) m ⟩
133
≡⟨ cong₂ _+_ (*-comm m n) (*-comm m o) ⟩
137
*-assoc : Associative _*_
138
*-assoc zero n o = refl
139
*-assoc (suc m) n o =
144
≡⟨ proj₂ distrib-*-+ o n (m * n) ⟩
146
≡⟨ cong (λ x → n * o + x) $ *-assoc m n o ⟩
152
*-identity : Identity 1 _*_
153
*-identity = proj₂ +-identity , n*1≡n
155
n*1≡n : RightIdentity 1 _*_
163
≡⟨ proj₂ +-identity n ⟩
167
isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ 0 1
168
isCommutativeSemiring = record
169
{ isSemiring = record
170
{ isSemiringWithoutAnnihilatingZero = record
171
{ +-isCommutativeMonoid = record
173
{ isSemigroup = record
174
{ isEquivalence = PropEq.isEquivalence
178
; identity = +-identity
182
; *-isMonoid = record
183
{ isSemigroup = record
184
{ isEquivalence = PropEq.isEquivalence
188
; identity = *-identity
190
; distrib = distrib-*-+
197
commutativeSemiring : CommutativeSemiring
198
commutativeSemiring = record
203
; isCommutativeSemiring = isCommutativeSemiring
206
import Algebra.RingSolver.Simple as Solver
207
import Algebra.RingSolver.AlmostCommutativeRing as ACR
208
module SemiringSolver =
209
Solver (ACR.fromCommutativeSemiring commutativeSemiring)
211
------------------------------------------------------------------------
212
-- (ℕ, ⊔, ⊓, 0) is a commutative semiring without one
216
⊔-assoc : Associative _⊔_
217
⊔-assoc zero _ _ = refl
218
⊔-assoc (suc m) zero o = refl
219
⊔-assoc (suc m) (suc n) zero = refl
220
⊔-assoc (suc m) (suc n) (suc o) = cong suc $ ⊔-assoc m n o
222
⊔-identity : Identity 0 _⊔_
223
⊔-identity = (λ _ → refl) , n⊔0≡n
225
n⊔0≡n : RightIdentity 0 _⊔_
229
⊔-comm : Commutative _⊔_
230
⊔-comm zero n = sym $ proj₂ ⊔-identity n
231
⊔-comm (suc m) zero = refl
232
⊔-comm (suc m) (suc n) =
237
≡⟨ cong suc (⊔-comm m n) ⟩
243
⊓-assoc : Associative _⊓_
244
⊓-assoc zero _ _ = refl
245
⊓-assoc (suc m) zero o = refl
246
⊓-assoc (suc m) (suc n) zero = refl
247
⊓-assoc (suc m) (suc n) (suc o) = cong suc $ ⊓-assoc m n o
250
⊓-zero = (λ _ → refl) , n⊓0≡0
252
n⊓0≡0 : RightZero 0 _⊓_
256
⊓-comm : Commutative _⊓_
257
⊓-comm zero n = sym $ proj₂ ⊓-zero n
258
⊓-comm (suc m) zero = refl
259
⊓-comm (suc m) (suc n) =
264
≡⟨ cong suc (⊓-comm m n) ⟩
270
distrib-⊓-⊔ : _⊓_ DistributesOver _⊔_
271
distrib-⊓-⊔ = (distribˡ-⊓-⊔ , distribʳ-⊓-⊔)
273
distribʳ-⊓-⊔ : _⊓_ DistributesOverʳ _⊔_
274
distribʳ-⊓-⊔ (suc m) (suc n) (suc o) = cong suc $ distribʳ-⊓-⊔ m n o
275
distribʳ-⊓-⊔ (suc m) (suc n) zero = cong suc $ refl
276
distribʳ-⊓-⊔ (suc m) zero o = refl
277
distribʳ-⊓-⊔ zero n o = begin
278
(n ⊔ o) ⊓ 0 ≡⟨ ⊓-comm (n ⊔ o) 0 ⟩
279
0 ⊓ (n ⊔ o) ≡⟨ refl ⟩
280
0 ⊓ n ⊔ 0 ⊓ o ≡⟨ ⊓-comm 0 n ⟨ cong₂ _⊔_ ⟩ ⊓-comm 0 o ⟩
283
distribˡ-⊓-⊔ : _⊓_ DistributesOverˡ _⊔_
284
distribˡ-⊓-⊔ m n o = begin
285
m ⊓ (n ⊔ o) ≡⟨ ⊓-comm m _ ⟩
286
(n ⊔ o) ⊓ m ≡⟨ distribʳ-⊓-⊔ m n o ⟩
287
n ⊓ m ⊔ o ⊓ m ≡⟨ ⊓-comm n m ⟨ cong₂ _⊔_ ⟩ ⊓-comm o m ⟩
290
⊔-⊓-0-isCommutativeSemiringWithoutOne
291
: IsCommutativeSemiringWithoutOne _≡_ _⊔_ _⊓_ 0
292
⊔-⊓-0-isCommutativeSemiringWithoutOne = record
293
{ isSemiringWithoutOne = record
294
{ +-isCommutativeMonoid = record
296
{ isSemigroup = record
297
{ isEquivalence = PropEq.isEquivalence
301
; identity = ⊔-identity
305
; *-isSemigroup = record
306
{ isEquivalence = PropEq.isEquivalence
310
; distrib = distrib-⊓-⊔
316
⊔-⊓-0-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne
317
⊔-⊓-0-commutativeSemiringWithoutOne = record
321
; isCommutativeSemiringWithoutOne =
322
⊔-⊓-0-isCommutativeSemiringWithoutOne
325
------------------------------------------------------------------------
326
-- (ℕ, ⊓, ⊔) is a lattice
330
absorptive-⊓-⊔ : Absorptive _⊓_ _⊔_
331
absorptive-⊓-⊔ = abs-⊓-⊔ , abs-⊔-⊓
333
abs-⊔-⊓ : _⊔_ Absorbs _⊓_
334
abs-⊔-⊓ zero n = refl
335
abs-⊔-⊓ (suc m) zero = refl
336
abs-⊔-⊓ (suc m) (suc n) = cong suc $ abs-⊔-⊓ m n
338
abs-⊓-⊔ : _⊓_ Absorbs _⊔_
339
abs-⊓-⊔ zero n = refl
340
abs-⊓-⊔ (suc m) (suc n) = cong suc $ abs-⊓-⊔ m n
341
abs-⊓-⊔ (suc m) zero = cong suc $
344
≡⟨ cong (_⊓_ m) $ sym $ proj₂ ⊔-identity m ⟩
350
isDistributiveLattice : IsDistributiveLattice _≡_ _⊓_ _⊔_
351
isDistributiveLattice = record
353
{ isEquivalence = PropEq.isEquivalence
360
; absorptive = absorptive-⊓-⊔
362
; ∨-∧-distribʳ = proj₂ distrib-⊓-⊔
365
distributiveLattice : DistributiveLattice
366
distributiveLattice = record
369
; isDistributiveLattice = isDistributiveLattice
372
------------------------------------------------------------------------
373
-- Converting between ≤ and ≤′
375
≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
377
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)
380
≤′⇒≤ ≤′-refl = ≤-refl
381
≤′⇒≤ (≤′-step m≤′n) = ≤-step (≤′⇒≤ m≤′n)
383
z≤′n : ∀ {n} → zero ≤′ n
384
z≤′n {zero} = ≤′-refl
385
z≤′n {suc n} = ≤′-step z≤′n
387
s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
388
s≤′s ≤′-refl = ≤′-refl
389
s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
393
≤⇒≤′ (s≤s m≤n) = s≤′s (≤⇒≤′ m≤n)
395
------------------------------------------------------------------------
396
-- Various order-related properties
398
≤-steps : ∀ {m n} k → m ≤ n → m ≤ k + n
399
≤-steps zero m≤n = m≤n
400
≤-steps (suc k) m≤n = ≤-step (≤-steps k m≤n)
402
m≤m+n : ∀ m n → m ≤ m + n
404
m≤m+n (suc m) n = s≤s (m≤m+n m n)
406
m≤′m+n : ∀ m n → m ≤′ m + n
407
m≤′m+n m n = ≤⇒≤′ (m≤m+n m n)
409
n≤′m+n : ∀ m n → n ≤′ m + n
410
n≤′m+n zero n = ≤′-refl
411
n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)
413
n≤m+n : ∀ m n → n ≤ m + n
414
n≤m+n m n = ≤′⇒≤ (n≤′m+n m n)
416
n≤1+n : ∀ n → n ≤ 1 + n
417
n≤1+n _ = ≤-step ≤-refl
419
1+n≰n : ∀ {n} → ¬ 1 + n ≤ n
420
1+n≰n (s≤s le) = 1+n≰n le
422
≤pred⇒≤ : ∀ m n → m ≤ pred n → m ≤ n
423
≤pred⇒≤ m zero le = le
424
≤pred⇒≤ m (suc n) le = ≤-step le
426
≤⇒pred≤ : ∀ m n → m ≤ n → pred m ≤ n
427
≤⇒pred≤ zero n le = le
428
≤⇒pred≤ (suc m) n le = start
433
¬i+1+j≤i : ∀ i {j} → ¬ i + suc j ≤ i
435
¬i+1+j≤i (suc i) le = ¬i+1+j≤i i (≤-pred le)
437
n∸m≤n : ∀ m n → n ∸ m ≤ n
438
n∸m≤n zero n = ≤-refl
439
n∸m≤n (suc m) zero = ≤-refl
440
n∸m≤n (suc m) (suc n) = start
445
n≤m+n∸m : ∀ m n → n ≤ m + (n ∸ m)
447
n≤m+n∸m zero (suc n) = ≤-refl
448
n≤m+n∸m (suc m) (suc n) = s≤s (n≤m+n∸m m n)
450
m⊓n≤m : ∀ m n → m ⊓ n ≤ m
452
m⊓n≤m (suc m) zero = z≤n
453
m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n
455
m≤m⊔n : ∀ m n → m ≤ m ⊔ n
457
m≤m⊔n (suc m) zero = ≤-refl
458
m≤m⊔n (suc m) (suc n) = s≤s $ m≤m⊔n m n
460
⌈n/2⌉≤′n : ∀ n → ⌈ n /2⌉ ≤′ n
461
⌈n/2⌉≤′n zero = ≤′-refl
462
⌈n/2⌉≤′n (suc zero) = ≤′-refl
463
⌈n/2⌉≤′n (suc (suc n)) = s≤′s (≤′-step (⌈n/2⌉≤′n n))
465
⌊n/2⌋≤′n : ∀ n → ⌊ n /2⌋ ≤′ n
466
⌊n/2⌋≤′n zero = ≤′-refl
467
⌊n/2⌋≤′n (suc n) = ≤′-step (⌈n/2⌉≤′n n)
469
<-trans : Transitive _<_
470
<-trans {i} {j} {k} i<j j<k = start
476
------------------------------------------------------------------------
477
-- (ℕ, _≡_, _<_) is a strict total order
479
m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
481
m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)
483
strictTotalOrder : StrictTotalOrder _ _ _
484
strictTotalOrder = record
488
; isStrictTotalOrder = record
489
{ isEquivalence = PropEq.isEquivalence
492
; <-resp-≈ = PropEq.resp₂ _<_
496
2+m+n≰m : ∀ {m n} → ¬ 2 + (m + n) ≤ m
497
2+m+n≰m (s≤s le) = 2+m+n≰m le
499
cmp : Trichotomous _≡_ _<_
500
cmp m n with compare m n
501
cmp .m .(suc (m + k)) | less m k = tri< (m≤m+n (suc m) k) (m≢1+m+n _) 2+m+n≰m
502
cmp .n .n | equal n = tri≈ 1+n≰n refl 1+n≰n
503
cmp .(suc (n + k)) .n | greater n k = tri> 2+m+n≰m (m≢1+m+n _ ∘ sym) (m≤m+n (suc n) k)
505
------------------------------------------------------------------------
506
-- Miscellaneous other properties
508
0∸n≡0 : LeftZero zero _∸_
512
∸-+-assoc : ∀ m n o → (m ∸ n) ∸ o ≡ m ∸ (n + o)
513
∸-+-assoc m n zero = cong (_∸_ m) (sym $ proj₂ +-identity n)
514
∸-+-assoc zero zero (suc o) = refl
515
∸-+-assoc zero (suc n) (suc o) = refl
516
∸-+-assoc (suc m) zero (suc o) = refl
517
∸-+-assoc (suc m) (suc n) (suc o) = ∸-+-assoc m n (suc o)
519
m+n∸n≡m : ∀ m n → (m + n) ∸ n ≡ m
520
m+n∸n≡m m zero = proj₂ +-identity m
521
m+n∸n≡m zero (suc n) = m+n∸n≡m zero n
522
m+n∸n≡m (suc m) (suc n) = begin
524
≡⟨ cong (λ x → x ∸ n) (m+1+n≡1+m+n m n) ⟩
526
≡⟨ m+n∸n≡m (suc m) n ⟩
530
m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
531
m⊓n+n∸m≡n zero n = refl
532
m⊓n+n∸m≡n (suc m) zero = refl
533
m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
535
[m∸n]⊓[n∸m]≡0 : ∀ m n → (m ∸ n) ⊓ (n ∸ m) ≡ 0
536
[m∸n]⊓[n∸m]≡0 zero zero = refl
537
[m∸n]⊓[n∸m]≡0 zero (suc n) = refl
538
[m∸n]⊓[n∸m]≡0 (suc m) zero = refl
539
[m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n
541
-- TODO: Can this proof be simplified? An automatic solver which can
542
-- handle ∸ would be nice...
544
i∸k∸j+j∸k≡i+j∸k : ∀ i j k → i ∸ (k ∸ j) + (j ∸ k) ≡ i + j ∸ k
545
i∸k∸j+j∸k≡i+j∸k zero j k = begin
546
0 ∸ (k ∸ j) + (j ∸ k)
547
≡⟨ cong (λ x → x + (j ∸ k)) (0∸n≡0 (k ∸ j)) ⟩
552
i∸k∸j+j∸k≡i+j∸k (suc i) j zero = begin
554
≡⟨ cong (λ x → suc i ∸ x + j) (0∸n≡0 j) ⟩
559
i∸k∸j+j∸k≡i+j∸k (suc i) zero (suc k) = begin
561
≡⟨ proj₂ +-identity _ ⟩
563
≡⟨ cong (λ x → x ∸ k) (sym (proj₂ +-identity _)) ⟩
566
i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin
567
suc i ∸ (k ∸ j) + (j ∸ k)
568
≡⟨ i∸k∸j+j∸k≡i+j∸k (suc i) j k ⟩
570
≡⟨ cong (λ x → x ∸ k)
571
(sym (m+1+n≡1+m+n i j)) ⟩
575
m+n∸m≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
577
m+n∸m≡n (s≤s m≤n) = cong suc $ m+n∸m≡n m≤n
579
i+j≡0⇒i≡0 : ∀ i {j} → i + j ≡ 0 → i ≡ 0
580
i+j≡0⇒i≡0 zero eq = refl
583
i+j≡0⇒j≡0 : ∀ i {j} → i + j ≡ 0 → j ≡ 0
584
i+j≡0⇒j≡0 i {j} i+j≡0 = i+j≡0⇒i≡0 j $ begin
592
i*j≡1⇒i≡1 : ∀ i j → i * j ≡ 1 → i ≡ 1
593
i*j≡1⇒i≡1 (suc zero) j _ = refl
595
i*j≡1⇒i≡1 (suc (suc i)) (suc (suc j)) ()
596
i*j≡1⇒i≡1 (suc (suc i)) (suc zero) ()
597
i*j≡1⇒i≡1 (suc (suc i)) zero eq with begin
603
i*j≡1⇒j≡1 : ∀ i j → i * j ≡ 1 → j ≡ 1
604
i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (begin
605
j * i ≡⟨ *-comm j i ⟩
609
cancel-+-left : ∀ i {j k} → i + j ≡ i + k → j ≡ k
610
cancel-+-left zero eq = eq
611
cancel-+-left (suc i) eq = cancel-+-left i (cong pred eq)
613
cancel-*-right : ∀ i j {k} → i * suc k ≡ j * suc k → i ≡ j
614
cancel-*-right zero zero eq = refl
615
cancel-*-right zero (suc j) ()
616
cancel-*-right (suc i) zero ()
617
cancel-*-right (suc i) (suc j) {k} eq =
618
cong suc (cancel-*-right i j (cancel-+-left (suc k) eq))
622
i * m ≡ j * m + n → (i ∸ j) * m ≡ n
623
im≡jm+n⇒[i∸j]m≡n i zero m n eq = eq
624
im≡jm+n⇒[i∸j]m≡n zero (suc j) m n eq =
625
sym $ i+j≡0⇒j≡0 (m + j * m) $ sym eq
626
im≡jm+n⇒[i∸j]m≡n (suc i) (suc j) m n eq =
627
im≡jm+n⇒[i∸j]m≡n i j m n (cancel-+-left m eq')
633
≡⟨ +-assoc m (j * m) n ⟩
637
i+1+j≢i : ∀ i {j} → i + suc j ≢ i
638
i+1+j≢i i eq = ¬i+1+j≤i i (reflexive eq)
639
where open DecTotalOrder decTotalOrder
641
⌊n/2⌋-mono : ⌊_/2⌋ Preserves _≤_ ⟶ _≤_
643
⌊n/2⌋-mono (s≤s z≤n) = z≤n
644
⌊n/2⌋-mono (s≤s (s≤s m≤n)) = s≤s (⌊n/2⌋-mono m≤n)
646
⌈n/2⌉-mono : ⌈_/2⌉ Preserves _≤_ ⟶ _≤_
647
⌈n/2⌉-mono m≤n = ⌊n/2⌋-mono (s≤s m≤n)
649
pred-mono : pred Preserves _≤_ ⟶ _≤_
651
pred-mono (s≤s le) = le
653
_+-mono_ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
654
_+-mono_ {zero} {m₂} {n₁} {n₂} z≤n n₁≤n₂ = start
658
s≤s m₁≤m₂ +-mono n₁≤n₂ = s≤s (m₁≤m₂ +-mono n₁≤n₂)
660
_*-mono_ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
661
z≤n *-mono n₁≤n₂ = z≤n
662
s≤s m₁≤m₂ *-mono n₁≤n₂ = n₁≤n₂ +-mono (m₁≤m₂ *-mono n₁≤n₂)
added
removed
src/Data/Nat/Properties.agda
