Fix Qsimpl hanging on goals with adjoint _

[wjbs]

A recent change (1.4.0?) phased out *_sa (id_sa, hadamard_sa, etc.) in favor of *_hermitian. However, trying to rewrite with a lemma whose statement is hermitian _ hangs. As a result, Qsimpl (which is autorewrite with Q_db) would hang in situations where one of these lemmas could be rewritten. Any goal with (σx) † should demonstrate this issue. This is a hotfix that removes the *_hermitian lemmas from Q_db and adds corresponding lemmas *_hermitian_rw back to Q_db.

I believe this to be the cause of VOQC not compiling on QuantumLib 1.4.0+, as I have found an instance in VOQC where Qsimpl hangs. I will test this and update with the results. (There is also a place in SQIR with a trivial missing Import issue brought on by recent updates, which I believe is unrelated.)

As rewriting with the *_hermitian lemmas fails, it is a question whether we want to stick with them or return to the *_sa-style variants, which unfold the definition of hermitian to explicitly state adjoint A = A. There are other, more complicated automation solutions that could be pursued to keep around hermitian. For instance, I could create hermitian_db to show a matrix is hermitian, including the *_hermitian variants as well as any other lemmas we want to include (like kron_hermitian), then write custom Ltac to try to replace any adjoint A in the goal with A using hermitian_db. That's a larger conversation, though - this hotfix should address the basic issue.

[adrianleh]

LGTM

[adrianleh]

Sorry, updating review. Please update the version numbers in the opam and dune files