Library CoLoR.Util.Vector.VecBool

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-06-08
useful definitions and lemmas on boolean vectors

Set Implicit Arguments.


Notation bools := (vector bool).

Fixpoint Vtrue n (bs : bools n) : nat :=
  match bs with
    | Vnil => 0
    | Vcons true bs' => S (Vtrue bs')
    | Vcons false bs' => Vtrue bs'
  end.

Lemma Vtrue_app : forall n1 (bs1 : bools n1) n2 (bs2 : bools n2),
  Vtrue (Vapp bs1 bs2) = Vtrue bs1 + Vtrue bs2.

Lemma Vtrue_break : forall n1 n2 (bs : bools (n1+n2)),
  Vtrue (fst (Vbreak bs)) + Vtrue (snd (Vbreak bs)) = Vtrue bs.


Lemma Vtrue_cast : forall n (bs : bools n) p (h:n=p),
  Vtrue (Vcast bs h) = Vtrue bs.

Definition Vtrue_cons_if (b : bool) n (bs : bools (S n)) :=
  if b then S (Vtrue (Vtail bs)) else Vtrue (Vtail bs).

Definition Vtrue_cons n (bs : bools (S n)) := Vtrue_cons_if (Vhead bs) bs.

Lemma Vtrue_cons_eq : forall n (bs : bools (S n)), Vtrue_cons bs = Vtrue bs.

Lemma Vtrue_cons_true : forall b n (bs : bools n),
  b = true -> S (Vtrue bs) = Vtrue (Vcons b bs).

Lemma Vtrue_cons_false : forall b n (bs : bools n),
  b = false -> Vtrue bs = Vtrue (Vcons b bs).

Lemma Vtrue_Sn_true : forall n (bs : bools (S n)),
  Vhead bs = true -> S (Vtrue (Vtail bs)) = Vtrue bs.

Lemma Vtrue_Sn_false : forall n (bs : bools (S n)),
  Vhead bs = false -> Vtrue (Vtail bs) = Vtrue bs.

Lemma Vtrue_Sn : forall n (bs : bools (S n)),
  Vtrue (Vcons (Vhead bs) (Vtail bs)) = Vtrue bs.