git.iko.soy/Idris-dev
on 2aa64bd help sign in
Idris-dev/tutorial/examples/binary.idr
62 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))
8instance 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 print (natToBin (fromInteger (cast x)))
39---------- Proofs ----------
41parity_lemma_1 = proof {
42 intros;
43 rewrite sym (plusSuccRightSucc j j);
44 trivial;
47natToBin_lemma_1 = proof {
48 intro;
49 intro;
50 rewrite sym (plusSuccRightSucc j j);
51 trivial;
54parity_lemma_2 = proof {
55 intro;
56 intro;
57 rewrite sym (plusSuccRightSucc j j);
58 trivial;