Define relation on numeric types.abstract

1 files changed, 158 insertions, 0 deletions

diff --git a/src/Helium/Data/Numeric.agda b/src/Helium/Data/Numeric.agda
new file mode 100644
index 0000000..57c15b5
--- /dev/null
+++ b/src/Helium/Data/Numeric.agda
@@ -0,0 +1,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 ])