definition of Irreducible and Rough; refactoring of Prime and Composite cf. #2180 (#2181)

* definition of `Irreducible`; refactoring of `Prime` and `Composite`

* tidying up old cruft

* knock-on consequences: `Coprimality`

* considerable refactoring of `Primality`

* knock-on consequences: `Coprimality`

* refactoring: no appeal to `Data.Nat.Induction`

* refactoring: renamed `SmoothAt` and its constructor; added pattern synonym; proved `Decidable Irreducible`; misc. tweaks

* knock-on consequences: `Coprimality`

* refactoring: removed `NonZero` analysis; misc. tweaks

* knock-on consequences: `Coprimality`; tightened `import`s

* knock-on consequences: `Coprimality`; tightened `import`s

* refactoring: every number is `1-rough`

* knock-on consequences: `Coprimality`; use of smart constructor

* refactoring: every number is `0-rough`; streamlining; inverse to `prime`; documentation

* attempt to optimise for a nearly-common case pseudo-constructor

* fiddling now

* refactoring: better use of `primality` API

* `Rough` is bounded

* removed unnecessary implicits

* comment

* refactoring: comprehensive shift over to `NonTrivial` instances

* refactoring: oops!

* tidying up: removed infixes

* tidying up: restored `rough⇒≤`

* further refinements; added `NonTrivial` proofs

* tidying up

* moving definitions to `Data.Nat.Base`

* propagated changes; many more explicit s required?

* `NonTrivial` is `Recomputable`

* all instances of `NonTrivial` now irrelevant; weird to need `NonTrivial 2` explicitly

* tidying up `Coprimality`, eg with `variable`s

* `NonTrivial` is `Decidable`

* systematise proofs of `Decidable` properties via the `UpTo` predicates

* explicit quantifier now in `composite≢`

* Nathan's simplification

* interaction of `NonZero` and `NonTrivial` instances

* divisor now a record field; final lemmas: closure under divisibility; plus partial `CHANGELOG` entries

* '(non-)instances' become '(counter-)examples'

* stylistics

* removed `k` as a variable/parameter

* renamed fields and smart constructors

* moved smart constructors; made  a local definition

* tidying up

* refactoring per review comments: equivalence of `UpTo` predicates; making more things `private`

* tidying up: names congruent to ordering relation

* removed variable `k`; removed old proof in favour of new one with `NonZero` instance

* removed `recomputable` in favour of a private lemma

* regularised use of instance brackets

* made instances more explicit

* made instances more explicit

* blank line

* made `nonTrivial⇒nonZero` take an explicit argument in lieu of being able to make it an `instance`

* regularised use of instance brackets

* regularised use of instance brackets

* trimming

* tidied up `Coprimality` entries

* Make HasBoundedNonTrivialDivisor infix

* Make NonTrivial into a record to fix instance resolution bug

* Move HasNonTrivialDivisor to Divisibility.Core and hide UpTo lemmas

* Rearrange file to follow standard ordering of lemmas in the rest of the library

* Move UpTo predicates into decidability proofs

* No-op refactoring to curb excessively long lines

* Make a couple of names consistent with style-guide

* new definition of `Prime`

* renamed fundamental definition

* one last reference in `CHANGELOG`

* more better words; one fewer definition

* tidied up `Definitions` section; rejigged order of proofs of properties to reflect definitional order

* refactored proof of `prime⇒irreducible`

* finishing touches

* missing lemma from irrelevant instance list

* regularised final proof to use `contradiction`

* added fixity `infix 10`

* added fixity `infix 10`; made `composite` a pattern synonym; knock-on improvements

* comprehensive `CHNAGELOG` entry; whitespace fixes

* Rename 1<2+ to sz<ss

* Rename hasNonTrivialDivisor relation

* Updated CHANGELOG

---------

Co-authored-by: MatthewDaggitt <matthewdaggitt@gmail.com>

Author: jamesmckinna

CHANGELOG.md

@@ -645,10 +645,14 @@ Non-backwards compatible changes
 * To make it easier to use, reason about and read, the definition has been
   changed to:
   ```agda
-  Prime 0 = ⊥
-  Prime 1 = ⊥
-  Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
+  record Prime (p : ℕ) : Set where
+    constructor prime
+    field
+      .{{nontrivial}} : NonTrivial p
+      notComposite    : ¬ Composite p
   ```
+  where `Composite` is now defined as the diagonal of the new relation
+  `_HasNonTrivialDivisorLessThan_` in `Data.Nat.Divisibility.Core`.
 
 ### Changes to operation reduction behaviour in `Data.Rational(.Unnormalised)`
 
@@ -2754,6 +2758,18 @@ Additions to existing modules
   s≤″s⁻¹ : suc m ≤″ suc n → m ≤″ n
   s<″s⁻¹ : suc m <″ suc n → m <″ n
 
+  pattern 2+ n = suc (suc n)
+  pattern 1<2+n {n} = s<s (z<s {n})
+
+  NonTrivial            : Pred ℕ 0ℓ
+  instance nonTrivial   : NonTrivial (2+ n)
+  n>1⇒nonTrivial        : 1 < n → NonTrivial n
+  nonZero⇒≢1⇒nonTrivial : .{{NonZero n}} → n ≢ 1 → NonTrivial n
+  recompute-nonTrivial  : .{{NonTrivial n}} → NonTrivial n
+  nonTrivial⇒nonZero    : .{{NonTrivial n}} → NonZero n
+  nonTrivial⇒n>1        : .{{NonTrivial n}} → 1 < n
+  nonTrivial⇒≢1         : .{{NonTrivial n}} → n ≢ 1
+
   _⊔′_ : ℕ → ℕ → ℕ
   _⊓′_ : ℕ → ℕ → ℕ
   ∣_-_∣′ : ℕ → ℕ → ℕ
@@ -2779,20 +2795,42 @@ Additions to existing modules
   <-asym : Asymmetric _<_
   ```
 
-* Added a new pattern synonym to `Data.Nat.Divisibility.Core`:
+* Added a new pattern synonym and a new definition to `Data.Nat.Divisibility.Core`:
   ```agda
   pattern divides-refl q = divides q refl
+  record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where
+  ```
+
+* Added new proofs to `Data.Nat.Divisibility`:
+  ```agda
+  hasNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → n HasNonTrivialDivisorLessThan n
+  hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n → m ∣ o → o HasNonTrivialDivisorLessThan n
+  hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n → n ≤ o → m HasNonTrivialDivisorLessThan o
   ```
 
-* Added new definitions and proofs to `Data.Nat.Primality`:
+* Added new definitions, smart constructors and proofs to `Data.Nat.Primality`:
   ```agda
-  Composite        : ℕ → Set
-  composite?       : Decidable Composite
-  composite⇒¬prime : Composite n → ¬ Prime n
-  ¬composite⇒prime : 2 ≤ n → ¬ Composite n → Prime n
-  prime⇒¬composite : Prime n → ¬ Composite n
-  ¬prime⇒composite : 2 ≤ n → ¬ Prime n → Composite n
-  euclidsLemma     : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n
+  infix 10 _Rough_
+  _Rough_           : ℕ → Pred ℕ _
+  0-rough           : 0 Rough n
+  1-rough           : 1 Rough n
+  2-rough           : 2 Rough n
+  rough⇒≤           : .{{NonTrivial n}} → m Rough n → m ≤ n
+  ∤⇒rough-suc        : m ∤ n → m Rough n → (suc m) Rough n
+  rough∧∣⇒rough     : m Rough o → n ∣ o → m Rough n
+  Composite         : ℕ → Set
+  composite-≢       : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → Composite n
+  composite-∣       : .{{NonZero n}} → Composite m → m ∣ n → Composite n
+  composite?        : Decidable Composite
+  Irreducible       : ℕ → Set
+  irreducible?      : Decidable Irreducible
+  composite⇒¬prime  : Composite n → ¬ Prime n
+  ¬composite⇒prime  : .{{NonTrivial n} → ¬ Composite n → Prime n
+  prime⇒¬composite  : Prime n → ¬ Composite n
+  ¬prime⇒composite  : .{{NonTrivial n} → ¬ Prime n → Composite n
+  prime⇒irreducible : Prime p → Irreducible p
+  irreducible⇒prime : .{{NonTrivial p}} → Irreducible p → Prime p
+  euclidsLemma      : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n
   ```
 
 * Added new proofs in `Data.Nat.Properties`:
@@ -2802,16 +2840,20 @@ Additions to existing modules
   n+1+m≢m   : n + suc m ≢ m
   m*n≡0⇒m≡0 : .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0
   n>0⇒n≢0   : n > 0 → n ≢ 0
-  m^n≢0     : .{{_ : NonZero m}} → NonZero (m ^ n)
   m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
+  m*n≢0⇒m≢0 : .{{NonZero (m * n)}} → NonZero m
+  m*n≢0⇒n≢0 : .{{NonZero (m * n)}} → NonZero n
+  m≢0∧n>1⇒m*n>1 : .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n)
+  n≢0∧m>1⇒m*n>1 : .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n)
+  m^n≢0     : .{{_ : NonZero m}} → NonZero (m ^ n)
   m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
 
   s<s-injective : s<s p ≡ s<s q → p ≡ q
   <-step        : m < n → m < 1 + n
   m<1+n⇒m<n∨m≡n : m < suc n → m < n ⊎ m ≡ n
 
   pred-mono-≤   : m ≤ n → pred m ≤ pred n
-  pred-mono-<   : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+  pred-mono-<   : .{{_ : NonZero m}} → m < n → pred m < pred n
 
   z<′s : zero <′ suc n
   s<′s : m <′ n → suc m <′ suc n
@@ -2852,7 +2894,7 @@ Additions to existing modules
   ⊓≡⊓′ : m ⊓ n ≡ m ⊓′ n
   ∣-∣≡∣-∣′ : ∣ m - n ∣ ≡ ∣ m - n ∣′
 
-  nonZero? : Decidable NonZero
+  nonTrivial? : Decidable NonTrivial
   eq? : A ↣ ℕ → DecidableEquality A
   ≤-<-connex : Connex _≤_ _<_
   ≥->-connex : Connex _≥_ _>_
@@ -2878,21 +2920,21 @@ Additions to existing modules
   m%n≤n           : .{{_ : NonZero n}} → m % n ≤ n
   m*n/m!≡n/[m∸1]! : .{{_ : NonZero m}} → m * n / m ! ≡ n / (pred m) !
 
-  %-congˡ             : .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o
-  %-congʳ             : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ≡ n → o % m ≡ o % n
-  m≤n⇒[n∸m]%m≡n%m     : .⦃ _ : NonZero m ⦄ → m ≤ n → (n ∸ m) % m ≡ n % m
-  m*n≤o⇒[o∸m*n]%n≡o%n : .⦃ _ : NonZero n ⦄ → m * n ≤ o → (o ∸ m * n) % n ≡ o % n
-  m∣n⇒o%n%m≡o%m       : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ∣ n → o % n % m ≡ o % m
-  m<n⇒m%n≡m           : .⦃ _ : NonZero n ⦄ → m < n → m % n ≡ m
-  m*n/o*n≡m/o         : .⦃ _ : NonZero o ⦄ ⦃ _ : NonZero (o * n) ⦄ → m * n / (o * n) ≡ m / o
-  m<n*o⇒m/o<n         : .⦃ _ : NonZero o ⦄ → m < n * o → m / o < n
-  [m∸n]/n≡m/n∸1       : .⦃ _ : NonZero n ⦄ → (m ∸ n) / n ≡ pred (m / n)
-  [m∸n*o]/o≡m/o∸n     : .⦃ _ : NonZero o ⦄ → (m ∸ n * o) / o ≡ m / o ∸ n
-  m/n/o≡m/[n*o]       : .⦃ _ : NonZero n ⦄ .⦃ _ : NonZero o ⦄ .⦃ _ : NonZero (n * o) ⦄ → m / n / o ≡ m / (n * o)
-  m%[n*o]/o≡m/o%n     : .⦃ _ : NonZero n ⦄ .⦃ _ : NonZero o ⦄ ⦃ _ : NonZero (n * o) ⦄ → m % (n * o) / o ≡ m / o % n
-  m%n*o≡m*o%[n*o]     : .⦃ _ : NonZero n ⦄ ⦃ _ : NonZero (n * o) ⦄ → m % n * o ≡ m * o % (n * o)
+  %-congˡ             : .{{_ : NonZero o}} → m ≡ n → m % o ≡ n % o
+  %-congʳ             : .{{_ : NonZero m}} .{{_ : NonZero n}} → m ≡ n → o % m ≡ o % n
+  m≤n⇒[n∸m]%m≡n%m     : .{{_ : NonZero m}} → m ≤ n → (n ∸ m) % m ≡ n % m
+  m*n≤o⇒[o∸m*n]%n≡o%n : .{{_ : NonZero n}} → m * n ≤ o → (o ∸ m * n) % n ≡ o % n
+  m∣n⇒o%n%m≡o%m       : .{{_ : NonZero m}} .{{_ : NonZero n}} → m ∣ n → o % n % m ≡ o % m
+  m<n⇒m%n≡m           : .{{_ : NonZero n}} → m < n → m % n ≡ m
+  m*n/o*n≡m/o         : .{{_ : NonZero o}} {{_ : NonZero (o * n)}} → m * n / (o * n) ≡ m / o
+  m<n*o⇒m/o<n         : .{{_ : NonZero o}} → m < n * o → m / o < n
+  [m∸n]/n≡m/n∸1       : .{{_ : NonZero n}} → (m ∸ n) / n ≡ pred (m / n)
+  [m∸n*o]/o≡m/o∸n     : .{{_ : NonZero o}} → (m ∸ n * o) / o ≡ m / o ∸ n
+  m/n/o≡m/[n*o]       : .{{_ : NonZero n}} .{{_ : NonZero o}} .{{_ : NonZero (n * o)}} → m / n / o ≡ m / (n * o)
+  m%[n*o]/o≡m/o%n     : .{{_ : NonZero n}} .{{_ : NonZero o}} {{_ : NonZero (n * o)}} → m % (n * o) / o ≡ m / o % n
+  m%n*o≡m*o%[n*o]     : .{{_ : NonZero n}} {{_ : NonZero (n * o)}} → m % n * o ≡ m * o % (n * o)
 
-  [m*n+o]%[p*n]≡[m*n]%[p*n]+o : ⦃ _ : NonZero (p * n) ⦄ → o < n → (m * n + o) % (p * n) ≡ (m * n) % (p * n) + o
+  [m*n+o]%[p*n]≡[m*n]%[p*n]+o : {{_ : NonZero (p * n)}} → o < n → (m * n + o) % (p * n) ≡ (m * n) % (p * n) + o
   ```
 
 * Added new proofs in `Data.Nat.Divisibility`:
@@ -3629,7 +3671,9 @@ This is a full list of proofs that have changed form to use irrelevant instance
 
 * In `Data.Nat.Coprimality`:
   ```
-  Bézout-coprime : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j
+  ¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2 + n)
+  Bézout-coprime  : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j
+  prime⇒coprime   : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n
   ```
 
 * In `Data.Nat.Divisibility`

src/Data/Nat/Base.agda

@@ -21,13 +21,17 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Unary using (Pred)
 
 ------------------------------------------------------------------------
 -- Types
 
 open import Agda.Builtin.Nat public
   using (zero; suc) renaming (Nat to ℕ)
 
+--smart constructor
+pattern 2+ n = suc (suc n)
+
 ------------------------------------------------------------------------
 -- Boolean equality relation
 
@@ -59,8 +63,9 @@ m < n = suc m ≤ n
 
 -- Smart constructors of _<_
 
-pattern z<s {n}         = s≤s (z≤n {n})
+pattern z<s     {n}     = s≤s (z≤n {n})
 pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
+pattern sz<ss   {n}     = s<s (z<s {n})
 
 -- Smart destructors of _≤_, _<_
 
@@ -72,7 +77,7 @@ s<s⁻¹ (s<s m<n) = m<n
 
 
 ------------------------------------------------------------------------
--- other ordering relations
+-- Other derived ordering relations
 
 _≥_ : Rel ℕ 0ℓ
 m ≥ n = n ≤ m
@@ -95,13 +100,19 @@ a ≯ b = ¬ a > b
 ------------------------------------------------------------------------
 -- Simple predicates
 
--- Defining `NonZero` in terms of `T` and therefore ultimately `⊤` and
--- `⊥` allows Agda to automatically infer nonZero-ness for any natural
--- of the form `suc n`. Consequently in many circumstances this
--- eliminates the need to explicitly pass a proof when the NonZero
--- argument is either an implicit or an instance argument.
+-- Defining these predicates in terms of `T` and therefore ultimately
+-- `⊤` and `⊥` allows Agda to automatically infer them for any natural
+-- of the correct form. Consequently in many circumstances this
+-- eliminates the need to explicitly pass a proof when the predicate
+-- argument is either an implicit or an instance argument. See `_/_`
+-- and `_%_` further down this file for examples.
 --
--- See `Data.Nat.DivMod` for an example.
+-- Furthermore, defining these predicates as single-field records
+-- (rather defining them directly as the type of their field) is
+-- necessary as the current version of Agda is far better at
+-- reconstructing meta-variable values for the record parameters.
+
+-- A predicate saying that a number is not equal to 0.
 
 record NonZero (n : ℕ) : Set where
   field
@@ -130,6 +141,34 @@ instance
 >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
 >-nonZero⁻¹ (suc n) = z<s
 
+-- The property of being a non-zero, non-unit
+
+record NonTrivial (n : ℕ) : Set where
+  field
+    nonTrivial : T (1 <ᵇ n)
+
+-- Instances
+
+instance
+  nonTrivial : ∀ {n} → NonTrivial (2+ n)
+  nonTrivial = _
+
+-- Constructors
+
+n>1⇒nonTrivial : ∀ {n} → n > 1 → NonTrivial n
+n>1⇒nonTrivial sz<ss = _
+
+-- Destructors
+
+nonTrivial⇒nonZero : ∀ n → .{{NonTrivial n}} → NonZero n
+nonTrivial⇒nonZero (2+ _) = _
+
+nonTrivial⇒n>1 : ∀ n → .{{NonTrivial n}} → n > 1
+nonTrivial⇒n>1 (2+ _) = sz<ss
+
+nonTrivial⇒≢1 : ∀ {n} → .{{NonTrivial n}} → n ≢ 1
+nonTrivial⇒≢1 {{()}} refl
+
 ------------------------------------------------------------------------
 -- Raw bundles