blob: 57c15b5bd2b49a39d503d006811658613f3ac4fc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
{-# OPTIONS --safe --without-K #-}
module Helium.Data.Numeric where
open import Algebra
open import Algebra.Morphism.Structures
open import Data.Integer as ℤ hiding (_⊔_)
import Data.Integer.DivMod as DivMod
import Data.Integer.Properties as ℤₚ
open import Data.Nat as ℕ using (ℕ; zero; suc)
import Data.Nat.Properties as ℕₚ
open import Data.Sum using ([_,_]′)
open import Function using (_∘_; id; flip)
open import Helium.Algebra.Field
open import Level renaming (suc to ℓsuc)
open import Relation.Binary
import Relation.Binary.Construct.StrictToNonStrict as STNS
open import Relation.Binary.Morphism.Structures
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
module _
{a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁)
(_<ʳ_ : Rel A ℓ₂)
where
record IsReal (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) (_⁻¹ : ∀ x {≢0 : ¬ x ≈ 0#} → A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isField : IsField _≈_ _+_ _*_ -_ 0# 1# _⁻¹
isStrictTotalOrder : IsStrictTotalOrder _≈_ _<ʳ_
open IsField isField public hiding (refl; reflexive; sym; trans)
open IsStrictTotalOrder isStrictTotalOrder public
record IsNumeric (+ʳ *ʳ : Op₂ A) (-ʳ : Op₁ A) (0ℝ 1ℝ : A)
(⁻¹ : ∀ x {≢0 : ¬ x ≈ 0ℝ} → A)
(⟦_⟧ : ℤ → A) (round : A → ℤ)
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
private
rawRing : RawRing a ℓ₁
rawRing = record
{ Carrier = A
; _≈_ = _≈_
; _+_ = +ʳ
; _*_ = *ʳ
; -_ = -ʳ
; 0# = 0ℝ
; 1# = 1ℝ
}
_≤ʳ_ = STNS._≤_ _≈_ _<ʳ_
field
isReal : IsReal +ʳ *ʳ -ʳ 0ℝ 1ℝ ⁻¹
⟦⟧-isOrderMonomorphism : IsOrderMonomorphism _≡_ _≈_ _<_ _<ʳ_ ⟦_⟧
⟦⟧-isRingHomomorphism : IsRingHomomorphism (Ring.rawRing ℤₚ.+-*-ring) rawRing ⟦_⟧
round-isOrderHomomorphism : IsOrderHomomorphism _≈_ _≡_ _≤ʳ_ _≤_ round
round-isRingHomomorphism : IsRingHomomorphism rawRing (Ring.rawRing ℤₚ.+-*-ring) round
round∘⟦⟧ : ∀ z → round ⟦ z ⟧ ≡ z
round-down : ∀ {x z} → x <ʳ ⟦ z ⟧ → round x < z
module real = IsReal isReal
module ⟦⟧-order = IsOrderMonomorphism ⟦⟧-isOrderMonomorphism
module ⟦⟧-ring = IsRingHomomorphism ⟦⟧-isRingHomomorphism
module round-order = IsOrderHomomorphism round-isOrderHomomorphism
module round-ring = IsRingHomomorphism round-isRingHomomorphism
private
foldn : ∀ {a} {A : Set a} → ℕ → Op₁ A → Op₁ A
foldn zero f = id
foldn (suc n) f = f ∘ foldn n f
record Numeric a ℓ₁ ℓ₂ : Set (ℓsuc a ⊔ ℓsuc ℓ₁ ⊔ ℓsuc ℓ₂) where
infix 10 _⁻¹
infix 9 _^_ _^ℕ_ _ℤ^ℕ_
infix 8 -ʳ_
infixl 7 _*ʳ_ _div_ _div′_ _mod_ _mod′_
infixl 6 _+ʳ_
infix 4 _≈ʳ_
field
ℝ : Set a
_≈ʳ_ : Rel ℝ ℓ₁
_<ʳ_ : Rel ℝ ℓ₂
_+ʳ_ : Op₂ ℝ
_*ʳ_ : Op₂ ℝ
-ʳ_ : Op₁ ℝ
0ℝ : ℝ
1ℝ : ℝ
_⁻¹ : ∀ x {≢0 : ¬ x ≈ʳ 0ℝ} → ℝ
⟦_⟧ : ℤ → ℝ
round : ℝ → ℤ
isNumeric : IsNumeric _≈ʳ_ _<ʳ_ _+ʳ_ _*ʳ_ -ʳ_ 0ℝ 1ℝ _⁻¹ ⟦_⟧ round
open IsNumeric isNumeric public
-- div and mod according to the manual
_div_ : ∀ (x y : ℤ) → {≢0 : False (y ≟ 0ℤ)} → ℤ
(x div y) {≢0} = round (⟦ x ⟧ *ʳ (⟦ y ⟧ ⁻¹) {⟦y⟧≢0})
where
open ≡-Reasoning
⟦y⟧≢0 = λ y≡0 → toWitnessFalse ≢0 (begin
y ≡˘⟨ round∘⟦⟧ y ⟩
round ⟦ y ⟧ ≡⟨ round-order.cong y≡0 ⟩
round 0ℝ ≡⟨ round-ring.0#-homo ⟩
0ℤ ∎)
_mod_ : ∀ (x y : ℤ) → {≢0 : False (y ≟ 0ℤ)} → ℤ
(x mod y) {≢0} = x + - (y * ((x div y) {≢0}))
-- regular integer division and modulus
_div′_ : ∀ (x y : ℤ) → {≢0 : False (y ≟ 0ℤ)} → ℤ
(x div′ y) {≢0} = (x DivMod.div y) {fromWitnessFalse (toWitnessFalse ≢0 ∘ ℤₚ.∣n∣≡0⇒n≡0)}
_mod′_ : ∀ (x y : ℤ) → {≢0 : False (y ≟ 0ℤ)} → ℕ
(x mod′ y) {≢0} = (x DivMod.mod y) {fromWitnessFalse (toWitnessFalse ≢0 ∘ ℤₚ.∣n∣≡0⇒n≡0)}
_^ℕ_ : ℝ → ℕ → ℝ
x ^ℕ zero = 1ℝ
x ^ℕ suc n = x *ʳ x ^ℕ n
_^_ : ∀ x {≢0 : False (x real.≟ 0ℝ)} → ℤ → ℝ
x ^ +0 = 1ℝ
x ^ +[1+ n ] = x ^ℕ (ℕ.suc n)
_^_ x {≢0} -[1+ n ] = (x ⁻¹) {toWitnessFalse ≢0} ^ℕ (ℕ.suc n)
_ℤ^ℕ_ : ℤ → ℕ → ℤ
x ℤ^ℕ zero = 1ℤ
x ℤ^ℕ suc y = x * x ℤ^ℕ y
x^y≡0⇒x≡0 : ∀ x y → x ℤ^ℕ y ≡ 0ℤ → x ≡ 0ℤ
x^y≡0⇒x≡0 x (suc y) x^y≡0 = [ id , x^y≡0⇒x≡0 x y ]′ (ℤₚ.m*n≡0⇒m≡0∨n≡0 x x^y≡0)
_<<_ : Op₂ ℤ
x << +0 = x
x << +[1+ n ] = x * ((+ 2) ℤ^ℕ (ℕ.suc n))
x << -[1+ n ] = round (⟦ x ⟧ *ʳ (_^_ ⟦ + 2 ⟧ {≢0} -[1+ n ]))
where
open ≡-Reasoning
≢0 = fromWitnessFalse (λ 2≡0 → flip contradiction (λ ()) (begin
+ 2 ≡˘⟨ round∘⟦⟧ (+ 2) ⟩
round ⟦ + 2 ⟧ ≡⟨ round-order.cong 2≡0 ⟩
round 0ℝ ≡⟨ round-ring.0#-homo ⟩
0ℤ ∎))
_>>_ : Op₂ ℤ
x >> n = x << (- n)
x<<+y≡0⇒x≡0 : ∀ x y → x << (+ y) ≡ 0ℤ → x ≡ 0ℤ
x<<+y≡0⇒x≡0 x zero eq = eq
x<<+y≡0⇒x≡0 x (suc y) eq = [ id , flip contradiction (λ ()) ∘ x^y≡0⇒x≡0 (+ 2) (ℕ.suc y) ]′ (ℤₚ.m*n≡0⇒m≡0∨n≡0 x eq)
hasBit : ∀ (i : ℕ) z →
let 2<<1+i≢0 = fromWitnessFalse (contraposition (x<<+y≡0⇒x≡0 (+ 2) (ℕ.suc i)) λ ()) in
Dec (+ (z mod′ (+ 2) << +[1+ i ]) {2<<1+i≢0} ≥ (+ 2) << (+ i))
hasBit i z = (+ 2) << (+ i) ≤? + (z mod′ (+ 2) << +[1+ i ])
|
