Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer

[mechvel]

lib-2.1-rc1 has general definitions for Irreducible, Prime for Magma, CancellativeCommutativeSemiring, and also some proofs for them (see Algebra/Definitions/ and certain other places). And ℕ, ℤ do have their instances *-magma, cancellativeCommutativeSemiring. So, it has sense for ℕ and ℤ to import the general definitions of Irreducible, Prime as specialization (by substituting the module parameters) and to use them instead of declaring ad-hoc definitions by new. For example, the parts of Nat.Primality.Prime can be derived from the general definition of Prime. If the ad-hoc local definitions occur useful, it would have sense to rename them and to hide them under private. The matter is that the general definitions and many their related properties work not only for ℕ, but also for ℤ and for polynomials over ℤ and for many other domains. For example, I use Nat.Factorization.factorise , but I need to convert the parts of PrimeFactorisation to general ones, say, to convert factorsPrime from the ad-hoc definition Prime to general Prime, and so on. Such renaming and conversion complicates the code.

[mechvel]

It is even worse. The general definition for _∣_ is not imported to Data.Nat.Divisibility.Core. Instead Nat...Core gives its own definition for _∣_ in which the parts of equality are swapped.

[mechvel]

Changing _∣_ in Nat.Divisibiliy may break backwards compatibiliy greatly. At least the team could add the conversion that allows people to use generic _∣_ and the ad-hoc one for Nat:

open Divisibility *-magma using (_∣_; _∤_; _,_)   -- generic

∣stdℕ⇒∣ :  _∣stdℕ_ ⇒  _∣_
∣stdℕ⇒∣ (dividesℕ q y≡qx) =  q , (sym y≡qx)             -- convert ad-hoc to generic

∣⇒∣stdℕ⇒∣ :  _∣_ ⇒  _∣stdℕ_                                       -- the reverse
∣⇒∣stdℕ⇒∣ (q , qx≡y) =  dividesℕ q (sym qx≡y)

As to Irreducible and Prime for Nat, they are probably more fresh, and they just can be changed to generic definitions as I asked above.

[MatthewDaggitt]

Yes, we should fix this in 3.0

[mechvel]

Currently I use Nat.Factorisation.factorise with converting the result parts to the generic (standard) definitions of Irreducible and Prime. I hope that in lib-3.0 this conversion will not be necessary. But the below two conversion functions may help you with fixing the things from lib-2.1 to lib-3.0.

-- Conversion between  Irreducible-std, Prime-std (ad-how for ℕ in lib-2.1)  and
-- Irreducible, Prime (general definitions in lib-2.1).

irreducible-std⇒Irreducible :  ∀ {p} → Irreducible-std p → p ∤ 1 →
                                                                     Irreducible p
irreducible-std⇒Irreducible {p} irredStd-p p∤1 =  mkIrred p∤1 split-∣1
  where
  p≢0 :  p ≢ 0
  p≢0 =  ≢-nonZero⁻¹ p {{irreducible⇒nonZero-std irredStd-p}}

  split-∣1 :  ∀ {x y} → p ≡ x * y → x ∣ 1 ⊎ y ∣ 1
  split-∣1 {x} {y} p≡xy =
    let
      xy≡p = sym p≡xy

      y∣p :  y ∣ p
      y∣p =  x , xy≡p

      y-∣stdℕ-p = ∣⇒∣stdℕ y∣p
    in
    case  irredStd-p y-∣stdℕ-p
    of \
    { (inj₁ y≡1) → inj₂ (∣-reflexive y≡1)
    ; (inj₂ y≡p) → 
         let
            xp≡1*p =   
                begin 
                     x * p     ≡⟨ cong (x *_) (sym y≡p) ⟩
                     x * y     ≡⟨ sym p≡xy ⟩
                     p          ≡⟨ sym (1* p) ⟩
                     1 * p
                ∎
            x≡1 =  *-cancelʳ-nonzero p x 1 p≢0 xp≡1*p

            x∣1 :  x ∣ 1
            x∣1 =  ∣-reflexive x≡1
         in
         inj₁ x∣1
    }

prime-std⇒Irreducible : ∀ {p} → Prime-std p → Irreducible p
prime-std⇒Irreducible {p} primeStd-p =
      irreducible-std⇒Irreducible (prime-std⇒Irreducible-std primeStd-p) p∤1
      where
      nonTriv-p = prime-std⇒nonTrivial primeStd-p
      p>1           = nonTrivial⇒n>1 p {{nonTriv-p}}
      p∤1           = >⇒∤ p>1 λ()

[jamesmckinna]

Cf #679 #2115 (and perhaps others, incl. #1578 ), so marking this as status:duplicate... and indeed, the most recent attempts also involved some breaking changes in v2.0, and any subsequent developments even more so (even at the level of reconciling the orientation of the relevant equality), so will have to wait for v3.0...

[mechvel]

It is better to use above the names Irreducible-adHoc and Prime-adHoc with using -adHoc instead of -std. Because both versions are in Standard of lib-2.1-rc1, only one is ad-hoc for Nat, and another is the general definition for Irreducible and Prime specialized by a setting parameter to the module.

[MatthewDaggitt]

Yes, okay closing as duplicate. Please feel free to continue the discussion in #2115