
      Generators and relations for 3-qubit Clifford+CS operators

                                * * *

This is the Agda code accompanying the paper "Generators and relations
for 3-qubit Clifford+CS operators" by Xiaoning Bian and Peter
Selinger.


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

This code was tested with Agda versions 2.6.2.2 and 2.6.4-b5105f4.

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


Files
-----

The code is organized as follows:

(a) Lib folder

  The folder contains general background material, similar to what is
  in Agda's 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.

  MaybeEq.agda:
   A semi-decidable equality type class to overload the symbol _=m?_.

  MaybeEq-Instances.agda:
   Instances for MaybeEq.

  List.agda:
   Basic properties of lists.

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

  Word.agda:
   Basic properties of words.

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

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

(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.

  Index.agda:
   Data types for indices used in the naming of generators.

  Theorem.agda:
   Generators and relations for our two groups, and statement of the
   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.

  TwoLevel-Lemmas.agda:
   Some automation for the 1- and 2-level operators.

  CosetNF.agda:
   Definitions related to semidirect products and normal forms.

  Gate.agda:
   Definitions for the gates used in our various sets of generators
   for Clifford+CS operators.

  Files in the folders Step1 -- Step8:
   Each of these steps transforms a set of generators and relations
   into an equivalent set of generators and relations, gradually
   simplifying the relations. Lemmas and tactics specific to each
   translation are included as appropriate.

  Soundness.agda:
   Proof of soundness.

  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) 2023 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.
