git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/tutorial002/tutorial002.idr
61 lines 1.3 kB history raw
1module Main
3data Binary : Nat -> Type where
4 BEnd : Binary Z
5 BO : Binary n -> Binary (n + n)
6 BI : Binary n -> Binary (S (n + n))
8implementation Show (Binary n) where
9 show (BO x) = show x ++ "0"
10 show (BI x) = show x ++ "1"
11 show BEnd = ""
13data Parity : Nat -> Type where
14 Even : Parity (n + n)
15 Odd : Parity (S (n + n))
17parity : (n:Nat) -> Parity n
18parity Z = Even {n=Z}
19parity (S Z) = Odd {n=Z}
20parity (S (S k)) with (parity k)
21 parity (S (S (j + j))) | Even ?= Even {n=S j}
22 parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}
24natToBin : (n:Nat) -> Binary n
25natToBin Z = BEnd
26natToBin (S k) with (parity k)
27 natToBin (S (j + j)) | Even = BI (natToBin j)
28 natToBin (S (S (j + j))) | Odd ?= BO (natToBin (S j))
30intToNat : Int -> Nat
31intToNat 0 = Z
32intToNat x = if (x>0) then (S (intToNat (x-1))) else Z
34main : IO ()
35main = do putStr "Enter a number: "
36 x <- getLine
37 printLn (natToBin (fromInteger (cast x)))
39---------- Proofs ----------
41Main.natToBin_lemma_1 = proof
42 intros
43 rewrite plusSuccRightSucc j j
44 rewrite sym (plusSuccRightSucc j j)
45 trivial
48parity_lemma_1 = proof
49 intros
50 rewrite sym (plusSuccRightSucc j j)
51 trivial
54parity_lemma_2 = proof {
55 intro;
56 intro;
57 rewrite sym (plusSuccRightSucc j j);
58 trivial;