summaryrefslogtreecommitdiff
path: root/src/Data/Nat
diff options
context:
space:
mode:
authorSean Whitton <spwhitton@spwhitton.name>2018-11-23 17:29:46 -0700
committerSean Whitton <spwhitton@spwhitton.name>2018-11-23 17:29:46 -0700
commit5a91775bd7c909bbaf3b3c8ee964136961a5146d (patch)
treecea89f085c1382f1567ff71a30b6f953708dc6a9 /src/Data/Nat
parent5d2b156377dce5bdca65b14639306eaed3ac3a92 (diff)
parenta19b25a865b2000bbd3acd909f5951a5407c1eec (diff)
Merge tag 'upstream/0.17'
Upstream version 0.17 # gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST # gpg: using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240 # gpg: issuer "spwhitton@spwhitton.name" # gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate] # Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4 753F 0F56 D055 3B6D 411B # Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC 248B 695B 7AE4 BF06 6240
Diffstat (limited to 'src/Data/Nat')
-rw-r--r--src/Data/Nat/Base.agda144
-rw-r--r--src/Data/Nat/Coprimality.agda53
-rw-r--r--src/Data/Nat/DivMod.agda203
-rw-r--r--src/Data/Nat/DivMod/Core.agda102
-rw-r--r--src/Data/Nat/DivMod/Unsafe.agda45
-rw-r--r--src/Data/Nat/Divisibility.agda207
-rw-r--r--src/Data/Nat/GCD.agda42
-rw-r--r--src/Data/Nat/GCD/Lemmas.agda76
-rw-r--r--src/Data/Nat/InfinitelyOften.agda41
-rw-r--r--src/Data/Nat/LCM.agda11
-rw-r--r--src/Data/Nat/Literals.agda17
-rw-r--r--src/Data/Nat/Primality.agda22
-rw-r--r--src/Data/Nat/Properties.agda763
-rw-r--r--src/Data/Nat/Solver.agda21
-rw-r--r--src/Data/Nat/Unsafe.agda13
15 files changed, 1246 insertions, 514 deletions
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 52367e1..2136fcf 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -6,92 +6,56 @@
module Data.Nat.Base where
-import Level using (zero)
-open import Function using (_∘_)
+open import Level using (0ℓ)
+open import Function using (_∘_; flip)
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.Core
-import Relation.Binary.PropositionalEquality.TrustMe as TrustMe
-open import Relation.Nullary using (¬_; Dec; yes; no)
-
-infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_)
------------------------------------------------------------------------
-- The types
open import Agda.Builtin.Nat public
- using ( zero; suc; _+_; _*_ )
- renaming ( Nat to ℕ
- ; _-_ to _∸_ )
+ using (zero; suc) renaming (Nat to ℕ)
-data _≤_ : Rel ℕ Level.zero where
+------------------------------------------------------------------------
+-- Standard ordering relations
+
+infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_
+
+data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
-_<_ : Rel ℕ Level.zero
+_<_ : Rel ℕ 0ℓ
m < n = suc m ≤ n
-_≥_ : Rel ℕ Level.zero
+_≥_ : Rel ℕ 0ℓ
m ≥ n = n ≤ m
-_>_ : Rel ℕ Level.zero
+_>_ : Rel ℕ 0ℓ
m > n = n < m
-_≰_ : Rel ℕ Level.zero
+_≰_ : Rel ℕ 0ℓ
a ≰ b = ¬ a ≤ b
-_≮_ : Rel ℕ Level.zero
+_≮_ : Rel ℕ 0ℓ
a ≮ b = ¬ a < b
-_≱_ : Rel ℕ Level.zero
+_≱_ : Rel ℕ 0ℓ
a ≱ b = ¬ a ≥ b
-_≯_ : Rel ℕ Level.zero
+_≯_ : Rel ℕ 0ℓ
a ≯ b = ¬ a > b
--- The following, alternative definition of _≤_ is more suitable for
--- well-founded induction (see Induction.Nat).
-
-infix 4 _≤′_ _<′_ _≥′_ _>′_
-
-data _≤′_ (m : ℕ) : ℕ → Set where
- ≤′-refl : m ≤′ m
- ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
-
-_<′_ : Rel ℕ Level.zero
-m <′ n = suc m ≤′ n
-
-_≥′_ : Rel ℕ Level.zero
-m ≥′ n = n ≤′ m
-
-_>′_ : Rel ℕ Level.zero
-m >′ n = n <′ m
-
--- Another alternative definition of _≤_.
-
-record _≤″_ (m n : ℕ) : Set where
- constructor less-than-or-equal
- field
- {k} : ℕ
- proof : m + k ≡ n
-
-infix 4 _≤″_ _<″_ _≥″_ _>″_
-
-_<″_ : Rel ℕ Level.zero
-m <″ n = suc m ≤″ n
-
-_≥″_ : Rel ℕ Level.zero
-m ≥″ n = n ≤″ m
-
-_>″_ : Rel ℕ Level.zero
-m >″ n = n <″ m
-
-erase : ∀ {m n} → m ≤″ n → m ≤″ n
-erase (less-than-or-equal eq) = less-than-or-equal (TrustMe.erase eq)
-
------------------------------------------------------------------------
-- Arithmetic
+open import Agda.Builtin.Nat public
+ using (_+_; _*_ ) renaming (_-_ to _∸_)
+
pred : ℕ → ℕ
pred zero = zero
pred (suc n) = n
@@ -137,33 +101,57 @@ _^_ : ℕ → ℕ → ℕ
x ^ zero = 1
x ^ suc n = x * x ^ n
+-- Distance
+
+∣_-_∣ : ℕ → ℕ → ℕ
+∣ zero - y ∣ = y
+∣ x - zero ∣ = x
+∣ suc x - suc y ∣ = ∣ x - y ∣
+
------------------------------------------------------------------------
--- Queries
+-- The following, alternative definition of _≤_ is more suitable for
+-- well-founded induction (see Induction.Nat).
-infix 4 _≟_ _≤?_
+infix 4 _≤′_ _<′_ _≥′_ _>′_
-_≟_ : Decidable {A = ℕ} _≡_
-zero ≟ zero = yes refl
-suc m ≟ suc n with m ≟ n
-suc m ≟ suc .m | yes refl = yes refl
-suc m ≟ suc n | no prf = no (prf ∘ (λ p → subst (λ x → m ≡ pred x) p refl))
-zero ≟ suc n = no λ()
-suc m ≟ zero = no λ()
+data _≤′_ (m : ℕ) : ℕ → Set where
+ ≤′-refl : m ≤′ m
+ ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n
-≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
-≤-pred (s≤s m≤n) = m≤n
+_<′_ : Rel ℕ 0ℓ
+m <′ n = suc m ≤′ n
-_≤?_ : Decidable _≤_
-zero ≤? _ = yes z≤n
-suc m ≤? zero = no λ()
-suc m ≤? suc n with m ≤? n
-... | yes m≤n = yes (s≤s m≤n)
-... | no m≰n = no (m≰n ∘ ≤-pred)
+_≥′_ : Rel ℕ 0ℓ
+m ≥′ n = n ≤′ m
+
+_>′_ : Rel ℕ 0ℓ
+m >′ n = n <′ m
+------------------------------------------------------------------------
+-- Another alternative definition of _≤_.
+
+record _≤″_ (m n : ℕ) : Set where
+ constructor less-than-or-equal
+ field
+ {k} : ℕ
+ proof : m + k ≡ n
+
+infix 4 _≤″_ _<″_ _≥″_ _>″_
+
+_<″_ : Rel ℕ 0ℓ
+m <″ n = suc m ≤″ n
+
+_≥″_ : Rel ℕ 0ℓ
+m ≥″ n = n ≤″ m
+
+_>″_ : Rel ℕ 0ℓ
+m >″ n = n <″ m
+
+------------------------------------------------------------------------
-- A comparison view. Taken from "View from the left"
-- (McBride/McKinna); details may differ.
-data Ordering : Rel ℕ Level.zero where
+data Ordering : Rel ℕ 0ℓ where
less : ∀ m k → Ordering m (suc (m + k))
equal : ∀ m → Ordering m m
greater : ∀ m k → Ordering (suc (m + k)) m
@@ -173,6 +161,6 @@ compare zero zero = equal zero
compare (suc m) zero = greater zero m
compare zero (suc n) = less zero n
compare (suc m) (suc n) with compare m n
-compare (suc .m) (suc .(suc m + k)) | less m k = less (suc m) k
-compare (suc .m) (suc .m) | equal m = equal (suc m)
-compare (suc .(suc m + k)) (suc .m) | greater m k = greater (suc m) k
+... | less m k = less (suc m) k
+... | equal m = equal (suc m)
+... | greater n k = greater (suc n) k
diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index 85ed06c..19fdbf5 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/src/Data/Nat/Coprimality.agda
@@ -8,27 +8,25 @@ module Data.Nat.Coprimality where
open import Data.Empty
open import Data.Fin using (toℕ; fromℕ≤)
-open import Data.Fin.Properties as FinProp
+open import Data.Fin.Properties using (toℕ-fromℕ≤)
open import Data.Nat
-open import Data.Nat.Primality
-import Data.Nat.Properties as NatProp
-open import Data.Nat.Divisibility as Div
+open import Data.Nat.Divisibility
open import Data.Nat.GCD
open import Data.Nat.GCD.Lemmas
+open import Data.Nat.Primality
+open import Data.Nat.Properties
open import Data.Product as Prod
open import Function
-open import Relation.Binary.PropositionalEquality as PropEq
- using (_≡_; _≢_; refl)
+open import Level using (0ℓ)
+open import Relation.Binary.PropositionalEquality as P
+ using (_≡_; _≢_; refl; cong; subst; module ≡-Reasoning)
open import Relation.Nullary
open import Relation.Binary
-open import Algebra
-private
- module P = Poset Div.poset
-- Coprime m n is inhabited iff m and n are coprime (relatively
-- prime), i.e. if their only common divisor is 1.
-Coprime : (m n : ℕ) → Set
+Coprime : Rel ℕ 0ℓ
Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1
-- Coprime numbers have 1 as their gcd.
@@ -37,15 +35,14 @@ coprime-gcd : ∀ {m n} → Coprime m n → GCD m n 1
coprime-gcd {m} {n} c = GCD.is (1∣ m , 1∣ n) greatest
where
greatest : ∀ {d} → d ∣ m × d ∣ n → d ∣ 1
- greatest cd with c cd
- greatest .{1} cd | refl = 1∣ 1
+ greatest cd with c cd
+ ... | refl = 1∣ 1
-- If two numbers have 1 as their gcd, then they are coprime.
gcd-coprime : ∀ {m n} → GCD m n 1 → Coprime m n
gcd-coprime g cd with GCD.greatest g cd
-gcd-coprime g cd | divides q eq =
- NatProp.i*j≡1⇒j≡1 q _ (PropEq.sym eq)
+... | divides q eq = i*j≡1⇒j≡1 q _ (P.sym eq)
-- Coprime is decidable.
@@ -59,12 +56,12 @@ private
coprime? : Decidable Coprime
coprime? i j with gcd i j
... | (0 , g) = no (0≢1 ∘ GCD.unique g ∘ coprime-gcd)
-... | (1 , g) = yes (λ {i} → gcd-coprime g {i})
+... | (1 , g) = yes (gcd-coprime g)
... | (suc (suc d) , g) = no (2+≢1 ∘ GCD.unique g ∘ coprime-gcd)
-- The coprimality relation is symmetric.
-sym : ∀ {m n} → Coprime m n → Coprime n m
+sym : Symmetric Coprime
sym c = c ∘ swap
-- Everything is coprime to 1.
@@ -75,12 +72,12 @@ sym c = c ∘ swap
-- Nothing except for 1 is coprime to 0.
0-coprimeTo-1 : ∀ {m} → Coprime 0 m → m ≡ 1
-0-coprimeTo-1 {m} c = c (m ∣0 , P.refl)
+0-coprimeTo-1 {m} c = c (m ∣0 , ∣-refl)
-- If m and n are coprime, then n + m and n are also coprime.
coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n
-coprime-+ c (d₁ , d₂) = c (∣-∸ d₁ d₂ , d₂)
+coprime-+ c (d₁ , d₂) = c (∣m+n∣m⇒∣n d₁ d₂ , d₂)
-- If the "gcd" in Bézout's identity is non-zero, then the "other"
-- divisors are coprime.
@@ -125,14 +122,13 @@ data GCD′ : ℕ → ℕ → ℕ → Set where
gcd-gcd′ : ∀ {d m n} → GCD m n d → GCD′ m n d
gcd-gcd′ g with GCD.commonDivisor g
gcd-gcd′ {zero} g | (divides q₁ refl , divides q₂ refl)
- with q₁ * 0 | NatProp.*-comm 0 q₁
- | q₂ * 0 | NatProp.*-comm 0 q₂
-... | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
+ with q₁ * 0 | *-comm 0 q₁ | q₂ * 0 | *-comm 0 q₂
+... | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
gcd-gcd′ {suc d} g | (divides q₁ refl , divides q₂ refl) =
gcd-* q₁ q₂ (Bézout-coprime (Bézout.identity g))
gcd′-gcd : ∀ {m n d} → GCD′ m n d → GCD m n d
-gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (∣-* q₁ , ∣-* q₂) (coprime-factors c)
+gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (n∣m*n q₁ , n∣m*n q₂) (coprime-factors c)
-- Calculates (the alternative representation of) the gcd of the
-- arguments.
@@ -149,11 +145,11 @@ prime⇒coprime 1 () _ _ _ _
prime⇒coprime (suc (suc m)) _ 0 () _ _
prime⇒coprime (suc (suc m)) _ _ _ _ {1} _ = refl
prime⇒coprime (suc (suc m)) p _ _ _ {0} (divides q 2+m≡q*0 , _) =
- ⊥-elim $ NatProp.i+1+j≢i 0 (begin
+ ⊥-elim $ i+1+j≢i 0 (begin
2 + m ≡⟨ 2+m≡q*0 ⟩
- q * 0 ≡⟨ proj₂ NatProp.*-zero q ⟩
+ q * 0 ≡⟨ *-zeroʳ q ⟩
0 ∎)
- where open PropEq.≡-Reasoning
+ where open ≡-Reasoning
prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
(2+i∣2+m , 2+i∣1+n) =
⊥-elim (p _ 2+i′∣2+m)
@@ -163,10 +159,9 @@ prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
3 + i ≤⟨ s≤s (∣⇒≤ 2+i∣1+n) ⟩
2 + n ≤⟨ 1+n<2+m ⟩
2 + m ∎)
- where open NatProp.≤-Reasoning
+ where open ≤-Reasoning
2+i′∣2+m : 2 + toℕ (fromℕ≤ i<m) ∣ 2 + m
- 2+i′∣2+m = PropEq.subst
- (λ j → j ∣ 2 + m)
- (PropEq.sym (PropEq.cong (_+_ 2) (FinProp.toℕ-fromℕ≤ i<m)))
+ 2+i′∣2+m = subst (_∣ 2 + m)
+ (P.sym (cong (2 +_) (toℕ-fromℕ≤ i<m)))
2+i∣2+m
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index a07726f..746e97e 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -6,143 +6,102 @@
module Data.Nat.DivMod where
-open import Data.Fin as Fin using (Fin; toℕ)
-import Data.Fin.Properties as FinP
-open import Data.Nat as Nat
-open import Data.Nat.Properties
-open import Relation.Nullary.Decidable
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
-import Relation.Binary.PropositionalEquality.TrustMe as TrustMe
- using (erase)
-
-open import Agda.Builtin.Nat using ( div-helper; mod-helper )
+open import Agda.Builtin.Nat using (div-helper; mod-helper)
-open SemiringSolver
-open P.≡-Reasoning
-open ≤-Reasoning
- renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩′_)
+open import Data.Fin using (Fin; toℕ; fromℕ≤)
+open import Data.Fin.Properties using (toℕ-fromℕ≤)
+open import Data.Nat as Nat
+open import Data.Nat.DivMod.Core
+open import Data.Nat.Properties using (≤⇒≤″; +-assoc; +-comm; +-identityʳ)
+open import Function using (_$_)
+open import Relation.Nullary.Decidable using (False)
+open import Relation.Binary.PropositionalEquality
-infixl 7 _div_ _mod_ _divMod_
+open ≡-Reasoning
--- A specification of integer division.
+------------------------------------------------------------------------
+-- Basic operations
-record DivMod (dividend divisor : ℕ) : Set where
- constructor result
- field
- quotient : ℕ
- remainder : Fin divisor
- property : dividend ≡ toℕ remainder + quotient * divisor
+infixl 7 _div_ _%_
--- Integer division.
+-- Integer division
_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
-(d div 0) {}
-(d div suc s) = div-helper 0 s d s
-
--- The remainder after integer division.
+(a div 0) {}
+(a div suc n) = div-helper 0 n a n
-private
- -- The remainder is not too large.
+-- Integer remainder (mod)
- mod-lemma : (acc d n : ℕ) →
- let s = acc + n in
- mod-helper acc s d n ≤ s
+_%_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
+(a % 0) {}
+(a % suc n) = mod-helper 0 n a n
- mod-lemma acc zero n = start
- acc ≤⟨ m≤m+n acc n ⟩
- acc + n □
+------------------------------------------------------------------------
+-- Properties
+
+a≡a%n+[a/n]*n : ∀ a n → a ≡ a % suc n + (a div (suc n)) * suc n
+a≡a%n+[a/n]*n a n = division-lemma 0 0 a n
+
+a%1≡0 : ∀ a → a % 1 ≡ 0
+a%1≡0 = a[modₕ]1≡0
+
+a%n<n : ∀ a n → a % suc n < suc n
+a%n<n a n = s≤s (a[modₕ]n<n 0 a n)
+
+n%n≡0 : ∀ n → suc n % suc n ≡ 0
+n%n≡0 n = n[modₕ]n≡0 0 n
+
+a%n%n≡a%n : ∀ a n → a % suc n % suc n ≡ a % suc n
+a%n%n≡a%n a n = modₕ-idem 0 a n
+
+[a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
+[a+n]%n≡a%n a n = a+n[modₕ]n≡a[modₕ]n 0 a n
+
+[a+kn]%n≡a%n : ∀ a k n → (a + k * (suc n)) % suc n ≡ a % suc n
+[a+kn]%n≡a%n a zero n = cong (_% suc n) (+-identityʳ a)
+[a+kn]%n≡a%n a (suc k) n = begin
+ (a + (m + k * m)) % m ≡⟨ cong (_% m) (sym (+-assoc a m (k * m))) ⟩
+ (a + m + k * m) % m ≡⟨ [a+kn]%n≡a%n (a + m) k n ⟩
+ (a + m) % m ≡⟨ [a+n]%n≡a%n a n ⟩
+ a % m ∎
+ where m = suc n
+
+kn%n≡0 : ∀ k n → k * (suc n) % suc n ≡ 0
+kn%n≡0 = [a+kn]%n≡a%n 0
+
+%-distribˡ-+ : ∀ a b n → (a + b) % suc n ≡ (a % suc n + b % suc n) % suc n
+%-distribˡ-+ a b n = begin
+ (a + b) % m ≡⟨ cong (λ v → (v + b) % m) (a≡a%n+[a/n]*n a n) ⟩
+ (a % m + a div m * m + b) % m ≡⟨ cong (_% m) (+-assoc (a % m) _ b) ⟩
+ (a % m + (a div m * m + b)) % m ≡⟨ cong (λ v → (a % m + v) % m) (+-comm _ b) ⟩
+ (a % m + (b + a div m * m)) % m ≡⟨ cong (_% m) (sym (+-assoc (a % m) b _)) ⟩
+ (a % m + b + a div m * m) % m ≡⟨ [a+kn]%n≡a%n (a % m + b) (a div m) n ⟩
+ (a % m + b) % m ≡⟨ cong (λ v → (a % m + v) % m) (a≡a%n+[a/n]*n b n) ⟩
+ (a % m + (b % m + (b div m) * m)) % m ≡⟨ sym (cong (_% m) (+-assoc (a % m) (b % m) _)) ⟩
+ (a % m + b % m + (b div m) * m) % m ≡⟨ [a+kn]%n≡a%n (a % m + b % m) (b div m) n ⟩
+ (a % m + b % m) % m ∎
+ where m = suc n
- mod-lemma acc (suc d) zero = start
- mod-helper zero (acc + 0) d (acc + 0) ≤⟨ mod-lemma zero d (acc + 0) ⟩
- acc + 0 □
+------------------------------------------------------------------------
+-- A specification of integer division.
- mod-lemma acc (suc d) (suc n) =
- P.subst (λ x → mod-helper (suc acc) x d n ≤ x)
- (P.sym (+-suc acc n))
- (mod-lemma (suc acc) d n)
+record DivMod (dividend divisor : ℕ) : Set where
+ constructor result
+ field
+ quotient : ℕ
+ remainder : Fin divisor
+ property : dividend ≡ toℕ remainder + quotient * divisor
_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
-(d mod 0) {}
-(d mod suc s) =
- Fin.fromℕ≤″ (mod-helper 0 s d s)
- (Nat.erase (≤⇒≤″ (s≤s (mod-lemma 0 d s))))
-
--- Integer division with remainder.
-
-private
-
- -- The quotient and remainder are related to the dividend and
- -- divisor in the right way.
-
- division-lemma :
- (mod-acc div-acc d n : ℕ) →
- let s = mod-acc + n in
- mod-acc + div-acc * suc s + d
- ≡
- mod-helper mod-acc s d n + div-helper div-acc s d n * suc s
-
- division-lemma mod-acc div-acc zero n = begin
-
- mod-acc + div-acc * suc s + zero ≡⟨ +-identityʳ _ ⟩
-
- mod-acc + div-acc * suc s ∎
-
- where s = mod-acc + n
-
- division-lemma mod-acc div-acc (suc d) zero = begin
-
- mod-acc + div-acc * suc s + suc d ≡⟨ solve 3
- (λ mod-acc div-acc d →
- let s = mod-acc :+ con 0 in
- mod-acc :+ div-acc :* (con 1 :+ s) :+ (con 1 :+ d)
- :=
- (con 1 :+ div-acc) :* (con 1 :+ s) :+ d)
- P.refl mod-acc div-acc d ⟩
- suc div-acc * suc s + d ≡⟨ division-lemma zero (suc div-acc) d s ⟩
-
- mod-helper zero s d s +
- div-helper (suc div-acc) s d s * suc s ≡⟨⟩
-
- mod-helper mod-acc s (suc d) zero +
- div-helper div-acc s (suc d) zero * suc s ∎
-
- where s = mod-acc + 0
-
- division-lemma mod-acc div-acc (suc d) (suc n) = begin
-
- mod-acc + div-acc * suc s + suc d ≡⟨ solve 4
- (λ mod-acc div-acc n d →
- mod-acc :+ div-acc :* (con 1 :+ (mod-acc :+ (con 1 :+ n))) :+ (con 1 :+ d)
- :=
- con 1 :+ mod-acc :+ div-acc :* (con 2 :+ mod-acc :+ n) :+ d)
- P.refl mod-acc div-acc n d ⟩
- suc mod-acc + div-acc * suc s′ + d ≡⟨ division-lemma (suc mod-acc) div-acc d n ⟩
-
- mod-helper (suc mod-acc) s′ d n +
- div-helper div-acc s′ d n * suc s′ ≡⟨ P.cong (λ s → mod-helper (suc mod-acc) s d n +
- div-helper div-acc s d n * suc s)
- (P.sym (+-suc mod-acc n)) ⟩
-
- mod-helper (suc mod-acc) s d n +
- div-helper div-acc s d n * suc s ≡⟨⟩
-
- mod-helper mod-acc s (suc d) (suc n) +
- div-helper div-acc s (suc d) (suc n) * suc s ∎
-
- where
- s = mod-acc + suc n
- s′ = suc mod-acc + n
+(a mod 0) {}
+(a mod suc n) = fromℕ≤ (a%n<n a n)
_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
DivMod dividend divisor
-(d divMod 0) {}
-(d divMod suc s) =
- result (d div suc s) (d mod suc s) (TrustMe.erase (begin
- d ≡⟨ division-lemma 0 0 d s ⟩
- mod-helper 0 s d s + div-helper 0 s d s * suc s ≡⟨ P.cong₂ _+_ (P.sym (FinP.toℕ-fromℕ≤ lemma)) P.refl ⟩
- toℕ (Fin.fromℕ≤ lemma) + div-helper 0 s d s * suc s ≡⟨ P.cong (λ n → toℕ n + div-helper 0 s d s * suc s)
- (FinP.fromℕ≤≡fromℕ≤″ lemma _) ⟩
- toℕ (Fin.fromℕ≤″ _ lemma′) + div-helper 0 s d s * suc s ∎))
+(a divMod 0) {}
+(a divMod suc n) = result (a div suc n) (a mod suc n) $ begin
+ a ≡⟨ a≡a%n+[a/n]*n a n ⟩
+ a % suc n + [a/n]*n ≡⟨ cong (_+ [a/n]*n) (sym (toℕ-fromℕ≤ (a%n<n a n))) ⟩
+ toℕ (fromℕ≤ (a%n<n a n)) + [a/n]*n ∎
where
- lemma = s≤s (mod-lemma 0 d s)
- lemma′ = Nat.erase (≤⇒≤″ lemma)
+ [a/n]*n = a div suc n * suc n
diff --git a/src/Data/Nat/DivMod/Core.agda b/src/Data/Nat/DivMod/Core.agda
new file mode 100644
index 0000000..dfd6eb1
--- /dev/null
+++ b/src/Data/Nat/DivMod/Core.agda
@@ -0,0 +1,102 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core lemmas for division and modulus operations
+------------------------------------------------------------------------
+
+module Data.Nat.DivMod.Core where
+
+open import Agda.Builtin.Nat using ()
+ renaming (div-helper to divₕ; mod-helper to modₕ)
+
+open import Data.Nat
+open import Data.Nat.Properties
+open import Relation.Binary.PropositionalEquality
+
+open ≡-Reasoning
+
+-------------------------------------------------------------------------
+-- mod lemmas
+
+modₕ-skipTo0 : ∀ acc n a b → modₕ acc n (b + a) a ≡ modₕ (a + acc) n b 0
+modₕ-skipTo0 acc n zero b = cong (λ v → modₕ acc n v 0) (+-identityʳ b)
+modₕ-skipTo0 acc n (suc a) b = begin
+ modₕ acc n (b + suc a) (suc a) ≡⟨ cong (λ v → modₕ acc n v (suc a)) (+-suc b a) ⟩
+ modₕ acc n (suc b + a) (suc a) ≡⟨⟩
+ modₕ (suc acc) n (b + a) a ≡⟨ modₕ-skipTo0 (suc acc) n a b ⟩
+ modₕ (a + suc acc) n b 0 ≡⟨ cong (λ v → modₕ v n b 0) (+-suc a acc) ⟩
+ modₕ (suc a + acc) n b 0 ∎
+
+modₕ-skipToEnd : ∀ acc n a b → modₕ acc n a (a + b) ≡ acc + a
+modₕ-skipToEnd acc n zero b = sym (+-identityʳ acc)
+modₕ-skipToEnd acc n (suc a) b = begin
+ modₕ (suc acc) n a (a + b) ≡⟨ modₕ-skipToEnd (suc acc) n a b ⟩
+ suc acc + a ≡⟨ sym (+-suc acc a) ⟩
+ acc + suc a ∎
+
+a[modₕ]1≡0 : ∀ a → modₕ 0 0 a 0 ≡ 0
+a[modₕ]1≡0 zero = refl
+a[modₕ]1≡0 (suc a) = a[modₕ]1≡0 a
+
+n[modₕ]n≡0 : ∀ acc v → modₕ acc (acc + v) (suc v) v ≡ 0
+n[modₕ]n≡0 acc v = modₕ-skipTo0 acc (acc + v) v 1
+
+a[modₕ]n<n : ∀ acc d n → modₕ acc (acc + n) d n ≤ acc + n
+a[modₕ]n<n acc zero n = m≤m+n acc n
+a[modₕ]n<n acc (suc d) zero = a[modₕ]n<n zero d (acc + 0)
+a[modₕ]n<n acc (suc d) (suc n)
+ rewrite +-suc acc n = a[modₕ]n<n (suc acc) d n
+
+modₕ-idem : ∀ acc a n → modₕ 0 (acc + n) (modₕ acc (acc + n) a n) (acc + n) ≡ modₕ acc (acc + n) a n
+modₕ-idem acc zero n = modₕ-skipToEnd 0 (acc + n) acc n
+modₕ-idem acc (suc a) zero rewrite +-identityʳ acc = modₕ-idem 0 a acc
+modₕ-idem acc (suc a) (suc n) rewrite +-suc acc n = modₕ-idem (suc acc) a n
+
+a+n[modₕ]n≡a[modₕ]n : ∀ acc a n → modₕ acc (acc + n) (acc + a + suc n) n ≡ modₕ acc (acc + n) a n
+a+n[modₕ]n≡a[modₕ]n acc zero n rewrite +-identityʳ acc = begin
+ modₕ acc (acc + n) (acc + suc n) n ≡⟨ cong (λ v → modₕ acc (acc + n) v n) (+-suc acc n) ⟩
+ modₕ acc (acc + n) (suc acc + n) n ≡⟨ modₕ-skipTo0 acc (acc + n) n (suc acc) ⟩
+ modₕ (acc + n) (acc + n) (suc acc) 0 ≡⟨⟩
+ modₕ 0 (acc + n) acc (acc + n) ≡⟨ modₕ-skipToEnd 0 (acc + n) acc n ⟩
+ acc ∎
+a+n[modₕ]n≡a[modₕ]n acc (suc a) zero rewrite +-identityʳ acc = begin
+ modₕ acc acc (acc + suc a + 1) 0 ≡⟨ cong (λ v → modₕ acc acc v 0) (+-comm (acc + suc a) 1) ⟩
+ modₕ acc acc (1 + (acc + suc a)) 0 ≡⟨⟩
+ modₕ 0 acc (acc + suc a) acc ≡⟨ cong (λ v → modₕ 0 acc v acc) (+-comm acc (suc a)) ⟩
+ modₕ 0 acc (suc a + acc) acc ≡⟨ cong (λ v → modₕ 0 acc v acc) (sym (+-suc a acc)) ⟩
+ modₕ 0 acc (a + suc acc) acc ≡⟨ a+n[modₕ]n≡a[modₕ]n 0 a acc ⟩
+ modₕ 0 acc a acc ∎
+a+n[modₕ]n≡a[modₕ]n acc (suc a) (suc n) rewrite +-suc acc n = begin
+ mod₁ (acc + suc a + (2 + n)) (suc n) ≡⟨ cong (λ v → mod₁ (v + suc (suc n)) (suc n)) (+-suc acc a) ⟩
+ mod₁ (suc acc + a + (2 + n)) (suc n) ≡⟨⟩
+ mod₂ (acc + a + (2 + n)) n ≡⟨ cong (λ v → mod₂ v n) (sym (+-assoc (acc + a) 1 (suc n))) ⟩
+ mod₂ (acc + a + 1 + suc n) n ≡⟨ cong (λ v → mod₂ (v + suc n) n) (+-comm (acc + a) 1) ⟩
+ mod₂ (suc acc + a + suc n) n ≡⟨ a+n[modₕ]n≡a[modₕ]n (suc acc) a n ⟩
+ mod₂ a n ∎
+ where
+ mod₁ = modₕ acc (suc acc + n)
+ mod₂ = modₕ (suc acc) (suc acc + n)
+
+-------------------------------------------------------------------------
+-- division lemmas
+
+-- The quotient and remainder are related to the dividend and
+-- divisor in the right way.
+
+division-lemma : ∀ accᵐ accᵈ d n →
+ accᵐ + accᵈ * suc (accᵐ + n) + d ≡
+ modₕ accᵐ (accᵐ + n) d n + divₕ accᵈ (accᵐ + n) d n * suc (accᵐ + n)
+division-lemma accᵐ accᵈ zero n = +-identityʳ _
+division-lemma accᵐ accᵈ (suc d) zero rewrite +-identityʳ accᵐ = begin
+ accᵐ + accᵈ * suc accᵐ + suc d ≡⟨ +-suc _ d ⟩
+ suc accᵈ * suc accᵐ + d ≡⟨ division-lemma zero (suc accᵈ) d accᵐ ⟩
+ modₕ 0 accᵐ d accᵐ +
+ divₕ (suc accᵈ) accᵐ d accᵐ * suc accᵐ ≡⟨⟩
+ modₕ accᵐ accᵐ (suc d) 0 +
+ divₕ accᵈ accᵐ (suc d) 0 * suc accᵐ ∎
+division-lemma accᵐ accᵈ (suc d) (suc n) rewrite +-suc accᵐ n = begin
+ accᵐ + accᵈ * m + suc d ≡⟨ +-suc _ d ⟩
+ suc (accᵐ + accᵈ * m + d) ≡⟨ division-lemma (suc accᵐ) accᵈ d n ⟩
+ modₕ _ _ d n + divₕ accᵈ _ d n * m ∎
+ where
+ m = 2 + accᵐ + n
diff --git a/src/Data/Nat/DivMod/Unsafe.agda b/src/Data/Nat/DivMod/Unsafe.agda
new file mode 100644
index 0000000..4e852d1
--- /dev/null
+++ b/src/Data/Nat/DivMod/Unsafe.agda
@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- More efficient (and unsafe) mod and divMod operations
+------------------------------------------------------------------------
+
+module Data.Nat.DivMod.Unsafe where
+
+open import Data.Nat using (ℕ; _+_; _*_; _≟_; zero; suc)
+open import Data.Nat.DivMod hiding (_mod_; _divMod_)
+open import Data.Nat.Properties using (≤⇒≤″)
+import Data.Nat.Unsafe as NatUnsafe
+open import Data.Fin using (Fin; toℕ; fromℕ≤″)
+open import Data.Fin.Properties using (toℕ-fromℕ≤″)
+open import Function using (_$_)
+open import Relation.Nullary.Decidable using (False)
+open import Relation.Binary.PropositionalEquality
+ using (refl; sym; cong; module ≡-Reasoning)
+import Relation.Binary.PropositionalEquality.TrustMe as TrustMe
+ using (erase)
+
+open ≡-Reasoning
+
+infixl 7 _mod_ _divMod_
+
+------------------------------------------------------------------------
+-- Certified modulus
+
+_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
+(a mod 0) {}
+(a mod suc n) = fromℕ≤″ (a % suc n) (NatUnsafe.erase (≤⇒≤″ (a%n<n a n)))
+
+------------------------------------------------------------------------
+-- Returns modulus and division result with correctness proof
+
+_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
+ DivMod dividend divisor
+(a divMod 0) {}
+(a divMod suc n) = result (a div suc n) (a mod suc n) $ TrustMe.erase $ begin
+ a ≡⟨ a≡a%n+[a/n]*n a n ⟩
+ a % suc n + [a/n]*n ≡⟨ cong (_+ [a/n]*n) (sym (toℕ-fromℕ≤″ lemma′)) ⟩
+ toℕ (fromℕ≤″ _ lemma′) + [a/n]*n ∎
+ where
+ lemma′ = NatUnsafe.erase (≤⇒≤″ (a%n<n a n))
+ [a/n]*n = a div suc n * suc n
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index 8faaa60..ac6a544 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -6,20 +6,24 @@
module Data.Nat.Divisibility where
+open import Algebra
open import Data.Nat as Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
+open import Data.Nat.Solver
open import Data.Fin using (Fin; zero; suc; toℕ)
import Data.Fin.Properties as FP
-open SemiringSolver
-open import Algebra
open import Data.Product
+open import Function
+open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary
+import Relation.Nullary.Decidable as Dec
open import Relation.Binary
import Relation.Binary.PartialOrderReasoning as PartialOrderReasoning
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst)
-open import Function
+
+open +-*-Solver
------------------------------------------------------------------------
-- m ∣ n is inhabited iff m divides n. Some sources, like Hardy and
@@ -30,8 +34,10 @@ open import Function
infix 4 _∣_ _∤_
-data _∣_ : ℕ → ℕ → Set where
- divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n
+record _∣_ (m n : ℕ) : Set where
+ constructor divides
+ field quotient : ℕ
+ equality : n ≡ quotient * m
_∤_ : Rel ℕ _
m ∤ n = ¬ (m ∣ n)
@@ -61,11 +67,10 @@ quotient (divides q _) = q
divides (q * p) (sym (*-assoc q p _))
∣-antisym : Antisymmetric _≡_ _∣_
-∣-antisym (divides {n = zero} _ _) (divides q refl) = *-comm q 0
-∣-antisym (divides p eq) (divides {n = zero} _ _) =
- trans (*-comm 0 p) (sym eq)
-∣-antisym (divides {n = suc _} p eq₁) (divides {n = suc _} q eq₂) =
- ≤-antisym (∣⇒≤ (divides p eq₁)) (∣⇒≤ (divides q eq₂))
+∣-antisym {m} {0} _ (divides q eq) = trans eq (*-comm q 0)
+∣-antisym {0} {n} (divides p eq) _ = sym (trans eq (*-comm p 0))
+∣-antisym {suc m} {suc n} (divides p eq₁) (divides q eq₂) =
+ ≤-antisym (∣⇒≤ (divides p eq₁)) (∣⇒≤ (divides q eq₂))
∣-isPreorder : IsPreorder _≡_ _∣_
∣-isPreorder = record
@@ -89,7 +94,8 @@ poset = record
}
module ∣-Reasoning = PartialOrderReasoning poset
- renaming (_≤⟨_⟩_ to _∣⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)
+ hiding (_≈⟨_⟩_)
+ renaming (_≤⟨_⟩_ to _∣⟨_⟩_)
------------------------------------------------------------------------
-- Simple properties of _∣_
@@ -105,8 +111,11 @@ n ∣0 = divides 0 refl
n∣n : ∀ {n} → n ∣ n
n∣n = ∣-refl
-n|m*n : ∀ m {n} → n ∣ m * n
-n|m*n m = divides m refl
+n∣m*n : ∀ m {n} → n ∣ m * n
+n∣m*n m = divides m refl
+
+m∣m*n : ∀ {m} n → m ∣ m * n
+m∣m*n n = divides n (*-comm _ n)
0∣⇒≡0 : ∀ {n} → 0 ∣ n → n ≡ 0
0∣⇒≡0 {n} 0∣n = ∣-antisym (n ∣0) 0∣n
@@ -117,92 +126,128 @@ n|m*n m = divides m refl
------------------------------------------------------------------------
-- Operators and divisibility
-∣m∣n⇒∣m+n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
-∣m∣n⇒∣m+n (divides p refl) (divides q refl) =
- divides (p + q) (sym (*-distribʳ-+ _ p q))
-
-∣m+n|m⇒|n : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
-∣m+n|m⇒|n {i} {m} {n} (divides p m+n≡p*i) (divides q m≡q*i) =
- divides (p ∸ q) (begin
- n ≡⟨ sym (m+n∸n≡m n m) ⟩
- n + m ∸ m ≡⟨ cong (_∸ m) (+-comm n m) ⟩
- m + n ∸ m ≡⟨ cong₂ _∸_ m+n≡p*i m≡q*i ⟩
- p * i ∸ q * i ≡⟨ sym (*-distribʳ-∸ i p q) ⟩
- (p ∸ q) * i ∎)
- where open PropEq.≡-Reasoning
+module _ where
+
+ open PropEq.≡-Reasoning
+
+ ∣m⇒∣m*n : ∀ {i m} n → i ∣ m → i ∣ m * n
+ ∣m⇒∣m*n {i} {m} n (divides q eq) = divides (q * n) $ begin
+ m * n ≡⟨ cong (_* n) eq ⟩
+ q * i * n ≡⟨ *-assoc q i n ⟩
+ q * (i * n) ≡⟨ cong (q *_) (*-comm i n) ⟩
+ q * (n * i) ≡⟨ sym (*-assoc q n i) ⟩
+ q * n * i ∎
+
+ ∣n⇒∣m*n : ∀ {i} m {n} → i ∣ n → i ∣ m * n
+ ∣n⇒∣m*n {i} m {n} (divides q eq) = divides (m * q) $ begin
+ m * n ≡⟨ cong (m *_) eq ⟩
+ m * (q * i) ≡⟨ sym (*-assoc m q i) ⟩
+ m * q * i ∎
+
+ ∣m∣n⇒∣m+n : ∀ {i m n} → i ∣ m → i ∣ n → i ∣ m + n
+ ∣m∣n⇒∣m+n (divides p refl) (divides q refl) =
+ divides (p + q) (sym (*-distribʳ-+ _ p q))
+
+ ∣m+n∣m⇒∣n : ∀ {i m n} → i ∣ m + n → i ∣ m → i ∣ n
+ ∣m+n∣m⇒∣n {i} {m} {n} (divides p m+n≡p*i) (divides q m≡q*i) =
+ divides (p ∸ q) $ begin
+ n ≡⟨ sym (m+n∸n≡m n m) ⟩
+ n + m ∸ m ≡⟨ cong (_∸ m) (+-comm n m) ⟩
+ m + n ∸ m ≡⟨ cong₂ _∸_ m+n≡p*i m≡q*i ⟩
+ p * i ∸ q * i ≡⟨ sym (*-distribʳ-∸ i p q) ⟩
+ (p ∸ q) * i ∎
+
+ ∣m∸n∣n⇒∣m : ∀ i {m n} → n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
+ ∣m∸n∣n⇒∣m i {m} {n} n≤m (divides p m∸n≡p*i) (divides q n≡q*o) =
+ divides (p + q) $ begin
+ m ≡⟨ sym (m+n∸m≡n n≤m) ⟩
+ n + (m ∸ n) ≡⟨ +-comm n (m ∸ n) ⟩
+ m ∸ n + n ≡⟨ cong₂ _+_ m∸n≡p*i n≡q*o ⟩
+ p * i + q * i ≡⟨ sym (*-distribʳ-+ i p q) ⟩
+ (p + q) * i ∎
+
+ *-cong : ∀ {i j} k → i ∣ j → k * i ∣ k * j
+ *-cong {i} {j} k (divides q j≡q*i) = divides q $ begin
+ k * j ≡⟨ cong (_*_ k) j≡q*i ⟩
+ k * (q * i) ≡⟨ sym (*-assoc k q i) ⟩
+ (k * q) * i ≡⟨ cong (_* i) (*-comm k q) ⟩
+ (q * k) * i ≡⟨ *-assoc q k i ⟩
+ q * (k * i) ∎
+
+ /-cong : ∀ {i j} k → suc k * i ∣ suc k * j → i ∣ j
+ /-cong {i} {j} k (divides q eq) =
+ divides q (*-cancelʳ-≡ j (q * i) (begin
+ j * (suc k) ≡⟨ *-comm j (suc k) ⟩
+ (suc k) * j ≡⟨ eq ⟩
+ q * ((suc k) * i) ≡⟨ cong (q *_) (*-comm (suc k) i) ⟩
+ q * (i * (suc k)) ≡⟨ sym (*-assoc q i (suc k)) ⟩
+ (q * i) * (suc k) ∎))
+
+ m%n≡0⇒n∣m : ∀ m n → m % (suc n) ≡ 0 → suc n ∣ m
+ m%n≡0⇒n∣m m n eq = divides (m div (suc n)) (begin
+ m ≡⟨ a≡a%n+[a/n]*n m n ⟩
+ m % (suc n) + m div (suc n) * (suc n) ≡⟨ cong₂ _+_ eq refl ⟩
+ m div (suc n) * (suc n) ∎)
+
+ n∣m⇒m%n≡0 : ∀ m n → suc n ∣ m → m % (suc n) ≡ 0
+ n∣m⇒m%n≡0 m n (divides v eq) = begin
+ m % (suc n) ≡⟨ cong (_% (suc n)) eq ⟩
+ (v * suc n) % (suc n) ≡⟨ kn%n≡0 v n ⟩
+ 0 ∎
+
+ m%n≡0⇔n∣m : ∀ m n → m % (suc n) ≡ 0 ⇔ suc n ∣ m
+ m%n≡0⇔n∣m m n = equivalence (m%n≡0⇒n∣m m n) (n∣m⇒m%n≡0 m n)
-∣m∸n∣n⇒∣m : ∀ i {m n} → n ≤ m → i ∣ m ∸ n → i ∣ n → i ∣ m
-∣m∸n∣n⇒∣m i {m} {n} n≤m (divides p m∸n≡p*i) (divides q n≡q*o) =
- divides (p + q) (begin
- m ≡⟨ sym (m+n∸m≡n n≤m) ⟩
- n + (m ∸ n) ≡⟨ +-comm n (m ∸ n) ⟩
- m ∸ n + n ≡⟨ cong₂ _+_ m∸n≡p*i n≡q*o ⟩
- p * i + q * i ≡⟨ sym (*-distribʳ-+ i p q) ⟩
- (p + q) * i ∎)
- where open PropEq.≡-Reasoning
+-- Divisibility is decidable.
-*-cong : ∀ {i j} k → i ∣ j → k * i ∣ k * j
-*-cong {i} {j} k (divides q j≡q*i) = divides q (begin
- k * j ≡⟨ cong (_*_ k) j≡q*i ⟩
- k * (q * i) ≡⟨ sym (*-assoc k q i) ⟩
- (k * q) * i ≡⟨ cong (_* i) (*-comm k q) ⟩
- (q * k) * i ≡⟨ *-assoc q k i ⟩
- q * (k * i) ∎)
- where open PropEq.≡-Reasoning
+infix 4 _∣?_
-/-cong : ∀ {i j} k → suc k * i ∣ suc k * j → i ∣ j
-/-cong {i} {j} k (divides q eq) =
- divides q (*-cancelʳ-≡ j (q * i) (begin
- j * (suc k) ≡⟨ *-comm j (suc k) ⟩
- (suc k) * j ≡⟨ eq ⟩
- q * ((suc k) * i) ≡⟨ cong (q *_) (*-comm (suc k) i) ⟩
- q * (i * (suc k)) ≡⟨ sym (*-assoc q i (suc k)) ⟩
- (q * i) * (suc k) ∎))
- where open PropEq.≡-Reasoning
+_∣?_ : Decidable _∣_
+zero ∣? zero = yes (0 ∣0)
+zero ∣? suc m = no ((λ()) ∘′ 0∣⇒≡0)
+suc n ∣? m = Dec.map (m%n≡0⇔n∣m m n) (m % (suc n) ≟ 0)
--- If the remainder after division is non-zero, then the divisor does
--- not divide the dividend.
+------------------------------------------------------------------------
+-- DEPRECATED - please use new names as continuing support for the old
+-- names is not guaranteed.
-nonZeroDivisor-lemma
- : ∀ m q (r : Fin (1 + m)) → toℕ r ≢ 0 →
- 1 + m ∤ toℕ r + q * (1 + m)
+∣-+ = ∣m∣n⇒∣m+n
+{-# WARNING_ON_USAGE ∣-+
+"Warning: ∣-+ was deprecated in v0.14.
+Please use ∣m∣n⇒∣m+n instead."
+#-}
+∣-∸ = ∣m+n∣m⇒∣n
+{-# WARNING_ON_USAGE ∣-∸
+"Warning: ∣-∸ was deprecated in v0.14.
+Please use ∣m+n∣m⇒∣n instead."
+#-}
+∣-* = n∣m*n
+{-# WARNING_ON_USAGE ∣-*
+"Warning: ∣-* was deprecated in v0.14.
+Please use n∣m*n instead."
+#-}
+
+nonZeroDivisor-lemma : ∀ m q (r : Fin (1 + m)) → toℕ r ≢ 0 →
+ 1 + m ∤ toℕ r + q * (1 + m)
nonZeroDivisor-lemma m zero r r≢zero (divides zero eq) = r≢zero $ begin
toℕ r ≡⟨ sym (*-identityˡ (toℕ r)) ⟩
1 * toℕ r ≡⟨ eq ⟩
0 ∎
where open PropEq.≡-Reasoning
nonZeroDivisor-lemma m zero r r≢zero (divides (suc q) eq) =
- ¬i+1+j≤i m $ begin
+ i+1+j≰i m $ begin
m + suc (q * suc m) ≡⟨ +-suc m (q * suc m) ⟩
suc (m + q * suc m) ≡⟨ sym eq ⟩
1 * toℕ r ≡⟨ *-identityˡ (toℕ r) ⟩
- toℕ r ≤⟨ ≤-pred $ FP.bounded r ⟩
+ toℕ r ≤⟨ FP.toℕ≤pred[n] r ⟩
m ∎
where open ≤-Reasoning
nonZeroDivisor-lemma m (suc q) r r≢zero d =
- nonZeroDivisor-lemma m q r r≢zero (∣m+n|m⇒|n d' ∣-refl)
+ nonZeroDivisor-lemma m q r r≢zero (∣m+n∣m⇒∣n d' ∣-refl)
where
lem = solve 3 (λ m r q → r :+ (m :+ q) := m :+ (r :+ q))
refl (suc m) (toℕ r) (q * suc m)
d' = subst (1 + m ∣_) lem d
-
--- Divisibility is decidable.
-
-infix 4 _∣?_
-
-_∣?_ : Decidable _∣_
-zero ∣? zero = yes (0 ∣0)
-zero ∣? suc n = no ((λ()) ∘′ 0∣⇒≡0)
-suc m ∣? n with n divMod suc m
-suc m ∣? .(q * suc m) | result q zero refl =
- yes $ divides q refl
-suc m ∣? .(1 + toℕ r + q * suc m) | result q (suc r) refl =
- no $ nonZeroDivisor-lemma m q (suc r) (λ())
-
-------------------------------------------------------------------------
--- DEPRECATED - please use new names as continuing support for the old
--- names is not guaranteed.
-
-∣-+ = ∣m∣n⇒∣m+n
-∣-∸ = ∣m+n|m⇒|n
-∣-* = n|m*n
+{-# WARNING_ON_USAGE nonZeroDivisor-lemma
+"Warning: nonZeroDivisor-lemma was deprecated in v0.17."
+#-}
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index de37813..a8ad363 100644
--- a/src/Data/Nat/GCD.agda
+++ b/src/Data/Nat/GCD.agda
@@ -7,17 +7,17 @@
module Data.Nat.GCD where
open import Data.Nat
-open import Data.Nat.Divisibility as Div
-open import Relation.Binary
-private module P = Poset Div.poset
+open import Data.Nat.Divisibility
+open import Data.Nat.GCD.Lemmas
+open import Data.Nat.Properties using (+-suc)
open import Data.Product
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst)
-open import Relation.Nullary using (Dec; yes; no)
+open import Function
open import Induction
-open import Induction.Nat using (<′-Rec; <′-rec-builder)
+open import Induction.Nat using (<′-Rec; <′-recBuilder)
open import Induction.Lexicographic
-open import Function
-open import Data.Nat.GCD.Lemmas
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_; subst)
+open import Relation.Nullary using (Dec; yes; no)
------------------------------------------------------------------------
-- Greatest common divisor
@@ -42,7 +42,7 @@ module GCD where
-- The gcd is unique.
unique : ∀ {d₁ d₂ m n} → GCD m n d₁ → GCD m n d₂ → d₁ ≡ d₂
- unique d₁ d₂ = P.antisym (GCD.greatest d₂ (GCD.commonDivisor d₁))
+ unique d₁ d₂ = ∣-antisym (GCD.greatest d₂ (GCD.commonDivisor d₁))
(GCD.greatest d₁ (GCD.commonDivisor d₂))
-- The gcd relation is "symmetric".
@@ -53,12 +53,12 @@ module GCD where
-- The gcd relation is "reflexive".
refl : ∀ {n} → GCD n n n
- refl = is (P.refl , P.refl) proj₁
+ refl = is (∣-refl , ∣-refl) proj₁
-- The GCD of 0 and n is n.
base : ∀ {n} → GCD 0 n n
- base {n} = is (n ∣0 , P.refl) proj₂
+ base {n} = is (n ∣0 , ∣-refl) proj₂
-- If d is the gcd of n and k, then it is also the gcd of n and
-- n + k.
@@ -68,7 +68,7 @@ module GCD where
step {n} {k} {d} g | (d₁ , d₂) = is (d₁ , ∣m∣n⇒∣m+n d₁ d₂) greatest′
where
greatest′ : ∀ {d′} → d′ ∣ n × d′ ∣ n + k → d′ ∣ d
- greatest′ (d₁ , d₂) = GCD.greatest g (d₁ , ∣m+n|m⇒|n d₂ d₁)
+ greatest′ (d₁ , d₂) = GCD.greatest g (d₁ , ∣m+n∣m⇒∣n d₂ d₁)
open GCD public using (GCD) hiding (module GCD)
@@ -99,10 +99,10 @@ module Bézout where
sym (-+ x y eq) = +- y x eq
refl : ∀ {d} → Identity d d d
- refl = -+ 0 1 PropEq.refl
+ refl = -+ 0 1 P.refl
base : ∀ {d} → Identity d 0 d
- base = -+ 0 1 PropEq.refl
+ base = -+ 0 1 P.refl
private
infixl 7 _⊕_
@@ -143,7 +143,7 @@ module Bézout where
stepˡ : ∀ {n k} → Lemma n (suc k) → Lemma n (suc (n + k))
stepˡ {n} {k} (result d g b) =
- PropEq.subst (Lemma n) (lem₀ n k) $
+ subst (Lemma n) (+-suc n k) $
result d (GCD.step g) (Identity.step b)
stepʳ : ∀ {n k} → Lemma (suc k) n → Lemma (suc (n + k)) n
@@ -155,7 +155,7 @@ module Bézout where
-- Euclidean algorithm.
lemma : (m n : ℕ) → Lemma m n
- lemma m n = build [ <′-rec-builder ⊗ <′-rec-builder ] P gcd (m , n)
+ lemma m n = build [ <′-recBuilder ⊗ <′-recBuilder ] P gcd (m , n)
where
P : ℕ × ℕ → Set
P (m , n) = Lemma m n
@@ -176,19 +176,19 @@ module Bézout where
identity : ∀ {m n d} → GCD m n d → Identity d m n
identity {m} {n} g with lemma m n
- identity g | result d g′ b with GCD.unique g g′
- identity g | result d g′ b | PropEq.refl = b
+ ... | result d g′ b with GCD.unique g g′
+ ... | P.refl = b
-- Calculates the gcd of the arguments.
gcd : (m n : ℕ) → ∃ λ d → GCD m n d
gcd m n with Bézout.lemma m n
-gcd m n | Bézout.result d g _ = (d , g)
+... | Bézout.result d g _ = (d , g)
-- gcd as a proposition is decidable
gcd? : (m n d : ℕ) → Dec (GCD m n d)
gcd? m n d with gcd m n
... | d′ , p with d′ ≟ d
-... | no ¬g = no (λ p′ → ¬g (GCD.unique p p′))
-... | yes g = yes (subst (GCD m n) g p)
+... | no ¬g = no (¬g ∘ GCD.unique p)
+... | yes g = yes (subst (GCD m n) g p)
diff --git a/src/Data/Nat/GCD/Lemmas.agda b/src/Data/Nat/GCD/Lemmas.agda
index 188e7d4..b0f3ff2 100644
--- a/src/Data/Nat/GCD/Lemmas.agda
+++ b/src/Data/Nat/GCD/Lemmas.agda
@@ -7,23 +7,41 @@
module Data.Nat.GCD.Lemmas where
open import Data.Nat
-import Data.Nat.Properties as NatProp
-open NatProp.SemiringSolver
+open import Data.Nat.Properties
+open import Data.Nat.Solver
+open import Function
open import Relation.Binary.PropositionalEquality
+
+open +-*-Solver
open ≡-Reasoning
-open import Function
-lem₀ = solve 2 (λ n k → n :+ (con 1 :+ k) := con 1 :+ n :+ k) refl
+private
+ distrib-comm : ∀ x k n → x * k + x * n ≡ x * (n + k)
+ distrib-comm =
+ solve 3 (λ x k n → x :* k :+ x :* n := x :* (n :+ k)) refl
+
+ distrib-comm₂ : ∀ d x k n → d + x * (n + k) ≡ d + x * k + x * n
+ distrib-comm₂ =
+ solve 4 (λ d x k n → d :+ x :* (n :+ k) := d :+ x :* k :+ x :* n) refl
+
+-- Other properties
+-- TODO: Can this proof be simplified? An automatic solver which can
+-- handle ∸ would be nice...
+lem₀ : ∀ i j m n → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
+lem₀ i j m n eq = begin
+ (i ∸ j) * m ≡⟨ *-distribʳ-∸ m i j ⟩
+ (i * m) ∸ (j * m) ≡⟨ cong (_∸ j * m) eq ⟩
+ (j * m + n) ∸ (j * m) ≡⟨ cong (_∸ j * m) (+-comm (j * m) n) ⟩
+ (n + j * m) ∸ (j * m) ≡⟨ m+n∸n≡m n (j * m) ⟩
+ n ∎
lem₁ : ∀ i j → 2 + i ≤′ 2 + j + i
-lem₁ i j = NatProp.≤⇒≤′ $ s≤s $ s≤s $ NatProp.n≤m+n j i
+lem₁ i j = ≤⇒≤′ $ s≤s $ s≤s $ n≤m+n j i
lem₂ : ∀ d x {k n} →
d + x * k ≡ x * n → d + x * (n + k) ≡ 2 * x * n
lem₂ d x {k} {n} eq = begin
- d + x * (n + k) ≡⟨ solve 4 (λ d x n k → d :+ x :* (n :+ k)
- := d :+ x :* k :+ x :* n)
- refl d x n k ⟩
+ d + x * (n + k) ≡⟨ distrib-comm₂ d x k n ⟩
d + x * k + x * n ≡⟨ cong₂ _+_ eq refl ⟩
x * n + x * n ≡⟨ solve 3 (λ x n k → x :* n :+ x :* n
:= con 2 :* x :* n)
@@ -34,10 +52,8 @@ lem₃ : ∀ d x {i k n} →
d + (1 + x + i) * k ≡ x * n →
d + (1 + x + i) * (n + k) ≡ (1 + 2 * x + i) * n
lem₃ d x {i} {k} {n} eq = begin
- d + y * (n + k) ≡⟨ solve 4 (λ d y n k → d :+ y :* (n :+ k)
- := (d :+ y :* k) :+ y :* n)
- refl d y n k ⟩
- (d + y * k) + y * n ≡⟨ cong₂ _+_ eq refl ⟩
+ d + y * (n + k) ≡⟨ distrib-comm₂ d y k n ⟩
+ d + y * k + y * n ≡⟨ cong₂ _+_ eq refl ⟩
x * n + y * n ≡⟨ solve 3 (λ x n i → x :* n :+ (con 1 :+ x :+ i) :* n
:= (con 1 :+ con 2 :* x :+ i) :* n)
refl x n i ⟩
@@ -48,19 +64,13 @@ lem₄ : ∀ d y {k i} n →
d + y * k ≡ (1 + y + i) * n →
d + y * (n + k) ≡ (1 + 2 * y + i) * n
lem₄ d y {k} {i} n eq = begin
- d + y * (n + k) ≡⟨ solve 4 (λ d y n k → d :+ y :* (n :+ k)
- := d :+ y :* k :+ y :* n)
- refl d y n k ⟩
+ d + y * (n + k) ≡⟨ distrib-comm₂ d y k n ⟩
d + y * k + y * n ≡⟨ cong₂ _+_ eq refl ⟩
(1 + y + i) * n + y * n ≡⟨ solve 3 (λ y i n → (con 1 :+ y :+ i) :* n :+ y :* n
:= (con 1 :+ con 2 :* y :+ i) :* n)
refl y i n ⟩
(1 + 2 * y + i) * n ∎
-private
- distrib-comm =
- solve 3 (λ x k n → x :* k :+ x :* n := x :* (n :+ k)) refl
-
lem₅ : ∀ d x {n k} →
d + x * n ≡ x * k →
d + 2 * x * n ≡ x * (n + k)
@@ -99,13 +109,13 @@ lem₈ : ∀ {i j k q} x y →
1 + y * j ≡ x * i → j * k ≡ q * i →
k ≡ (x * k ∸ y * q) * i
lem₈ {i} {j} {k} {q} x y eq eq′ =
- sym (NatProp.im≡jm+n⇒[i∸j]m≡n (x * k) (y * q) i k lemma)
+ sym (lem₀ (x * k) (y * q) i k lemma)
where
lemma = begin
x * k * i ≡⟨ solve 3 (λ x k i → x :* k :* i
:= x :* i :* k)
refl x k i ⟩
- x * i * k ≡⟨ cong (λ n → n * k) (sym eq) ⟩
+ x * i * k ≡⟨ cong (_* k) (sym eq) ⟩
(1 + y * j) * k ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
:= y :* (j :* k) :+ k)
refl y j k ⟩
@@ -119,7 +129,7 @@ lem₉ : ∀ {i j k q} x y →
1 + x * i ≡ y * j → j * k ≡ q * i →
k ≡ (y * q ∸ x * k) * i
lem₉ {i} {j} {k} {q} x y eq eq′ =
- sym (NatProp.im≡jm+n⇒[i∸j]m≡n (y * q) (x * k) i k lemma)
+ sym (lem₀ (y * q) (x * k) i k lemma)
where
lem = solve 3 (λ a b c → a :* b :* c := b :* c :* a) refl
lemma = begin
@@ -136,9 +146,9 @@ lem₁₀ : ∀ {a′} b c {d} e f → let a = suc a′ in
a + b * (c * d * a) ≡ e * (f * d * a) →
d ≡ 1
lem₁₀ {a′} b c {d} e f eq =
- NatProp.i*j≡1⇒j≡1 (e * f ∸ b * c) d
- (NatProp.im≡jm+n⇒[i∸j]m≡n (e * f) (b * c) d 1
- (NatProp.*-cancelʳ-≡ (e * f * d) (b * c * d + 1) (begin
+ i*j≡1⇒j≡1 (e * f ∸ b * c) d
+ (lem₀ (e * f) (b * c) d 1
+ (*-cancelʳ-≡ (e * f * d) (b * c * d + 1) (begin
e * f * d * a ≡⟨ solve 4 (λ e f d a → e :* f :* d :* a
:= e :* (f :* d :* a))
refl e f d a ⟩
@@ -153,18 +163,14 @@ lem₁₁ : ∀ {i j m n k d} x y →
1 + y * j ≡ x * i → i * k ≡ m * d → j * k ≡ n * d →
k ≡ (x * m ∸ y * n) * d
lem₁₁ {i} {j} {m} {n} {k} {d} x y eq eq₁ eq₂ =
- sym (NatProp.im≡jm+n⇒[i∸j]m≡n (x * m) (y * n) d k lemma)
- where
- assoc = solve 3 (λ x y z → x :* y :* z := x :* (y :* z)) refl
-
- lemma = begin
- x * m * d ≡⟨ assoc x m d ⟩
- x * (m * d) ≡⟨ cong (_*_ x) (sym eq₁) ⟩
- x * (i * k) ≡⟨ sym (assoc x i k) ⟩
+ sym (lem₀ (x * m) (y * n) d k (begin
+ x * m * d ≡⟨ *-assoc x m d ⟩
+ x * (m * d) ≡⟨ cong (x *_) (sym eq₁) ⟩
+ x * (i * k) ≡⟨ sym (*-assoc x i k) ⟩
x * i * k ≡⟨ cong₂ _*_ (sym eq) refl ⟩
(1 + y * j) * k ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
:= y :* (j :* k) :+ k)
refl y j k ⟩
y * (j * k) + k ≡⟨ cong (λ p → y * p + k) eq₂ ⟩
- y * (n * d) + k ≡⟨ cong₂ _+_ (sym $ assoc y n d) refl ⟩
- y * n * d + k ∎
+ y * (n * d) + k ≡⟨ cong₂ _+_ (sym $ *-assoc y n d) refl ⟩
+ y * n * d + k ∎))
diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index dfeb6c7..f3e6883 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/src/Data/Nat/InfinitelyOften.agda
@@ -6,30 +6,34 @@
module Data.Nat.InfinitelyOften where
-import Level
-open import Algebra
-open import Category.Monad
-open import Data.Empty
-open import Function
+open import Category.Monad using (RawMonad)
+open import Level using (0ℓ)
+open import Data.Empty using (⊥-elim)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod hiding (map)
open import Data.Sum hiding (map)
+open import Function
open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
-open import Relation.Nullary.Negation
-open import Relation.Unary using (_∪_; _⊆_)
-open RawMonad (¬¬-Monad {p = Level.zero})
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
+open import Relation.Unary using (Pred; _∪_; _⊆_)
+open RawMonad (¬¬-Monad {p = 0ℓ})
-- Only true finitely often.
-Fin : (ℕ → Set) → Set
+Fin : ∀ {ℓ} → Pred ℕ ℓ → Set ℓ
Fin P = ∃ λ i → ∀ j → i ≤ j → ¬ P j
+-- A non-constructive definition of "true infinitely often".
+
+Inf : ∀ {ℓ} → Pred ℕ ℓ → Set ℓ
+Inf P = ¬ Fin P
+
-- Fin is preserved by binary sums.
-_∪-Fin_ : ∀ {P Q} → Fin P → Fin Q → Fin (P ∪ Q)
-_∪-Fin_ {P} {Q} (i , ¬p) (j , ¬q) = (i ⊔ j , helper)
+_∪-Fin_ : ∀ {ℓp ℓq P Q} → Fin {ℓp} P → Fin {ℓq} Q → Fin (P ∪ Q)
+_∪-Fin_ {P = P} {Q} (i , ¬p) (j , ¬q) = (i ⊔ j , helper)
where
open ≤-Reasoning
@@ -44,11 +48,6 @@ _∪-Fin_ {P} {Q} (i , ¬p) (j , ¬q) = (i ⊔ j , helper)
i ⊔ j ≤⟨ i⊔j≤k ⟩
k ∎) q
--- A non-constructive definition of "true infinitely often".
-
-Inf : (ℕ → Set) → Set
-Inf P = ¬ Fin P
-
-- Inf commutes with binary sums (in the double-negation monad).
commutes-with-∪ : ∀ {P Q} → Inf (P ∪ Q) → ¬ ¬ (Inf P ⊎ Inf Q)
@@ -59,14 +58,14 @@ commutes-with-∪ p∪q =
-- Inf is functorial.
-map : ∀ {P Q} → P ⊆ Q → Inf P → Inf Q
+map : ∀ {ℓp ℓq P Q} → P ⊆ Q → Inf {ℓp} P → Inf {ℓq} Q
map P⊆Q ¬fin = ¬fin ∘ Prod.map id (λ fin j i≤j → fin j i≤j ∘ P⊆Q)
-- Inf is upwards closed.
-up : ∀ {P} n → Inf P → Inf (P ∘ _+_ n)
+up : ∀ {ℓ P} n → Inf {ℓ} P → Inf (P ∘ _+_ n)
up zero = id
-up {P} (suc n) = up n ∘ up₁
+up {P = P} (suc n) = up n ∘ up₁
where
up₁ : Inf P → Inf (P ∘ suc)
up₁ ¬fin (i , fin) = ¬fin (suc i , helper)
@@ -76,7 +75,7 @@ up {P} (suc n) = up n ∘ up₁
-- A witness.
-witness : ∀ {P} → Inf P → ¬ ¬ ∃ P
+witness : ∀ {ℓ P} → Inf {ℓ} P → ¬ ¬ ∃ P
witness ¬fin ¬p = ¬fin (0 , λ i _ Pi → ¬p (i , Pi))
-- Two different witnesses.
diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda
index e044d33..e0688c6 100644
--- a/src/Data/Nat/LCM.agda
+++ b/src/Data/Nat/LCM.agda
@@ -6,9 +6,10 @@
module Data.Nat.LCM where
+open import Algebra
open import Data.Nat
-import Data.Nat.Properties as NatProp
-open NatProp.SemiringSolver
+open import Data.Nat.Properties
+open import Data.Nat.Solver
open import Data.Nat.GCD
open import Data.Nat.Divisibility as Div
open import Data.Nat.Coprimality as Coprime
@@ -16,8 +17,10 @@ open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_; refl)
-open import Algebra
open import Relation.Binary
+
+open +-*-Solver
+
private
module P = Poset Div.poset
@@ -90,7 +93,7 @@ lcm .(q₁ * d) .(q₂ * d) | (d , gcd-* q₁ q₂ q₁-q₂-coprime) =
q₂∣q₃ : q₂ ∣ q₃
q₂∣q₃ = coprime-divisor (Coprime.sym q₁-q₂-coprime)
- (divides q₄ $ NatProp.*-cancelʳ-≡ _ _ (begin
+ (divides q₄ $ *-cancelʳ-≡ _ _ (begin
q₁ * q₃ * d′ ≡⟨ lem₁ q₁ q₃ d′ ⟩
q₃ * (q₁ * d′) ≡⟨ PropEq.sym eq₃ ⟩
m ≡⟨ eq₄ ⟩
diff --git a/src/Data/Nat/Literals.agda b/src/Data/Nat/Literals.agda
new file mode 100644
index 0000000..b084a3c
--- /dev/null
+++ b/src/Data/Nat/Literals.agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Natural Literals
+------------------------------------------------------------------------
+
+module Data.Nat.Literals where
+
+open import Agda.Builtin.FromNat
+open import Agda.Builtin.Nat
+open import Data.Unit
+
+number : Number Nat
+number = record
+ { Constraint = λ _ → ⊤
+ ; fromNat = λ n → n
+ }
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index b632f9e..4ab2fa6 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -6,29 +6,29 @@
module Data.Nat.Primality where
-open import Data.Empty
-open import Data.Fin as Fin hiding (_+_)
-open import Data.Fin.Dec
-open import Data.Nat
-open import Data.Nat.Divisibility
-open import Relation.Nullary
-open import Relation.Nullary.Decidable
-open import Relation.Nullary.Negation
-open import Relation.Unary
+open import Data.Empty using (⊥)
+open import Data.Fin using (Fin; toℕ)
+open import Data.Fin.Properties using (all?)
+open import Data.Nat using (ℕ; suc; _+_)
+open import Data.Nat.Divisibility using (_∤_; _∣?_)
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (from-yes)
+open import Relation.Nullary.Negation using (¬?)
+open import Relation.Unary using (Decidable)
-- Definition of primality.
Prime : ℕ → Set
Prime 0 = ⊥
Prime 1 = ⊥
-Prime (suc (suc n)) = (i : Fin n) → ¬ (2 + Fin.toℕ i ∣ 2 + n)
+Prime (suc (suc n)) = (i : Fin n) → 2 + toℕ i ∤ 2 + n
-- Decision procedure for primality.
prime? : Decidable Prime
prime? 0 = no λ()
prime? 1 = no λ()
-prime? (suc (suc n)) = all? λ _ → ¬? (_ ∣? _)
+prime? (suc (suc n)) = all? (λ _ → ¬? (_ ∣? _))
private
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index f3df5b3..9e9ebf3 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -9,24 +9,26 @@
module Data.Nat.Properties where
-open import Relation.Binary
-open import Function
open import Algebra
-import Algebra.RingSolver.Simple as Solver
-import Algebra.RingSolver.AlmostCommutativeRing as ACR
-open import Algebra.Structures
-open import Data.Nat as Nat
+open import Algebra.Morphism
+open import Function
+open import Function.Injection using (_↣_)
+open import Data.Nat.Base
open import Data.Product
open import Data.Sum
+open import Level using (0ℓ)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
+open import Relation.Nullary.Decidable using (via-injection; map′)
open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.PropositionalEquality
+
open import Algebra.FunctionProperties (_≡_ {A = ℕ})
hiding (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.FunctionProperties
using (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.FunctionProperties.Consequences (setoid ℕ)
-
+open import Algebra.Structures (_≡_ {A = ℕ})
open ≡-Reasoning
------------------------------------------------------------------------
@@ -35,13 +37,23 @@ open ≡-Reasoning
suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
suc-injective refl = refl
+infix 4 _≟_
+
+_≟_ : Decidable {A = ℕ} _≡_
+zero ≟ zero = yes refl
+zero ≟ suc n = no λ()
+suc m ≟ zero = no λ()
+suc m ≟ suc n with m ≟ n
+... | yes refl = yes refl
+... | no m≢n = no (m≢n ∘ suc-injective)
+
≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
≡-isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_ = _≟_
}
-≡-decSetoid : DecSetoid _ _
+≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = record
{ Carrier = ℕ
; _≈_ = _≡_
@@ -51,6 +63,9 @@ suc-injective refl = refl
------------------------------------------------------------------------
-- Properties of _≤_
+≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
+≤-pred (s≤s m≤n) = m≤n
+
-- Relation-theoretic properties of _≤_
≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive {zero} refl = z≤n
@@ -75,6 +90,18 @@ suc-injective refl = refl
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ n≤m = inj₂ (s≤s n≤m)
+infix 4 _≤?_ _≥?_
+
+_≤?_ : Decidable _≤_
+zero ≤? _ = yes z≤n
+suc m ≤? zero = no λ()
+suc m ≤? suc n with m ≤? n
+... | yes m≤n = yes (s≤s m≤n)
+... | no m≰n = no (m≰n ∘ ≤-pred)
+
+_≥?_ : Decidable _≥_
+_≥?_ = flip _≤?_
+
≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
{ isEquivalence = isEquivalence
@@ -82,7 +109,7 @@ suc-injective refl = refl
; trans = ≤-trans
}
-≤-preorder : Preorder _ _ _
+≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
≤-preorder = record
{ isPreorder = ≤-isPreorder
}
@@ -93,13 +120,18 @@ suc-injective refl = refl
; antisym = ≤-antisym
}
+≤-poset : Poset 0ℓ 0ℓ 0ℓ
+≤-poset = record
+ { isPartialOrder = ≤-isPartialOrder
+ }
+
≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
{ isPartialOrder = ≤-isPartialOrder
; total = ≤-total
}
-≤-totalOrder : TotalOrder _ _ _
+≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record
{ isTotalOrder = ≤-isTotalOrder
}
@@ -111,12 +143,19 @@ suc-injective refl = refl
; _≤?_ = _≤?_
}
-≤-decTotalOrder : DecTotalOrder _ _ _
+≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
{ isDecTotalOrder = ≤-isDecTotalOrder
}
-- Other properties of _≤_
+s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
+s≤s-injective refl = refl
+
+≤-irrelevance : Irrelevant _≤_
+≤-irrelevance z≤n z≤n = refl
+≤-irrelevance (s≤s m≤n₁) (s≤s m≤n₂) = cong s≤s (≤-irrelevance m≤n₁ m≤n₂)
+
≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
≤-step z≤n = z≤n
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)
@@ -124,9 +163,12 @@ suc-injective refl = refl
n≤1+n : ∀ n → n ≤ 1 + n
n≤1+n _ = ≤-step ≤-refl
-1+n≰n : ∀ {n} → ¬ 1 + n ≤ n
+1+n≰n : ∀ {n} → 1 + n ≰ n
1+n≰n (s≤s le) = 1+n≰n le
+n≤0⇒n≡0 : ∀ {n} → n ≤ 0 → n ≡ 0
+n≤0⇒n≡0 z≤n = refl
+
pred-mono : pred Preserves _≤_ ⟶ _≤_
pred-mono z≤n = z≤n
pred-mono (s≤s le) = le
@@ -143,8 +185,6 @@ pred-mono (s≤s le) = le
-- Properties of _<_
-- Relation theoretic properties of _<_
-_<?_ : Decidable _<_
-x <? y = suc x ≤? y
<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl (s≤s n<n) = <-irrefl refl n<n
@@ -170,6 +210,30 @@ x <? y = suc x ≤? y
... | tri≈ ≰ ≡ ≱ = tri≈ (≰ ∘ ≤-pred) (cong suc ≡) (≱ ∘ ≤-pred)
... | tri> ≰ ≢ ≥ = tri> (≰ ∘ ≤-pred) (≢ ∘ suc-injective) (s≤s ≥)
+infix 4 _<?_ _>?_
+
+_<?_ : Decidable _<_
+x <? y = suc x ≤? y
+
+_>?_ : Decidable _>_
+_>?_ = flip _<?_
+
+<-resp₂-≡ : _<_ Respects₂ _≡_
+<-resp₂-≡ = subst (_ <_) , subst (_< _)
+
+<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
+<-isStrictPartialOrder = record
+ { isEquivalence = isEquivalence
+ ; irrefl = <-irrefl
+ ; trans = <-trans
+ ; <-resp-≈ = <-resp₂-≡
+ }
+
+<-strictPartialOrder : StrictPartialOrder 0ℓ 0ℓ 0ℓ
+<-strictPartialOrder = record
+ { isStrictPartialOrder = <-isStrictPartialOrder
+ }
+
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
{ isEquivalence = isEquivalence
@@ -177,12 +241,15 @@ x <? y = suc x ≤? y
; compare = <-cmp
}
-<-strictTotalOrder : StrictTotalOrder _ _ _
+<-strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
<-strictTotalOrder = record
{ isStrictTotalOrder = <-isStrictTotalOrder
}
-- Other properties of _<_
+<-irrelevance : Irrelevant _<_
+<-irrelevance = ≤-irrelevance
+
<⇒≤pred : ∀ {m n} → m < n → m ≤ pred n
<⇒≤pred (s≤s le) = le
@@ -192,6 +259,10 @@ x <? y = suc x ≤? y
<⇒≢ : _<_ ⇒ _≢_
<⇒≢ m<n refl = 1+n≰n m<n
+≤⇒≯ : _≤_ ⇒ _≯_
+≤⇒≯ z≤n ()
+≤⇒≯ (s≤s m≤n) (s≤s n≤m) = ≤⇒≯ m≤n n≤m
+
<⇒≱ : _<_ ⇒ _≱_
<⇒≱ (s≤s m+1≤n) (s≤s n≤m) = <⇒≱ m+1≤n n≤m
@@ -214,11 +285,17 @@ x <? y = suc x ≤? y
≮⇒≥ {zero} {suc j} 1≮j+1 = contradiction (s≤s z≤n) 1≮j+1
≮⇒≥ {suc i} {suc j} i+1≮j+1 = s≤s (≮⇒≥ (i+1≮j+1 ∘ s≤s))
-≤+≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
-≤+≢⇒< {_} {zero} z≤n m≢n = contradiction refl m≢n
-≤+≢⇒< {_} {suc n} z≤n m≢n = s≤s z≤n
-≤+≢⇒< {_} {suc n} (s≤s m≤n) 1+m≢1+n =
- s≤s (≤+≢⇒< m≤n (1+m≢1+n ∘ cong suc))
+≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
+≤∧≢⇒< {_} {zero} z≤n m≢n = contradiction refl m≢n
+≤∧≢⇒< {_} {suc n} z≤n m≢n = s≤s z≤n
+≤∧≢⇒< {_} {suc n} (s≤s m≤n) 1+m≢1+n =
+ s≤s (≤∧≢⇒< m≤n (1+m≢1+n ∘ cong suc))
+
+n≮n : ∀ n → n ≮ n
+n≮n n = <-irrefl (refl {x = n})
+
+m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
+m<n⇒n≢0 (s≤s m≤n) ()
------------------------------------------------------------------------
-- Properties of _≤′_
@@ -239,6 +316,25 @@ s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
≤⇒≤′ z≤n = z≤′n
≤⇒≤′ (s≤s m≤n) = s≤′s (≤⇒≤′ m≤n)
+≤′-step-injective : ∀ {m n} {p q : m ≤′ n} → ≤′-step p ≡ ≤′-step q → p ≡ q
+≤′-step-injective refl = refl
+
+-- Decidablity for _≤'_
+
+infix 4 _≤′?_ _<′?_ _≥′?_ _>′?_
+
+_≤′?_ : Decidable _≤′_
+x ≤′? y = map′ ≤⇒≤′ ≤′⇒≤ (x ≤? y)
+
+_<′?_ : Decidable _<′_
+x <′? y = suc x ≤′? y
+
+_≥′?_ : Decidable _≥′_
+_≥′?_ = flip _≤′?_
+
+_>′?_ : Decidable _>′_
+_>′?_ = flip _<′?_
+
------------------------------------------------------------------------
-- Properties of _≤″_
@@ -259,6 +355,22 @@ s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
proof z≤n = refl
proof (s≤s m≤n) = cong suc (proof m≤n)
+-- Decidablity for _≤″_
+
+infix 4 _≤″?_ _<″?_ _≥″?_ _>″?_
+
+_≤″?_ : Decidable _≤″_
+x ≤″? y = map′ ≤⇒≤″ ≤″⇒≤ (x ≤? y)
+
+_<″?_ : Decidable _<″_
+x <″? y = suc x ≤″? y
+
+_≥″?_ : Decidable _≥″_
+_≥″?_ = flip _≤″?_
+
+_>″?_ : Decidable _>″_
+_>″?_ = flip _<″?_
+
------------------------------------------------------------------------
-- Properties of _+_
@@ -289,20 +401,41 @@ s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)
suc (n + m) ≡⟨ sym (+-suc n m) ⟩
n + suc m ∎
-+-isSemigroup : IsSemigroup _≡_ _+_
++-isSemigroup : IsSemigroup _+_
+-isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = +-assoc
; ∙-cong = cong₂ _+_
}
-+-0-isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ 0
++-semigroup : Semigroup 0ℓ 0ℓ
++-semigroup = record
+ { isSemigroup = +-isSemigroup
+ }
+
++-0-isMonoid : IsMonoid _+_ 0
++-0-isMonoid = record
+ { isSemigroup = +-isSemigroup
+ ; identity = +-identity
+ }
+
++-0-monoid : Monoid 0ℓ 0ℓ
++-0-monoid = record
+ { isMonoid = +-0-isMonoid
+ }
+
++-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0
+-0-isCommutativeMonoid = record
{ isSemigroup = +-isSemigroup
; identityˡ = +-identityˡ
; comm = +-comm
}
++-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
++-0-commutativeMonoid = record
+ { isCommutativeMonoid = +-0-isCommutativeMonoid
+ }
+
-- Other properties of _+_ and _≡_
+-cancelˡ-≡ : LeftCancellative _≡_ _+_
@@ -343,6 +476,13 @@ i+j≡0⇒j≡0 i {j} i+j≡0 = i+j≡0⇒i≡0 j (trans (+-comm j i) (i+j≡0))
+-cancel-≤ : Cancellative _≤_ _+_
+-cancel-≤ = +-cancelˡ-≤ , +-cancelʳ-≤
+≤-stepsˡ : ∀ {m n} o → m ≤ n → m ≤ o + n
+≤-stepsˡ zero m≤n = m≤n
+≤-stepsˡ (suc o) m≤n = ≤-step (≤-stepsˡ o m≤n)
+
+≤-stepsʳ : ∀ {m n} o → m ≤ n → m ≤ n + o
+≤-stepsʳ {m} o m≤n = subst (m ≤_) (+-comm o _) (≤-stepsˡ o m≤n)
+
m≤m+n : ∀ m n → m ≤ m + n
m≤m+n zero n = z≤n
m≤m+n (suc m) n = s≤s (m≤m+n m n)
@@ -351,10 +491,6 @@ n≤m+n : ∀ m n → n ≤ m + n
n≤m+n m zero = z≤n
n≤m+n m (suc n) = subst (suc n ≤_) (sym (+-suc m n)) (s≤s (n≤m+n m n))
-≤-steps : ∀ {m n} k → m ≤ n → m ≤ k + n
-≤-steps zero m≤n = m≤n
-≤-steps (suc k) m≤n = ≤-step (≤-steps k m≤n)
-
m+n≤o⇒m≤o : ∀ m {n o} → m + n ≤ o → m ≤ o
m+n≤o⇒m≤o zero m+n≤o = z≤n
m+n≤o⇒m≤o (suc m) (s≤s m+n≤o) = s≤s (m+n≤o⇒m≤o m m+n≤o)
@@ -367,25 +503,41 @@ m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
+-mono-≤ {_} {m} z≤n o≤p = ≤-trans o≤p (n≤m+n m _)
+-mono-≤ {_} {_} (s≤s m≤n) o≤p = s≤s (+-mono-≤ m≤n o≤p)
-+-monoˡ-< : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
-+-monoˡ-< {_} {suc y} (s≤s z≤n) u≤v = s≤s (≤-steps y u≤v)
-+-monoˡ-< {_} {_} (s≤s (s≤s x<y)) u≤v = s≤s (+-monoˡ-< (s≤s x<y) u≤v)
++-monoˡ-≤ : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
++-monoˡ-≤ n m≤o = +-mono-≤ m≤o (≤-refl {n})
+
++-monoʳ-≤ : ∀ n → (n +_) Preserves _≤_ ⟶ _≤_
++-monoʳ-≤ n m≤o = +-mono-≤ (≤-refl {n}) m≤o
-+-monoʳ-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
-+-monoʳ-< {_} {y} z≤n u<v = ≤-trans u<v (n≤m+n y _)
-+-monoʳ-< {_} {_} (s≤s x≤y) u<v = s≤s (+-monoʳ-< x≤y u<v)
++-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
++-mono-<-≤ {_} {suc y} (s≤s z≤n) u≤v = s≤s (≤-stepsˡ y u≤v)
++-mono-<-≤ {_} {_} (s≤s (s≤s x<y)) u≤v = s≤s (+-mono-<-≤ (s≤s x<y) u≤v)
+
++-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
++-mono-≤-< {_} {y} z≤n u<v = ≤-trans u<v (n≤m+n y _)
++-mono-≤-< {_} {_} (s≤s x≤y) u<v = s≤s (+-mono-≤-< x≤y u<v)
+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
-+-mono-< x≤y = +-monoʳ-< (<⇒≤ x≤y)
++-mono-< x≤y = +-mono-≤-< (<⇒≤ x≤y)
+
++-monoˡ-< : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
++-monoˡ-< n = +-monoˡ-≤ n
-¬i+1+j≤i : ∀ i {j} → i + suc j ≰ i
-¬i+1+j≤i zero ()
-¬i+1+j≤i (suc i) le = ¬i+1+j≤i i (≤-pred le)
++-monoʳ-< : ∀ n → (n +_) Preserves _<_ ⟶ _<_
++-monoʳ-< zero m≤o = m≤o
++-monoʳ-< (suc n) m≤o = s≤s (+-monoʳ-< n m≤o)
+
+i+1+j≰i : ∀ i {j} → i + suc j ≰ i
+i+1+j≰i zero ()
+i+1+j≰i (suc i) le = i+1+j≰i i (≤-pred le)
m+n≮n : ∀ m n → m + n ≮ n
-m+n≮n zero n = <-irrefl refl
+m+n≮n zero n = n≮n n
m+n≮n (suc m) (suc n) (s≤s m+n<n) = m+n≮n m (suc n) (≤-step m+n<n)
+m+n≮m : ∀ m n → m + n ≮ m
+m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
+
m≤′m+n : ∀ m n → m ≤′ m + n
m≤′m+n m n = ≤⇒≤′ (m≤m+n m n)
@@ -460,21 +612,56 @@ n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)
n * o + m * (n * o) ≡⟨⟩
suc m * (n * o) ∎
-*-isSemigroup : IsSemigroup _≡_ _*_
+*-isSemigroup : IsSemigroup _*_
*-isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = *-assoc
; ∙-cong = cong₂ _*_
}
-*-1-isCommutativeMonoid : IsCommutativeMonoid _≡_ _*_ 1
+*-semigroup : Semigroup 0ℓ 0ℓ
+*-semigroup = record
+ { isSemigroup = *-isSemigroup
+ }
+
+*-1-isMonoid : IsMonoid _*_ 1
+*-1-isMonoid = record
+ { isSemigroup = *-isSemigroup
+ ; identity = *-identity
+ }
+
+*-1-monoid : Monoid 0ℓ 0ℓ
+*-1-monoid = record
+ { isMonoid = *-1-isMonoid
+ }
+
+*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1
*-1-isCommutativeMonoid = record
{ isSemigroup = *-isSemigroup
; identityˡ = *-identityˡ
; comm = *-comm
}
-*-+-isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ 0 1
+*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+*-1-commutativeMonoid = record
+ { isCommutativeMonoid = *-1-isCommutativeMonoid
+ }
+
+*-+-isSemiring : IsSemiring _+_ _*_ 0 1
+*-+-isSemiring = record
+ { isSemiringWithoutAnnihilatingZero = record
+ { +-isCommutativeMonoid = +-0-isCommutativeMonoid
+ ; *-isMonoid = *-1-isMonoid
+ ; distrib = *-distrib-+ }
+ ; zero = *-zero
+ }
+
+*-+-semiring : Semiring 0ℓ 0ℓ
+*-+-semiring = record
+ { isSemiring = *-+-isSemiring
+ }
+
+*-+-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ 0 1
*-+-isCommutativeSemiring = record
{ +-isCommutativeMonoid = +-0-isCommutativeMonoid
; *-isCommutativeMonoid = *-1-isCommutativeMonoid
@@ -482,7 +669,7 @@ n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)
; zeroˡ = *-zeroˡ
}
-*-+-commutativeSemiring : CommutativeSemiring _ _
+*-+-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
*-+-commutativeSemiring = record
{ isCommutativeSemiring = *-+-isCommutativeSemiring
}
@@ -511,7 +698,7 @@ i*j≡1⇒i≡1 zero j ()
i*j≡1⇒i≡1 (suc (suc i)) (suc (suc j)) ()
i*j≡1⇒i≡1 (suc (suc i)) (suc zero) ()
i*j≡1⇒i≡1 (suc (suc i)) zero eq =
- contradiction (trans (*-comm 0 i) eq) λ()
+ contradiction (trans (sym $ *-zeroʳ i) eq) λ()
i*j≡1⇒j≡1 : ∀ i j → i * j ≡ 1 → j ≡ 1
i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (trans (*-comm j i) eq)
@@ -526,6 +713,12 @@ i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (trans (*-comm j i) eq)
*-mono-≤ z≤n _ = z≤n
*-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
+*-monoˡ-≤ : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_
+*-monoˡ-≤ n m≤o = *-mono-≤ m≤o (≤-refl {n})
+
+*-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
+*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o
+
*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
*-mono-< (s≤s z≤n) (s≤s u≤v) = s≤s z≤n
*-mono-< (s≤s (s≤s m≤n)) (s≤s u≤v) =
@@ -534,7 +727,7 @@ i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (trans (*-comm j i) eq)
*-monoˡ-< : ∀ n → (_* suc n) Preserves _<_ ⟶ _<_
*-monoˡ-< n (s≤s z≤n) = s≤s z≤n
*-monoˡ-< n (s≤s (s≤s m≤o)) =
- +-monoʳ-< (≤-refl {suc n}) (*-monoˡ-< n (s≤s m≤o))
+ +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< n (s≤s m≤o))
*-monoʳ-< : ∀ n → (suc n *_) Preserves _<_ ⟶ _<_
*-monoʳ-< zero (s≤s m≤o) = +-mono-≤ (s≤s m≤o) z≤n
@@ -544,6 +737,18 @@ i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (trans (*-comm j i) eq)
------------------------------------------------------------------------
-- Properties of _^_
+^-identityʳ : RightIdentity 1 _^_
+^-identityʳ zero = refl
+^-identityʳ (suc x) = cong suc (^-identityʳ x)
+
+^-zeroˡ : LeftZero 1 _^_
+^-zeroˡ zero = refl
+^-zeroˡ (suc e) = begin
+ 1 ^ suc e ≡⟨⟩
+ 1 * (1 ^ e) ≡⟨ *-identityˡ (1 ^ e) ⟩
+ 1 ^ e ≡⟨ ^-zeroˡ e ⟩
+ 1 ∎
+
^-distribˡ-+-* : ∀ m n p → m ^ (n + p) ≡ m ^ n * m ^ p
^-distribˡ-+-* m zero p = sym (+-identityʳ (m ^ p))
^-distribˡ-+-* m (suc n) p = begin
@@ -551,6 +756,29 @@ i*j≡1⇒j≡1 i j eq = i*j≡1⇒i≡1 j i (trans (*-comm j i) eq)
m * ((m ^ n) * (m ^ p)) ≡⟨ sym (*-assoc m _ _) ⟩
(m * (m ^ n)) * (m ^ p) ∎
+^-semigroup-morphism : ∀ {n} → (n ^_) Is +-semigroup -Semigroup⟶ *-semigroup
+^-semigroup-morphism = record
+ { ⟦⟧-cong = cong (_ ^_)
+ ; ∙-homo = ^-distribˡ-+-* _
+ }
+
+^-monoid-morphism : ∀ {n} → (n ^_) Is +-0-monoid -Monoid⟶ *-1-monoid
+^-monoid-morphism = record
+ { sm-homo = ^-semigroup-morphism
+ ; ε-homo = refl
+ }
+
+^-*-assoc : ∀ m n p → (m ^ n) ^ p ≡ m ^ (n * p)
+^-*-assoc m n zero = begin
+ 1 ≡⟨⟩
+ m ^ 0 ≡⟨ cong (m ^_) (sym $ *-zeroʳ n) ⟩
+ m ^ (n * 0) ∎
+^-*-assoc m n (suc p) = begin
+ (m ^ n) * ((m ^ n) ^ p) ≡⟨ cong ((m ^ n) *_) (^-*-assoc m n p) ⟩
+ (m ^ n) * (m ^ (n * p)) ≡⟨ sym (^-distribˡ-+-* m n (n * p)) ⟩
+ m ^ (n + n * p) ≡⟨ cong (m ^_) (sym (+-*-suc n p)) ⟩
+ m ^ (n * (suc p)) ∎
+
i^j≡0⇒i≡0 : ∀ i j → i ^ j ≡ 0 → i ≡ 0
i^j≡0⇒i≡0 i zero ()
i^j≡0⇒i≡0 i (suc j) eq = [ id , i^j≡0⇒i≡0 i j ]′ (i*j≡0⇒i≡0∨j≡0 i eq)
@@ -656,28 +884,43 @@ i^j≡1⇒j≡0∨i≡1 i (suc j) eq = inj₂ (i*j≡1⇒i≡1 i (i ^ j) eq)
⊓-⊔-absorptive : Absorptive _⊓_ _⊔_
⊓-⊔-absorptive = ⊓-abs-⊔ , ⊔-abs-⊓
-⊔-isSemigroup : IsSemigroup _≡_ _⊔_
+⊔-isSemigroup : IsSemigroup _⊔_
⊔-isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = ⊔-assoc
; ∙-cong = cong₂ _⊔_
}
-⊔-0-isCommutativeMonoid : IsCommutativeMonoid _≡_ _⊔_ 0
+⊔-semigroup : Semigroup 0ℓ 0ℓ
+⊔-semigroup = record
+ { isSemigroup = ⊔-isSemigroup
+ }
+
+⊔-0-isCommutativeMonoid : IsCommutativeMonoid _⊔_ 0
⊔-0-isCommutativeMonoid = record
{ isSemigroup = ⊔-isSemigroup
- ; identityˡ = ⊔-identityˡ
+ ; identityˡ = ⊔-identityˡ
; comm = ⊔-comm
}
-⊓-isSemigroup : IsSemigroup _≡_ _⊓_
+⊔-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+⊔-0-commutativeMonoid = record
+ { isCommutativeMonoid = ⊔-0-isCommutativeMonoid
+ }
+
+⊓-isSemigroup : IsSemigroup _⊓_
⊓-isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = ⊓-assoc
; ∙-cong = cong₂ _⊓_
}
-⊔-⊓-isSemiringWithoutOne : IsSemiringWithoutOne _≡_ _⊔_ _⊓_ 0
+⊓-semigroup : Semigroup 0ℓ 0ℓ
+⊓-semigroup = record
+ { isSemigroup = ⊔-isSemigroup
+ }
+
+⊔-⊓-isSemiringWithoutOne : IsSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isSemiringWithoutOne = record
{ +-isCommutativeMonoid = ⊔-0-isCommutativeMonoid
; *-isSemigroup = ⊓-isSemigroup
@@ -686,19 +929,19 @@ i^j≡1⇒j≡0∨i≡1 i (suc j) eq = inj₂ (i*j≡1⇒i≡1 i (i ^ j) eq)
}
⊔-⊓-isCommutativeSemiringWithoutOne
- : IsCommutativeSemiringWithoutOne _≡_ _⊔_ _⊓_ 0
+ : IsCommutativeSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isCommutativeSemiringWithoutOne = record
{ isSemiringWithoutOne = ⊔-⊓-isSemiringWithoutOne
; *-comm = ⊓-comm
}
-⊔-⊓-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
+⊔-⊓-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne 0ℓ 0ℓ
⊔-⊓-commutativeSemiringWithoutOne = record
{ isCommutativeSemiringWithoutOne =
⊔-⊓-isCommutativeSemiringWithoutOne
}
-⊓-⊔-isLattice : IsLattice _≡_ _⊓_ _⊔_
+⊓-⊔-isLattice : IsLattice _⊓_ _⊔_
⊓-⊔-isLattice = record
{ isEquivalence = isEquivalence
; ∨-comm = ⊓-comm
@@ -710,13 +953,18 @@ i^j≡1⇒j≡0∨i≡1 i (suc j) eq = inj₂ (i*j≡1⇒i≡1 i (i ^ j) eq)
; absorptive = ⊓-⊔-absorptive
}
-⊓-⊔-isDistributiveLattice : IsDistributiveLattice _≡_ _⊓_ _⊔_
+⊓-⊔-lattice : Lattice 0ℓ 0ℓ
+⊓-⊔-lattice = record
+ { isLattice = ⊓-⊔-isLattice
+ }
+
+⊓-⊔-isDistributiveLattice : IsDistributiveLattice _⊓_ _⊔_
⊓-⊔-isDistributiveLattice = record
{ isLattice = ⊓-⊔-isLattice
; ∨-∧-distribʳ = ⊓-distribʳ-⊔
}
-⊓-⊔-distributiveLattice : DistributiveLattice _ _
+⊓-⊔-distributiveLattice : DistributiveLattice 0ℓ 0ℓ
⊓-⊔-distributiveLattice = record
{ isDistributiveLattice = ⊓-⊔-isDistributiveLattice
}
@@ -743,11 +991,43 @@ m⊓n≤m⊔n zero n = ≤-refl
m⊓n≤m⊔n (suc m) zero = ≤-refl
m⊓n≤m⊔n (suc m) (suc n) = s≤s (m⊓n≤m⊔n m n)
+m≤n⇒m⊓n≡m : ∀ {m n} → m ≤ n → m ⊓ n ≡ m
+m≤n⇒m⊓n≡m z≤n = refl
+m≤n⇒m⊓n≡m (s≤s m≤n) = cong suc (m≤n⇒m⊓n≡m m≤n)
+
+m≤n⇒n⊓m≡m : ∀ {m n} → m ≤ n → n ⊓ m ≡ m
+m≤n⇒n⊓m≡m {m} m≤n = trans (⊓-comm _ m) (m≤n⇒m⊓n≡m m≤n)
+
+m⊓n≡m⇒m≤n : ∀ {m n} → m ⊓ n ≡ m → m ≤ n
+m⊓n≡m⇒m≤n m⊓n≡m = subst (_≤ _) m⊓n≡m (m⊓n≤n _ _)
+
+m⊓n≡n⇒n≤m : ∀ {m n} → m ⊓ n ≡ n → n ≤ m
+m⊓n≡n⇒n≤m m⊓n≡n = subst (_≤ _) m⊓n≡n (m⊓n≤m _ _)
+
+m≤n⇒n⊔m≡n : ∀ {m n} → m ≤ n → n ⊔ m ≡ n
+m≤n⇒n⊔m≡n z≤n = ⊔-identityʳ _
+m≤n⇒n⊔m≡n (s≤s m≤n) = cong suc (m≤n⇒n⊔m≡n m≤n)
+
+m≤n⇒m⊔n≡n : ∀ {m n} → m ≤ n → m ⊔ n ≡ n
+m≤n⇒m⊔n≡n {m} m≤n = trans (⊔-comm m _) (m≤n⇒n⊔m≡n m≤n)
+
+n⊔m≡m⇒n≤m : ∀ {m n} → n ⊔ m ≡ m → n ≤ m
+n⊔m≡m⇒n≤m n⊔m≡m = subst (_ ≤_) n⊔m≡m (m≤m⊔n _ _)
+
+n⊔m≡n⇒m≤n : ∀ {m n} → n ⊔ m ≡ n → m ≤ n
+n⊔m≡n⇒m≤n n⊔m≡n = subst (_ ≤_) n⊔m≡n (n≤m⊔n _ _)
+
⊔-mono-≤ : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
⊔-mono-≤ {x} {y} {u} {v} x≤y u≤v with ⊔-sel x u
... | inj₁ x⊔u≡x rewrite x⊔u≡x = ≤-trans x≤y (m≤m⊔n y v)
... | inj₂ x⊔u≡u rewrite x⊔u≡u = ≤-trans u≤v (n≤m⊔n y v)
+⊔-monoˡ-≤ : ∀ n → (_⊔ n) Preserves _≤_ ⟶ _≤_
+⊔-monoˡ-≤ n m≤o = ⊔-mono-≤ m≤o (≤-refl {n})
+
+⊔-monoʳ-≤ : ∀ n → (n ⊔_) Preserves _≤_ ⟶ _≤_
+⊔-monoʳ-≤ n m≤o = ⊔-mono-≤ (≤-refl {n}) m≤o
+
⊔-mono-< : _⊔_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊔-mono-< = ⊔-mono-≤
@@ -756,6 +1036,12 @@ m⊓n≤m⊔n (suc m) (suc n) = s≤s (m⊓n≤m⊔n m n)
... | inj₁ y⊓v≡y rewrite y⊓v≡y = ≤-trans (m⊓n≤m x u) x≤y
... | inj₂ y⊓v≡v rewrite y⊓v≡v = ≤-trans (m⊓n≤n x u) u≤v
+⊓-monoˡ-≤ : ∀ n → (_⊓ n) Preserves _≤_ ⟶ _≤_
+⊓-monoˡ-≤ n m≤o = ⊓-mono-≤ m≤o (≤-refl {n})
+
+⊓-monoʳ-≤ : ∀ n → (n ⊓_) Preserves _≤_ ⟶ _≤_
+⊓-monoʳ-≤ n m≤o = ⊓-mono-≤ (≤-refl {n}) m≤o
+
⊓-mono-< : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊓-mono-< = ⊓-mono-≤
@@ -790,6 +1076,23 @@ m⊓n≤m+n m n with ⊓-sel m n
+-distrib-⊓ : _+_ DistributesOver _⊓_
+-distrib-⊓ = +-distribˡ-⊓ , +-distribʳ-⊓
+-- Other properties
+⊓-triangulate : ∀ x y z → x ⊓ y ⊓ z ≡ (x ⊓ y) ⊓ (y ⊓ z)
+⊓-triangulate x y z = begin
+ x ⊓ y ⊓ z ≡⟨ cong (λ v → x ⊓ v ⊓ z) (sym (⊓-idem y)) ⟩
+ x ⊓ (y ⊓ y) ⊓ z ≡⟨ ⊓-assoc x _ _ ⟩
+ x ⊓ ((y ⊓ y) ⊓ z) ≡⟨ cong (x ⊓_) (⊓-assoc y _ _) ⟩
+ x ⊓ (y ⊓ (y ⊓ z)) ≡⟨ sym (⊓-assoc x _ _) ⟩
+ (x ⊓ y) ⊓ (y ⊓ z) ∎
+
+⊔-triangulate : ∀ x y z → x ⊔ y ⊔ z ≡ (x ⊔ y) ⊔ (y ⊔ z)
+⊔-triangulate x y z = begin
+ x ⊔ y ⊔ z ≡⟨ cong (λ v → x ⊔ v ⊔ z) (sym (⊔-idem y)) ⟩
+ x ⊔ (y ⊔ y) ⊔ z ≡⟨ ⊔-assoc x _ _ ⟩
+ x ⊔ ((y ⊔ y) ⊔ z) ≡⟨ cong (x ⊔_) (⊔-assoc y _ _) ⟩
+ x ⊔ (y ⊔ (y ⊔ z)) ≡⟨ sym (⊔-assoc x _ _) ⟩
+ (x ⊔ y) ⊔ (y ⊔ z) ∎
+
------------------------------------------------------------------------
-- Properties of _∸_
@@ -801,6 +1104,38 @@ n∸n≡0 : ∀ n → n ∸ n ≡ 0
n∸n≡0 zero = refl
n∸n≡0 (suc n) = n∸n≡0 n
+-- Ordering properties of _∸_
+n∸m≤n : ∀ m n → n ∸ m ≤ n
+n∸m≤n zero n = ≤-refl
+n∸m≤n (suc m) zero = ≤-refl
+n∸m≤n (suc m) (suc n) = ≤-trans (n∸m≤n m n) (n≤1+n n)
+
+m≮m∸n : ∀ m n → m ≮ m ∸ n
+m≮m∸n zero (suc n) ()
+m≮m∸n m zero = n≮n m
+m≮m∸n (suc m) (suc n) = m≮m∸n m n ∘ ≤-trans (n≤1+n (suc m))
+
+∸-mono : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
+∸-mono z≤n (s≤s n₁≥n₂) = z≤n
+∸-mono (s≤s m₁≤m₂) (s≤s n₁≥n₂) = ∸-mono m₁≤m₂ n₁≥n₂
+∸-mono m₁≤m₂ (z≤n {n = n₁}) = ≤-trans (n∸m≤n n₁ _) m₁≤m₂
+
+∸-monoˡ-≤ : ∀ {m n} o → m ≤ n → m ∸ o ≤ n ∸ o
+∸-monoˡ-≤ o m≤n = ∸-mono {u = o} m≤n ≤-refl
+
+∸-monoʳ-≤ : ∀ {m n} o → m ≤ n → o ∸ m ≥ o ∸ n
+∸-monoʳ-≤ _ m≤n = ∸-mono ≤-refl m≤n
+
+m∸n≡0⇒m≤n : ∀ {m n} → m ∸ n ≡ 0 → m ≤ n
+m∸n≡0⇒m≤n {zero} {_} _ = z≤n
+m∸n≡0⇒m≤n {suc m} {zero} ()
+m∸n≡0⇒m≤n {suc m} {suc n} eq = s≤s (m∸n≡0⇒m≤n eq)
+
+m≤n⇒m∸n≡0 : ∀ {m n} → m ≤ n → m ∸ n ≡ 0
+m≤n⇒m∸n≡0 {n = n} z≤n = 0∸n≡0 n
+m≤n⇒m∸n≡0 {_} (s≤s m≤n) = m≤n⇒m∸n≡0 m≤n
+
+-- Properties of _∸_ and _+_
+-∸-comm : ∀ {m} n {o} → o ≤ m → (m + n) ∸ o ≡ (m ∸ o) + n
+-∸-comm {zero} _ {suc o} ()
+-∸-comm {zero} _ {zero} _ = refl
@@ -822,11 +1157,6 @@ n∸n≡0 (suc n) = n∸n≡0 n
(m + n) ∸ o ≡⟨ +-∸-assoc m o≤n ⟩
m + (n ∸ o) ∎
-n∸m≤n : ∀ m n → n ∸ m ≤ n
-n∸m≤n zero n = ≤-refl
-n∸m≤n (suc m) zero = ≤-refl
-n∸m≤n (suc m) (suc n) = ≤-trans (n∸m≤n m n) (n≤1+n n)
-
n≤m+n∸m : ∀ m n → n ≤ m + (n ∸ m)
n≤m+n∸m m zero = z≤n
n≤m+n∸m zero (suc n) = ≤-refl
@@ -846,6 +1176,41 @@ m+n∸m≡n {m} {n} m≤n = begin
(n + m) ∸ m ≡⟨ m+n∸n≡m n m ⟩
n ∎
+m∸n+n≡m : ∀ {m n} → n ≤ m → (m ∸ n) + n ≡ m
+m∸n+n≡m {m} {n} n≤m = begin
+ (m ∸ n) + n ≡⟨ sym (+-∸-comm n n≤m) ⟩
+ (m + n) ∸ n ≡⟨ m+n∸n≡m m n ⟩
+ m ∎
+
+m∸[m∸n]≡n : ∀ {m n} → n ≤ m → m ∸ (m ∸ n) ≡ n
+m∸[m∸n]≡n {m} {_} z≤n = n∸n≡0 m
+m∸[m∸n]≡n {suc m} {suc n} (s≤s n≤m) = begin
+ suc m ∸ (m ∸ n) ≡⟨ +-∸-assoc 1 (n∸m≤n n m) ⟩
+ suc (m ∸ (m ∸ n)) ≡⟨ cong suc (m∸[m∸n]≡n n≤m) ⟩
+ suc n ∎
+
+[i+j]∸[i+k]≡j∸k : ∀ i j k → (i + j) ∸ (i + k) ≡ j ∸ k
+[i+j]∸[i+k]≡j∸k zero j k = refl
+[i+j]∸[i+k]≡j∸k (suc i) j k = [i+j]∸[i+k]≡j∸k i j k
+
+-- Properties of _∸_ and _*_
+*-distribʳ-∸ : _*_ DistributesOverʳ _∸_
+*-distribʳ-∸ i zero zero = refl
+*-distribʳ-∸ zero zero (suc k) = sym (0∸n≡0 (k * zero))
+*-distribʳ-∸ (suc i) zero (suc k) = refl
+*-distribʳ-∸ i (suc j) zero = refl
+*-distribʳ-∸ i (suc j) (suc k) = begin
+ (j ∸ k) * i ≡⟨ *-distribʳ-∸ i j k ⟩
+ j * i ∸ k * i ≡⟨ sym $ [i+j]∸[i+k]≡j∸k i _ _ ⟩
+ i + j * i ∸ (i + k * i) ∎
+
+*-distribˡ-∸ : _*_ DistributesOverˡ _∸_
+*-distribˡ-∸ = comm+distrʳ⇒distrˡ (cong₂ _∸_) *-comm *-distribʳ-∸
+
+*-distrib-∸ : _*_ DistributesOver _∸_
+*-distrib-∸ = *-distribˡ-∸ , *-distribʳ-∸
+
+-- Properties of _∸_ and _⊓_ and _⊔_
m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
m⊓n+n∸m≡n zero n = refl
m⊓n+n∸m≡n (suc m) zero = refl
@@ -857,40 +1222,14 @@ m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n
[m∸n]⊓[n∸m]≡0 (suc m) zero = refl
[m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n
-[i+j]∸[i+k]≡j∸k : ∀ i j k → (i + j) ∸ (i + k) ≡ j ∸ k
-[i+j]∸[i+k]≡j∸k zero j k = refl
-[i+j]∸[i+k]≡j∸k (suc i) j k = [i+j]∸[i+k]≡j∸k i j k
-
--- TODO: Can this proof be simplified? An automatic solver which can
--- handle ∸ would be nice...
-i∸k∸j+j∸k≡i+j∸k : ∀ i j k → i ∸ (k ∸ j) + (j ∸ k) ≡ i + j ∸ k
-i∸k∸j+j∸k≡i+j∸k zero j k = begin
- 0 ∸ (k ∸ j) + (j ∸ k) ≡⟨ cong (_+ (j ∸ k)) (0∸n≡0 (k ∸ j)) ⟩
- 0 + (j ∸ k) ≡⟨⟩
- j ∸ k ∎
-i∸k∸j+j∸k≡i+j∸k (suc i) j zero = begin
- suc i ∸ (0 ∸ j) + j ≡⟨ cong (λ x → suc i ∸ x + j) (0∸n≡0 j) ⟩
- suc i ∸ 0 + j ≡⟨⟩
- suc (i + j) ∎
-i∸k∸j+j∸k≡i+j∸k (suc i) zero (suc k) = begin
- i ∸ k + 0 ≡⟨ +-identityʳ _ ⟩
- i ∸ k ≡⟨ cong (_∸ k) (sym (+-identityʳ _)) ⟩
- i + 0 ∸ k ∎
-i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin
- suc i ∸ (k ∸ j) + (j ∸ k) ≡⟨ i∸k∸j+j∸k≡i+j∸k (suc i) j k ⟩
- suc i + j ∸ k ≡⟨ cong (_∸ k) (sym (+-suc i j)) ⟩
- i + suc j ∸ k ∎
-
-*-distribʳ-∸ : _*_ DistributesOverʳ _∸_
-*-distribʳ-∸ i zero k = begin
- (0 ∸ k) * i ≡⟨ cong (_* i) (0∸n≡0 k) ⟩
- 0 ≡⟨ sym $ 0∸n≡0 (k * i) ⟩
- 0 ∸ (k * i) ∎
-*-distribʳ-∸ i (suc j) zero = refl
-*-distribʳ-∸ i (suc j) (suc k) = begin
- (j ∸ k) * i ≡⟨ *-distribʳ-∸ i j k ⟩
- j * i ∸ k * i ≡⟨ sym $ [i+j]∸[i+k]≡j∸k i _ _ ⟩
- i + j * i ∸ (i + k * i) ∎
+∸-distribˡ-⊓-⊔ : ∀ x y z → x ∸ (y ⊓ z) ≡ (x ∸ y) ⊔ (x ∸ z)
+∸-distribˡ-⊓-⊔ x zero zero = sym (⊔-idem x)
+∸-distribˡ-⊓-⊔ zero zero (suc z) = refl
+∸-distribˡ-⊓-⊔ zero (suc y) zero = refl
+∸-distribˡ-⊓-⊔ zero (suc y) (suc z) = refl
+∸-distribˡ-⊓-⊔ (suc x) (suc y) zero = sym (m≤n⇒m⊔n≡n (≤-step (n∸m≤n y x)))
+∸-distribˡ-⊓-⊔ (suc x) zero (suc z) = sym (m≤n⇒n⊔m≡n (≤-step (n∸m≤n z x)))
+∸-distribˡ-⊓-⊔ (suc x) (suc y) (suc z) = ∸-distribˡ-⊓-⊔ x y z
∸-distribʳ-⊓ : _∸_ DistributesOverʳ _⊓_
∸-distribʳ-⊓ zero y z = refl
@@ -898,24 +1237,102 @@ i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin
∸-distribʳ-⊓ (suc x) (suc y) zero = sym (⊓-zeroʳ (y ∸ x))
∸-distribʳ-⊓ (suc x) (suc y) (suc z) = ∸-distribʳ-⊓ x y z
+∸-distribˡ-⊔-⊓ : ∀ x y z → x ∸ (y ⊔ z) ≡ (x ∸ y) ⊓ (x ∸ z)
+∸-distribˡ-⊔-⊓ x zero zero = sym (⊓-idem x)
+∸-distribˡ-⊔-⊓ zero zero z = 0∸n≡0 z
+∸-distribˡ-⊔-⊓ zero (suc y) z = 0∸n≡0 (suc y ⊔ z)
+∸-distribˡ-⊔-⊓ (suc x) (suc y) zero = sym (m≤n⇒m⊓n≡m (≤-step (n∸m≤n y x)))
+∸-distribˡ-⊔-⊓ (suc x) zero (suc z) = sym (m≤n⇒n⊓m≡m (≤-step (n∸m≤n z x)))
+∸-distribˡ-⊔-⊓ (suc x) (suc y) (suc z) = ∸-distribˡ-⊔-⊓ x y z
+
∸-distribʳ-⊔ : _∸_ DistributesOverʳ _⊔_
∸-distribʳ-⊔ zero y z = refl
∸-distribʳ-⊔ (suc x) zero z = refl
∸-distribʳ-⊔ (suc x) (suc y) zero = sym (⊔-identityʳ (y ∸ x))
∸-distribʳ-⊔ (suc x) (suc y) (suc z) = ∸-distribʳ-⊔ x y z
-im≡jm+n⇒[i∸j]m≡n : ∀ i j m n → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
-im≡jm+n⇒[i∸j]m≡n i j m n eq = begin
- (i ∸ j) * m ≡⟨ *-distribʳ-∸ m i j ⟩
- (i * m) ∸ (j * m) ≡⟨ cong (_∸ j * m) eq ⟩
- (j * m + n) ∸ (j * m) ≡⟨ cong (_∸ j * m) (+-comm (j * m) n) ⟩
- (n + j * m) ∸ (j * m) ≡⟨ m+n∸n≡m n (j * m) ⟩
- n ∎
-
-∸-mono : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
-∸-mono z≤n (s≤s n₁≥n₂) = z≤n
-∸-mono (s≤s m₁≤m₂) (s≤s n₁≥n₂) = ∸-mono m₁≤m₂ n₁≥n₂
-∸-mono m₁≤m₂ (z≤n {n = n₁}) = ≤-trans (n∸m≤n n₁ _) m₁≤m₂
+------------------------------------------------------------------------
+-- Properties of ∣_-_∣
+
+n≡m⇒∣n-m∣≡0 : ∀ {n m} → n ≡ m → ∣ n - m ∣ ≡ 0
+n≡m⇒∣n-m∣≡0 {zero} refl = refl
+n≡m⇒∣n-m∣≡0 {suc n} refl = n≡m⇒∣n-m∣≡0 {n} refl
+
+m≤n⇒∣n-m∣≡n∸m : ∀ {n m} → m ≤ n → ∣ n - m ∣ ≡ n ∸ m
+m≤n⇒∣n-m∣≡n∸m {zero} z≤n = refl
+m≤n⇒∣n-m∣≡n∸m {suc n} z≤n = refl
+m≤n⇒∣n-m∣≡n∸m (s≤s m≤n) = m≤n⇒∣n-m∣≡n∸m m≤n
+
+∣n-m∣≡0⇒n≡m : ∀ {n m} → ∣ n - m ∣ ≡ 0 → n ≡ m
+∣n-m∣≡0⇒n≡m {zero} {zero} eq = refl
+∣n-m∣≡0⇒n≡m {zero} {suc m} ()
+∣n-m∣≡0⇒n≡m {suc n} {zero} ()
+∣n-m∣≡0⇒n≡m {suc n} {suc m} eq = cong suc (∣n-m∣≡0⇒n≡m eq)
+
+∣n-m∣≡n∸m⇒m≤n : ∀ {n m} → ∣ n - m ∣ ≡ n ∸ m → m ≤ n
+∣n-m∣≡n∸m⇒m≤n {zero} {zero} eq = z≤n
+∣n-m∣≡n∸m⇒m≤n {zero} {suc m} ()
+∣n-m∣≡n∸m⇒m≤n {suc n} {zero} eq = z≤n
+∣n-m∣≡n∸m⇒m≤n {suc n} {suc m} eq = s≤s (∣n-m∣≡n∸m⇒m≤n eq)
+
+∣n-n∣≡0 : ∀ n → ∣ n - n ∣ ≡ 0
+∣n-n∣≡0 n = n≡m⇒∣n-m∣≡0 {n} refl
+
+∣n-n+m∣≡m : ∀ n m → ∣ n - n + m ∣ ≡ m
+∣n-n+m∣≡m zero m = refl
+∣n-n+m∣≡m (suc n) m = ∣n-n+m∣≡m n m
+
+∣n+m-n+o∣≡∣m-o| : ∀ n m o → ∣ n + m - n + o ∣ ≡ ∣ m - o ∣
+∣n+m-n+o∣≡∣m-o| zero m o = refl
+∣n+m-n+o∣≡∣m-o| (suc n) m o = ∣n+m-n+o∣≡∣m-o| n m o
+
+n∸m≤∣n-m∣ : ∀ n m → n ∸ m ≤ ∣ n - m ∣
+n∸m≤∣n-m∣ n m with ≤-total m n
+... | inj₁ m≤n = subst (n ∸ m ≤_) (sym (m≤n⇒∣n-m∣≡n∸m m≤n)) ≤-refl
+... | inj₂ n≤m = subst (_≤ ∣ n - m ∣) (sym (m≤n⇒m∸n≡0 n≤m)) z≤n
+
+∣n-m∣≤n⊔m : ∀ n m → ∣ n - m ∣ ≤ n ⊔ m
+∣n-m∣≤n⊔m zero m = ≤-refl
+∣n-m∣≤n⊔m (suc n) zero = ≤-refl
+∣n-m∣≤n⊔m (suc n) (suc m) = ≤-step (∣n-m∣≤n⊔m n m)
+
+∣-∣-comm : Commutative ∣_-_∣
+∣-∣-comm zero zero = refl
+∣-∣-comm zero (suc m) = refl
+∣-∣-comm (suc n) zero = refl
+∣-∣-comm (suc n) (suc m) = ∣-∣-comm n m
+
+∣n-m∣≡[n∸m]∨[m∸n] : ∀ m n → (∣ n - m ∣ ≡ n ∸ m) ⊎ (∣ n - m ∣ ≡ m ∸ n)
+∣n-m∣≡[n∸m]∨[m∸n] m n with ≤-total m n
+... | inj₁ m≤n = inj₁ $ m≤n⇒∣n-m∣≡n∸m m≤n
+... | inj₂ n≤m = inj₂ $ begin
+ ∣ n - m ∣ ≡⟨ ∣-∣-comm n m ⟩
+ ∣ m - n ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m n≤m ⟩
+ m ∸ n ∎
+
+private
+
+ *-distribˡ-∣-∣-aux : ∀ a m n → m ≤ n → a * ∣ n - m ∣ ≡ ∣ a * n - a * m ∣
+ *-distribˡ-∣-∣-aux a m n m≤n = begin
+ a * ∣ n - m ∣ ≡⟨ cong (a *_) (m≤n⇒∣n-m∣≡n∸m m≤n) ⟩
+ a * (n ∸ m) ≡⟨ *-distribˡ-∸ a n m ⟩
+ a * n ∸ a * m ≡⟨ sym $′ m≤n⇒∣n-m∣≡n∸m (*-monoʳ-≤ a m≤n) ⟩
+ ∣ a * n - a * m ∣ ∎
+
+*-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣
+*-distribˡ-∣-∣ a m n with ≤-total m n
+... | inj₁ m≤n = begin
+ a * ∣ m - n ∣ ≡⟨ cong (a *_) (∣-∣-comm m n) ⟩
+ a * ∣ n - m ∣ ≡⟨ *-distribˡ-∣-∣-aux a m n m≤n ⟩
+ ∣ a * n - a * m ∣ ≡⟨ ∣-∣-comm (a * n) (a * m) ⟩
+ ∣ a * m - a * n ∣ ∎
+... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m
+
+*-distribʳ-∣-∣ : _*_ DistributesOverʳ ∣_-_∣
+*-distribʳ-∣-∣ = comm+distrˡ⇒distrʳ (cong₂ ∣_-_∣) *-comm *-distribˡ-∣-∣
+
+*-distrib-∣-∣ : _*_ DistributesOver ∣_-_∣
+*-distrib-∣-∣ = *-distribˡ-∣-∣ , *-distribʳ-∣-∣
------------------------------------------------------------------------
-- Properties of ⌊_/2⌋
@@ -938,17 +1355,22 @@ im≡jm+n⇒[i∸j]m≡n i j m n eq = begin
⌊n/2⌋≤′n (suc n) = ≤′-step (⌈n/2⌉≤′n n)
------------------------------------------------------------------------
--- Modules for reasoning about natural number relations
+-- Other properties
+
+-- If there is an injection from a type to ℕ, then the type has
+-- decidable equality.
--- A module for automatically solving propositional equivalences
-module SemiringSolver =
- Solver (ACR.fromCommutativeSemiring *-+-commutativeSemiring) _≟_
+eq? : ∀ {a} {A : Set a} → A ↣ ℕ → Decidable {A = A} _≡_
+eq? inj = via-injection inj _≟_
+
+------------------------------------------------------------------------
+-- Modules for reasoning about natural number relations
-- A module for reasoning about the _≤_ relation
module ≤-Reasoning where
open import Relation.Binary.PartialOrderReasoning
(DecTotalOrder.poset ≤-decTotalOrder) public
- renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
+ hiding (_≈⟨_⟩_)
infixr 2 _<⟨_⟩_
@@ -961,23 +1383,140 @@ module ≤-Reasoning where
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
+-- Version 0.14
+
_*-mono_ = *-mono-≤
+{-# WARNING_ON_USAGE _*-mono_
+"Warning: _*-mono_ was deprecated in v0.14.
+Please use *-mono-≤ instead."
+#-}
_+-mono_ = +-mono-≤
-
+{-# WARNING_ON_USAGE _+-mono_
+"Warning: _+-mono_ was deprecated in v0.14.
+Please use +-mono-≤ instead."
+#-}
+-right-identity = +-identityʳ
+{-# WARNING_ON_USAGE +-right-identity
+"Warning: +-right-identity was deprecated in v0.14.
+Please use +-identityʳ instead."
+#-}
*-right-zero = *-zeroʳ
+{-# WARNING_ON_USAGE *-right-zero
+"Warning: *-right-zero was deprecated in v0.14.
+Please use *-zeroʳ instead."
+#-}
distribʳ-*-+ = *-distribʳ-+
+{-# WARNING_ON_USAGE distribʳ-*-+
+"Warning: distribʳ-*-+ was deprecated in v0.14.
+Please use *-distribʳ-+ instead."
+#-}
*-distrib-∸ʳ = *-distribʳ-∸
+{-# WARNING_ON_USAGE *-distrib-∸ʳ
+"Warning: *-distrib-∸ʳ was deprecated in v0.14.
+Please use *-distribʳ-∸ instead."
+#-}
cancel-+-left = +-cancelˡ-≡
+{-# WARNING_ON_USAGE cancel-+-left
+"Warning: cancel-+-left was deprecated in v0.14.
+Please use +-cancelˡ-≡ instead."
+#-}
cancel-+-left-≤ = +-cancelˡ-≤
+{-# WARNING_ON_USAGE cancel-+-left-≤
+"Warning: cancel-+-left-≤ was deprecated in v0.14.
+Please use +-cancelˡ-≤ instead."
+#-}
cancel-*-right = *-cancelʳ-≡
+{-# WARNING_ON_USAGE cancel-*-right
+"Warning: cancel-*-right was deprecated in v0.14.
+Please use *-cancelʳ-≡ instead."
+#-}
cancel-*-right-≤ = *-cancelʳ-≤
-
+{-# WARNING_ON_USAGE cancel-*-right-≤
+"Warning: cancel-*-right-≤ was deprecated in v0.14.
+Please use *-cancelʳ-≤ instead."
+#-}
strictTotalOrder = <-strictTotalOrder
+{-# WARNING_ON_USAGE strictTotalOrder
+"Warning: strictTotalOrder was deprecated in v0.14.
+Please use <-strictTotalOrder instead."
+#-}
isCommutativeSemiring = *-+-isCommutativeSemiring
+{-# WARNING_ON_USAGE isCommutativeSemiring
+"Warning: isCommutativeSemiring was deprecated in v0.14.
+Please use *-+-isCommutativeSemiring instead."
+#-}
commutativeSemiring = *-+-commutativeSemiring
+{-# WARNING_ON_USAGE commutativeSemiring
+"Warning: commutativeSemiring was deprecated in v0.14.
+Please use *-+-commutativeSemiring instead."
+#-}
isDistributiveLattice = ⊓-⊔-isDistributiveLattice
+{-# WARNING_ON_USAGE isDistributiveLattice
+"Warning: isDistributiveLattice was deprecated in v0.14.
+Please use ⊓-⊔-isDistributiveLattice instead."
+#-}
distributiveLattice = ⊓-⊔-distributiveLattice
+{-# WARNING_ON_USAGE distributiveLattice
+"Warning: distributiveLattice was deprecated in v0.14.
+Please use ⊓-⊔-distributiveLattice instead."
+#-}
⊔-⊓-0-isSemiringWithoutOne = ⊔-⊓-isSemiringWithoutOne
+{-# WARNING_ON_USAGE ⊔-⊓-0-isSemiringWithoutOne
+"Warning: ⊔-⊓-0-isSemiringWithoutOne was deprecated in v0.14.
+Please use ⊔-⊓-isSemiringWithoutOne instead."
+#-}
⊔-⊓-0-isCommutativeSemiringWithoutOne = ⊔-⊓-isCommutativeSemiringWithoutOne
+{-# WARNING_ON_USAGE ⊔-⊓-0-isCommutativeSemiringWithoutOne
+"Warning: ⊔-⊓-0-isCommutativeSemiringWithoutOne was deprecated in v0.14.
+Please use ⊔-⊓-isCommutativeSemiringWithoutOne instead."
+#-}
⊔-⊓-0-commutativeSemiringWithoutOne = ⊔-⊓-commutativeSemiringWithoutOne
+{-# WARNING_ON_USAGE ⊔-⊓-0-commutativeSemiringWithoutOne
+"Warning: ⊔-⊓-0-commutativeSemiringWithoutOne was deprecated in v0.14.
+Please use ⊔-⊓-commutativeSemiringWithoutOne instead."
+#-}
+
+-- Version 0.15
+
+¬i+1+j≤i = i+1+j≰i
+{-# WARNING_ON_USAGE ¬i+1+j≤i
+"Warning: ¬i+1+j≤i was deprecated in v0.15.
+Please use i+1+j≰i instead."
+#-}
+≤-steps = ≤-stepsˡ
+{-# WARNING_ON_USAGE ≤-steps
+"Warning: ≤-steps was deprecated in v0.15.
+Please use ≤-stepsˡ instead."
+#-}
+
+-- Version 0.17
+
+i∸k∸j+j∸k≡i+j∸k : ∀ i j k → i ∸ (k ∸ j) + (j ∸ k) ≡ i + j ∸ k
+i∸k∸j+j∸k≡i+j∸k zero j k = cong (_+ (j ∸ k)) (0∸n≡0 (k ∸ j))
+i∸k∸j+j∸k≡i+j∸k (suc i) j zero = cong (λ x → suc i ∸ x + j) (0∸n≡0 j)
+i∸k∸j+j∸k≡i+j∸k (suc i) zero (suc k) = begin
+ i ∸ k + 0 ≡⟨ +-identityʳ _ ⟩
+ i ∸ k ≡⟨ cong (_∸ k) (sym (+-identityʳ _)) ⟩
+ i + 0 ∸ k ∎
+i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin
+ suc i ∸ (k ∸ j) + (j ∸ k) ≡⟨ i∸k∸j+j∸k≡i+j∸k (suc i) j k ⟩
+ suc i + j ∸ k ≡⟨ cong (_∸ k) (sym (+-suc i j)) ⟩
+ i + suc j ∸ k ∎
+{-# WARNING_ON_USAGE i∸k∸j+j∸k≡i+j∸k
+"Warning: i∸k∸j+j∸k≡i+j∸k was deprecated in v0.17."
+#-}
+im≡jm+n⇒[i∸j]m≡n : ∀ i j m n → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
+im≡jm+n⇒[i∸j]m≡n i j m n eq = begin
+ (i ∸ j) * m ≡⟨ *-distribʳ-∸ m i j ⟩
+ (i * m) ∸ (j * m) ≡⟨ cong (_∸ j * m) eq ⟩
+ (j * m + n) ∸ (j * m) ≡⟨ cong (_∸ j * m) (+-comm (j * m) n) ⟩
+ (n + j * m) ∸ (j * m) ≡⟨ m+n∸n≡m n (j * m) ⟩
+ n ∎
+{-# WARNING_ON_USAGE im≡jm+n⇒[i∸j]m≡n
+"Warning: im≡jm+n⇒[i∸j]m≡n was deprecated in v0.17."
+#-}
+≤+≢⇒< = ≤∧≢⇒<
+{-# WARNING_ON_USAGE ≤+≢⇒<
+"Warning: ≤+≢⇒< was deprecated in v0.17.
+Please use ≤∧≢⇒< instead."
+#-}
diff --git a/src/Data/Nat/Solver.agda b/src/Data/Nat/Solver.agda
new file mode 100644
index 0000000..21a8e33
--- /dev/null
+++ b/src/Data/Nat/Solver.agda
@@ -0,0 +1,21 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Automatic solvers for equations over naturals
+------------------------------------------------------------------------
+
+-- See README.Nat for examples of how to use this solver
+
+module Data.Nat.Solver where
+
+import Algebra.Solver.Ring.Simple as Solver
+import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
+open import Data.Nat using (_≟_)
+open import Data.Nat.Properties
+
+------------------------------------------------------------------------
+-- A module for automatically solving propositional equivalences
+-- containing _+_ and _*_
+
+module +-*-Solver =
+ Solver (ACR.fromCommutativeSemiring *-+-commutativeSemiring) _≟_
diff --git a/src/Data/Nat/Unsafe.agda b/src/Data/Nat/Unsafe.agda
new file mode 100644
index 0000000..34839cf
--- /dev/null
+++ b/src/Data/Nat/Unsafe.agda
@@ -0,0 +1,13 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe natural number types and operations
+------------------------------------------------------------------------
+
+module Data.Nat.Unsafe where
+
+open import Data.Nat.Base
+import Relation.Binary.PropositionalEquality.TrustMe as TrustMe
+
+erase : ∀ {m n} → m ≤″ n → m ≤″ n
+erase (less-than-or-equal eq) = less-than-or-equal (TrustMe.erase eq)
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-01 09:43:04 +0000