# The congruence relations on the natural numbers

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-01-26.

module elementary-number-theory.congruence-natural-numbers where

Imports
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.distance-natural-numbers
open import elementary-number-theory.divisibility-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types


## Properties

### The congruence relations on the natural numbers

cong-ℕ :
ℕ → ℕ → ℕ → UU lzero
cong-ℕ k x y = div-ℕ k (dist-ℕ x y)

_≡_mod_ : ℕ → ℕ → ℕ → UU lzero
x ≡ y mod k = cong-ℕ k x y

concatenate-eq-cong-eq-ℕ :
(k : ℕ) {x1 x2 x3 x4 : ℕ} →
x1 ＝ x2 → cong-ℕ k x2 x3 → x3 ＝ x4 → cong-ℕ k x1 x4
concatenate-eq-cong-eq-ℕ k refl H refl = H

concatenate-eq-cong-ℕ :
(k : ℕ) {x1 x2 x3 : ℕ} →
x1 ＝ x2 → cong-ℕ k x2 x3 → cong-ℕ k x1 x3
concatenate-eq-cong-ℕ k refl H = H

concatenate-cong-eq-ℕ :
(k : ℕ) {x1 x2 x3 : ℕ} →
cong-ℕ k x1 x2 → x2 ＝ x3 → cong-ℕ k x1 x3
concatenate-cong-eq-ℕ k H refl = H

is-indiscrete-cong-one-ℕ :
(x y : ℕ) → cong-ℕ 1 x y
is-indiscrete-cong-one-ℕ x y = div-one-ℕ (dist-ℕ x y)

is-discrete-cong-zero-ℕ :
(x y : ℕ) → cong-ℕ zero-ℕ x y → x ＝ y
is-discrete-cong-zero-ℕ x y (pair k p) =
eq-dist-ℕ x y ((inv p) ∙ (right-zero-law-mul-ℕ k))

cong-zero-ℕ :
(k : ℕ) → cong-ℕ k k zero-ℕ
pr1 (cong-zero-ℕ k) = 1
pr2 (cong-zero-ℕ k) =
(left-unit-law-mul-ℕ k) ∙ (inv (right-unit-law-dist-ℕ k))

refl-cong-ℕ : (k : ℕ) → is-reflexive (cong-ℕ k)
pr1 (refl-cong-ℕ k x) = zero-ℕ
pr2 (refl-cong-ℕ k x) =
(left-zero-law-mul-ℕ (succ-ℕ k)) ∙ (inv (dist-eq-ℕ x x refl))

cong-identification-ℕ :
(k : ℕ) {x y : ℕ} → x ＝ y → cong-ℕ k x y
cong-identification-ℕ k {x} refl = refl-cong-ℕ k x

symmetric-cong-ℕ : (k : ℕ) → is-symmetric (cong-ℕ k)
pr1 (symmetric-cong-ℕ k x y (pair d p)) = d
pr2 (symmetric-cong-ℕ k x y (pair d p)) = p ∙ (symmetric-dist-ℕ x y)

cong-zero-ℕ' : (k : ℕ) → cong-ℕ k zero-ℕ k
cong-zero-ℕ' k =
symmetric-cong-ℕ k k zero-ℕ (cong-zero-ℕ k)

transitive-cong-ℕ : (k : ℕ) → is-transitive (cong-ℕ k)
transitive-cong-ℕ k x y z e d with is-total-dist-ℕ x y z
transitive-cong-ℕ k x y z e d | inl α =
concatenate-div-eq-ℕ (div-add-ℕ k (dist-ℕ x y) (dist-ℕ y z) d e) α
transitive-cong-ℕ k x y z e d | inr (inl α) =
div-right-summand-ℕ k (dist-ℕ y z) (dist-ℕ x z) e
( concatenate-div-eq-ℕ d (inv α))
transitive-cong-ℕ k x y z e d | inr (inr α) =
div-left-summand-ℕ k (dist-ℕ x z) (dist-ℕ x y) d
( concatenate-div-eq-ℕ e (inv α))

concatenate-cong-eq-cong-ℕ :
{k x1 x2 x3 x4 : ℕ} →
cong-ℕ k x1 x2 → x2 ＝ x3 → cong-ℕ k x3 x4 → cong-ℕ k x1 x4
concatenate-cong-eq-cong-ℕ {k} {x} {y} {.y} {z} H refl K =
transitive-cong-ℕ k x y z K H

concatenate-eq-cong-eq-cong-eq-ℕ :
(k : ℕ) {x1 x2 x3 x4 x5 x6 : ℕ} →
x1 ＝ x2 → cong-ℕ k x2 x3 → x3 ＝ x4 →
cong-ℕ k x4 x5 → x5 ＝ x6 → cong-ℕ k x1 x6
concatenate-eq-cong-eq-cong-eq-ℕ k
{x} {.x} {y} {.y} {z} {.z} refl H refl K refl =
transitive-cong-ℕ k x y z K H

eq-cong-le-dist-ℕ :
(k x y : ℕ) → le-ℕ (dist-ℕ x y) k → cong-ℕ k x y → x ＝ y
eq-cong-le-dist-ℕ k x y H K =
eq-dist-ℕ x y (is-zero-div-ℕ k (dist-ℕ x y) H K)

eq-cong-le-ℕ :
(k x y : ℕ) → le-ℕ x k → le-ℕ y k → cong-ℕ k x y → x ＝ y
eq-cong-le-ℕ k x y H K =
eq-cong-le-dist-ℕ k x y (strict-upper-bound-dist-ℕ k x y H K)

eq-cong-nat-Fin :
(k : ℕ) (x y : Fin k) → cong-ℕ k (nat-Fin k x) (nat-Fin k y) → x ＝ y
eq-cong-nat-Fin (succ-ℕ k) x y H =
is-injective-nat-Fin (succ-ℕ k)
( eq-cong-le-ℕ (succ-ℕ k) (nat-Fin (succ-ℕ k) x) (nat-Fin (succ-ℕ k) y)
( strict-upper-bound-nat-Fin (succ-ℕ k) x)
( strict-upper-bound-nat-Fin (succ-ℕ k) y)
( H))

cong-is-zero-nat-zero-Fin :
{k : ℕ} → cong-ℕ (succ-ℕ k) (nat-Fin (succ-ℕ k) (zero-Fin k)) zero-ℕ
cong-is-zero-nat-zero-Fin {k} =
cong-identification-ℕ (succ-ℕ k) (is-zero-nat-zero-Fin {k})

eq-cong-zero-ℕ : (x y : ℕ) → cong-ℕ zero-ℕ x y → x ＝ y
eq-cong-zero-ℕ x y H =
eq-dist-ℕ x y (is-zero-div-zero-ℕ (dist-ℕ x y) H)

is-one-cong-succ-ℕ : {k : ℕ} (x : ℕ) → cong-ℕ k x (succ-ℕ x) → is-one-ℕ k
is-one-cong-succ-ℕ {k} x H =
is-one-div-one-ℕ k (tr (div-ℕ k) (is-one-dist-succ-ℕ x) H)


### Congruence is invariant under scalar multiplication

scalar-invariant-cong-ℕ :
(k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (z *ℕ x) (z *ℕ y)
pr1 (scalar-invariant-cong-ℕ k x y z (pair d p)) = z *ℕ d
pr2 (scalar-invariant-cong-ℕ k x y z (pair d p)) =
( associative-mul-ℕ z d k) ∙
( ( ap (z *ℕ_) p) ∙
( left-distributive-mul-dist-ℕ x y z))

scalar-invariant-cong-ℕ' :
(k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (x *ℕ z) (y *ℕ z)
scalar-invariant-cong-ℕ' k x y z H =
concatenate-eq-cong-eq-ℕ k
( commutative-mul-ℕ x z)
( scalar-invariant-cong-ℕ k x y z H)
( commutative-mul-ℕ z y)


### Multiplication respects the congruence relation

congruence-mul-ℕ :
(k : ℕ) {x y x' y' : ℕ} →
cong-ℕ k x x' → cong-ℕ k y y' → cong-ℕ k (x *ℕ y) (x' *ℕ y')
congruence-mul-ℕ k {x} {y} {x'} {y'} H K =
transitive-cong-ℕ k (x *ℕ y) (x *ℕ y') (x' *ℕ y')
( scalar-invariant-cong-ℕ' k x x' y' H)
( scalar-invariant-cong-ℕ k y y' x K)


### The congruence is translation invariant

translation-invariant-cong-ℕ :
(k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (z +ℕ x) (z +ℕ y)
pr1 (translation-invariant-cong-ℕ k x y z (pair d p)) = d
pr2 (translation-invariant-cong-ℕ k x y z (pair d p)) =
p ∙ inv (translation-invariant-dist-ℕ z x y)

translation-invariant-cong-ℕ' :
(k x y z : ℕ) → cong-ℕ k x y → cong-ℕ k (x +ℕ z) (y +ℕ z)
translation-invariant-cong-ℕ' k x y z H =
concatenate-eq-cong-eq-ℕ k
( translation-invariant-cong-ℕ k x y z H)

step-invariant-cong-ℕ :
(k x y : ℕ) → cong-ℕ k x y → cong-ℕ k (succ-ℕ x) (succ-ℕ y)
step-invariant-cong-ℕ k x y = translation-invariant-cong-ℕ' k x y 1

{k : ℕ} (x : ℕ) {y z : ℕ} → cong-ℕ k (x +ℕ y) (x +ℕ z) → cong-ℕ k y z
pr1 (reflects-cong-add-ℕ {k} x {y} {z} (pair d p)) = d
pr2 (reflects-cong-add-ℕ {k} x {y} {z} (pair d p)) =
p ∙ translation-invariant-dist-ℕ x y z