QuantumLib.Permutations
Facts about permutations and matrices that implement them.
Local Open Scope nat_scope.
Definition permutation (n : nat) (f : nat → nat) :=
∃ g, ∀ x, x < n → (f x < n ∧ g x < n ∧ g (f x) = x ∧ f (g x) = x).
Lemma permutation_is_injective : ∀ n f,
permutation n f →
∀ x y, x < n → y < n → f x = f y → x = y.
Lemma permutation_compose : ∀ n f g,
permutation n f →
permutation n g →
permutation n (f ∘ g)%prg.
Lemma fswap_at_boundary_permutation : ∀ n f x,
permutation (S n) f →
(x < S n)%nat → f x = n →
permutation n (fswap f x n).
∃ g, ∀ x, x < n → (f x < n ∧ g x < n ∧ g (f x) = x ∧ f (g x) = x).
Lemma permutation_is_injective : ∀ n f,
permutation n f →
∀ x y, x < n → y < n → f x = f y → x = y.
Lemma permutation_compose : ∀ n f g,
permutation n f →
permutation n g →
permutation n (f ∘ g)%prg.
Lemma fswap_at_boundary_permutation : ∀ n f x,
permutation (S n) f →
(x < S n)%nat → f x = n →
permutation n (fswap f x n).
vsum terms can be arbitrarily reordered
Lemma vsum_reorder : ∀ {d} n (v : nat → Vector d) f,
permutation n f →
big_sum v n = big_sum (fun i ⇒ v (f i)) n.
permutation n f →
big_sum v n = big_sum (fun i ⇒ v (f i)) n.
Definition perm_mat n (p : nat → nat) : Square n :=
(fun x y ⇒ if (x =? p y) && (x <? n) && (y <? n) then C1 else C0).
Lemma perm_mat_WF : ∀ n p, WF_Matrix (perm_mat n p).
#[export] Hint Resolve perm_mat_WF : wf_db.
Lemma perm_mat_unitary : ∀ n p,
permutation n p → WF_Unitary (perm_mat n p).
Lemma perm_mat_Mmult : ∀ n f g,
permutation n g →
perm_mat n f × perm_mat n g = perm_mat n (f ∘ g)%prg.
Lemma perm_mat_I : ∀ n f,
(∀ x, x < n → f x = x) →
perm_mat n f = I n.
Given a permutation p over n qubits, construct a permutation over 2^n indices.
Definition qubit_perm_to_nat_perm n (p : nat → nat) :=
fun x:nat ⇒ funbool_to_nat n ((nat_to_funbool n x) ∘ p)%prg.
Lemma qubit_perm_to_nat_perm_bij : ∀ n p,
permutation n p → permutation (2^n) (qubit_perm_to_nat_perm n p).
fun x:nat ⇒ funbool_to_nat n ((nat_to_funbool n x) ∘ p)%prg.
Lemma qubit_perm_to_nat_perm_bij : ∀ n p,
permutation n p → permutation (2^n) (qubit_perm_to_nat_perm n p).
Transform a (0,...,n-1) permutation into a 2^n by 2^n matrix.
Definition perm_to_matrix n p :=
perm_mat (2 ^ n) (qubit_perm_to_nat_perm n p).
Lemma perm_to_matrix_permutes_qubits : ∀ n p f,
permutation n p →
perm_to_matrix n p × f_to_vec n f = f_to_vec n (fun x ⇒ f (p x)).
Lemma perm_to_matrix_unitary : ∀ n p,
permutation n p →
WF_Unitary (perm_to_matrix n p).
Lemma qubit_perm_to_nat_perm_compose : ∀ n f g,
permutation n f →
(qubit_perm_to_nat_perm n f ∘ qubit_perm_to_nat_perm n g =
qubit_perm_to_nat_perm n (g ∘ f))%prg.
Lemma perm_to_matrix_Mmult : ∀ n f g,
permutation n f →
permutation n g →
perm_to_matrix n f × perm_to_matrix n g = perm_to_matrix n (g ∘ f)%prg.
Lemma perm_to_matrix_I : ∀ n f,
permutation n f →
(∀ x, x < n → f x = x) →
perm_to_matrix n f = I (2 ^ n).
Lemma perm_to_matrix_WF : ∀ n p, WF_Matrix (perm_to_matrix n p).
#[export] Hint Resolve perm_to_matrix_WF : wf_db.
perm_mat (2 ^ n) (qubit_perm_to_nat_perm n p).
Lemma perm_to_matrix_permutes_qubits : ∀ n p f,
permutation n p →
perm_to_matrix n p × f_to_vec n f = f_to_vec n (fun x ⇒ f (p x)).
Lemma perm_to_matrix_unitary : ∀ n p,
permutation n p →
WF_Unitary (perm_to_matrix n p).
Lemma qubit_perm_to_nat_perm_compose : ∀ n f g,
permutation n f →
(qubit_perm_to_nat_perm n f ∘ qubit_perm_to_nat_perm n g =
qubit_perm_to_nat_perm n (g ∘ f))%prg.
Lemma perm_to_matrix_Mmult : ∀ n f g,
permutation n f →
permutation n g →
perm_to_matrix n f × perm_to_matrix n g = perm_to_matrix n (g ∘ f)%prg.
Lemma perm_to_matrix_I : ∀ n f,
permutation n f →
(∀ x, x < n → f x = x) →
perm_to_matrix n f = I (2 ^ n).
Lemma perm_to_matrix_WF : ∀ n p, WF_Matrix (perm_to_matrix n p).
#[export] Hint Resolve perm_to_matrix_WF : wf_db.