git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/samples/binary.idr
95 lines 2.9 kB history raw
1module main
3data Bit : Nat -> Type where
4 b0 : Bit 0
5 b1 : Bit 1
7instance Show (Bit n) where
8 show b0 = "0"
9 show b1 = "1"
11infixl 5 #
13data Binary : (width : Nat) -> (value : Nat) -> Type where
14 zero : Binary Z Z
15 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
17instance Show (Binary w k) where
18 show zero = ""
19 show (bin # bit) = show bin ++ show bit
21pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
22term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
24addBit : Bit x -> Bit y -> Bit c ->
25 (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
26addBit b0 b0 b0 = bitpair b0 b0
27addBit b0 b0 b1 = bitpair b0 b1
28addBit b0 b1 b0 = bitpair b0 b1
29addBit b0 b1 b1 = bitpair b1 b0
30addBit b1 b0 b0 = bitpair b0 b1
31addBit b1 b0 b1 = bitpair b1 b0
32addBit b1 b1 b0 = bitpair b1 b0
33addBit b1 b1 b1 = bitpair b1 b1
35adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
36adc zero zero carry ?= zero # carry
37adc (numx # bx) (numy # by) carry
38 ?= let (bitpair carry0 lsb) = addBit bx by carry in
39 adc numx numy carry0 # lsb
41main : IO ()
42main = do let n1 = zero # b1 # b0 # b1 # b0
43 let n2 = zero # b1 # b1 # b1 # b0
44 print (adc n1 n2 b0)
54---------- Proofs ----------
56-- There is almost certainly an easier proof. I don't care, for now :)
58main.adc_lemma_2 = proof {
59 intro c,w,v,bit0,num0;
60 intro b0,v1,bit1,num1,b1;
61 intro bc,x,x1,bx,bx1,prf;
62 intro;
63 rewrite sym (plusZeroRightNeutral v);
64 rewrite sym (plusZeroRightNeutral v1);
65 rewrite sym (plusAssociative (plus c (plus bit0 (plus v v))) bit1 (plus v1 v1));
66 rewrite (plusAssociative c (plus bit0 (plus v v)) bit1);
67 rewrite (plusAssociative bit0 (plus v v) bit1);
68 rewrite sym (plusCommutative (plus v v) bit1);
69 rewrite sym (plusAssociative c bit0 (plus bit1 (plus v v)));
70 rewrite sym (plusAssociative (plus c bit0) bit1 (plus v v));
71 rewrite sym prf;
72 rewrite sym (plusZeroRightNeutral x);
73 rewrite plusAssociative x1 (plus x x) (plus v v);
74 rewrite plusAssociative x x (plus v v);
75 rewrite sym (plusAssociative x v v);
76 rewrite plusCommutative v (plus x v);
77 rewrite sym (plusAssociative x v (plus x v));
78 rewrite plusAssociative x1 (plus (plus x v) (plus x v)) (plus v1 v1);
79 rewrite plusAssociative (plus x v) (plus x v) (plus v1 v1);
80 rewrite plusAssociative x v (plus v1 v1);
81 rewrite sym (plusAssociative v v1 v1);
82 rewrite sym (plusAssociative x (plus v v1) v1);
83 rewrite sym (plusAssociative x v v1);
84 rewrite sym (plusCommutative (plus (plus x v) v1) v1);
85 rewrite plusZeroRightNeutral (plus (plus x v) v1);
86 rewrite sym (plusAssociative (plus x v) v1 (plus (plus (plus x v) v1) Z));
87 trivial;
90main.adc_lemma_1 = proof {
91 intros;
92 rewrite sym (plusZeroRightNeutral c) ;
93 trivial;