proposition: Lemma existandb_dotprod : forall n (v w : vec n), dot_product v w = true <-> exists z, exists hz : z<n, Is_true (andb (Vnth v hz) (Vnth w hz)).
proof: Proof. induction n; intros; unfold dot_product in *; unfold Vfold_left. simpl; unfold A0; split; intro. discr. destruct H; destruct H; auto with *. assert (v = Vcons (Vhead v) (Vtail v)) as Hv. apply VSn_eq. assert (w = Vcons (Vhead w) (Vtail w)) as Hw. apply VSn_eq. simpl; unfold Aplus; split; intros. apply orb_prop in H. destruct H. unfold dot_product in IHn. rewrite IHn in H; repeat destruct H. exists (S x); exists (NatCompat.lt_n_S x0); clear IHn. rewrite Hv, Hw. simpl. assert (NatCompat.lt_S_n (NatCompat.lt_n_S x0) = x0). apply lt_unique. rewrite H0. hyp. exists 0; exists (Nat.lt_0_succ n); rewrite Hv, Hw; auto. unfold Amult in *; auto with *. repeat destruct H; unfold Amult; apply Is_true_eq_true; apply orb_prop_intro. destruct x. right. rewrite <- (Vnth_cons_head (Vhead v) (Vtail v) x0); auto. rewrite <-Hv, <- (Vnth_cons_head (Vhead w) (Vtail w) x0); auto. rewrite <-Hw. auto. left. rewrite Hv, Hw in H. simpl in H. apply Is_true_eq_left. rewrite IHn. exists x. exists (NatCompat.lt_S_n x0). hyp. Qed.
imports: Coq(Bool) CoLoR(Matrix Path Iter SCC ListExtras OrdSemiRing VecUtil RelSub RelUtil NatUtil Log2 LogicUtil BoundNat)