test/basic002/test006.idr · Idris-dev

git.iko.soy/Idris-dev

on 7afa310 help sign in

38 lines 856 B history raw

1module Main

3data Parity : Nat -> Type where

4 even : {n : Nat} -> Parity (n + n)

5 odd : {n : Nat} -> Parity (S (n + n))

7parity : (n:Nat) -> Parity n

8parity Z = even {n=Z}

9parity (S Z) = odd {n=Z}

10parity (S (S k)) with (parity k)

11 parity (S (S (j + j))) | (even {n = j}) ?= even {n=S j}

12 parity (S (S (S (j + j)))) | (odd {n = j}) ?= odd {n=S j}

14natToBin : Nat -> List Bool

15natToBin Z = Nil

16natToBin k with (parity k)

17 natToBin (j + j) | even {n = j} = False :: natToBin j

18 natToBin (S (j + j)) | odd {n = j} = True :: natToBin j

20main : IO ()

21main = do print (natToBin 42)

23---------- Proofs ----------

25Main.parity_lemma_2 = proof {

26 intro;

27 intro;

28 rewrite sym (plusSuccRightSucc j j);

29 trivial;

32Main.parity_lemma_1 = proof {

33 intro j;

34 intro;

35 rewrite sym (plusSuccRightSucc j j);

36 trivial;