How to do an inductive proof

Question

I have to show that :

Lemma bsuccOK: forall l, value (bsucc l) = S (value l).

with an induction proof, but I don't understand how to do it.

Here is the bsucc function:

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

Lemma bsucc_test1: bsucc [false;true;false;true] = [true;true;false;true].

Proof.
easy.
Admitted.

It gives the successor of a list of booleans representing a binary number.

Any help would be very appreciated!

Answer 1

Which binary representation do you use ? If you consider Least significant bits first, then for instance 4 is represented as [false;false;true].

Here is a definition of bsuccand value. Note the order of arguments in list notations, and a slight change in bsucc []. Hope it's OK.

Require Import List Lia.
Import ListNotations. 

(** Least significant bit first  *)

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

Fixpoint value (s:list bool):  nat:=
  match s with
  | []   => 0
  | true::r => S (2 * value r)
  | false::r => 2 * value r
  end.

Compute value [false;false;true]. (* 4 *)

Then, your goal is solvable, by induction on l. Tactics you may also use are cbnor simpl, case, rewrite, and lia(for linear arithmetic).

Answer 2

Thanks to you, here the answer I finally found:

Lemma bsuccOK: forall l, value (bsucc l) = S (value l).
Proof.
induction l; auto.
destruct a.
-simpl.
rewrite IHl.
lia.
-simpl.
lia.
Qed.