Generators and relations for 2-qubit Clifford+T operators

                                * * *

This is the Agda code accompanying the paper "Generators and relations
for 2-qubit Clifford+T operators". The code is described in more
detail in the paper.


Compatibility
-------------

This code was tested with Agda version 2.6.0.1.

For instructions on how to install and use Agda, see
https://agda.readthedocs.io/en/latest/


Files
-----

The code is organized as follows:

(a) Background:

  The files in this section contain general background material,
  similar to what is in the standard library, but self-contained.

  Boolean.agda:
   The type of booleans.

  Proposition.agda:
   Basic definitions in propositional logic.

  Equality.agda:
   Basic properties of equality.

  Decidable.agda:
   Some definitions to deal with decidable properties.

  Inspect.agda:
   Agda's "inspect" paradigm, to assist with pattern matching.

  Nat.agda:
   Basic properties of the natural numbers.

  Maybe.agda:
   The "Maybe" type.

  List.agda:
   Basic properties of lists.

(b) Statement of the result

  The files in this section contain the statement of the main result,
  and the definitions that are required to state it.

  Word.agda:
   Basic properties of words.

  Generator.agda:
   Generators and relations for our two groups, and statement of main result.

(c) Proof of the result

  The files in this section contain the proof of the main result, as
  well as many auxiliary definitions and tactics that are used in the
  proof.

  Word-Lemmas.agda:
   Basic lemmas about monoids and groups, and equational reasoning.

  Reidemeister-Schreier.agda:
   Two versions of the Reidemeister-Schreier theorem.

  Word-Tactics.agda:
   Some tactics for proving properties of words.

  Clifford-Lemmas.agda:
   A decision procedure for equality of 2-qubit Clifford operators.

  Clifford+T-Lemmas.agda:
   Properties and tactics for Clifford+T operators.

  Greylyn-Lemmas.agda:
   Some automation for Greylyn's 1- and 2-level operators.

  Soundness.agda:
   Proof of soundness.

  Greylyn-Simplified.agda:
   A smaller set of generators and relations for Greylyn's operators.

  PauliRotations.agda:
   Definitions, properties, and tactics for Pauli rotations.

  Equation1.agda -- Equation46.agda:
   Explicit proofs of 46 relations required for completeness.

  Completeness.agda:
   Proof of completeness.

(d) Top-level proof witness

  The purpose of this file is to provide a single entry point for
  checking the proof of the main result without having to read any of
  the files in section (c).

  Proof.agda:
   The final witness for soundness and completeness.


Authors
-------

Xiaoning Bian <bian@dal.ca>

Peter Selinger <selinger@dal.ca>


Copyright and License
---------------------

(C) 2022 Xiaoning Bian and Peter Selinger.

This works is licensed under the Creative Commons CC BY 2.0 license.
See https://creativecommons.org/licenses/by/2.0/ for more details.