odd+odd, even+even, even+odd

eveneven.ctt

module eveneven where

Path (A : U) (a b : A) : U = PathP (<_> A) a b

data bool = true | false

data nat = zero
         | suc (n : nat)

add (m : nat) : nat -> nat = split
  zero -> m
  suc n -> suc (add m n)

mutual
  even : nat -> bool = split
    zero -> true
    suc n -> odd n

  odd : nat -> bool = split
    zero -> false
    suc n -> even n

and (x:bool) : bool -> bool = split
  true -> x
  false -> false

andtrue : (x:bool) -> Path bool x (and true x) = split
  true -> <i> true
  false -> <i> false

andfalse : (x:bool) -> Path bool false (and false x) = split
  true -> <i> false
  false -> <i> false

andsym (a:bool) : (b:bool) -> Path bool (and a b) (and b a) = split
  true -> andtrue a
  false -> andfalse a

evenodd : (n : nat) -> Path bool (even n) (odd (suc n)) = split
  zero -> <i> true
  suc n -> <i> odd n
     
addsuc (a:nat) : (n : nat) -> Path nat (add (suc a) n) (suc (add a n)) = split
  zero  ->  <i> suc a
  suc m -> <i> suc (addsuc a m @ i)

mutual
  even_plus_even_is_even (n:nat) : (m : nat) -> Path bool (and (even n) (even m)) (even(add n m)) = split
    zero -> <i> even n
    suc m -> even_plus_odd_is_odd n m

  odd_plus_even_is_odd (n:nat) : (m : nat) -> Path bool (and (odd n) (even m)) (odd(add n m)) = split
    zero ->  <i> odd n
    suc m -> odd_plus_odd_is_even n m

  even_plus_odd_is_odd (n:nat) : (m : nat) -> Path bool (and (even n) (odd m)) (odd(add n m)) = split
    zero ->  ? -- TODO
    suc m -> even_plus_even_is_even n m

  odd_plus_odd_is_even (n:nat) : (m : nat) -> Path bool (and (odd n) (odd m)) (even(add n m)) = split
    zero ->  ? -- TODO
    suc m -> odd_plus_even_is_odd n m
    

module eveneven where

Path (A : U) (a b : A) : U = PathP (<_> A) a b

data bool = true | false

data nat = zero
         | suc (n : nat)

add (m : nat) : nat -> nat = split
  zero -> m
  suc n -> suc (add m n)

data tt = trivial
data ff =

mutual
  evenT : nat -> U = split
    zero -> tt
    suc n -> oddT n

  oddT : nat -> U = split
    zero -> ff
    suc n -> evenT n

zeroIsEvenT : evenT zero = trivial

evenSuccIsOddT (n: nat) (pn: evenT n): oddT (suc n) = pn
oddSuccIsEvenT (n: nat) (pn: oddT n): evenT (suc n) = pn

evenPredIsOddT: (n: nat) (pn: oddT (suc n)) -> evenT n = split
  zero -> \(pn: oddT (suc zero)) -> pn
  suc n' ->  \(pn: oddT (suc (suc n'))) -> pn

efq (A:U) : ff -> A = split {}
neg (A:U) : U = A -> ff

mutual
  evenPlusEvenIsEven : (n m:nat) (pn:evenT n) (pm : evenT m) -> evenT (add m n) = split
    zero   -> \(m : nat) (pn : evenT zero)    (pm : evenT m) -> pm
    suc n' -> \(m : nat) (pn : oddT n')       (pm : evenT m) -> oddPlusEvenIsOdd n' m pn pm

  oddPlusEvenIsOdd : (n m:nat) (pn:oddT n) (pm: evenT m) -> oddT (add m n) = split
    zero   -> \(m : nat) (pn : oddT zero)  (pm : evenT m) -> efq (oddT m) pn
    suc n' -> \(m : nat) (pn : evenT n')   (pm : evenT m) -> evenPlusEvenIsEven n' m pn pm

  oddPlusOddIsEven : (n m:nat) (pn:oddT n) (pm : oddT m) -> evenT (add m n) = split
    zero   -> \(m : nat) (pn : oddT zero)  (pm : oddT m) -> efq (evenT m) pn
    suc n' -> \(m : nat) (pn : evenT n')   (pm : oddT m) -> evenPlusOddIsOdd n' m pn pm

  evenPlusOddIsOdd : (n m:nat) (pn:evenT n) (pm : oddT m) -> oddT (add m n) = split
    zero   -> \(m : nat) (pn : evenT zero)  (pm : oddT m) -> pm
    suc n' -> \(m : nat) (pn : oddT n')     (pm : oddT m) -> oddPlusOddIsEven n' m pn pm