[coq] start bool matrix stuff
This commit is contained in:
parent
2453a7a5fc
commit
c3c94f3e35
|
@ -0,0 +1,29 @@
|
||||||
|
Require Import Vector.
|
||||||
|
Require Import Bvector.
|
||||||
|
(* Import VectorNotations. *)
|
||||||
|
|
||||||
|
Definition matrix (rows cols: nat): Type :=
|
||||||
|
Vector.t (Bvector cols) rows.
|
||||||
|
|
||||||
|
Axiom zip: forall {A B: Type} {n:nat},
|
||||||
|
Vector.t A n -> Vector.t B n -> Vector.t (A*B) n.
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
|
||||||
|
Definition vecMatrixProd {rows cols: nat}
|
||||||
|
(vec: Bvector rows) (mat: matrix cols rows): Bvector cols :=
|
||||||
|
Vector.map (fun mrow => dotProduct vec mrow) mat.
|
||||||
|
|
||||||
|
End Matrix.
|
Loading…
Reference in New Issue