module Data.ForeignNat.Divisibility where

open import Data.ForeignNat

open import Data.Bool using (Bool; true; false)
open import Relation.Binary.Core
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Nat
open import Data.Nat.Divisibility
open import Relation.Binary.PropositionalEquality
open import Data.Product

open import Algebra
import Data.Nat.Properties as Nat
private
  module ℕ = CommutativeSemiring Nat.commutativeSemiring

{-# IMPORT Data.ForeignNat.Impl #-}

postulate
  _/′_ : ℕ′ → ℕ′ → ℕ′
  _%′_ : ℕ′ → ℕ′ → ℕ′
  
  muldiv : ∀ {m n q r} → (q ≡ unmarshalℕ ((marshalℕ n) /′ (marshalℕ m))) → (r ≡ unmarshalℕ ((marshalℕ n) %′ (marshalℕ m))) → n ≡ q * m + r
  ∣-%-consistency : ∀ {m n} → m ∣ n → (marshalℕ n %′ marshalℕ m) ≡ zero
  
{-# COMPILED _/′_ Data.ForeignNat.Impl.divide #-}
{-# COMPILED _%′_ Data.ForeignNat.Impl.modulo #-}

_∣?′_ : Decidable _∣_
m ∣?′ n with ((marshalℕ n) %′ (marshalℕ m)) ≟′ zero
...    | yes noRem with muldiv refl (cong unmarshalℕ (sym noRem))
...                | n=q*m+0 = yes (divides q n=q*m)
                                  where q = unmarshalℕ ((marshalℕ n) /′ (marshalℕ m))
                                        n=q*m = begin
                                                  n
                                                ≡⟨ n=q*m+0 ⟩
                                                  q * m + 
                                                ≡⟨ proj₂ ℕ.+-identity (q * m) ⟩
                                                  q * m
                                                ∎ where open ≡-Reasoning
m ∣?′ n | no rem = no λ m∣n → contradiction (∣-%-consistency m∣n) rem