← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Data/Nat/Properties.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat/Properties.agda
23
23
open PropEq.≡-Reasoning
24
24
import Algebra.FunctionProperties as P; open P (_≡_ {A = ℕ})
25
25
open import Data.Product
 
26
open import Data.Sum
26
27
 
27
28
------------------------------------------------------------------------
28
29
-- (ℕ, +, *, 0, 1) is a commutative semiring
164
165
import Algebra.RingSolver.Simple as Solver
165
166
import Algebra.RingSolver.AlmostCommutativeRing as ACR
166
167
module SemiringSolver =
167
 
  Solver (ACR.fromCommutativeSemiring commutativeSemiring)
 
168
  Solver (ACR.fromCommutativeSemiring commutativeSemiring) _≟_
168
169
 
169
170
------------------------------------------------------------------------
170
171
-- (ℕ, ⊔, ⊓, 0) is a commutative semiring without one
471
472
0∸n≡0 zero    = refl
472
473
0∸n≡0 (suc _) = refl
473
474
 
 
475
n∸n≡0 : ∀ n → n ∸ n ≡ 0
 
476
n∸n≡0 zero    = refl
 
477
n∸n≡0 (suc n) = n∸n≡0 n
 
478
 
474
479
∸-+-assoc : ∀ m n o → (m ∸ n) ∸ o ≡ m ∸ (n + o)
475
480
∸-+-assoc m       n       zero    = cong (_∸_ m) (sym $ proj₂ +-identity n)
476
481
∸-+-assoc zero    zero    (suc o) = refl
478
483
∸-+-assoc (suc m) zero    (suc o) = refl
479
484
∸-+-assoc (suc m) (suc n) (suc o) = ∸-+-assoc m n (suc o)
480
485
 
 
486
+-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
 
487
+-∸-assoc m (z≤n {n = n})             = begin m + n ∎
 
488
+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin
 
489
  (m + suc n) ∸ suc o  ≡⟨ cong (λ n → n ∸ suc o) (m+1+n≡1+m+n m n) ⟩
 
490
  suc (m + n) ∸ suc o  ≡⟨ refl ⟩
 
491
  (m + n) ∸ o          ≡⟨ +-∸-assoc m o≤n ⟩
 
492
  m + (n ∸ o)          ∎
 
493
 
481
494
m+n∸n≡m : ∀ m n → (m + n) ∸ n ≡ m
482
 
m+n∸n≡m m       zero    = proj₂ +-identity m
483
 
m+n∸n≡m zero    (suc n) = m+n∸n≡m zero n
484
 
m+n∸n≡m (suc m) (suc n) = begin
485
 
  m + suc n ∸ n
486
 
                 ≡⟨ cong (λ x → x ∸ n) (m+1+n≡1+m+n m n) ⟩
487
 
  suc m + n ∸ n
488
 
                 ≡⟨ m+n∸n≡m (suc m) n ⟩
489
 
  suc m
490
 
                 ∎
 
495
m+n∸n≡m m n = begin
 
496
  (m + n) ∸ n  ≡⟨ +-∸-assoc m (≤-refl {x = n}) ⟩
 
497
  m + (n ∸ n)  ≡⟨ cong (_+_ m) (n∸n≡0 n) ⟩
 
498
  m + 0        ≡⟨ proj₂ +-identity m ⟩
 
499
  m            ∎
 
500
 
 
501
m+n∸m≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
 
502
m+n∸m≡n {m} {n} m≤n = begin
 
503
  m + (n ∸ m)  ≡⟨ sym $ +-∸-assoc m m≤n ⟩
 
504
  (m + n) ∸ m  ≡⟨ cong (λ n → n ∸ m) (+-comm m n) ⟩
 
505
  (n + m) ∸ m  ≡⟨ m+n∸n≡m n m ⟩
 
506
  n            ∎
491
507
 
492
508
m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
493
509
m⊓n+n∸m≡n zero    n       = refl
538
554
  i + suc j ∸ k
539
555
                             ∎
540
556
 
541
 
m+n∸m≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
542
 
m+n∸m≡n z≤n       = refl
543
 
m+n∸m≡n (s≤s m≤n) = cong suc $ m+n∸m≡n m≤n
544
 
 
545
557
i+j≡0⇒i≡0 : ∀ i {j} → i + j ≡ 0 → i ≡ 0
546
558
i+j≡0⇒i≡0 zero    eq = refl
547
559
i+j≡0⇒i≡0 (suc i) ()
555
567
  0
556
568
    ∎
557
569
 
 
570
i*j≡0⇒i≡0∨j≡0 : ∀ i {j} → i * j ≡ 0 → i ≡ 0 ⊎ j ≡ 0
 
571
i*j≡0⇒i≡0∨j≡0 zero    {j}     eq = inj₁ refl
 
572
i*j≡0⇒i≡0∨j≡0 (suc i) {zero}  eq = inj₂ refl
 
573
i*j≡0⇒i≡0∨j≡0 (suc i) {suc j} ()
 
574
 
558
575
i*j≡1⇒i≡1 : ∀ i j → i * j ≡ 1 → i ≡ 1
559
576
i*j≡1⇒i≡1 (suc zero)    j             _  = refl
560
577
i*j≡1⇒i≡1 zero          j             ()
640
657
_*-mono_ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
641
658
z≤n       *-mono n₁≤n₂ = z≤n
642
659
s≤s m₁≤m₂ *-mono n₁≤n₂ = n₁≤n₂ +-mono (m₁≤m₂ *-mono n₁≤n₂)
 
660
 
 
661
∸-mono : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
 
662
∸-mono           z≤n         (s≤s n₁≥n₂)    = z≤n
 
663
∸-mono           (s≤s m₁≤m₂) (s≤s n₁≥n₂)    = ∸-mono m₁≤m₂ n₁≥n₂
 
664
∸-mono {m₁} {m₂} m₁≤m₂       (z≤n {n = n₁}) = start
 
665
  m₁ ∸ n₁  ≤⟨ n∸m≤n n₁ m₁ ⟩
 
666
  m₁       ≤⟨ m₁≤m₂ ⟩
 
667
  m₂       □