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!
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 bsucc
and 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 cbn
or simpl
, case
, rewrite
, and lia
(for linear arithmetic).