49 lines
1.4 KiB
Coq
49 lines
1.4 KiB
Coq
Require Import Vector.
|
|
Require Import Bvector.
|
|
(* Import VectorNotations. *)
|
|
|
|
Definition matrix (rows cols: nat): Type :=
|
|
Vector.t (Bvector cols) rows.
|
|
|
|
(* Uses /convoy pattern/.
|
|
|
|
See: https://stackoverflow.com/questions/59290356/dependent-pattern-matching-zip-two-vectors
|
|
*)
|
|
Fixpoint zip {A B: Type} {n:nat}
|
|
(av: Vector.t A n) (bv: Vector.t B n): Vector.t (A*B) n :=
|
|
match av in Vector.t _ n
|
|
return Vector.t B n -> Vector.t (A*B) n with
|
|
| [] => fun _ => []
|
|
| a::av' => fun bv => (a, Vector.hd bv) :: zip av' (Vector.tl bv)
|
|
end bv.
|
|
|
|
Section Matrix.
|
|
Context {A: Type}.
|
|
|
|
Definition dotProduct {n:nat}
|
|
(v1 v2: Vector.t bool n): bool :=
|
|
let v12 := zip v1 v2 in
|
|
let ires := Vector.map (fun '(a, b) => andb a b) v12 in
|
|
fold_right (fun elem res => xorb elem res) ires false.
|
|
|
|
Definition vecMatrixProd {rows cols: nat}
|
|
(vec: Bvector rows) (mat: matrix cols rows): Bvector cols :=
|
|
Vector.map (fun mrow => dotProduct vec mrow) mat.
|
|
End Matrix.
|
|
|
|
Definition isAllZero {n:nat} (v: Vector.t bool n): bool :=
|
|
negb (Vector.fold_right (fun elem acc => orb elem acc) v false).
|
|
|
|
|
|
(* Make vector of size [sz] with its [i]-th bit set, where indexing
|
|
starts from 0. *)
|
|
Fixpoint seti (i sz:nat): Vector.t bool sz :=
|
|
match sz with
|
|
| O => []
|
|
| S sz' =>
|
|
match i with
|
|
| O => true :: (repeat false sz')
|
|
| S i' => false :: (seti i' sz')
|
|
end
|
|
end.
|