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.