Library Asm.Bitvector.Tactics

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]).

This page has been generated by coqdoc