QuantumLib.Pad

Require Export Complex.
Require Export Quantum.

This file provides padding functions to extend a matrix to a larger space. This is useful for describing the effect of 1- and 2-qubit gates on a larger quantum space.

Definition pad {n} (start dim : nat) (A : Square (2^n)) : Square (2^dim) :=
  if start + n <=? dim then I (2^start) ⊗ A ⊗ I (2^(dim - (start + n ))) else Zero.

Lemma WF_pad : ∀ n start dim (A : Square (2^n)),
  WF_Matrix A →
  WF_Matrix (pad start dim A).

Lemma pad_mult : ∀ n dim start (A B : Square (2^n)),
  pad start dim A × pad start dim B = pad start dim (A × B).

Lemma pad_id : ∀ n dim,
  (n < dim)%nat → @pad 1 n dim (I 2) = I (2 ^ dim).

Definition pad_u (dim n : nat) (u : Square 2) : Square (2^dim) := @pad 1 n dim u.

Definition pad_ctrl (dim m n: nat) (u: Square 2) :=
  if (m <? n) then
    @pad (1+(n -m -1)+1) m dim (∣1⟩⟨1∣ ⊗ I (2^(n -m -1)) ⊗ u .+ ∣0⟩⟨0∣ ⊗ I (2^(n -m -1)) ⊗ I 2)
  else if (n <? m) then
    @pad (1+(m -n -1)+1) n dim (u ⊗ I (2^(m -n -1)) ⊗ ∣1⟩⟨1∣ .+ I 2 ⊗ I (2^(m -n -1)) ⊗ ∣0⟩⟨0∣)
  else
    Zero.

Definition pad_swap (dim m n: nat) :=
  pad_ctrl dim m n σ x × pad_ctrl dim n m σ x × pad_ctrl dim m n σ x.

Well-formedness

Lemma WF_pad_u : ∀ dim n u, WF_Matrix u → WF_Matrix (pad_u dim n u).

Lemma WF_pad_ctrl : ∀ dim m n u, WF_Matrix u → WF_Matrix (pad_ctrl dim m n u).

Lemma WF_pad_swap : ∀ dim m n, WF_Matrix (pad_swap dim m n).

#[export] Hint Resolve WF_pad WF_pad_u WF_pad_ctrl WF_pad_swap : wf_db.

Unitarity

Lemma pad_unitary : ∀ n (u : Square (2^n)) start dim,
    (start + n ≤ dim)%nat →
    WF_Unitary u →
    WF_Unitary (pad start dim u).

Lemma pad_u_unitary : ∀ dim n u,
    (n < dim)%nat →
    WF_Unitary u →
    WF_Unitary (pad_u dim n u).

Lemma pad_ctrl_unitary : ∀ dim m n u,
    m ≠ n →
    (m < dim)%nat →
    (n < dim)%nat →
    WF_Unitary u →
    WF_Unitary (pad_ctrl dim m n u).

Lemma pad_swap_unitary : ∀ dim m n,
    m ≠ n →
    (m < dim)%nat →
    (n < dim)%nat →
    WF_Unitary (pad_swap dim m n).

Lemmas about commutation

Lemma pad_A_B_commutes : ∀ dim m n A B,
  m ≠ n →
  WF_Matrix A →
  WF_Matrix B →
  pad_u dim m A × pad_u dim n B = pad_u dim n B × pad_u dim m A.

Lemma pad_A_ctrl_commutes : ∀ dim m n o A B,
  m ≠ n →
  m ≠ o →
  WF_Matrix A →
  WF_Matrix B →
  pad_u dim m A × pad_ctrl dim n o B = pad_ctrl dim n o B × pad_u dim m A.

Lemma pad_ctrl_ctrl_commutes : ∀ dim m n o p A B,
  m ≠ o →
  m ≠ p →
  n ≠ o →
  n ≠ p →
  WF_Matrix A →
  WF_Matrix B →
  pad_ctrl dim m n A × pad_ctrl dim o p B = pad_ctrl dim o p B × pad_ctrl dim m n A.