# ZX-calculus: pi-copy rule not required for completeness?

In ZX-calculus, the $$\pi$$-copy rule is quite famous, and is used for instance here:

However, this paper never introduces this rule, and says that this set is enough to prove the Clifford completeness of the ZX calculus:

Is it just that they forgot it, or is this rule derivable from others?

• In figure 1 of this paper, they give the $\pi$-copy rule in the set of the rules of ZX. I don't think they derive it from any other rule in here. Sep 3 at 12:52
• @epelaaez Yes, like many papers. Does that mean that the paper I mention just forgot it, or am I missing something else? Sep 3 at 13:13

It's indeed not, and so are other rules frequently used, like what we called Hopf law. These things were derived in the 2011 ZX-paper with Ross Duncan. Think of them as shortcuts. Many more of those have been derived by others and are frequently used. In our dodo book we have an entirely different rule taking care of red-green-phase interaction. This is really what a lot of maths is about: deriving results that simplify reasoning.

• Welcome to QCSE, Bob! It's very cool to see you join! I took the liberty to add links to your answer, but note that you should be able to roll back or edit further if you disagree with my change. Sep 7 at 18:43
• Cheers Adam! Didn't even know this existed, that's called being old. Sep 7 at 19:15
• Thank you very much for your answer, and welcome! So I've been reading your paper, but I can't find where is the proof; The closest I can find are proofs page 67 but they all seem to implicitely use rules that are not in the above list. For instance, bialge => comul seems to use the "comonoid homomorphism laws" (which seems to be basically a $\pi$-copy rule, see e.g. 2.6), but this rule is not in the list I provided. Also, you do introduce K1 in the list of rules in figure 1, while the Hopf rule is not present and derived later. Am I missing something obvious to derive K1? Sep 8 at 17:19
• Also, concerning the dodo book, I recently bought it, and it is definitely a great book, I love it, thanks for it! But I'm trying to read it linearly (no spoil:-P), and I'm not yet that far, I'm still seing classical maps. But I tried to jump a bit ahead, and the rule that you introduced is interesting, But I still need to find how to obtain it given the above rules, and how this rule can be used to derive other equations (as far as I can see this is not explained in the book). But it's quite surprising to see that such few rules are needed! Sep 8 at 17:38
• Btw @LéoColisson are you aware of the ZX-calc Discord where questions likes these are frequently discussed? Join here: zxcalculus.com Sep 9 at 9:24

After asking on the Discord (thanks for pointing me to that Bob!), I got several proofs.

# First proof (thanks Miriam Backens)

Lemma A.13, A.14 and A.15 of this paper, which contains also many interesting proofs. This method also works in the real stabiliser fragment, where Lemma A.13 is taken as a an axiom instead of the EU rule.

# Second proof (thanks John van de Wetering)

First, we derive the Y-state-identity, for instance given here in appendix A (I rewrote the proof with scalars):

It is now trivial to derive the equivalence between the two forms of the Hadamard (it is also possible to show that the last form is true when inverting all angles by using the fact that $$HH=I$$):

Then, John was proposing this reduction (sorry, I've no time to write it down properly, so I shamefully copy/pasted his picture), where the Y-state identity is used in the last equation of the first line, and where the Hadamard identity is used right after, then it is the Hopf rule and the last equality can be proven using the K-rule + bialgebra + hopf (one may need also a proper analysis of scalars...):