Test extraction of Reals -> Floats

[khieta]

We extract Coq's axiomatized Reals (used for continuous gate parameters) to OCaml floats. This invites the possibility of floating point rounding error, which is not accounted for in our proofs. The best(?) way to get around this would be to actually reason about float parameters in Coq -- but I'd rather avoid this if possible.

If we are going to leave the extraction as-is, then we should at least have solid evidence that it isn't doing significant harm. Here are a couple random ideas for testing:

• Optimize (small) random programs with optimize_1q_gates, compute the matrices corresponding to the input and output programs, and check the two for equivalence.
• Compare the results of VOQC's optimize_1q_gates and Qiskit's Optimize1qGates on random input programs.