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 ≡ 
suc x ∣ℤ y = fibre (_*ℤ possuc x) y

infix  _∣ℤ_

∣ℤ-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  =  , 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 ∣ℤ 
∣ℤ-zero = dividesℤ  refl

∣ℤ-one : ∀ {x} →  ∣ℤ x
∣ℤ-one {x} = dividesℤ x (*ℤ-oner x)

m∣ℤsn→m≤sn : ∀ {x y} → ¬ (y ≡ ) → 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