\begin{code}

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

open import MLTT.Spartan renaming (_+_ to _โˆ”_)
open import Naturals.Addition
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
                              (addition-commutativity m n)
                               (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}