| Useful tactics related to bitvectors |
Require Import Bool Bvector.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.Vector.
Version of Asm.Util.Vector.myVOtac for Bvector
|
Ltac myVOtac := unfold Bvector in *; VOtac.
Version of Asm.Util.Vector.myVSntac for Bvector
|
Ltac myVSntac H x := unfold Bvector in *; VSntac H x.
Induction skeleton for proving goals of the form forall (len : nat) (v : Bvector len), _
|
Ltac vec_ind :=
let H := fresh in let Htail := fresh in
(intro len; induction len as [ | len IHlen ]; intro v;
[myVOtac; try (simpl; intuition; fail)
| myVSntac H v; destruct (Vhead v); simpl; myrewrite;
generalize (IHlen (Vtail v)); try (intuition; fail); try omega; intro Htail]).