open import 1Lab.Prelude

open import Data.Int
open import Data.Nat as Nat

module Data.Int.Divisible where

Divisibility of integersπŸ”—

We define what it means for an integer to be divisible by a natural number, as a straightforward generalisation of the case for natural numbers.

_βˆ£β„€_ : Nat β†’ Int β†’ Type
zero  βˆ£β„€ y = y ≑ 0
suc x βˆ£β„€ y = fibre (_*β„€ possuc x) y

infix 7 _βˆ£β„€_

βˆ£β„€-is-prop : βˆ€ x y β†’ is-prop (x βˆ£β„€ y)
βˆ£β„€-is-prop zero y n k = prop!
βˆ£β„€-is-prop (suc x) y (n , p) (n' , q) = Ξ£-prop-path! (*β„€-injectiver-possuc x n n' (p βˆ™ sym q))

βˆ£β„€-is-truncation : βˆ€ {x y} β†’ (x βˆ£β„€ y) ≃ βˆ₯ fibre (_*β„€ pos x) y βˆ₯
βˆ£β„€-is-truncation {zero} {y} =
  prop-ext!
    (Ξ» p β†’ inc (y , *β„€-zeror y βˆ™ sym p))
    (rec! Ξ» x p β†’ sym p βˆ™ *β„€-zeror x )
βˆ£β„€-is-truncation {suc x} {y} = Equiv.to is-prop≃equivβˆ₯-βˆ₯ (βˆ£β„€-is-prop (suc x) y)

βˆ£β„€β†’fibre : βˆ€ {x y} β†’ x βˆ£β„€ y β†’ fibre (_*β„€ pos x) y
βˆ£β„€β†’fibre {zero} wit  = 0 , sym wit
βˆ£β„€β†’fibre {suc x} wit = wit

fibreβ†’βˆ£β„€ : βˆ€ {x y} β†’ fibre (_*β„€ pos x) y β†’ x βˆ£β„€ y
fibreβ†’βˆ£β„€ f = Equiv.from βˆ£β„€-is-truncation (inc f)

dividesβ„€ : βˆ€ {x y} (q : Int) β†’ q *β„€ pos x ≑ y β†’ x βˆ£β„€ y
dividesβ„€ x p = fibreβ†’βˆ£β„€ (x , p)

βˆ£β„€-zero : βˆ€ {x} β†’ x βˆ£β„€ 0
βˆ£β„€-zero = dividesβ„€ 0 refl

βˆ£β„€-one : βˆ€ {x} β†’ 1 βˆ£β„€ x
βˆ£β„€-one {x} = dividesβ„€ x (*β„€-oner x)

mβˆ£β„€snβ†’m≀sn : βˆ€ {x y} β†’ Β¬ (y ≑ 0) β†’ x βˆ£β„€ y β†’ x Nat.≀ abs y
mβˆ£β„€snβ†’m≀sn {x} {y} nz p with βˆ£β„€β†’fibre p
... | posz , p = absurd (nz (sym p))
... | possuc k , p = difference→≀ (k * x)
  (ap abs (sym (assign-pos (x + k * x))) βˆ™ ap abs p)
... | negsuc k , p = difference→≀ (k * x)
  (sym (abs-negβ„€ (pos (x + k * x))) βˆ™ ap abs (sym (assign-neg (x + k * x))) βˆ™ ap abs p)

βˆ£β„€-+ : βˆ€ {k n m} β†’ k βˆ£β„€ n β†’ k βˆ£β„€ m β†’ k βˆ£β„€ (n +β„€ m)
βˆ£β„€-+ {zero} {n} {m} p q = apβ‚‚ _+β„€_ p q
βˆ£β„€-+ {suc k} (x , p) (y , q) = x +β„€ y , *β„€-distribr (possuc k) x y βˆ™ apβ‚‚ _+β„€_ p q

βˆ£β„€-negβ„€ : βˆ€ {k n} β†’ k βˆ£β„€ n β†’ k βˆ£β„€ negβ„€ n
βˆ£β„€-negβ„€ {zero} d = ap negβ„€ d
βˆ£β„€-negβ„€ {suc k} (x , p) = negβ„€ x , *β„€-negl x _ βˆ™ ap negβ„€ p