Add permutations

[wjbs]

Introduces machinery for manipulating permutations to VyZX. In particular:

• Defines ZXperm n, a predicate defining the subset of ZX n n which are
  permutation-like, i.e. stacks and compositions of Empty, Wire, and Swap.
• Defines perm_of_zx, which gives the underlying permutation of a ZXperm, and
  shows that this determines the semantics of the diagram, so that showing the
  equivalence of ZXperms reduces to showing the equality of their underlying
  permutations. This task in invariably far simpler (in particular, tractable),
  and we also provide significant automation for completing this task.
  Moreover, we show Z and X spiders absorb ZXperms.
• Defines zx_of_perm, which realizes an arbitrary permutation as a ZX diagram.
  We prove this is suitably inverse to perm_of_zx.
• Defines zx_comm n m : ZX (n + m) (m + n) and proves its naturality, i.e.
  (zx0 ↕ zx1) ⟷ zx_comm m q ∝ zx_comm n p ⟷ (zx1 ↕ zx0)
  (see zx_comm_commutes_r in ZXpermFacts.v). This gives pulling arbitrary
  diagrams through Swap. Similarly generalize a_swap to show arbitrary
  diagrams can be pulled through it.

This development is housed in the new Permutations subdirectory of src, and
comprises the following files. Dependency is indicated by the parentheticals
following each file, e.g. (1, 2) indicates dependence on (1) and (2) (only
immediate dependence is indicated).

Background files:
(1) PermutationAuxiliary: A collection of helpful lemmas across various domains,
including bool, Prop, nat, and C. They are broadly broken down by focus.
Ideally, this file should be split up and its lemmas distributed to their
various appropriate destinations.
(2) MatEquivSetoid: Declares a Relation (Setoid) instance for mat_equiv and
Proper instances for many matrix operations (Mmult, transpose, etc.). Also
defines an alternate to direct_sum, direct_sum', that is Proper with
respect to mat_equiv (the original direct_sum is not, as it implicitly assumes
its input matrices are WF)

Permutation Files
(3) PermutationDefinitions: Definitions of permutations and operations on them.
swap_perm swaps any two elements, perm_inv' is a WF_perm version of
perm_inv, and rotr / rotl "rotate" left / right. The main operators
are stack_perms : permutation n -> permutation m -> permutation (n + m)
and tensor_perms : permutation n -> permutation m -> permutation (n * m).
(4) ZXperm (3): Defines ZXperm, perm_of_zx, and (essentially) zx_of_perm.
Also defines some (now mostly obsolete) permutations specific to VyZX.
(5) PermutationAutomation (3,4): A large amount of automation for various tasks
across the project. This includes, amongst others:
General:
- replace_bool_lia a b: useful for simplifying bools in the goal. Roughly
equivalent to replace a with b by (bdestruct a; bdestruct b; lia).
- bdestructΩ': bdestruct all boolean expressions in the goal and
dispatch as many remaining goals as possible with easy and lia.
bdestructΩ'simp does this and performs intermediate simplification.
- solve_simple_mod_eqns: attempts to extend lia to more intelligently
handle expressions with mod.
- show_nonzero: proves a nat is nonzero using lia and
- show_pow2_le: preprocesses to simplify powers and applies nia
- show_moddy_lt: a powerful tactic to show a < b, where a includes
mod and/or /. For instance, given k < 2 ^ (m + n + o), it can show
k mod (2^m) * 2^(n+o) + (k/(2^(m+n))) * 2^n + ((k/(2^m)) mod 2^n) is
less than the same upper bound. It works by computing a simple upper bound
on a (e.g. a mod c <= c - 1 for c <> 0) which it shows is >= a and <b.
- simplify_bools_[moddy_]lia_one_kernel: finds each atomic (not containing
andb, orb, or an if) boolean expression and attempts to replace it
with each of true and false by bdestructΩ' and, if moddy_ is
added, show_moddy_lt.
- simplify_bools_lia: repeats the previous tactic. In practice,
undesirably expensive; do n [previous tactic] is preferred, manually
determining the value of n to use.
Permutations:
- solve_modular_permutation_equalities: uses solve_simple_mod_eqns,
bdestructΩ', and functional to show two nat -> nats are equal.
- cleanup_perm_inv: rewrites with perm_inv_db and calls auto with all
perm databases below.
- cleanup_perm: rewrites with the previous and perm_cleanup_db, calls
auto as the previous. simplifications for permutations
- eq_by_WF_perm_eq n: shows f = g from perm_eq n f g, WF_Perm n f,
and WF_Perm n g, applying automation to the latter two
- perm_eq_by_inv_inj f n: shows perm_eq n g h from f being inverse
to each of g and h, applying automation to all goals.
- permutation_eq_by_WF_inv_inj f n: like the previous, but for equality
- perm_by_inverse finv: shows permutation n f by giving an explicit
inverse, applying automation to all goals.
VyZX / ZXperm:
- simpl_permlike_zx: performs a number of reductions akin to those of
cleanup_zx, though often more quickly.
- clean_eqns tac: performs tac and solves any shelved goals with lia.
Useful for using VyZX cast lemmas that may leave impossible side goals.
- cleanup_perm_of_zx: rewrites & calls auto, with all below databases.
The following are the defined databases. All new defined lemmas should be
put in the appropriate database to appropriately extend the automation.
- perm_db: results permutation n f
- perm_bounded_db: results perm_bounded n f
- perm_inv_db: results perm_eq n (perm_inv n f) _, perm_inv' n f = _,
and (for now) any random results about perm_eq
- perm_cleanup_db: general results to simplify instances of permutations
- zxperm_db: results ZXperm n zx
- perm_of_zx_cleanup_db: any results about perm_of_zx, zx_of_perm
(6) PermutationFacts (1,5) and
(7) PermutationInstances (6): Theoretically, (6) contains facts about
general and specific permutations, while (7) contains proofs that
instances are permutations, perm_bounded, WF_Perm, etc. In practice,
there is significant intrusion of (7) into (6), as, for instance, many
facts about permutations rely on them being permutations.
Each permutation instance should have lemmas showing it is a permutation,
showing it is a WF_Perm (if it is, which it almost always should be), and
defining its perm_inv (if possible, which again it often should be), each
of which should be added to the appropriate database. We have done this for
each permutation and operator that we define.
(8) PermMatrixFacts (2,7): Results about perm_mat and perm_to_matrix, as
well as some helper lemmas to prove them. We show that the transpose of
perm_mat n f is perm_mat n (perm_inv n f) of the inverse and is an
inverse (both left and right) of perm_mat n f. We also show that
perm_mat, perm_to_matrix are injective, so perm_mat n f = perm_mat n g
implies perm_eq n f g.
(9) KronComm (8): the theory of kron_comm p q : Matrix (p*q) (q*p), which
commutes the tensor product. That is the main result, though we also show
it is perm_mat (p*q) (kron_comm_perm p q) along with various results
about it.
(10) PermutationSemantics (9): Specific values of perm_to_matrix, specifically
those relevant for VyZX, such as rotr.
(11) ZXpermSemantics (10): Proof that the semantics of a ZXperm is determined
by its underlying permutation, perm_of_zx (up to strict equality, and
hence up to proportionality). Gives rise to the tactic by_perm_eq, which
shows zx0 ∝ zx1 from ZXperm n zx0, ZXperm n zx1, and
perm_eq n (perm_of_zx zx0) (perm_of_zx zx1), applying automation to all
these goals.
(12) ZXpermFacts (11): Results about perm_of_zx and zx_of_perm, including
that they are mutually inverse. Also contains instances of ZXperm for
VyZX functions (transpose, adjoint, etc.) and some specific ZX diagrams
(e.g. a_swap). Contains rules about zx_of_perm relating ZX and
permutation operations (e.g. Stack and stack_perms). Finally, contains
definitions of zx_comm p q : ZX (p + q) (q + p) and
zx_gap_comm p m q : ZX (p + m + q) (q + m + p) along with proofs that
each commute stacking appropriately, that Swap and a_swap n are
special cases zx_comm 1 1 and zx_gap_comm 1 (n-2) 1 (if n >= 2),
and therefore that Swap and a_perm commute stacking. Also includes
results showing that X and Z spiders absorb ZXperms, as well as
zx_comm and zx_gap_comm.
(13) PermutationRules (12 / all): Exports relevant files. Designed to be
imported when permutations are to be used.

Some of this work belongs in QuantumLib. How much is up for debate, but for
the moment, I believe it is better to at least have this be usable in VyZX and
move things into QuantumLib from there. As the material is mostly broken down
by section, it should be possible to assess how much material is needed to,
for example, move KronComm into QuantumLib. Much of the theory of
permutations could be further migrated into QuantumLib, though that would
require including a significant amount of the automation as it is used
extensively throughout.