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 l2 with |  => l1 | true :: l2 => bsucc (badd (badd l1 l2) l2) | false :: l2 => badd (badd l1 l2) l2 end.
Here is my proof so far (value give the decimal value of the binary number) :
Lemma baddOK: forall l1 l2, value (badd l1 l2) = value l1 + value l2. Proof. intros l1 l2. generalize dependent l1. induction l2; auto. rewrite IHl2. (* this fail *) Admitted.
The problem I have now is that I have IHl2 that correspond to
IHl2: forall l1 : list bool, value (badd l1 l2) = value l1 + value l2
And my goal is :
forall l1 : list bool, value (badd l1 (a :: l2)) = value l1 + value (a :: l2)
The problem is that I can't rewrite using IHl2 as the generic part of it (i.e. l1) does not match with l3 (i.e. a::l2) but with l1 itself.
Here is the value function to be able to follow the proof:
Fixpoint value (l: list bool) := match l with |  => 0 | true :: l => 2 * (value l) + 1 | false :: l => 2 * (value l) end.