Set Implicit Arguments.

Require Import VecUtil.
Require Import LogicUtil.

Notation bools := (Vector.t bool).

Fixpoint Vtrue n (bs : bools n) {struct bs} : nat :=
  match bs with
    | Vector.nil ⇒ 0
    | Vector.cons true _ bs' ⇒ S (Vtrue bs')
    | Vector.cons false _ bs' ⇒ Vtrue bs'
  end.

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

Proof.
induction bs1; simpl. auto. intros. ded (IHbs1 n2 bs2). rewrite H.
case h; refl.
Qed.

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

Proof.
induction n1; simpl; intros. refl. VSntac bs. simpl. case (Vector.hd bs); simpl.
apply (f_equal S). apply IHn1. apply IHn1.
Qed.

Implicit Arguments Vtrue_break [n1 n2].

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

Proof.
induction bs; induction p; intros. castrefl h.
discriminate. discriminate. simpl. case h. apply (f_equal S). apply IHbs.
apply IHbs.
Qed.

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

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

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

Proof.
intros. VSntac bs. unfold Vtrue_cons, Vtrue_cons_if. simpl. refl.
Qed.

Lemma Vtrue_cons_true : ∀ b n (bs : bools n),
  b = true → S (Vtrue bs) = Vtrue (Vector.cons b bs).

Proof.
intros. subst b. refl.
Qed.

Lemma Vtrue_cons_false : ∀ b n (bs : bools n),
  b = false → Vtrue bs = Vtrue (Vector.cons b bs).

Proof.
intros. subst b. refl.
Qed.

Lemma Vtrue_Sn_true : ∀ n (bs : bools (S n)),
  Vector.hd bs = true → S (Vtrue (Vector.tl bs)) = Vtrue bs.

Proof.
intros. VSntac bs. apply Vtrue_cons_true. assumption.
Qed.

Lemma Vtrue_Sn_false : ∀ n (bs : bools (S n)),
  Vector.hd bs = false → Vtrue (Vector.tl bs) = Vtrue bs.

Proof.
intros. VSntac bs. apply Vtrue_cons_false. assumption.
Qed.

Lemma Vtrue_Sn : ∀ n (bs : bools (S n)),
  Vtrue (Vector.cons (Vector.hd bs) (Vector.tl bs)) = Vtrue bs.

Proof.
intros. rewrite <- VSn_eq. refl.
Qed.