parity.kind2

Flip (n: Nat) : Nat
Flip Nat.zero            = 1n
Flip (Nat.succ Nat.zero) = 0n

Mod2 (n: Nat) : Nat
Mod2 Nat.zero     = Nat.zero
Mod2 (Nat.succ n) = Flip (Mod2 n)

IsEven (n: Nat) : Type
IsEven Nat.zero                = Unit
IsEven (Nat.succ Nat.zero)     = Empty
IsEven (Nat.succ (Nat.succ n)) = IsEven n

// ------------------

Theorem (n: Nat) (is_even: IsEven n) : Equal Nat (Mod2 n) Nat.zero
Theorem Nat.zero                is_even = Equal.refl
Theorem (Nat.succ Nat.zero)     is_even = Empty.absurd is_even
Theorem (Nat.succ (Nat.succ p)) is_even =
  let ind = Theorem p is_even
  let prf = Equal.apply (x => Flip (Flip x)) ind
  prf

// ------------------

Theorem (n: Nat) (is_even: IsEven n) : Equal Nat (Mod2 n) Nat.zero
Theorem n is_even =
  match Nat n with (is_even : IsEven n) {
    zero => Equal.refl
    succ => match Nat n.pred with (is_even : IsEven (Nat.succ n.pred)) {
      zero => Empty.absurd is_even
      succ =>
        let ind = Theorem n.pred.pred is_even
        let prf = Equal.apply (x => Flip (Flip x)) ind
        prf
    }: Equal Nat (Flip (Mod2 n.pred)) 0n
  }: Equal Nat (Mod2 n) Nat.zero

// ------------------

Theorem (n: Nat) (is_even: IsEven n) : Equal Nat (Mod2 n) Nat.zero
Theorem n is_even =
  ((Nat.match n (n => (is_even: IsEven n) -> Equal Nat (Mod2 n) Nat.zero)
    // case zero
    (is_even => Equal.refl)
    // case succ
    (pred => is_even =>
      ((Nat.match pred (pred => (is_even: (IsEven (Nat.succ pred))) -> (Equal Nat (Flip (Mod2 pred)) 0n))
        // case zero
        (is_even => Empty.absurd is_even)
        // case succ
        (pred => is_even =>
          let ind = Theorem pred is_even
          let prf = Equal.apply (x => Flip (Flip x)) ind
          prf)
      ) is_even)
    )
  ) is_even)

// ------------------

Theorem (n: Nat) (is_even: IsEven n) : Equal Nat (Mod2 n) Nat.zero
Theorem n is_even =
  ((Nat.match.parity n (n => (is_even: IsEven n) -> Equal Nat (Mod2 n) Nat.zero)
    (half => is_even => Theorem.aux0 half)
    (half_pred => is_even => Theorem.aux1 half_pred is_even)
  ) is_even)

Theorem.aux0 (m: Nat) : Equal Nat (Mod2 (Nat.double m)) 0n
Theorem.aux0 Nat.zero     = Equal.refl
Theorem.aux0 (Nat.succ n) =
  let ind = Theorem.aux0 n
  let prf = Equal.apply (x => Flip (Flip x)) ind
  prf

Theorem.aux1 (m: Nat) (e: IsEven (Nat.succ (Nat.double m))) : Equal Nat (Flip (Mod2 (Nat.double m))) 0n
Theorem.aux1 Nat.zero     e = Empty.absurd e
Theorem.aux1 (Nat.succ p) e =
  let ind = Theorem.aux1 p e
  let prf = Equal.apply (x => Flip (Flip x)) ind
  prf

// ------------------

Nat.to_bits (n: Nat) : Bits
Bits.to_nat (b: Bits) : Nat
Iso (n: Nat) : Equal Nat (Bits.to_nat (Nat.to_bits n)) n