@@ -0,0 +1,95 @@
1+module main
2+
3+data Bit : Nat -> Set where
4+ b0 : Bit 0
5+ b1 : Bit 1
6+
7+instance Show (Bit n) where
8+ show b0 = "0"
9+ show b1 = "1"
10+
11+infixl 5 #
12+
13+data Binary : (width : Nat) -> (value : Nat) -> Set where
14+ zero : Binary O O
15+ (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)
16+
17+instance Show (Binary w k) where
18+ show zero = ""
19+ show (bin # bit) = show bin ++ show bit
20+
21+pattern syntax bitpair [x] [y] = (_ ** (_ ** (x, y, _)))
22+term syntax bitpair [x] [y] = (_ ** (_ ** (x, y, refl)))
23+
24+addBit : Bit x -> Bit y -> Bit c ->
25+ (bx ** (by ** (Bit bx, Bit by, c + x + y = by + 2 * bx)))
26+addBit b0 b0 b0 = bitpair b0 b0
27+addBit b0 b0 b1 = bitpair b0 b1
28+addBit b0 b1 b0 = bitpair b0 b1
29+addBit b0 b1 b1 = bitpair b1 b0
30+addBit b1 b0 b0 = bitpair b0 b1
31+addBit b1 b0 b1 = bitpair b1 b0
32+addBit b1 b1 b0 = bitpair b1 b0
33+addBit b1 b1 b1 = bitpair b1 b1
34+
35+adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (c + x + y)
36+adc zero zero carry ?= zero # carry
37+adc (numx # bx) (numy # by) carry
38+ ?= let (bitpair carry0 lsb) = addBit bx by carry in
39+ adc numx numy carry0 # lsb
40+
41+main : IO ()
42+main = do let n1 = zero # b1 # b0 # b1 # b0
43+ let n2 = zero # b1 # b1 # b1 # b0
44+ print (adc n1 n2 b0)
45+
46+
47+
48+
49+
50+
51+
52+
53+
54+---------- Proofs ----------
55+
56+-- There is almost certainly an easier proof. I don't care, for now :)
57+
58+main.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) O));
87+ trivial;
88+}
89+
90+main.adc_lemma_1 = proof {
91+ intros;
92+ rewrite sym (plusZeroRightNeutral c) ;
93+ trivial;
94+}
95+