proving a binary add function

Question

I'm fairly new to the Coq language and I want to prove a function that does an binary add from numbers represented as a list (least significant bit upfront).

I have created this badd function that does that and now I want to prove it:

Fixpoint badd (l1 l2: list bool): list bool := 
  match l1 with
  | [] => l2
  | true :: l1 =>  bsucc (badd l1 (badd l1 l2))
  | false :: l1 => badd l1 (badd l1 l2)
end.

Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2.

Here are bsucc and value:

Fixpoint bsucc (l: list bool):  list bool :=
  match l with
  | []  =>[true]
  | true::r => false:: (bsucc r)
  | false::r => true::r
end.

Fixpoint value (l: list bool) :=
  match l with
  | [] => 0
  | true :: r => 1 + 2 * value r
  | false :: r => 2 * value r
end.

Thank you in advance for your help!

Answer 1

You can prove your goal by induction on l1, with the same tools as your previous proof of correctness of bsucc.

Lemma bsucc_ok l : value (bsucc l) = S (value l).

Note that in the case of an odd number (first digit is true), you may use this lemma with rewrite bsucc_ok.