  A quantum circuit is a computational unit that transforms an input quantum
state to an output one. A natural way to reason about its behavior is to
compute explicitly the unitary matrix implemented by it. However, when the
number of qubits increases, the matrix dimension grows exponentially and the
computation becomes intractable.
  In this paper, we propose a symbolic approach to reasoning about quantum
circuits. It is based on a small set of laws involving some basic manipulations
on vectors and matrices. This symbolic reasoning scales better than the
explicit one and is well suited to be automated in Coq, as demonstrated with
some typical examples.
