\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan renaming (_+_ to _โ_)
open import Naturals.Division
open import Naturals.Exponentiation
open import Naturals.Multiplication
open import Naturals.Properties
open import UF.Subsingletons

module Naturals.Parity where

even odd : โ โ ๐คโ ฬ
even 0        = ๐
even (succ n) = odd n
odd 0         = ๐
odd (succ n)  = even n

zero-not-odd : (n : โ) โ odd n โ ยฌ (n ๏ผ 0)
zero-not-odd 0        on e = on
zero-not-odd (succ n) on e = positive-not-zero n e

even-is-prop : (n : โ) โ is-prop (even n)
even-is-prop 0               = ๐-is-prop
even-is-prop 1               = ๐-is-prop
even-is-prop (succ (succ n)) = even-is-prop n

odd-is-prop : (n : โ) โ is-prop (odd n)
odd-is-prop 0               = ๐-is-prop
odd-is-prop 1               = ๐-is-prop
odd-is-prop (succ (succ n)) = odd-is-prop n

even-not-odd : (n : โ) โ even n โ ยฌ odd n
even-not-odd 0               even-n odd-n = odd-n
even-not-odd 1               even-n odd-n = even-n
even-not-odd (succ (succ n)) even-n odd-n = even-not-odd n even-n odd-n

odd-not-even : (n : โ) โ odd n โ ยฌ even n
odd-not-even n odd-n even-n = even-not-odd n even-n odd-n

even-or-odd : (n : โ) โ even n โ odd n
even-or-odd 0               = inl โ
even-or-odd 1               = inr โ
even-or-odd (succ (succ n)) = even-or-odd n

even-or-odd-is-prop : (n : โ) โ is-prop (even n โ odd n)
even-or-odd-is-prop n =  ฮณ
where
ฮณ : is-prop (even n โ odd n)
ฮณ = +-is-prop (even-is-prop n) (odd-is-prop n) (even-not-odd n)

succ-even-is-odd : (n : โ) โ even n โ odd (succ n)
succ-even-is-odd n = id

succ-odd-is-even : (n : โ) โ odd n โ even (succ n)
succ-odd-is-even n = id

odd-succ-succ : (n : โ) โ odd n โ odd (succ (succ n))
odd-succ-succ n = id

odd-succ-succ' : (n : โ) โ odd (succ (succ n)) โ odd n
odd-succ-succ' n = id

even-succ-succ : (n : โ) โ even n โ even (succ (succ n))
even-succ-succ n = id

even-succ-succ' : (n : โ) โ even (succ (succ n)) โ even n
even-succ-succ' n = id

even+even : (n m : โ) โ even n โ even m โ even (n + m)
even+even n 0               even-n even-m = even-n
even+even n 1               even-n even-m = ๐-elim even-m
even+even n (succ (succ m)) even-n even-m = even+even n m even-n even-m

even+odd : (n m : โ) โ even n โ odd m โ odd (n + m)
even+odd n 0               even-n odd-m = ๐-elim odd-m
even+odd n 1               even-n odd-m = even-n
even+odd n (succ (succ m)) even-n odd-m = even+odd n m even-n odd-m

odd+even : (n m : โ) โ odd n โ even m โ odd (n + m)
odd+even n m odd-n even-m = transport
odd
(even+odd m n even-m odd-n)

odd+odd : (n m : โ) โ odd n โ odd m โ even (n + m)
odd+odd n 0               odd-n odd-m = ๐-elim odd-m
odd+odd n 1               odd-n odd-m = odd-n
odd+odd n (succ (succ m)) odd-n odd-m = odd+odd n m odd-n odd-m

even*even : (n m : โ) โ even n โ even m โ even (n * m)
even*even n 0               even-n even-m = even-m
even*even n 1               even-n even-m = even-n
even*even n (succ (succ m)) even-n even-m = even+even n (n + n * m) even-n I
where
IH : even (n * m)
IH = even*even n m even-n even-m
I : even (n + n * m)
I = even+even n (n * m) even-n IH

odd*odd : (n m : โ) โ odd n โ odd m โ odd (n * m)
odd*odd n 0               odd-n odd-m = odd-m
odd*odd n 1               odd-n odd-m = odd-n
odd*odd n (succ (succ m)) odd-n odd-m = odd+even n (n + n * m) odd-n I
where
IH : odd (n * m)
IH = odd*odd n m odd-n odd-m

I : even (n + n * m)
I = odd+odd n (n * m) odd-n IH

even*odd : (n m : โ) โ even n โ odd m โ even (n * m)
even*odd n 0               even-n odd-m = โ
even*odd n 1               even-n odd-m = even-n
even*odd n (succ (succ m)) even-n odd-m = even+even n (n + n * m) even-n I
where
IH : even (n * m)
IH = even*odd n m even-n odd-m
I : even (n + n * m)
I = even+even n (n * m) even-n IH

odd*even : (n m : โ) โ odd n โ even m โ even (n * m)
odd*even n m odd-n even-m = ฮณ
where
ฮณ : even (n * m)
ฮณ = transport even (mult-commutativity m n) (even*odd m n even-m odd-n)

multiple-of-two-even-lemma : (n k : โ) โ n ๏ผ 2 * k โ even n
multiple-of-two-even-lemma n 0               e = transport even (e โปยน) โ
multiple-of-two-even-lemma n 1               e = transport even (e โปยน) โ
multiple-of-two-even-lemma n (succ (succ k)) e = transport even (e โปยน) III
where
I : even (2 * k)
I = multiple-of-two-even-lemma (2 * k) k refl
II : even (2 + 2 * k)
II = even+even 2 (2 * k) โ I
III : even (2 + (2 + 2 * k))
III = even+even 2 (2 + 2 * k) โ II

multiple-of-two-even : (n : โ) โ ฮฃ k ๊ โ , n ๏ผ 2 * k โ even n
multiple-of-two-even n (k , e) = multiple-of-two-even-lemma n k e

succ-multiple-of-two-odd : (n k : โ) โ n ๏ผ succ (2 * k) โ odd n
succ-multiple-of-two-odd 0        k e = positive-not-zero (2 * k) (e โปยน)
succ-multiple-of-two-odd (succ n) k e = multiple-of-two-even n (k , (succ-lc e))

even-is-multiple-of-two : (n : โ) โ even n โ ฮฃ k ๊ โ , n ๏ผ 2 * k
even-is-multiple-of-two 0               even-0  = 0 , refl
even-is-multiple-of-two 1               even-1  = ๐-elim even-1
even-is-multiple-of-two (succ (succ n)) even-sn = II IH
where
IH : ฮฃ k ๊ โ , n ๏ผ 2 * k
IH = even-is-multiple-of-two n even-sn

II : ฮฃ k ๊ โ , n ๏ผ 2 * k โ ฮฃ k ๊ โ , succ (succ n) ๏ผ 2 * k
II (k , e) = (succ k) , I
where
I : succ (succ n) ๏ผ 2 * succ k
I = succ (succ n) ๏ผโจ addition-commutativity n 2 โฉ
2 + n         ๏ผโจ ap (2 +_) e                โฉ
2 + 2 * k     ๏ผโจ refl                       โฉ
2 * succ k    โ

odd-is-succ-multiple-of-two : (n : โ) โ odd n โ ฮฃ k ๊ โ , n ๏ผ succ (2 * k)
odd-is-succ-multiple-of-two 0        odd-n = ๐-elim odd-n
odd-is-succ-multiple-of-two (succ n) odd-sn = II I
where
I : ฮฃ k ๊ โ , n ๏ผ 2 * k
I = even-is-multiple-of-two n odd-sn

II : ฮฃ k ๊ โ , n ๏ผ 2 * k โ ฮฃ k ๊ โ , succ n ๏ผ succ (2 * k)
II (k , e) = k , (ap succ e)

times-even-is-even : (m n  : โ) โ even m โ even (m * n)
times-even-is-even m n em = I (even-or-odd n)
where
I : even n โ odd n โ even (m * n)
I (inl en) = even*even m n em en
I (inr on) = even*odd m n em on

times-even-is-even' : (m n  : โ) โ even n โ even (m * n)
times-even-is-even' m n en = ฮณ
where
ฮณ : even (m * n)
ฮณ = transport even (mult-commutativity n m) (times-even-is-even n m en)

only-odd-divides-odd : (d n : โ) โ odd n โ d โฃ n โ odd d
only-odd-divides-odd d n on (k , e) = I (even-or-odd d) (even-or-odd k)
where
I : even d โ odd d โ even k โ odd k โ odd d
I (inr od) _        = od
I (inl ed) (inl ek) = ๐-elim ฮณ
where
en : even n
en = transport even e (even*even d k ed ek)

ฮณ : ๐
ฮณ = even-not-odd n en on

I (inl ed) (inr ok) = ๐-elim ฮณ
where
en : even n
en = transport even e (even*odd d k ed ok)

ฮณ : ๐
ฮณ = even-not-odd n en on

2-exponents-even : (n : โ) โ even (2^ (succ n))
2-exponents-even 0        = โ    -- 2 even
2-exponents-even (succ n) = even*even 2 (2^ (succ n)) โ (2-exponents-even n)

odd-factors-of-2-exponents : (d n : โ) โ d โฃ 2^ n โ odd d โ d ๏ผ 1
odd-factors-of-2-exponents d 0        (k , e) od = left-factor-one d k e
odd-factors-of-2-exponents d (succ n) (k , e) od = Cases (even-or-odd k) ฮณโ ฮณโ
where
I : even (2^ (succ n))
I = 2-exponents-even n

ฮณโ : even k โ d ๏ผ 1
ฮณโ ek = II (even-is-multiple-of-two k ek)
where
II : ฮฃ k' ๊ โ , k ๏ผ 2 * k' โ d ๏ผ 1
II (k' , e') = odd-factors-of-2-exponents d n ฮณโ od
where
III : 2 * (d * k') ๏ผ 2 * 2^ n
III = 2 * (d * k') ๏ผโจ mult-commutativity 2 (d * k')       โฉ
d * k' * 2   ๏ผโจ mult-associativity d k' 2           โฉ
d * (k' * 2) ๏ผโจ ap (d *_) (mult-commutativity k' 2) โฉ
d * (2 * k') ๏ผโจ ap (d *_) (e' โปยน)                   โฉ
d * k        ๏ผโจ e                                   โฉ
2 * 2^ n     โ

IV : d * k' ๏ผ 2^ n
IV = mult-left-cancellable (d * k') (2^ n) 1 III

ฮณโ : d โฃ 2^ n
ฮณโ = k' , IV

ฮณโ : odd k โ d ๏ผ 1
ฮณโ ok = ๐-elim (even-not-odd (2^ (succ n)) I II)
where
II : odd (2^ (succ n))
II = transport odd e (odd*odd d k od ok)

factors-of-2-exponents : (d n : โ) โ d โฃ 2^ n โ (d ๏ผ 1) โ even d
factors-of-2-exponents d n d|2^n = I (even-or-odd d)
where
I : even d โ odd d โ (d ๏ผ 1) โ even d
I (inl ed) = inr ed
I (inr od) = inl (odd-factors-of-2-exponents d n d|2^n od)

odd-power-of-two-coprime : (d x n : โ) โ odd x โ d โฃ x โ d โฃ 2^ n โ d โฃ 1
odd-power-of-two-coprime d x n ox d|x d|2^n = Cases ฮฑ ฮณโ ฮณโ
where
ฮฑ : (d ๏ผ 1) โ even d
ฮฑ = factors-of-2-exponents d n d|2^n

od : odd d
od = only-odd-divides-odd d x ox d|x

ฮณโ : d ๏ผ 1 โ d โฃ 1
ฮณโ e = 1 , e

ฮณโ : even d โ d โฃ 1
ฮณโ ed = ๐-elim (odd-not-even d od ed)

even-transport : (z : โ) โ (ez : even z) (p : even z โ odd z) โ p ๏ผ inl ez
even-transport z ez (inl ez') = ap inl (even-is-prop z ez' ez)
even-transport z ez (inr oz)  = ๐-elim (even-not-odd z ez oz)

odd-transport : (z : โ) โ (oz : odd z) (p : even z โ odd z) โ p ๏ผ inr oz
odd-transport z oz (inl ez)  = ๐-elim (even-not-odd z ez oz)
odd-transport z oz (inr oz') = ap inr (odd-is-prop z oz' oz)

\end{code}

Sometimes the following definitions and constructions are useful:

\begin{code}

is-even' is-odd' : โ โ ๐คโ ฬ
is-even' n = ฮฃ k ๊ โ ,  double k ๏ผ n
is-odd'  n = ฮฃ k ๊ โ , sdouble k ๏ผ n

even-or-odd' : (n : โ) โ is-even' n โ is-odd' n
even-or-odd' 0        = inl (0 , refl)
even-or-odd' (succ n) =
Cases (even-or-odd' n)
(ฮป ((k , e) : is-even' n)
โ inr (k , ap succ e))
(ฮป ((k , e) : is-odd' n)
โ inl (succ k , ap succ e))

even-not-odd' : (n k : โ) โ ยฌ (double n ๏ผ sdouble k)
even-not-odd' 0        k e = zero-not-positive (double k) e
even-not-odd' (succ n) k e = even-not-odd' k n ((succ-lc e)โปยน)

not-even-and-odd' : (n : โ) โ ยฌ (is-even' n ร is-odd' n)
not-even-and-odd' n ((k , e) , (k' , e')) =
even-not-odd' k k'
(double k   ๏ผโจ e โฉ
n          ๏ผโจ e' โปยน โฉ
sdouble k' โ)

\end{code}