From fc152a7589ba8ce40a44d224bc704c0f0d230ce2 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Sat, 22 Jan 2022 17:03:54 -0500 Subject: [PATCH] Some more doc edits --- Matrix.v | 97 +++++++++++++------------------------------------- Measurement.v | 9 ++--- Pad.v | 11 ++++-- Permutations.v | 11 +++--- Proportional.v | 2 ++ README.md | 2 -- 6 files changed, 43 insertions(+), 89 deletions(-) diff --git a/Matrix.v b/Matrix.v index 0ec4bf4..3026fe0 100644 --- a/Matrix.v +++ b/Matrix.v @@ -8,9 +8,9 @@ Require Import List. (* TODO: Use matrix equality everywhere, declare equivalence relation *) (* TODO: Make all nat arguments to matrix lemmas implicit *) -(*******************************************) -(** Matrix Definitions and Infrastructure **) -(*******************************************) +(*********************************************) +(** * Matrix definitions and infrastructure **) +(*********************************************) Declare Scope matrix_scope. Delimit Scope matrix_scope with M. @@ -20,8 +20,6 @@ Local Open Scope nat_scope. Definition Matrix (m n : nat) := nat -> nat -> C. -(* Definition Vector (n : nat) := Matrix n 1. *) - Definition WF_Matrix {m n: nat} (A : Matrix m n) : Prop := forall x y, x >= m \/ y >= n -> A x y = C0. @@ -29,14 +27,14 @@ Notation Vector n := (Matrix n 1). Notation Square n := (Matrix n n). -(* Showing equality via functional extensionality *) +(** Equality via functional extensionality *) Ltac prep_matrix_equality := let x := fresh "x" in let y := fresh "y" in apply functional_extensionality; intros x; apply functional_extensionality; intros y. -(* Matrix Equivalence *) +(** Matrix equivalence *) Definition mat_equiv {m n : nat} (A B : Matrix m n) : Prop := forall i j, i < m -> j < n -> A i j = B i j. @@ -62,7 +60,7 @@ Proof. + rewrite WFA, WFB; trivial; left; try lia. Qed. -(* Printing *) +(** Printing *) Parameter print_C : C -> string. Fixpoint print_row {m n} i j (A : Matrix m n) : string := @@ -78,7 +76,7 @@ Fixpoint print_rows {m n} i j (A : Matrix m n) : string := Definition print_matrix {m n} (A : Matrix m n) : string := print_rows m n A. -(* 2D List Representation *) +(** 2D list representation *) Definition list2D_to_matrix (l : list (list C)) : Matrix (length l) (length (hd [] l)) := @@ -104,7 +102,7 @@ Proof. simpl; lia. Qed. -(* Example *) +(** Example *) Definition M23 : Matrix 2 3 := fun x y => match (x, y) with @@ -130,9 +128,9 @@ Proof. do 4 (try destruct x; try destruct y; simpl; trivial). Qed. -(*****************************) -(** Operands and Operations **) -(*****************************) +(*******************************) +(** * Operands and operations **) +(*******************************) Definition Zero {m n : nat} : Matrix m n := fun x y => 0%R. @@ -142,7 +140,7 @@ Definition I (n : nat) : Square n := (* Optional coercion to scalar (should be limited to 1 × 1 matrices): Definition to_scalar (m n : nat) (A: Matrix m n) : C := A 0 0. Coercion to_scalar : Matrix >-> C. - *) +*) (* This isn't used, but is interesting *) Definition I__inf := fun x y => if x =? y then C1 else C0. @@ -180,14 +178,14 @@ Definition inner_product {n} (u v : Vector n) : C := Definition outer_product {n} (u v : Vector n) : Square n := Mmult u (adjoint v). -(* Kronecker of n copies of A *) +(** Kronecker of n copies of A *) Fixpoint kron_n n {m1 m2} (A : Matrix m1 m2) : Matrix (m1^n) (m2^n) := match n with | 0 => I 1 | S n' => kron (kron_n n' A) A end. -(* Kronecker product of a list *) +(** Kronecker product of a list *) Fixpoint big_kron {m n} (As : list (Matrix m n)) : Matrix (m^(length As)) (n^(length As)) := match As with @@ -195,20 +193,21 @@ Fixpoint big_kron {m n} (As : list (Matrix m n)) : | A :: As' => kron A (big_kron As') end. -(* Product of n copies of A *) +(** Product of n copies of A *) Fixpoint Mmult_n n {m} (A : Square m) : Square m := match n with | 0 => I m | S n' => Mmult A (Mmult_n n' A) end. -(* Indexed sum over matrices *) +(** Indexed sum over matrices *) Fixpoint Msum {m1 m2} n (f : nat -> Matrix m1 m2) : Matrix m1 m2 := match n with | 0 => Zero | S n' => Mplus (Msum n' f) (f n') end. +(** Notations *) Infix "∘" := dot (at level 40, left associativity) : matrix_scope. Infix ".+" := Mplus (at level 50, left associativity) : matrix_scope. Infix ".*" := scale (at level 40, left associativity) : matrix_scope. @@ -307,9 +306,9 @@ Lemma Mscale_simplify : forall (n m: nat) (a b : Matrix n m) (c d : C), Proof. intros; subst; easy. Qed. -(**********************************) -(** Proofs about Well-Formedness **) -(**********************************) +(************************************) +(** * Proofs about well-formedness **) +(************************************) Lemma WF_Matrix_dim_change : forall (m n m' n' : nat) (A : Matrix m n), m = m' -> @@ -382,30 +381,6 @@ Proof. assumption. Qed. - -(* More succinct but sometimes doesn't succeed -Lemma WF_kron : forall {m n o p: nat} (A : Matrix m n) (B : Matrix o p), - WF_Matrix A -> WF_Matrix B -> WF_Matrix (A ⊗ B). -Proof. - unfold WF_Matrix, kron. - intros m n o p A B WFA WFB x y H. - bdestruct (o =? 0). rewrite WFB; [lca|lia]. - bdestruct (p =? 0). rewrite WFB; [lca|lia]. - rewrite WFA. - rewrite Cmult_0_l; reflexivity. - destruct H. - unfold ge in *. - left. - apply Nat.div_le_lower_bound; trivial. - rewrite Nat.mul_comm. - assumption. - right. - apply Nat.div_le_lower_bound; trivial. - rewrite Nat.mul_comm. - assumption. -Qed. -*) - Lemma WF_transpose : forall {m n : nat} (A : Matrix m n), WF_Matrix A -> WF_Matrix A⊤. Proof. unfold WF_Matrix, transpose. intros m n A H x y H0. apply H. @@ -475,35 +450,14 @@ Qed. Local Close Scope nat_scope. -(***************************************) -(* Tactics for showing well-formedness *) -(***************************************) +(****************************************) +(** Tactics for showing well-formedness *) +(****************************************) Local Open Scope nat. Local Open Scope R. Local Open Scope C. -(* -Ltac show_wf := - repeat match goal with - | [ |- WF_Matrix _ _ (?A × ?B) ] => apply WF_mult - | [ |- WF_Matrix _ _ (?A .+ ?B) ] => apply WF_plus - | [ |- WF_Matrix _ _ (?p .* ?B) ] => apply WF_scale - | [ |- WF_Matrix _ _ (?A ⊗ ?B) ] => apply WF_kron - | [ |- WF_Matrix _ _ (?A⊤) ] => apply WF_transpose - | [ |- WF_Matrix _ _ (?A†) ] => apply WF_adjoint - | [ |- WF_Matrix _ _ (I _) ] => apply WF_I - end; - trivial; - unfold WF_Matrix; - let x := fresh "x" in - let y := fresh "y" in - let H := fresh "H" in - intros x y [H | H]; - repeat (destruct x; try reflexivity; try lia); - repeat (destruct y; try reflexivity; try lia). -*) - (* Much less awful *) Ltac show_wf := unfold WF_Matrix; @@ -522,10 +476,7 @@ Ltac show_wf := WF_Mmult_n WF_Msum : wf_db. #[export] Hint Extern 2 (_ = _) => unify_pows_two : wf_db. -(* Hint Resolve WF_Matrix_dim_change : wf_db. *) - - -(** Basic Matrix Lemmas **) +(** * Basic matrix lemmas *) Lemma WF0_Zero_l :forall (n : nat) (A : Matrix 0%nat n), WF_Matrix A -> A = Zero. Proof. diff --git a/Measurement.v b/Measurement.v index 1711a90..6427265 100644 --- a/Measurement.v +++ b/Measurement.v @@ -1,16 +1,13 @@ Require Import VectorStates. -(* ============================== *) -(** Measurement predicates **) -(* ============================== *) +(** This file contains predicates for describing the outcomes of measurement. *) -(* What is the probability of outcome ϕ given input ψ? *) +(** * Probability of outcome ϕ given input ψ *) Definition probability_of_outcome {n} (ϕ ψ : Vector n) : R := let c := (ϕ† × ψ) O O in (Cmod c) ^ 2. -(* What is the probability of measuring ϕ on the first m qubits given - (m + n) qubit input ψ? *) +(** * Probability of measuring ϕ on the first m qubits given (m + n) qubit input ψ *) Definition prob_partial_meas {m n} (ϕ : Vector (2^m)) (ψ : Vector (2^(m + n))) := Rsum (2^n) (fun y => probability_of_outcome (ϕ ⊗ basis_vector (2^n) y) ψ). diff --git a/Pad.v b/Pad.v index d7da43a..f8b855a 100644 --- a/Pad.v +++ b/Pad.v @@ -1,7 +1,10 @@ Require Export Complex. Require Export Quantum. -(* Padding; used to extend a matrix to a larger space *) +(** 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. @@ -40,7 +43,7 @@ Definition pad_ctrl (dim m n: nat) (u: Square 2) := 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 **) +(** Well-formedness *) Lemma WF_pad_u : forall dim n u, WF_Matrix u -> WF_Matrix (pad_u dim n u). Proof. @@ -67,6 +70,8 @@ Qed. #[export] Hint Resolve WF_pad WF_pad_u WF_pad_ctrl WF_pad_swap : wf_db. +(** Unitarity *) + Lemma pad_unitary : forall n (u : Square (2^n)) start dim, (start + n <= dim)%nat -> WF_Unitary u -> @@ -131,7 +136,7 @@ Proof. apply pad_ctrl_unitary; auto; apply σx_unitary. Qed. -(* Lemmas about commutation *) +(** Lemmas about commutation *) Lemma pad_A_B_commutes : forall dim m n A B, m <> n -> diff --git a/Permutations.v b/Permutations.v index b944bd6..b068c6c 100644 --- a/Permutations.v +++ b/Permutations.v @@ -1,10 +1,10 @@ Require Import VectorStates. -(* Facts about permutations and matrices that implement them *) +(** Facts about permutations and matrices that implement them. *) Local Open Scope nat_scope. -(* permutation on [0,...,n-1] *) +(** * Permutations on (0,...,n-1) *) Definition permutation (n : nat) (f : nat -> nat) := exists g, forall x, x < n -> (f x < n /\ g x < n /\ g (f x) = x /\ f (g x) = x). @@ -99,7 +99,7 @@ Proof. destruct (Hg x0) as [_ [_ [_ ?]]]; lia. Qed. -(* vsum terms can be arbitrarily reordered *) +(** vsum terms can be arbitrarily reordered *) Lemma vsum_reorder : forall {d} n (v : nat -> Vector d) f, permutation n f -> vsum n v = vsum n (fun i => v (f i)). @@ -121,7 +121,7 @@ Proof. exists g. auto. Qed. -(* Permutation matrices *) +(** * Permutation matrices *) Definition perm_mat n (p : nat -> nat) : Square n := (fun x y => if (x =? p y) && (x nat) := fun x:nat => funbool_to_nat n ((nat_to_funbool n x) ∘ p)%prg. @@ -252,6 +252,7 @@ Proof. rewrite nat_to_funbool_inverse; auto. Qed. +(** 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). diff --git a/Proportional.v b/Proportional.v index 620640e..8e2fbc4 100644 --- a/Proportional.v +++ b/Proportional.v @@ -1,6 +1,8 @@ Require Export Matrix. Require Import Setoid. +(** Relation for equality up to a global phase. *) + Definition proportional {m n : nat} (A B : Matrix m n) := exists θ, A = Cexp θ .* B. Infix "∝" := proportional (at level 70). diff --git a/README.md b/README.md index c3cd889..8da8974 100644 --- a/README.md +++ b/README.md @@ -20,8 +20,6 @@ Run `make doc` to generate documentation. ## Directory Contents -**TODO: Improve summaries. (Or remove entirely if the coqdoc documentation is sufficient.)** - * Complex.v - Definition of Complex numbers, extending [Coquelicot](http://coquelicot.saclay.inria.fr/)'s. * Ctopology.v - A topology of open/closed sets is defined for the complex numbers, with lemmas about compactness. * DiscreteProb.v - Theory of discrete probability distributions and utility to describe running a quantum program ("apply_u") and sampling from the output distribution.