Load "nat.tt";

Match power : Nat -> Nat -> Nat =
    power n O = (S O)
  | power n (S k) = mult n (power n k);

Data Bit : Nat -> * = On : Bit (S O) | Off : Bit O;

Data BitPair : Nat -> * 
  = bitpair : (cv:Nat)(carry:Bit cv)->(bv:Nat)(b:Bit bv)->
              (BitPair (plus bv (mult (S (S O)) cv)));

Data Number : (len:Nat)(val:Nat)*
  = none : Number O O
  | bit : (bv:Nat)(b:Bit bv)->
          (len:Nat)(val:Nat)(num:Number len val)->
	  (Number (S len) (plus (mult (power (S (S O)) len) bv) val));

Data NumCarry : (len:Nat)(val:Nat)*
  = numcarry : (cv:Nat)(carry:Bit cv)->(len:Nat)(val:Nat)(n:Number len val)->
               (NumCarry len (plus (mult (power (S (S O)) len) cv) val));

Match addBit : (cv:Nat)(carry:Bit cv)->
              (lv:Nat)(l:Bit lv)->
              (rv:Nat)(r:Bit rv)->
	      (BitPair (plus cv (plus lv rv))) =
  addBit _ Off _ Off _ Off = bitpair _ Off _ Off
| addBit _ Off _ On _ Off = bitpair _ Off _ On
| addBit _ On _ Off _ Off = bitpair _ Off _ On
| addBit _ On _ On _ Off = bitpair _ On _ Off
| addBit _ Off _ Off _ On = bitpair _ Off _ On
| addBit _ Off _ On _ On = bitpair _ On _ Off
| addBit _ On _ Off _ On = bitpair _ On _ Off
| addBit _ On _ On _ On = bitpair _ On _ On;

addBitLemma: (len,mv,cv,lv:Nat)Eq _ 
   (plus (mult (power (S (S O)) len) (plus mv (mult (S (S O)) cv))) lv) 
   (plus (mult (power (S (S O)) (S len)) cv) (plus (mult (power (S (S O)) len) mv) lv));
intros;
unfold power;
generalise power (S (S O)) len;
intros;
generalise (S (S O));
intro two;
replace mult_comm x mv;
replace plus_comm mv (mult two cv);
replace mult_comm two x;
replace sym mult_assoc x two cv;
replace mult_comm x (mult two cv);
replace plus_assoc (mult (mult two cv) x) (mult mv x) lv;
replace mult_distrib (mult two cv) mv x;
replace mult_comm x (plus (mult two cv) mv);
refine refl;
Qed;

reindex : (A:*)(T:A->*)(a,b:A)(P:(Eq _ a b))(T a)->(T b);
intros;
replace sym P;
fill X0;
Qed;

addNumBit : (len:Nat)(bv:Nat)(bits:BitPair bv)->
			  (nv:Nat)(n:Number len nv)->
			  (NumCarry (S len) 
			     (plus (mult (power (S (S O)) len) bv) nv));
intros;
case bits;
intro cv carry mv msb;
replace addBitLemma len mv cv nv;
fill (numcarry cv carry (S len) _ (bit mv msb len nv n));
Qed;

doAddNumBit :(len:Nat)(cv:Nat)(carry:Bit cv)(blv,brv:Nat)
      (bl:Bit blv)(br:Bit brv)(numlval,numrval:Nat)
      (numl:Number len numlval)(numr:Number len numrval)
(NumCarry len (plus (plus numlval numrval) cv))->
(NumCarry (S len) (plus (plus (plus (mult (power (S (S O)) len) blv) numlval) (plus (mult (power (S (S O)) len) brv) numrval)) cv));

intro len cv carry blv brv bl br numlval numrval;
replace plus_assoc (plus (mult (power (S (S O)) len) blv) numlval) (mult (power (S (S O)) len) brv) numrval;
replace plus_comm (plus (mult (power (S (S O)) len) blv) numlval) (mult (power (S (S O)) len) brv); 
replace plus_assoc (mult (power (S (S O)) len) brv) (mult (power (S (S O)) len) blv) numlval;
replace sym plus_assoc (plus (plus (mult (power (S (S O)) len) brv) (mult (power (S (S O)) len) blv)) numlval) numrval cv;
replace sym plus_assoc (plus (mult (power (S (S O)) len) brv) (mult (power (S (S O)) len) blv)) numlval (plus numrval cv);
replace plus_assoc numlval numrval cv;
intro numl numr;
generalise (plus (plus numlval numrval) cv);
intro recval X;
case X;
intros;
local bp : BitPair (plus cv0 (plus blv brv));
fill addBit _ carry0 _ bl _ br;
replace mult_comm (power (S (S O)) len1) brv;
replace mult_comm (power (S (S O)) len1) blv;
replace mult_distrib brv blv (power (S (S O)) len1);
replace mult_comm (power (S (S O)) len1) cv0;
replace plus_assoc (mult (plus brv blv) (power (S (S O)) len1)) (mult cv0 (power (S (S O)) len1)) val0;
replace mult_distrib (plus brv blv) cv0 (power (S (S O)) len1);
replace plus_comm (plus brv blv) cv0;
refine addNumBit;
replace mult_comm (plus cv0 (plus brv blv)) (power (S (S O)) len1);
refine addNumBit;
replace plus_comm brv blv;
fill bp;
fill n;
Qed;

multid: (n:Nat)(Eq _ n (mult (S O) n));
intros;
equiv (Eq _ n (plus n O));
replace plusnO n;
refine refl;
Qed;

noneCase : (cv:Nat)(carry:Bit cv)
   (NumCarry O cv);
intros;
replace multid cv;
fill numcarry _ carry O _ none;
replace sym plusnO (mult (S O) cv);
fill numcarry _ carry _ _ none;
Qed;

Match addNumber : (len:Nat)(cv:Nat)(carry:Bit cv)->
                          (lv:Nat)(l:Number len lv)->
                          (rv:Nat)(r:Number len rv)->
			  (NumCarry len (plus (plus lv rv) cv)) =
   addNumber _ cv carry _ none _ none = noneCase _ carry
 | addNumber (S len) cv carry _ (bit blv bl len _ numl)
                              _ (bit brv br len _ numr) = 
     doAddNumBit len _ carry _ _ bl br _ _ numl numr (addNumber len _ carry _ numl _ numr);


test0 : Number (S (S (S O))) O;
fill bit _ Off _ _ (bit _ Off _ _ (bit _ Off _ _ none));
Qed;

test1 : Number (S (S (S O))) (S O);
fill bit _ Off _ _ (bit _ Off _ _ (bit _ On _ _ none));
Qed;

test2 : Number (S (S (S O))) (S (S O));
fill bit _ Off _ _ (bit _ On _ _ (bit _ Off _ _ none));
Qed;

test3 : Number (S (S (S O))) (S (S (S O)));
fill bit _ Off _ _ (bit _ On _ _ (bit _ On _ _ none));
Qed;

test4 : Number (S (S (S O))) (S (S (S (S O))));
fill bit _ On _ _ (bit _ Off _ _ (bit _ Off _ _ none));
Qed;

test5 : Number (S (S (S O))) (S (S (S (S (S O)))));
fill bit _ On _ _ (bit _ Off _ _ (bit _ On _ _ none));
Qed;

test6 : Number (S (S (S O))) (S (S (S (S (S (S O))))));
fill bit _ On _ _ (bit _ On _ _ (bit _ Off _ _ none));
Qed;

test7 : Number (S (S (S O))) (S (S (S (S (S (S (S O)))))));
fill bit _ On _ _ (bit _ On _ _ (bit _ On _ _ none));
Qed;

Eval addNumber _ _ Off _ test3 _ test7;
Eval addNumber _ _ On _ test3 _ test3;

Check addNumber _ _ On _ test3 _ test2;