# Addition on integer fractions

Content created by Fredrik Bakke, Egbert Rijke, Fernando Chu and malarbol.

Created on 2023-04-08.
Last modified on 2024-04-09.

module elementary-number-theory.addition-integer-fractions where

Imports
open import elementary-number-theory.addition-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.multiplication-positive-and-negative-integers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types


## Idea

We introduce addition on integer fractions and derive its basic properties. Note that the properties only hold up to fraction similarity.

## Definition

add-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ
pr1 (add-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos)) =
(m *ℤ n') +ℤ (m' *ℤ n)
pr1 (pr2 (add-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
n *ℤ n'
pr2 (pr2 (add-fraction-ℤ (m , n , n-pos) (m' , n' , n'-pos))) =
is-positive-mul-ℤ n-pos n'-pos

add-fraction-ℤ' : fraction-ℤ → fraction-ℤ → fraction-ℤ
add-fraction-ℤ' x y = add-fraction-ℤ y x

infixl 35 _+fraction-ℤ_
_+fraction-ℤ_ = add-fraction-ℤ

ap-add-fraction-ℤ :
{x y x' y' : fraction-ℤ} → x ＝ x' → y ＝ y' →
x +fraction-ℤ y ＝ x' +fraction-ℤ y'
ap-add-fraction-ℤ p q = ap-binary add-fraction-ℤ p q


## Properties

### Addition respects the similarity relation

abstract
sim-fraction-add-fraction-ℤ :
{x x' y y' : fraction-ℤ} →
sim-fraction-ℤ x x' →
sim-fraction-ℤ y y' →
sim-fraction-ℤ (x +fraction-ℤ y) (x' +fraction-ℤ y')
sim-fraction-add-fraction-ℤ
{(nx , dx , dxp)} {(nx' , dx' , dx'p)}
{(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q =
equational-reasoning
((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ (dx' *ℤ dy')
＝ ((nx *ℤ dy) *ℤ (dx' *ℤ dy')) +ℤ ((ny *ℤ dx) *ℤ (dx' *ℤ dy'))
by right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) (dx' *ℤ dy')
＝ ((dy *ℤ nx) *ℤ (dx' *ℤ dy')) +ℤ ((dx *ℤ ny) *ℤ (dy' *ℤ dx'))
by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ nx dy) refl)
(ap-mul-ℤ (commutative-mul-ℤ ny dx) (commutative-mul-ℤ dx' dy'))
＝ (((dy *ℤ nx) *ℤ dx') *ℤ dy') +ℤ (((dx *ℤ ny) *ℤ dy') *ℤ dx')
by ap-add-ℤ (inv (associative-mul-ℤ (dy *ℤ nx) dx' dy'))
(inv (associative-mul-ℤ (dx *ℤ ny) dy' dx'))
＝ ((dy *ℤ (nx *ℤ dx')) *ℤ dy') +ℤ ((dx *ℤ (ny *ℤ dy')) *ℤ dx')
by ap-add-ℤ (ap-mul-ℤ (associative-mul-ℤ dy nx dx') refl)
(ap-mul-ℤ (associative-mul-ℤ dx ny dy') refl)
＝ ((dy *ℤ (dx *ℤ nx')) *ℤ dy') +ℤ ((dx *ℤ (dy *ℤ ny')) *ℤ dx')
by ap-add-ℤ
(ap-mul-ℤ (ap-mul-ℤ (refl {x = dy}) (p ∙ commutative-mul-ℤ nx' dx))
(refl {x = dy'}))
(ap-mul-ℤ (ap-mul-ℤ (refl {x = dx}) (q ∙ commutative-mul-ℤ ny' dy))
(refl {x = dx'}))
＝ (((dy *ℤ dx) *ℤ nx') *ℤ dy') +ℤ (((dx *ℤ dy) *ℤ ny') *ℤ dx')
by ap-add-ℤ (ap-mul-ℤ (inv (associative-mul-ℤ dy dx nx')) refl)
(ap-mul-ℤ (inv (associative-mul-ℤ dx dy ny')) refl)
＝ ((nx' *ℤ (dy *ℤ dx)) *ℤ dy') +ℤ ((ny' *ℤ (dx *ℤ dy)) *ℤ dx')
by ap-add-ℤ (ap-mul-ℤ (commutative-mul-ℤ (dy *ℤ dx) nx') refl)
(ap-mul-ℤ (commutative-mul-ℤ (dx *ℤ dy) ny') refl)
＝ (nx' *ℤ ((dy *ℤ dx) *ℤ dy')) +ℤ (ny' *ℤ ((dx *ℤ dy) *ℤ dx'))
by ap-add-ℤ (associative-mul-ℤ nx' (dy *ℤ dx) dy')
(associative-mul-ℤ ny' (dx *ℤ dy) dx')
＝ (nx' *ℤ (dy' *ℤ (dy *ℤ dx))) +ℤ (ny' *ℤ (dx' *ℤ (dx *ℤ dy)))
by ap-add-ℤ
(ap-mul-ℤ (refl {x = nx'}) (commutative-mul-ℤ (dy *ℤ dx) dy'))
(ap-mul-ℤ (refl {x = ny'}) (commutative-mul-ℤ (dx *ℤ dy) dx'))
＝ ((nx' *ℤ dy') *ℤ (dy *ℤ dx)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy))
by ap-add-ℤ (inv (associative-mul-ℤ nx' dy' (dy *ℤ dx)))
(inv (associative-mul-ℤ ny' dx' (dx *ℤ dy)))
＝ ((nx' *ℤ dy') *ℤ (dx *ℤ dy)) +ℤ ((ny' *ℤ dx') *ℤ (dx *ℤ dy))
by ap-add-ℤ
(ap-mul-ℤ (refl {x = nx' *ℤ dy'}) (commutative-mul-ℤ dy dx)) refl
＝ ((nx' *ℤ dy') +ℤ (ny' *ℤ dx')) *ℤ (dx *ℤ dy)
by inv (right-distributive-mul-add-ℤ (nx' *ℤ dy') _ (dx *ℤ dy))


### Unit laws

abstract
left-unit-law-add-fraction-ℤ :
(k : fraction-ℤ) →
sim-fraction-ℤ (zero-fraction-ℤ +fraction-ℤ k) k
left-unit-law-add-fraction-ℤ (m , n , p) =
ap-mul-ℤ (right-unit-law-mul-ℤ m) refl

right-unit-law-add-fraction-ℤ :
(k : fraction-ℤ) →
sim-fraction-ℤ (k +fraction-ℤ zero-fraction-ℤ) k
right-unit-law-add-fraction-ℤ (m , n , p) =
ap-mul-ℤ
( ap-add-ℤ (right-unit-law-mul-ℤ m) refl ∙ right-unit-law-add-ℤ m)
( inv (right-unit-law-mul-ℤ n))


### Addition is associative

abstract
associative-add-fraction-ℤ :
(x y z : fraction-ℤ) →
sim-fraction-ℤ
((x +fraction-ℤ y) +fraction-ℤ z)
(x +fraction-ℤ (y +fraction-ℤ z))
associative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) =
ap-mul-ℤ (eq-num) (inv (associative-mul-ℤ dx dy dz))
where
eq-num :
( ((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)) ＝
( (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx))
eq-num =
equational-reasoning
(((nx *ℤ dy) +ℤ (ny *ℤ dx)) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy))
＝ (((nx *ℤ dy) *ℤ dz) +ℤ ((ny *ℤ dx) *ℤ dz)) +ℤ
(nz *ℤ (dx *ℤ dy))
by ap-add-ℤ
(right-distributive-mul-add-ℤ (nx *ℤ dy) (ny *ℤ dx) dz) refl
＝ ((nx *ℤ dy) *ℤ dz) +ℤ
(((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)))
by associative-add-ℤ
((nx *ℤ dy) *ℤ dz) ((ny *ℤ dx) *ℤ dz) _
＝ (nx *ℤ (dy *ℤ dz)) +ℤ
(((ny *ℤ dx) *ℤ dz) +ℤ (nz *ℤ (dx *ℤ dy)))
by ap-add-ℤ (associative-mul-ℤ nx dy dz) refl
＝ (nx *ℤ (dy *ℤ dz)) +ℤ
((ny *ℤ (dz *ℤ dx)) +ℤ (nz *ℤ (dy *ℤ dx)))
by ap-add-ℤ
(refl {x = nx *ℤ (dy *ℤ dz)})
(ap-add-ℤ
(associative-mul-ℤ ny dx dz ∙ ap-mul-ℤ (refl {x = ny})
(commutative-mul-ℤ dx dz))
(ap-mul-ℤ (refl {x = nz}) (commutative-mul-ℤ dx dy)))
＝ (nx *ℤ (dy *ℤ dz)) +ℤ
(((ny *ℤ dz) *ℤ dx) +ℤ ((nz *ℤ dy) *ℤ dx))
by ap-add-ℤ
(refl {x = nx *ℤ (dy *ℤ dz)})
(inv
(ap-add-ℤ
( associative-mul-ℤ ny dz dx)
( associative-mul-ℤ nz dy dx)))
＝ (nx *ℤ (dy *ℤ dz)) +ℤ (((ny *ℤ dz) +ℤ (nz *ℤ dy)) *ℤ dx)
by ap-add-ℤ
(refl {x = nx *ℤ (dy *ℤ dz)})
(inv (right-distributive-mul-add-ℤ (ny *ℤ dz) (nz *ℤ dy) dx))


### Addition is commutative

abstract
commutative-add-fraction-ℤ :
(x y : fraction-ℤ) →
sim-fraction-ℤ
(x +fraction-ℤ y)
(y +fraction-ℤ x)
commutative-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) =
ap-mul-ℤ
( commutative-add-ℤ (nx *ℤ dy) (ny *ℤ dx))
( commutative-mul-ℤ dy dx)


### The numerator of the sum of an integer fraction and its negative is zero

abstract
is-zero-numerator-add-left-neg-fraction-ℤ :
(x : fraction-ℤ) →
is-zero-ℤ (numerator-fraction-ℤ (add-fraction-ℤ (neg-fraction-ℤ x) x))
is-zero-numerator-add-left-neg-fraction-ℤ (p , q , H) =
ap (_+ℤ (p *ℤ q)) (left-negative-law-mul-ℤ p q) ∙
left-inverse-law-add-ℤ (p *ℤ q)

is-zero-numerator-add-right-neg-fraction-ℤ :
(x : fraction-ℤ) →
is-zero-ℤ (numerator-fraction-ℤ (add-fraction-ℤ x (neg-fraction-ℤ x)))
is-zero-numerator-add-right-neg-fraction-ℤ (p , q , H) =
ap ((p *ℤ q) +ℤ_) (left-negative-law-mul-ℤ p q) ∙
right-inverse-law-add-ℤ (p *ℤ q)


### Distributivity of negatives over addition on the integer fractions

abstract
distributive-neg-add-fraction-ℤ :
(x y : fraction-ℤ) →
sim-fraction-ℤ
(neg-fraction-ℤ (x +fraction-ℤ y))
(neg-fraction-ℤ x +fraction-ℤ neg-fraction-ℤ y)
distributive-neg-add-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) =
ap
( _*ℤ (dx *ℤ dy))
( ( distributive-neg-add-ℤ (nx *ℤ dy) (ny *ℤ dx)) ∙
( ap-add-ℤ
( inv (left-negative-law-mul-ℤ nx dy))
( inv (left-negative-law-mul-ℤ ny dx))))