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
    

isEven (n: nat): U = Path bool (even n) true
isOdd (n: nat): U = Path bool (odd n) true

zeroIsEven : isEven zero = <i> true

evenSuccIsOdd (n: nat) (pn: isEven n): isOdd (suc n) = pn
oddSuccIsEven (n: nat) (pn: isOdd n): isEven (suc n) = pn

evenPredIsOdd: (n: nat) (pn: isOdd (suc n)) -> isEven n = split
  zero -> \(pn: isOdd (suc zero)) -> pn
  suc n' ->  \(pn: isOdd (suc (suc n'))) -> pn

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

isEven (n: nat): U = Path bool (even n) true
isOdd  (n: nat): U = Path bool (odd n)  true

zeroIsEven : isEven zero = <i> true

evenPlusEvenIsEven : (n:nat) (m:nat) (pn:isEven n) (pm:isEven m) -> isEven (add m n) = split
  zero   -> \(m : nat) -> \(pn : isEven zero) -> \(pm : isEven m) -> pm
  suc n' -> \(m : nat) -> \(pn : isOdd n') -> \(pm : isEven m) ->
    evenPlusEvenIsEven (suc n') m pn pm

Вот это почти:

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

Ни один Path в ходе работы над этими определениями не пострадал :) можно в принципе даже без data обойтись для tt и ff, но это следующий уровень тайп-фу

Ну сформулировать теорему теперь просто:

evenSumIsEven: (n m: nat) (p: evenT n) (q: evenT m) -> evenT (add n m) = undefined

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